:: Context-Free Grammar - Part 1 :: by Patricia L. Carlson and Grzegorz Bancerek :: :: Received February 21, 1992 :: Copyright (c) 1992-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, STRUCT_0, RELAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, TDGROUP, TARSKI, ORDINAL4, ARYTM_3, CARD_1, FUNCT_1, XXREAL_0, NAT_1, ZFMISC_1, ORDINAL1, FINSET_1, LANG1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, DOMAIN_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, FINSET_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_2, XXREAL_0, PRE_POLY; constructors PARTFUN1, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0, RELSET_1, PRE_POLY; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, FINSEQ_1, STRUCT_0, ORDINAL1, CARD_1, RELSET_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; 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 struct(1-sorted) DTConstrStr (# carrier -> set, Rules -> Relation of the carrier, (the carrier)* #); end; registration cluster non empty strict for DTConstrStr; end; definition struct(DTConstrStr) GrammarStr (# carrier -> set, InitialSym -> Element of the carrier, Rules -> Relation of the carrier, (the carrier)* #); end; registration cluster non empty for GrammarStr; 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; reserve G for non empty DTConstrStr, s for Symbol of G, n,m for String of G; definition let G,s; let n be FinSequence; pred s ==> n means :: LANG1:def 1 [s,n] in the Rules of G; end; definition let G; func Terminals G -> set equals :: LANG1:def 2 { s : not ex n being FinSequence st s ==> n}; func NonTerminals G -> set equals :: LANG1:def 3 { s : ex n being FinSequence st s ==> n}; end; theorem :: LANG1:1 Terminals(G) \/ NonTerminals(G) = the carrier of G; definition let G,n,m; pred n ==> m means :: LANG1:def 4 ex n1,n2,n3 being String of G, s st n = n1^<*s*>^n2 & m = n1^n3^n2 & s ==> n3; end; reserve n1,n2,n3 for String of G; theorem :: LANG1:2 s ==> n implies n1^<*s*>^n2 ==> n1^n^n2; theorem :: LANG1:3 s ==> n implies <*s*> ==> n; theorem :: LANG1:4 <*s*> ==> n implies s ==> n; theorem :: LANG1:5 n1 ==> n2 implies n^n1 ==> n^n2 & n1^n ==> n2^n; definition let G, n, m; 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 ex a ,b being String of G st p.i = a & p.(i+1) = b & a ==> b; end; theorem :: LANG1:6 n is_derivable_from n; theorem :: LANG1:7 n ==> m implies m is_derivable_from n; theorem :: LANG1:8 n1 is_derivable_from n2 & n2 is_derivable_from n3 implies n1 is_derivable_from n3; :: 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*>}; end; theorem :: LANG1:9 for G being non empty GrammarStr, n being String of G holds n in Lang( G) iff rng n c= Terminals(G) & n is_derivable_from <*the InitialSym of G*>; :: 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, a be Element of [:D,E:]; redefine func {a} -> Relation of D,E; let b be Element of [:D,E:]; redefine func {a,b} -> Relation of D,E; end; definition let a be set; func EmptyGrammar a -> strict GrammarStr means :: LANG1:def 7 the carrier of it = {a } & the Rules of it = {[a,{}]}; let b be set; func SingleGrammar(a,b) -> strict GrammarStr means :: LANG1:def 8 the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b*>]}; func IterGrammar(a,b) -> strict GrammarStr means :: LANG1:def 9 the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b,a*>],[a,{}]}; end; registration let a be set; cluster EmptyGrammar a -> non empty; let b be set; cluster SingleGrammar(a,b) -> non empty; cluster IterGrammar(a,b) -> non empty; end; definition let D be non empty set; func TotalGrammar D -> strict GrammarStr means :: 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,{}]}; end; registration let D be non empty set; cluster TotalGrammar D -> non empty; end; reserve a,b,c for set, D for non empty set, d for Element of D; theorem :: LANG1:10 Terminals EmptyGrammar a = {}; theorem :: LANG1:11 Lang EmptyGrammar a = {{}}; theorem :: LANG1:12 a <> b implies Terminals SingleGrammar(a,b) = {b}; theorem :: LANG1:13 a <> b implies Lang SingleGrammar(a,b) = {<*b*>}; theorem :: LANG1:14 a <> b implies Terminals IterGrammar(a,b) = {b}; theorem :: LANG1:15 a <> b implies Lang IterGrammar(a,b) = {b}*; theorem :: LANG1:16 Terminals TotalGrammar D = D; theorem :: LANG1:17 Lang TotalGrammar D = D*; definition let IT be non empty GrammarStr; attr IT is effective means :: LANG1:def 11 Lang IT is non empty & the InitialSym of IT in NonTerminals IT & for s being Symbol of IT st s in Terminals IT ex p being String of IT st p in Lang(IT) & s in rng p; end; definition let IT be GrammarStr; attr IT is finite means :: LANG1:def 12 the Rules of IT is finite; end; registration cluster effective finite for non empty GrammarStr; end; definition let G be effective non empty GrammarStr; redefine func NonTerminals G -> non empty Subset of G; end; definition let X,Y be non empty set, p be FinSequence of X, f be Function of X,Y; redefine func f*p -> Element of Y*; 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; end; reserve R for Relation, x,y for set; theorem :: LANG1:18 R c= R[*]; definition let X be non empty set, R be Relation of X; redefine func R[*] -> Relation of X; 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*) #); end; :: The goal is to show: :: f is_one-to-one implies f*.:Lang(G) = Lang(G.f)