:: LANG1 semantic presentation

definition

attr a₁ is strict;
struct DTConstrStr -> 1-sorted ;
aggr DTConstrStr(# carrier, Rules #) -> DTConstrStr ;
sel Rules c₁ -> Relation of the carrier of a₁,the carrier of a₁ * ;

end;

registration

cluster non empty strict DTConstrStr ;
existence

proof end;

end;

definition

attr a₁ is strict;
struct GrammarStr -> DTConstrStr ;
aggr GrammarStr(# carrier, InitialSym, Rules #) -> GrammarStr ;
sel InitialSym c₁ -> Element of the carrier of a₁;

end;

registration

cluster non empty GrammarStr ;
existence

proof end;

end;

definition

let c₁ be DTConstrStr ;
mode Symbol of a₁ is Element of a₁;
mode String of a₁ is Element of the carrier of a₁ * ;

end;

definition

let c₁ be set ;
let c₂, c₃ be Element of c₁ * ;
redefine func ^ as c₂ ^ c₃ -> Element of a₁ * ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster empty Element of a₁ * ;
existence

proof end;

end;

definition

let c₁ be set ;
redefine func <*> as <*> c₁ -> empty Element of a₁ * ;
coherence by FINSEQ_1:def 11;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func <* as <*c₂*> -> Element of a₁ * ;
coherence

proof end;

let c₃ be Element of c₁;
redefine func <* as <*c₂,c₃*> -> Element of a₁ * ;
coherence

proof end;

end;

definition

let c₁ be non empty DTConstrStr ;
let c₂ be Symbol of c₁;
let c₃ be FinSequence;
pred c₂ ==> c₃ means :Def1: :: LANG1:def 1
[a₂,a₃] in the Rules of a₁;

end;

:: deftheorem Def1 defines ==> LANG1:def 1 :

definition

let c₁ be non empty DTConstrStr ;
func Terminals c₁ -> set equals :: LANG1:def 2
{ b₁ where B is Symbol of a₁ : for b₁ being FinSequence holds not b₁ ==> b₂ } ;
coherence ;
func NonTerminals c₁ -> set equals :: LANG1:def 3
{ b₁ where B is Symbol of a₁ : ex b₁ being FinSequence st b₁ ==> b₂ } ;
coherence ;

end;

:: deftheorem Def2 defines Terminals LANG1:def 2 :

:: deftheorem Def3 defines NonTerminals LANG1:def 3 :

theorem Th1: :: LANG1:1

for b₁ being non empty DTConstrStr holds (Terminals b₁) \/ (NonTerminals b₁) = the carrier of b₁

proof end;

definition

let c₁ be non empty DTConstrStr ;
let c₂, c₃ be String of c₁;
pred c₂ ==> c₃ means :: LANG1:def 4
ex b₁, b₂, b₃ being String of a₁ex b₄ being Symbol of a₁ st
( a₂ = (b₁ ^ <*b₄*>) ^ b₂ & a₃ = (b₁ ^ b₃) ^ b₂ & b₄ ==> b₃ );

end;

:: deftheorem Def4 defines ==> LANG1:def 4 :

theorem Th2: :: LANG1:2

for b₁ being non empty DTConstrStr
for b₂ being Symbol of b₁
for b₃, b₄, b₅ being String of b₁ st b₂ ==> b₃ holds
(b₄ ^ <*b₂*>) ^ b₅ ==> (b₄ ^ b₃) ^ b₅

proof end;

theorem Th3: :: LANG1:3

for b₁ being non empty DTConstrStr
for b₂ being Symbol of b₁
for b₃ being String of b₁ st b₂ ==> b₃ holds
<*b₂*> ==> b₃

proof end;

theorem Th4: :: LANG1:4

for b₁ being non empty DTConstrStr
for b₂ being Symbol of b₁
for b₃ being String of b₁ st <*b₂*> ==> b₃ holds
b₂ ==> b₃

proof end;

theorem Th5: :: LANG1:5

for b₁ being non empty DTConstrStr
for b₂, b₃, b₄ being String of b₁ st b₃ ==> b₄ holds
( b₂ ^ b₃ ==> b₂ ^ b₄ & b₃ ^ b₂ ==> b₄ ^ b₂ )

proof end;

definition

let c₁ be non empty DTConstrStr ;
let c₂, c₃ be String of c₁;
pred c₃ is_derivable_from c₂ means :Def5: :: LANG1:def 5
ex b₁ being FinSequence st
( len b₁ >= 1 & b₁ . 1 = a₂ & b₁ . (len b₁) = a₃ & ( for b₂ being Nat st b₂ >= 1 & b₂ < len b₁ holds
ex b₃, b₄ being String of a₁ st
( b₁ . b₂ = b₃ & b₁ . (b₂ + 1) = b₄ & b₃ ==> b₄ ) ) );

end;

:: deftheorem Def5 defines is_derivable_from LANG1:def 5 :

theorem Th6: :: LANG1:6

for b₁ being non empty DTConstrStr
for b₂ being String of b₁ holds b₂ is_derivable_from b₂

proof end;

theorem Th7: :: LANG1:7

for b₁ being non empty DTConstrStr
for b₂, b₃ being String of b₁ st b₂ ==> b₃ holds
b₃ is_derivable_from b₂

proof end;

theorem Th8: :: LANG1:8

for b₁ being non empty DTConstrStr
for b₂, b₃, b₄ being String of b₁ st b₂ is_derivable_from b₃ & b₃ is_derivable_from b₄ holds
b₂ is_derivable_from b₄

proof end;

definition

let c₁ be non empty GrammarStr ;
func Lang c₁ -> set equals :: LANG1:def 6
{ b₁ where B is Element of the carrier of a₁ * : ( rng b₁ c= Terminals a₁ & b₁ is_derivable_from <*the InitialSym of a₁*> ) } ;
coherence ;

end;

:: deftheorem Def6 defines Lang LANG1:def 6 :

theorem Th9: :: LANG1:9

for b₁ being non empty GrammarStr
for b₂ being String of b₁ holds
( b₂ in Lang b₁ iff ( rng b₂ c= Terminals b₁ & b₂ is_derivable_from <*the InitialSym of b₁*> ) )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Element of [:c₁,c₂:];
redefine func { as {c₃} -> Relation of a₁,a₂;
coherence

proof end;

let c₄ be Element of [:c₁,c₂:];
redefine func { as {c₃,c₄} -> Relation of a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
func EmptyGrammar c₁ -> strict GrammarStr means :Def7: :: LANG1:def 7
( the carrier of a₂ = {a₁} & the Rules of a₂ = {[a₁,{} ]} );
existence

proof end;

uniqueness

proof end;

let c₂ be set ;
func SingleGrammar c₁,c₂ -> strict GrammarStr means :Def8: :: LANG1:def 8
( the carrier of a₃ = {a₁,a₂} & the InitialSym of a₃ = a₁ & the Rules of a₃ = {[a₁,<*a₂*>]} );
existence

proof end;

uniqueness ;
func IterGrammar c₁,c₂ -> strict GrammarStr means :Def9: :: LANG1:def 9
( the carrier of a₃ = {a₁,a₂} & the InitialSym of a₃ = a₁ & the Rules of a₃ = {[a₁,<*a₂,a₁*>],[a₁,{} ]} );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines EmptyGrammar LANG1:def 7 :

:: deftheorem Def8 defines SingleGrammar LANG1:def 8 :

:: deftheorem Def9 defines IterGrammar LANG1:def 9 :

registration

let c₁ be set ;
cluster EmptyGrammar a₁ -> non empty strict ;
coherence

proof end;

let c₂ be set ;
cluster SingleGrammar a₁,a₂ -> non empty strict ;
coherence

proof end;

cluster IterGrammar a₁,a₂ -> non empty strict ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
func TotalGrammar c₁ -> strict GrammarStr means :Def10: :: LANG1:def 10
( the carrier of a₂ = a₁ \/ {a₁} & the InitialSym of a₂ = a₁ & the Rules of a₂ = { [a₁,<*b₁,a₁*>] where B is Element of a₁ : b₁ = b₁ } \/ {[a₁,{} ]} );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def10 defines TotalGrammar LANG1:def 10 :

registration

let c₁ be non empty set ;
cluster TotalGrammar a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th10: :: LANG1:10

for b₁ being set holds Terminals (EmptyGrammar b₁) = {}

proof end;

theorem Th11: :: LANG1:11

for b₁ being set holds Lang (EmptyGrammar b₁) = {{} }

proof end;

theorem Th12: :: LANG1:12

for b₁, b₂ being set st b₁ <> b₂ holds
Terminals (SingleGrammar b₁,b₂) = {b₂}

proof end;

theorem Th13: :: LANG1:13

for b₁, b₂ being set st b₁ <> b₂ holds
Lang (SingleGrammar b₁,b₂) = {<*b₂*>}

proof end;

theorem Th14: :: LANG1:14

for b₁, b₂ being set st b₁ <> b₂ holds
Terminals (IterGrammar b₁,b₂) = {b₂}

proof end;

theorem Th15: :: LANG1:15

for b₁, b₂ being set st b₁ <> b₂ holds
Lang (IterGrammar b₁,b₂) = {b₂} *

proof end;

theorem Th16: :: LANG1:16

for b₁ being non empty set holds Terminals (TotalGrammar b₁) = b₁

proof end;

theorem Th17: :: LANG1:17

for b₁ being non empty set holds Lang (TotalGrammar b₁) = b₁ *

proof end;

definition

let c₁ be non empty GrammarStr ;
attr a₁ is efective means :Def11: :: LANG1:def 11
( not Lang a₁ is empty & the InitialSym of a₁ in NonTerminals a₁ & ( for b₁ being Symbol of a₁ st b₁ in Terminals a₁ holds
ex b₂ being String of a₁ st
( b₂ in Lang a₁ & b₁ in rng b₂ ) ) );

end;

:: deftheorem Def11 defines efective LANG1:def 11 :

definition

let c₁ be GrammarStr ;
attr a₁ is finite means :: LANG1:def 12
the Rules of a₁ is finite;

end;

:: deftheorem Def12 defines finite LANG1:def 12 :

registration

cluster non empty efective finite GrammarStr ;
existence

proof end;

end;

definition

let c₁ be non empty efective GrammarStr ;
redefine func NonTerminals as NonTerminals c₁ -> non empty Subset of a₁;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be FinSequence of c₁;
let c₄ be Function of c₁,c₂;
redefine func * as c₄ * c₃ -> Element of a₂ * ;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
canceled;
func c₃ * -> Function of a₁ * ,a₂ * means :: LANG1:def 14
for b₁ being Element of a₁ * holds a₄ . b₁ = a₃ * b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 LANG1:def 13 :

:: deftheorem Def14 defines * LANG1:def 14 :

theorem Th18: :: LANG1:18

for b₁ being Relation holds b₁ c= b₁ [*]

proof end;

definition

let c₁ be non empty set ;
let c₂ be Relation of c₁;
redefine func [*] as c₂ [*] -> Relation of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty GrammarStr ;
let c₂ be non empty set ;
let c₃ be Function of the carrier of c₁,c₂;
func c₁ . c₃ -> strict GrammarStr equals :: LANG1:def 15
GrammarStr(# a₂,(a₃ . the InitialSym of a₁),(((a₃ ~ ) * the Rules of a₁) * (a₃ * )) #);
correctness ;

end;

:: deftheorem Def15 defines . LANG1:def 15 :