:: by Patricia L. Carlson and Grzegorz Bancerek

::

:: Received February 21, 1992

:: Copyright (c) 1992-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct DTConstrStr -> 1-sorted ;

aggr DTConstrStr(# carrier, Rules #) -> DTConstrStr ;

sel Rules c_{1} -> Relation of the carrier of c_{1},( the carrier of c_{1} *);

end;
struct DTConstrStr -> 1-sorted ;

aggr DTConstrStr(# carrier, Rules #) -> DTConstrStr ;

sel Rules c

registration
end;

definition

attr c_{1} is strict ;

struct GrammarStr -> DTConstrStr ;

aggr GrammarStr(# carrier, InitialSym, Rules #) -> GrammarStr ;

sel InitialSym c_{1} -> Element of the carrier of c_{1};

end;
struct GrammarStr -> DTConstrStr ;

aggr GrammarStr(# carrier, InitialSym, Rules #) -> GrammarStr ;

sel InitialSym c

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;
mode Symbol of G is Element of G;

mode String of G is Element of the carrier of G * ;

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

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 ;

{ s where s is Symbol of G : for n being FinSequence holds not s ==> n } is set ;

{ s where s is Symbol of G : ex n being FinSequence st s ==> n } is set ;

end;
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 } ;

{ 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 } ;

{ s where s is Symbol of G : ex n being FinSequence st s ==> n } is set ;

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

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 } ;

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

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

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

for s being Symbol of G

for n, n1, n2 being String of G st s ==> n holds

(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2

proof end;

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

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

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 )

for n, n1, n2 being String of G st n1 ==> n2 holds

( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n )

proof 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 & 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 ) ) ) );

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

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 ;

{ 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;
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*> ) } ;

{ 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 ;

:: 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*> ) } ;

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*> ) )

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}

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

:: original: {

redefine func {a,b} -> Relation of D,E;

coherence

{a,b} is Relation of D,E

end;
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;

definition

let a be set ;

ex b_{1} being strict GrammarStr st

( the carrier of b_{1} = {a} & the Rules of b_{1} = {[a,{}]} )

for b_{1}, b_{2} being strict GrammarStr st the carrier of b_{1} = {a} & the Rules of b_{1} = {[a,{}]} & the carrier of b_{2} = {a} & the Rules of b_{2} = {[a,{}]} holds

b_{1} = b_{2}

ex b_{1} being strict GrammarStr st

( the carrier of b_{1} = {a,b} & the InitialSym of b_{1} = a & the Rules of b_{1} = {[a,<*b*>]} )

for b_{1}, b_{2} being strict GrammarStr st the carrier of b_{1} = {a,b} & the InitialSym of b_{1} = a & the Rules of b_{1} = {[a,<*b*>]} & the carrier of b_{2} = {a,b} & the InitialSym of b_{2} = a & the Rules of b_{2} = {[a,<*b*>]} holds

b_{1} = b_{2}
;

ex b_{1} being strict GrammarStr st

( the carrier of b_{1} = {a,b} & the InitialSym of b_{1} = a & the Rules of b_{1} = {[a,<*b,a*>],[a,{}]} )

for b_{1}, b_{2} being strict GrammarStr st the carrier of b_{1} = {a,b} & the InitialSym of b_{1} = a & the Rules of b_{1} = {[a,<*b,a*>],[a,{}]} & the carrier of b_{2} = {a,b} & the InitialSym of b_{2} = a & the Rules of b_{2} = {[a,<*b,a*>],[a,{}]} holds

b_{1} = b_{2}
;

end;
func EmptyGrammar a -> strict GrammarStr means :Def7: :: LANG1:def 7

( the carrier of it = {a} & the Rules of it = {[a,{}]} );

existence ( the carrier of it = {a} & the Rules of it = {[a,{}]} );

ex b

( the carrier of b

proof end;

uniqueness for 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 ( the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b*>]} );

ex b

( the carrier of b

proof end;

uniqueness for 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 ( the carrier of it = {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b,a*>],[a,{}]} );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def7 defines EmptyGrammar LANG1:def 7 :

for a being set

for b_{2} being strict GrammarStr holds

( b_{2} = EmptyGrammar a iff ( the carrier of b_{2} = {a} & the Rules of b_{2} = {[a,{}]} ) );

for a being set

for b

( b

:: deftheorem Def8 defines SingleGrammar LANG1:def 8 :

for a, b being set

for b_{3} being strict GrammarStr holds

( b_{3} = SingleGrammar (a,b) iff ( the carrier of b_{3} = {a,b} & the InitialSym of b_{3} = a & the Rules of b_{3} = {[a,<*b*>]} ) );

for a, b being set

for b

( b

:: deftheorem Def9 defines IterGrammar LANG1:def 9 :

for a, b being set

for b_{3} being strict GrammarStr holds

( b_{3} = IterGrammar (a,b) iff ( the carrier of b_{3} = {a,b} & the InitialSym of b_{3} = a & the Rules of b_{3} = {[a,<*b,a*>],[a,{}]} ) );

for a, b being set

for b

( b

registration

let a be set ;

coherence

not EmptyGrammar a is empty

coherence

not SingleGrammar (a,b) is empty

not IterGrammar (a,b) is empty

end;
coherence

not EmptyGrammar a is empty

proof end;

let b be set ;coherence

not SingleGrammar (a,b) is empty

proof end;

coherence not IterGrammar (a,b) is empty

proof end;

definition

let D be non empty set ;

ex b_{1} being strict GrammarStr st

( the carrier of b_{1} = succ D & the InitialSym of b_{1} = D & the Rules of b_{1} = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} )

for b_{1}, b_{2} being strict GrammarStr st the carrier of b_{1} = succ D & the InitialSym of b_{1} = D & the Rules of b_{1} = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} & the carrier of b_{2} = succ D & the InitialSym of b_{2} = D & the Rules of b_{2} = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} holds

b_{1} = b_{2}
;

end;
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 ( 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,{}]} );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines TotalGrammar LANG1:def 10 :

for D being non empty set

for b_{2} being strict GrammarStr holds

( b_{2} = TotalGrammar D iff ( the carrier of b_{2} = succ D & the InitialSym of b_{2} = D & the Rules of b_{2} = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} ) );

for D being non empty set

for b

( b

:: deftheorem Def11 defines efective LANG1:def 11 :

for IT being non empty GrammarStr holds

( IT is efective 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 ) ) ) );

for IT being non empty GrammarStr holds

( IT is efective 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
end;

:: deftheorem defines finite LANG1:def 12 :

for IT being GrammarStr holds

( IT is finite iff the Rules of IT is finite );

for IT being GrammarStr holds

( IT is finite iff the Rules of IT is finite );

registration
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

end;
:: original: NonTerminals

redefine func NonTerminals G -> non empty Subset of G;

coherence

NonTerminals G is non empty Subset of G

proof 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 *

end;
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;

definition

let X, Y be non empty set ;

let f be Function of X,Y;

ex b_{1} being Function of (X *),(Y *) st

for p being Element of X * holds b_{1} . p = f * p

for b_{1}, b_{2} being Function of (X *),(Y *) st ( for p being Element of X * holds b_{1} . p = f * p ) & ( for p being Element of X * holds b_{2} . p = f * p ) holds

b_{1} = b_{2}

end;
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 for p being Element of X * holds it . p = f * p;

ex b

for p being Element of X * holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines * LANG1:def 13 :

for X, Y being non empty set

for f being Function of X,Y

for b_{4} being Function of (X *),(Y *) holds

( b_{4} = f * iff for p being Element of X * holds b_{4} . p = f * p );

for X, Y being non empty set

for f being Function of X,Y

for b

( b

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

end;
let R be Relation of X;

:: original: [*]

redefine func R [*] -> Relation of X;

coherence

R [*] is Relation of X

proof end;

definition

let G be non empty GrammarStr ;

let X be non empty set ;

let f be Function of the carrier of G,X;

coherence

GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #) is strict GrammarStr ;

;

end;
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 GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #);

coherence

GrammarStr(# X,(f . the InitialSym of G),(((f ~) * the Rules of G) * (f *)) #) is strict GrammarStr ;

;

:: 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 *)) #);

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

:: a set of non-terminal and terminal symbols, I is an initial symbol,

:: and R is a set of rules (ordered pairs).