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

:: 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

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

end;

registration

cluster non empty strict for DTConstrStr ;

existence
ex b₁ being DTConstrStr st
( not b₁ is empty & b₁ is strict )

proof end;

end;

definition

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

end;

registration

cluster non empty for GrammarStr ;

existence
not for b₁ being GrammarStr holds b₁ is empty

proof end;

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;

pred s ==> n means :: LANG1:def 1
[s,n] in the Rules of G;

end;

:: deftheorem 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

proof end;

definition

let G be non empty DTConstrStr ;
let n, m be String of G;

pred n ==> m means :: LANG1:def 4
ex n1, n2, n3 being String of G ex s being Symbol of G st
( n = (n1 ^ <*s*>) ^ n2 & m = (n1 ^ n3) ^ n2 & 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 & m = (n1 ^ n3) ^ n2 & 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 ;

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

proof end;

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

proof end;

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 & n1 ^ n ==> n2 ^ n )

proof end;

definition

let G be non empty DTConstrStr ;
let n, m be String of G;

pred m is_derivable_from n means :: LANG1:def 5
ex p being FinSequence st
( len p >= 1 & p . 1 = n & p . (len p) = m & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) );

end;

:: deftheorem 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 & p . 1 = n & p . (len p) = m & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) ) );

theorem Th6: :: LANG1:6

for G being non empty DTConstrStr
for n being String of G holds n is_derivable_from n

proof end;

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

proof end;

theorem Th8: :: LANG1:8

for G being non empty DTConstrStr
for n1, n2, n3 being String of G st n1 is_derivable_from n2 & n2 is_derivable_from n3 holds
n1 is_derivable_from n3

proof end;

:: 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 & a is_derivable_from <* the InitialSym of G*> ) } ;

coherence
{ a where a is Element of the carrier of G * : ( rng a c= Terminals G & 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 & 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 & n is_derivable_from <* the InitialSym of G*> ) )

proof end;

:: 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

proof end;

let b be Element of [:D,E:];
:: original: {
redefine func {a,b} -> Relation of D,E;
coherence
{a,b} is Relation of D,E

proof end;

end;

definition

let a be set ;

func EmptyGrammar a -> strict GrammarStr means :Def7: :: LANG1:def 7
( the carrier of it = {a} & the Rules of it = {[a,{}]} );

existence
ex b₁ being strict GrammarStr st
( the carrier of b₁ = {a} & the Rules of b₁ = {[a,{}]} )

proof end;

uniqueness
for b₁, b₂ being strict GrammarStr st the carrier of b₁ = {a} & the Rules of b₁ = {[a,{}]} & the carrier of b₂ = {a} & the Rules of b₂ = {[a,{}]} holds
b₁ = b₂

proof end;

let b be set ;

func SingleGrammar (a,b) -> strict GrammarStr means :Def8: :: LANG1:def 8
( the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b*>]} );

existence
ex b₁ being strict GrammarStr st
( the carrier of b₁ = {a,b} & the InitialSym of b₁ = a & the Rules of b₁ = {[a,<*b*>]} )

proof end;

uniqueness
for b₁, b₂ being strict GrammarStr st the carrier of b₁ = {a,b} & the InitialSym of b₁ = a & the Rules of b₁ = {[a,<*b*>]} & the carrier of b₂ = {a,b} & the InitialSym of b₂ = a & the Rules of b₂ = {[a,<*b*>]} holds
b₁ = b₂ ;

func IterGrammar (a,b) -> strict GrammarStr means :Def9: :: LANG1:def 9
( the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b,a*>],[a,{}]} );

existence
ex b₁ being strict GrammarStr st
( the carrier of b₁ = {a,b} & the InitialSym of b₁ = a & the Rules of b₁ = {[a,<*b,a*>],[a,{}]} )

proof end;

uniqueness
for b₁, b₂ being strict GrammarStr st the carrier of b₁ = {a,b} & the InitialSym of b₁ = a & the Rules of b₁ = {[a,<*b,a*>],[a,{}]} & the carrier of b₂ = {a,b} & the InitialSym of b₂ = a & the Rules of b₂ = {[a,<*b,a*>],[a,{}]} holds
b₁ = b₂ ;

end;

:: deftheorem Def7 defines EmptyGrammar LANG1:def 7 :
for a being set
for b₂ being strict GrammarStr holds
( b₂ = EmptyGrammar a iff ( the carrier of b₂ = {a} & the Rules of b₂ = {[a,{}]} ) );

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

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

registration

let a be set ;

cluster EmptyGrammar a -> non empty strict ;

coherence
not EmptyGrammar a is empty

proof end;

let b be set ;

cluster SingleGrammar (a,b) -> non empty strict ;

coherence
not SingleGrammar (a,b) is empty

proof end;

cluster IterGrammar (a,b) -> non empty strict ;

coherence
not IterGrammar (a,b) is empty

proof end;

end;

definition

let D be non empty set ;

func TotalGrammar D -> strict GrammarStr means :Def10: :: LANG1:def 10
( the carrier of it = succ D & the InitialSym of it = D & the Rules of it = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} );

existence
ex b₁ being strict GrammarStr st
( the carrier of b₁ = succ D & the InitialSym of b₁ = D & the Rules of b₁ = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} )

proof end;

uniqueness
for b₁, b₂ being strict GrammarStr st the carrier of b₁ = succ D & the InitialSym of b₁ = D & the Rules of b₁ = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} & the carrier of b₂ = succ D & the InitialSym of b₂ = D & the Rules of b₂ = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} holds
b₁ = b₂ ;

end;

:: deftheorem Def10 defines TotalGrammar LANG1:def 10 :
for D being non empty set
for b₂ being strict GrammarStr holds
( b₂ = TotalGrammar D iff ( the carrier of b₂ = succ D & the InitialSym of b₂ = D & the Rules of b₂ = { [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

proof end;

end;

theorem Th10: :: LANG1:10

for a being set holds Terminals (EmptyGrammar a) = {}

proof end;

theorem Th11: :: LANG1:11

for a being set holds Lang (EmptyGrammar a) = {{}}

proof end;

theorem Th12: :: LANG1:12

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

proof end;

theorem :: LANG1:13

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

proof end;

theorem Th14: :: LANG1:14

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

proof end;

theorem :: LANG1:15

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

proof end;

theorem Th16: :: LANG1:16

for D being non empty set holds Terminals (TotalGrammar D) = D

proof end;

theorem :: LANG1:17

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

proof end;

definition

let IT be non empty GrammarStr ;

attr IT is effective means :Def11: :: LANG1:def 11
( not Lang IT is empty & the InitialSym of IT in NonTerminals IT & ( for s being Symbol of IT st s in Terminals IT holds
ex p being String of IT st
( p in Lang IT & s in rng p ) ) );

end;

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

definition

let IT be GrammarStr ;

attr IT 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 effective finite for GrammarStr ;

existence
ex b₁ being non empty GrammarStr st
( b₁ is effective & b₁ is finite )

proof end;

end;

definition

let G be non empty effective GrammarStr ;
:: original: NonTerminals
redefine func NonTerminals G -> non empty Subset of G;
coherence
NonTerminals G is non empty Subset of G

proof end;

end;

definition

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

proof end;

end;

definition

let X, Y be non empty set ;
let f be Function of X,Y;

func f * -> Function of (X *),(Y *) means :: LANG1:def 13
for p being Element of X * holds it . p = f * p;

existence
ex b₁ being Function of (X *),(Y *) st
for p being Element of X * holds b₁ . p = f * p

proof end;

uniqueness
for b₁, b₂ being Function of (X *),(Y *) st ( for p being Element of X * holds b₁ . p = f * p ) & ( for p being Element of X * holds b₂ . p = f * p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines * LANG1:def 13 :
for X, Y being non empty set
for f being Function of X,Y
for b₄ being Function of (X *),(Y *) holds
( b₄ = f * iff for p being Element of X * holds b₄ . p = f * p );

theorem :: LANG1:18

for R being Relation holds R c= R [*]

proof end;

definition

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

proof end;

end;

definition

let G be non empty GrammarStr ;
let X be non empty set ;
let f be Function of the carrier of G,X;

func G . 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 *)) #);