The abstract of the Mizar article:

Context-Free Grammar --- Part I

by

Patricia L. Carlson, and

Grzegorz Bancerek

Received February 21, 1992

MML identifier: LANG1

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FINSEQ_1, TDGROUP, BOOLE, FUNCT_1, FINSET_1, LANG1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, DOMAIN_1,
      RELAT_1, STRUCT_0, RELSET_1, FUNCT_1, FINSEQ_1, FINSET_1, FUNCT_2,
      FINSEQ_2;
 constructors STRUCT_0, NAT_1, DOMAIN_1, FUNCT_2, FINSEQ_2, XREAL_0, MEMBERED,
      XBOOLE_0;
 clusters SUBSET_1, RELAT_1, FINSEQ_1, FINSET_1, RELSET_1, STRUCT_0, XBOOLE_0,
      XREAL_0, ARYTM_3, ZFMISC_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;

definition
 cluster non empty strict DTConstrStr;
end;

definition
  struct(DTConstrStr) GrammarStr (#
           carrier -> set,
           InitialSym -> Element of the carrier,
           Rules -> Relation of the carrier, (the carrier)*
         #);
end;

definition
 cluster non empty 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;

   definition
    let D be set;
    let p, q be Element of D*;
    redefine func p^q -> Element of D*;
   end;

   definition
    let D be set;
    cluster empty Element of D*;
   end;

   definition
    let D be set;
    redefine func <*> D -> empty Element of D*;
   end;

   definition
    let D be non empty set;
    let d be Element of D;
    redefine func <*d*> -> Element of D*;
    let e be Element of D;
    func <*d,e*> -> Element of D*;
   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 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:];
 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;

definition
 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 = D \/ {D} & the InitialSym of it = D &
       the Rules of it = {[D,<*d,D*>] where d is Element of D: d = d} \/
        {[D,{}]};
end;

definition 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 efective 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;

definition
 cluster efective finite (non empty GrammarStr);
end;

definition
 let G be efective (non empty GrammarStr);
 redefine
  func NonTerminals G -> non empty Subset of G;
end;

definition
 let X be set, Y be non empty set;
 cluster Function-like Relation of X,Y;
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 R be Relation;
 func R* -> Relation means
:: LANG1:def 13

  for x,y being set holds [x,y] in it iff x in field R & y in field R &
   ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y &
    for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R;
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 14
     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 15
     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)

theorem :: LANG1:19
   for D1,D2 being set st D1 c= D2 holds D1* c= D2*;