:: Context-Free Grammar - Part 1
:: by Patricia L. Carlson and Grzegorz Bancerek
::
:: Received February 21, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

:: Grammar structure is introduced as triple (S, I, R) where S is
:: a set of non-terminal and terminal symbols, I is an initial symbol,
:: and R is a set of rules (ordered pairs).
definition
attrc1 is strict ;
struct DTConstrStr  ->  1-sorted ;
aggrDTConstrStr(# carrier, Rules #) ->  DTConstrStr ;
sel Rules c1 ->  Relation of the carrier of c1,( the carrier of c1 *);
end;

registration
cluster non empty strict for DTConstrStr ;
existence
 ex b1 being DTConstrStr st
( not b1 is empty & b1 is strict )
proofend;
end;

definition
attrc1 is strict ;
struct GrammarStr  ->  DTConstrStr ;
aggrGrammarStr(# carrier, InitialSym, Rules #) ->  GrammarStr ;
sel InitialSym c1 ->  Element of the carrier of c1;
end;

registration
cluster non empty for GrammarStr ;
existence
 not for b1 being GrammarStr holds b1 is empty
proofend;
end;

definition
let G be DTConstrStr ;
mode Symbol of G is Element of G;
mode String of G is Element of the carrier of G * ;
end;

definition
let G be non empty DTConstrStr ;
let s be Symbol of G;
let n be FinSequence;
preds ==> n means :Def1: :: LANG1:def 1
[s,n] in the Rules of G;
end;

:: deftheorem Def1 defines ==> LANG1:def_1_:_
 for G being non empty DTConstrStr
for s being Symbol of G
for n being FinSequence holds
( s ==> n iff [s,n] in the Rules of G );

definition
let G be non empty DTConstrStr ;
func Terminals G ->  set  equals :: LANG1:def 2
 {  s where s is Symbol of G : for n being FinSequence holds not s ==> n  }  ;
coherence
  {  s where s is Symbol of G : for n being FinSequence holds not s ==> n  }  is set ;
func NonTerminals G ->  set  equals :: LANG1:def 3
 {  s where s is Symbol of G : ex n being FinSequence st s ==> n  }  ;
coherence
  {  s where s is Symbol of G : ex n being FinSequence st s ==> n  }  is set ;
end;

:: deftheorem  defines Terminals LANG1:def_2_:_
 for G being non empty DTConstrStr holds Terminals G =  {  s where s is Symbol of G : for n being FinSequence holds not s ==> n  }  ;

:: deftheorem  defines NonTerminals LANG1:def_3_:_
 for G being non empty DTConstrStr holds NonTerminals G =  {  s where s is Symbol of G : ex n being FinSequence st s ==> n  }  ;

theorem :: LANG1:1
for G being non empty DTConstrStr holds (Terminals G) \/ (NonTerminals G) = the carrier of G
proofend;

definition
let G be non empty DTConstrStr ;
let n, m be String of G;
predn ==> m means :: LANG1:def 4
 ex n1, n2, n3 being String of G ex s being Symbol of G st
( n = (n1 ^ <*s*>) ^ n2 &amp; m = (n1 ^ n3) ^ n2 &amp; s ==> n3 );
end;

:: deftheorem  defines ==> LANG1:def_4_:_
 for G being non empty DTConstrStr
for n, m being String of G holds
( n ==> m iff ex n1, n2, n3 being String of G ex s being Symbol of G st
( n = (n1 ^ <*s*>) ^ n2 &amp; m = (n1 ^ n3) ^ n2 &amp; s ==> n3 ) );

theorem :: LANG1:2
for G being non empty DTConstrStr
for s being Symbol of G
for n, n1, n2 being String of G st s ==> n holds
(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
proofend;

theorem Th3: :: LANG1:3
for G being non empty DTConstrStr
for s being Symbol of G
for n being String of G st s ==> n holds
<*s*> ==> n
proofend;

theorem Th4: :: LANG1:4
for G being non empty DTConstrStr
for s being Symbol of G
for n being String of G st <*s*> ==> n holds
s ==> n
proofend;

theorem Th5: :: LANG1:5
for G being non empty DTConstrStr
for n, n1, n2 being String of G st n1 ==> n2 holds
( n ^ n1 ==> n ^ n2 &amp; n1 ^ n ==> n2 ^ n )
proofend;

definition
let G be non empty DTConstrStr ;
let n, m be String of G;
predm is_derivable_from n means :Def5: :: LANG1:def 5
 ex p being FinSequence st
( len p >= 1 &amp; p . 1 = n &amp; p . (len p) = m &amp; ( for i being Element of NAT st i >= 1 &amp; i < len p holds
ex a, b being String of G st
( p . i = a &amp; p . (i + 1) = b &amp; a ==> b ) ) );
end;

:: deftheorem Def5 defines is_derivable_from LANG1:def_5_:_
 for G being non empty DTConstrStr
for n, m being String of G holds
( m is_derivable_from n iff ex p being FinSequence st
( len p >= 1 &amp; p . 1 = n &amp; p . (len p) = m &amp; ( for i being Element of NAT st i >= 1 &amp; i < len p holds
ex a, b being String of G st
( p . i = a &amp; p . (i + 1) = b &amp; a ==> b ) ) ) );

theorem Th6: :: LANG1:6
for G being non empty DTConstrStr
for n being String of G holds n is_derivable_from n
proofend;

theorem Th7: :: LANG1:7
for G being non empty DTConstrStr
for n, m being String of G st n ==> m holds
m is_derivable_from n
proofend;

theorem Th8: :: LANG1:8
for G being non empty DTConstrStr
for n1, n2, n3 being String of G st n1 is_derivable_from n2 &amp; n2 is_derivable_from n3 holds
n1 is_derivable_from n3
proofend;

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

:: deftheorem  defines Lang LANG1:def_6_:_
 for G being non empty GrammarStr holds Lang G =  {  a where a is Element of the carrier of G * : ( rng a c= Terminals G &amp; a is_derivable_from <* the InitialSym of G*> )  }  ;

theorem :: LANG1:9
for G being non empty GrammarStr
for n being String of G holds
( n in Lang G iff ( rng n c= Terminals G &amp; n is_derivable_from <* the InitialSym of G*> ) )
proofend;

:: GrammarStr(#{a},a,{[a,{}{a}]}#) -> Lang = {{}}
:: GrammarStr(#{a,b},a,{[a,<*b*>]}#) -> Lang = {b}
:: GrammarStr(#{a,b},a,{[a,{}{a}],[a,<*a,b*>]}#) -> Lang = {{}, b, bb, ...}
:: GrammarStr(#{a,b,c},a,{[a,<*b*>}],[a,<*c*>]}#) -> Lang = {b, c}
definition
let D, E be non empty set ;
let a be Element of [:D,E:];
:: original:{
redefine func{a} ->  Relation of D,E;
coherence
 {a} is Relation of D,E
proofend;
let b be Element of [:D,E:];
:: original:{
redefine func{a,b} ->  Relation of D,E;
coherence
 {a,b} is Relation of D,E
proofend;
end;

definition
let a be set ;
func EmptyGrammar a ->  strict GrammarStr  means :Def7: :: LANG1:def 7
( the carrier of it = {a} &amp; the Rules of it = {[a,{}]} );
existence
 ex b1 being strict GrammarStr st
( the carrier of b1 = {a} &amp; the Rules of b1 = {[a,{}]} )
proofend;
uniqueness
 for b1, b2 being strict GrammarStr st the carrier of b1 = {a} &amp; the Rules of b1 = {[a,{}]} &amp; the carrier of b2 = {a} &amp; the Rules of b2 = {[a,{}]} holds
b1 = b2
proofend;
let b be set ;
func SingleGrammar (a,b) ->  strict GrammarStr  means :Def8: :: LANG1:def 8
( the carrier of it = {a,b} &amp; the InitialSym of it = a &amp; the Rules of it = {[a,<*b*>]} );
existence
 ex b1 being strict GrammarStr st
( the carrier of b1 = {a,b} &amp; the InitialSym of b1 = a &amp; the Rules of b1 = {[a,<*b*>]} )
proofend;
uniqueness
 for b1, b2 being strict GrammarStr st the carrier of b1 = {a,b} &amp; the InitialSym of b1 = a &amp; the Rules of b1 = {[a,<*b*>]} &amp; the carrier of b2 = {a,b} &amp; the InitialSym of b2 = a &amp; the Rules of b2 = {[a,<*b*>]} holds
b1 = b2 ;
func IterGrammar (a,b) ->  strict GrammarStr  means :Def9: :: LANG1:def 9
( the carrier of it = {a,b} &amp; the InitialSym of it = a &amp; the Rules of it = {[a,<*b,a*>],[a,{}]} );
existence
 ex b1 being strict GrammarStr st
( the carrier of b1 = {a,b} &amp; the InitialSym of b1 = a &amp; the Rules of b1 = {[a,<*b,a*>],[a,{}]} )
proofend;
uniqueness
 for b1, b2 being strict GrammarStr st the carrier of b1 = {a,b} &amp; the InitialSym of b1 = a &amp; the Rules of b1 = {[a,<*b,a*>],[a,{}]} &amp; the carrier of b2 = {a,b} &amp; the InitialSym of b2 = a &amp; the Rules of b2 = {[a,<*b,a*>],[a,{}]} holds
b1 = b2 ;
end;

:: deftheorem Def7 defines EmptyGrammar LANG1:def_7_:_
 for a being set
for b2 being strict GrammarStr holds
( b2 = EmptyGrammar a iff ( the carrier of b2 = {a} &amp; the Rules of b2 = {[a,{}]} ) );

:: deftheorem Def8 defines SingleGrammar LANG1:def_8_:_
 for a, b being set
for b3 being strict GrammarStr holds
( b3 = SingleGrammar (a,b) iff ( the carrier of b3 = {a,b} &amp; the InitialSym of b3 = a &amp; the Rules of b3 = {[a,<*b*>]} ) );

:: deftheorem Def9 defines IterGrammar LANG1:def_9_:_
 for a, b being set
for b3 being strict GrammarStr holds
( b3 = IterGrammar (a,b) iff ( the carrier of b3 = {a,b} &amp; the InitialSym of b3 = a &amp; the Rules of b3 = {[a,<*b,a*>],[a,{}]} ) );

registration
let a be set ;
cluster EmptyGrammar a ->  non empty strict ;
coherence
 not EmptyGrammar a is empty
proofend;
let b be set ;
cluster SingleGrammar (a,b) ->  non empty strict ;
coherence
 not SingleGrammar (a,b) is empty
proofend;
cluster IterGrammar (a,b) ->  non empty strict ;
coherence
 not IterGrammar (a,b) is empty
proofend;
end;

definition
let D be non empty set ;
func TotalGrammar D ->  strict GrammarStr  means :Def10: :: LANG1:def 10
( the carrier of it = succ D &amp; the InitialSym of it = D &amp; the Rules of it =  {  [D,<*d,D*>] where d is Element of D : d = d  }  \/ {[D,{}]} );
existence
 ex b1 being strict GrammarStr st
( the carrier of b1 = succ D &amp; the InitialSym of b1 = D &amp; the Rules of b1 =  {  [D,<*d,D*>] where d is Element of D : d = d  }  \/ {[D,{}]} )
proofend;
uniqueness
 for b1, b2 being strict GrammarStr st the carrier of b1 = succ D &amp; the InitialSym of b1 = D &amp; the Rules of b1 =  {  [D,<*d,D*>] where d is Element of D : d = d  }  \/ {[D,{}]} &amp; the carrier of b2 = succ D &amp; the InitialSym of b2 = D &amp; the Rules of b2 =  {  [D,<*d,D*>] where d is Element of D : d = d  }  \/ {[D,{}]} holds
b1 = b2 ;
end;

:: deftheorem Def10 defines TotalGrammar LANG1:def_10_:_
 for D being non empty set
for b2 being strict GrammarStr holds
( b2 = TotalGrammar D iff ( the carrier of b2 = succ D &amp; the InitialSym of b2 = D &amp; the Rules of b2 =  {  [D,<*d,D*>] where d is Element of D : d = d  }  \/ {[D,{}]} ) );

registration
let D be non empty set ;
cluster TotalGrammar D ->  non empty strict ;
coherence
 not TotalGrammar D is empty
proofend;
end;

theorem Th10: :: LANG1:10
for a being set holds Terminals (EmptyGrammar a) = {}
proofend;

theorem Th11: :: LANG1:11
for a being set holds Lang (EmptyGrammar a) = {{}}
proofend;

theorem Th12: :: LANG1:12
for a, b being set st a <> b holds
Terminals (SingleGrammar (a,b)) = {b}
proofend;

theorem :: LANG1:13
for a, b being set st a <> b holds
Lang (SingleGrammar (a,b)) = {<*b*>}
proofend;

theorem Th14: :: LANG1:14
for a, b being set st a <> b holds
Terminals (IterGrammar (a,b)) = {b}
proofend;

theorem :: LANG1:15
for a, b being set st a <> b holds
Lang (IterGrammar (a,b)) = {b} *
proofend;

theorem Th16: :: LANG1:16
for D being non empty set holds Terminals (TotalGrammar D) = D
proofend;

theorem :: LANG1:17
for D being non empty set holds Lang (TotalGrammar D) = D *
proofend;

definition
let IT be non empty GrammarStr ;
attrIT is efective  means :Def11: :: LANG1:def 11
( not Lang IT is empty &amp; the InitialSym of IT in NonTerminals IT &amp; ( for s being Symbol of IT st s in Terminals IT holds
ex p being String of IT st
( p in Lang IT &amp; s in rng p ) ) );
end;

:: deftheorem Def11 defines efective LANG1:def_11_:_
 for IT being non empty GrammarStr holds
( IT is efective iff ( not Lang IT is empty &amp; the InitialSym of IT in NonTerminals IT &amp; ( for s being Symbol of IT st s in Terminals IT holds
ex p being String of IT st
( p in Lang IT &amp; s in rng p ) ) ) );

definition
let IT be GrammarStr ;
attrIT is finite  means :: LANG1:def 12
 the Rules of IT is finite ;
end;

:: deftheorem  defines finite LANG1:def_12_:_
 for IT being GrammarStr holds
( IT is finite iff the Rules of IT is finite );

registration
cluster non empty efective finite for GrammarStr ;
existence
 ex b1 being non empty GrammarStr st
( b1 is efective &amp; b1 is finite )
proofend;
end;

definition
let G be non empty efective GrammarStr ;
:: original:NonTerminals
redefine func NonTerminals G ->  non empty Subset of G;
coherence
 NonTerminals G is non empty Subset of G
proofend;
end;

definition
let X, Y be non empty set ;
let p be FinSequence of X;
let f be Function of X,Y;
:: original:*
redefine funcf * p ->  Element of Y * ;
coherence
 p * f is Element of Y *
proofend;
end;

definition
let X, Y be non empty set ;
let f be Function of X,Y;
funcf *  ->  Function of (X *),(Y *) means :: LANG1:def 13
 for p being Element of X * holds it . p = f * p;
existence
 ex b1 being Function of (X *),(Y *) st
for p being Element of X * holds b1 . p = f * p
proofend;
uniqueness
 for b1, b2 being Function of (X *),(Y *) st ( for p being Element of X * holds b1 . p = f * p ) &amp; ( for p being Element of X * holds b2 . p = f * p ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines * LANG1:def_13_:_
 for X, Y being non empty set
for f being Function of X,Y
for b4 being Function of (X *),(Y *) holds
( b4 = f * iff for p being Element of X * holds b4 . p = f * p );

theorem :: LANG1:18
for R being Relation holds R c= R [*]
proofend;

definition
let X be non empty set ;
let R be Relation of X;
:: original:[*]
redefine funcR [*]  ->  Relation of X;
coherence
 R [*] is Relation of X
proofend;
end;

definition
let G be non empty GrammarStr ;
let X be non empty set ;
let f be Function of the carrier of G,X;
funcG . f ->  strict GrammarStr  equals :: LANG1:def 14
 GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #);
correctness
coherence
GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #) is strict GrammarStr ;
;
end;

:: deftheorem  defines . LANG1:def_14_:_
 for G being non empty GrammarStr
for X being non empty set
for f being Function of the carrier of G,X holds G . f = GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #);