The abstract of the Mizar article:

On Defining Functions on Trees

by

Grzegorz Bancerek, and

Piotr Rudnicki

Received October 12, 1993

MML identifier: DTCONSTR

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, TREES_3, RELAT_1, FUNCT_1, FINSET_1, TREES_2, BOOLE,
      TREES_4, FUNCT_3, MCART_1, LANG1, TDGROUP, PROB_1, TARSKI, TREES_1,
      FUNCT_6, BINOP_1, FINSOP_1, FINSEQ_2, DTCONSTR;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      RELSET_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      FINSET_1, MCART_1, PROB_1, DOMAIN_1, BINOP_1, FINSOP_1, LANG1, TREES_1,
      TREES_2, TREES_3, TREES_4, FINSEQOP;
 constructors NAT_1, PROB_1, DOMAIN_1, BINOP_1, FINSOP_1, LANG1, TREES_4,
      MEMBERED, PARTFUN1, XBOOLE_0, FINSEQOP;
 clusters SUBSET_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, FUNCT_1,
      RELSET_1, FINSEQ_1, STRUCT_0, XREAL_0, NAT_1, MEMBERED, ZFMISC_1,
      XBOOLE_0, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

theorem :: DTCONSTR:1  :: This really belongs elsewhere
for D being non empty set, p being FinSequence of FinTrees D holds
 p is FinSequence of Trees D;

theorem :: DTCONSTR:2
 for x,y being set, p being FinSequence of x
   st y in dom p holds p.y in x;
:: This definition really belongs elsewhere

definition
 let X be set;
 cluster -> Relation-like Function-like Element of X*;
  :: for x being Element of X* holds x is Function-like
end;

definition
 let X be set;
 cluster -> FinSequence-like Element of X*;
end;

definition
 let D be non empty set, t be Element of FinTrees D;
 cluster dom t -> finite;
end;

definition
 let D be non empty set, T be DTree-set of D;
 cluster -> DTree-yielding FinSequence of T;
end;

definition
 let D be non empty set;
 let F be non empty DTree-set of D;
 let Tset be non empty Subset of F;
 redefine mode Element of Tset -> Element of F;
end;

definition
 let p be FinSequence such that
 p is DTree-yielding;
 func roots p -> FinSequence means
:: DTCONSTR:def 1
  dom it = dom p & for i being Nat st i in dom p
   ex T being DecoratedTree st T = p.i & it.i = T.{};
end;

definition
 let D be non empty set, T be DTree-set of D;
 let p be FinSequence of T;
  redefine func roots p -> FinSequence of D;
end;
theorem :: DTCONSTR:3
roots {} = {};

theorem :: DTCONSTR:4
for T being DecoratedTree holds roots <*T*> = <*T.{}*>;

theorem :: DTCONSTR:5
for D being non empty set, F being (Subset of FinTrees D),
    p being FinSequence of F st len roots p = 1
  ex x being Element of FinTrees D st p = <*x*> & x in F;

theorem :: DTCONSTR:6
  for T1, T2 being DecoratedTree holds
  roots <*T1, T2*> = <*T1.{}, T2.{}*>;

definition
 let f be Function;
 func pr1 f -> Function means
:: DTCONSTR:def 2
  dom it = dom f & for x being set st x in dom f holds it.x = (f.x)`1;
 func pr2 f -> Function means
:: DTCONSTR:def 3
  dom it = dom f & for x being set st x in dom f holds it.x = (f.x)`2;
end;

definition
 let X, Y be set, f be FinSequence of [:X, Y:];
 redefine func pr1 f -> FinSequence of X;
          func pr2 f -> FinSequence of Y;
end;

theorem :: DTCONSTR:7
pr1 {} = {} & pr2 {} = {};

scheme MonoSetSeq { f() -> Function, A() -> set, H(set, set) -> set}:
 for k, s being Nat holds f().k c= f().(k+s)
provided
 for n being Nat holds f().(n+1) = f().n \/ H(n, f().n);

begin

definition
  let A be non empty set, R be Relation of A,A*;
 cluster DTConstrStr(#A,R#) -> non empty;
end;

scheme DTConstrStrEx { S() -> non empty set,
                       P[set, set] }:
 ex G be strict non empty DTConstrStr st the carrier of G = S() &
  for x being Symbol of G, p being FinSequence of the carrier of G
   holds x ==> p iff P[x, p];

scheme DTConstrStrUniq { S() -> non empty set,
                         P[set, set] }:
 for G1, G2 being strict non empty DTConstrStr
  st (the carrier of G1 = S() &
       for x being Symbol of G1, p being FinSequence of the carrier of G1
         holds x ==> p iff P[x, p]) &
      (the carrier of G2 = S() &
       for x being Symbol of G2, p being FinSequence of the carrier of G2
         holds x ==> p iff P[x, p])
   holds G1 = G2;

theorem :: DTCONSTR:8
  for G being non empty DTConstrStr holds
      Terminals G misses NonTerminals G;

scheme DTCMin { f() -> Function,
                G() -> non empty DTConstrStr, D() -> non empty set,
                TermVal(set) -> Element of D(),
                NTermVal(set, set, set) -> Element of D()}:
ex X being Subset of FinTrees [:the carrier of G(), D():]
 st X = Union f() &
    (for d being Symbol of G() st d in Terminals G()
                               holds root-tree [d, TermVal(d)] in X) &
    (for o being Symbol of G(),
         p being FinSequence of X st o ==> pr1 roots p
            holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
    (for F being Subset of FinTrees [:the carrier of G(), D():] st
        (for d being Symbol of G() st d in Terminals G()
                               holds root-tree [d, TermVal(d)] in F ) &
        (for o being Symbol of G(),
             p being FinSequence of F st o ==> pr1 roots p
            holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F)
       holds X c= F )
provided
  dom f() = NAT and
  f().0 = { root-tree [t, d] where t is Symbol of G(),
                                  d is Element of D() :
           t in Terminals G() & d = TermVal(t) or
           t ==> {} & d = NTermVal(t, {}, {}) } and
  for n being Nat holds f().(n+1) =
     f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
           where o is Symbol of G(), p is Element of (f().n)* :
            ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
                               p = q & o ==> pr1 roots q };

scheme DTCSymbols { f() -> Function,
                    G() -> non empty DTConstrStr, D() -> non empty set,
                    TermVal(set) -> Element of D(),
                    NTermVal(set, set, set) -> Element of D()}:
ex X1 being Subset of FinTrees(the carrier of G()) st
 X1 = { t`1 where t is Element of FinTrees [:(the carrier of G()), D():] :
                    t in Union f() } &
 (for d being Symbol of G() st d in Terminals G() holds root-tree d in X1) &
 (for o being Symbol of G(), p being FinSequence of X1 st o ==> roots p
    holds o-tree p in X1) &
 for F being Subset of FinTrees the carrier of G() st
  (for d being Symbol of G() st d in Terminals G() holds root-tree d in F) &
  (for o being Symbol of G(), p being FinSequence of F st o ==> roots p
           holds o-tree p in F)
  holds X1 c= F
provided
  dom f() = NAT and
  f().0 = { root-tree [t, d] where t is Symbol of G(),
                                  d is Element of D() :
           t in Terminals G() & d = TermVal(t) or
           t ==> {} & d = NTermVal(t, {}, {}) } and
  for n being Nat holds f().(n+1) =
     f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
           where o is Symbol of G(), p is Element of (f().n)* :
            ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
                               p = q & o ==> pr1 roots q };

scheme DTCHeight { f() -> Function,
                   G() -> non empty DTConstrStr, D() -> non empty set,
                   TermVal(set) -> Element of D(),
                   NTermVal(set, set, set) -> Element of D()}:
for n being Nat, dt being Element of FinTrees [:the carrier of G(), D():]
 st dt in Union f() holds dt in f().n iff height dom dt <= n
provided
  dom f() = NAT and
  f().0 = { root-tree [t, d] where t is Symbol of G(),
                                  d is Element of D() :
           t in Terminals G() & d = TermVal(t) or
           t ==> {} & d = NTermVal(t, {}, {}) } and
  for n being Nat holds f().(n+1) =
     f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
           where o is Symbol of G(), p is Element of (f().n)* :
            ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
                               p = q & o ==> pr1 roots q };

scheme DTCUniq { f() -> Function,
                   G() -> non empty DTConstrStr, D() -> non empty set,
                   TermVal(set) -> Element of D(),
                   NTermVal(set, set, set) -> Element of D()}:
for dt1, dt2 being DecoratedTree of [:(the carrier of G()), D():]
 st dt1 in Union f() & dt2 in Union f() & dt1`1 = dt2`1 holds dt1 = dt2
provided
  dom f() = NAT and
  f().0 = { root-tree [t, d] where t is Symbol of G(),
                                  d is Element of D() :
           t in Terminals G() & d = TermVal(t) or
           t ==> {} & d = NTermVal(t, {}, {}) } and
  for n being Nat holds f().(n+1) =
     f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
           where o is Symbol of G(), p is Element of (f().n)* :
            ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
                               p = q & o ==> pr1 roots q };

definition
 let G be non empty DTConstrStr;
 func TS(G) -> Subset of FinTrees(the carrier of G) means
:: DTCONSTR:def 4

  (for d being Symbol of G st d in Terminals G holds root-tree d in it) &
  (for o being Symbol of G, p being FinSequence of it st o ==> roots p
         holds o-tree p in it) &
  for F being Subset of FinTrees the carrier of G st
  (for d being Symbol of G st d in Terminals G holds root-tree d in F) &
  (for o being Symbol of G, p being FinSequence of F st o ==> roots p
         holds o-tree p in F)
   holds it c= F;
end;

scheme DTConstrInd{ G()->non empty DTConstrStr, P[set] }:
 for t being DecoratedTree of the carrier of G()
       st t in TS(G()) holds P[t]
 provided
 for s being Symbol of G() st s in Terminals G() holds P[root-tree s]
    and
 for nt being Symbol of G(),
       ts being FinSequence of TS(G()) st nt ==> roots ts &
            for t being DecoratedTree of the carrier of G() st t in rng ts
                      holds P[t]
    holds P[nt-tree ts];

scheme DTConstrIndDef{G()->non empty DTConstrStr, D()->non empty set,
                   TermVal(set) -> Element of D(),
                   NTermVal(set, set, set) -> Element of D()
                   }:
 ex f being Function of TS(G()), D() st
  (for t being Symbol of G() st t in Terminals G()
         holds f.(root-tree t) = TermVal(t)) &
  (for nt being Symbol of G(),
       ts being FinSequence of TS(G()) st nt ==> roots ts
         holds f.(nt-tree ts) = NTermVal(nt, roots ts, f * ts));

scheme DTConstrUniqDef{G()->non empty DTConstrStr, D()->non empty set,
                   TermVal(set) -> Element of D(),
                   NTermVal(set, set, set) -> Element of D(),
                   f1, f2() -> Function of TS(G()), D()
                   }:
 f1() = f2()
provided
  (for t being Symbol of G() st t in Terminals G()
            holds f1().(root-tree t) = TermVal(t)) &
     (for nt being Symbol of G(),
          ts being FinSequence of TS(G()) st nt ==> roots ts
              holds f1().(nt-tree ts) = NTermVal(nt, roots ts, f1() * ts))
and
  (for t being Symbol of G() st t in Terminals G()
            holds f2().(root-tree t) = TermVal(t)) &
     (for nt being Symbol of G(),
          ts being FinSequence of TS(G()) st nt ==> roots ts
              holds f2().(nt-tree ts) = NTermVal(nt, roots ts, f2() * ts));

begin

definition
 func PeanoNat -> strict non empty DTConstrStr means
:: DTCONSTR:def 5
 the carrier of it = {0, 1} &
        for x being Symbol of it, y being FinSequence of the carrier of it
         holds x ==> y iff x=1 & (y=<*0*> or y=<*1*>);
end;

begin

:: Some properties of decorated tree constructions :::::::::::::::::::::::::

definition let G be non empty DTConstrStr;
 attr G is with_terminals means
:: DTCONSTR:def 6
 Terminals G <> {};
 attr G is with_nonterminals means
:: DTCONSTR:def 7
  NonTerminals G <> {};
 attr G is with_useful_nonterminals means
:: DTCONSTR:def 8
  for nt being Symbol of G st nt in NonTerminals G
   ex p being FinSequence of TS(G) st nt ==> roots p;
end;

definition
 cluster with_terminals with_nonterminals with_useful_nonterminals strict
         (non empty DTConstrStr);
end;

definition
 let G be with_terminals (non empty DTConstrStr);
 redefine func Terminals G -> non empty Subset of G;
  cluster TS G -> non empty;
end;

definition
 let G be with_useful_nonterminals (non empty DTConstrStr);
 cluster TS G -> non empty;
end;

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

definition
 let G be with_terminals (non empty DTConstrStr);
 mode Terminal of G is Element of Terminals G;
end;

definition
 let G be with_nonterminals (non empty DTConstrStr);
 mode NonTerminal of G is Element of NonTerminals G;
end;

definition
 let G be with_nonterminals with_useful_nonterminals (non empty DTConstrStr);
 let nt be NonTerminal of G;
 mode SubtreeSeq of nt -> FinSequence of TS(G) means
:: DTCONSTR:def 9

  nt ==> roots it;
end;

definition
 let G be with_terminals (non empty DTConstrStr);
 let t be Terminal of G;
 redefine func root-tree t -> Element of TS(G);
end;

definition
 let G be with_nonterminals with_useful_nonterminals (non empty DTConstrStr);
 let nt be NonTerminal of G;
 let p be SubtreeSeq of nt;
 redefine func nt-tree p -> Element of TS(G);
end;

theorem :: DTCONSTR:9
for G being with_terminals (non empty DTConstrStr),
               tsg being Element of TS G,
                 s being Terminal of G
               st tsg.{} = s holds tsg = root-tree s;

theorem :: DTCONSTR:10
 for G being with_terminals with_nonterminals (non empty DTConstrStr),
               tsg being Element of TS G,
                nt being NonTerminal of G
               st tsg.{} = nt
               ex ts being FinSequence of TS G
                st tsg = nt-tree ts & nt ==> roots ts;

begin

:: Peano naturals continued ::::::::::::::::::::::::::::::::::::::::::::::::

definition
 cluster PeanoNat ->
     with_terminals with_nonterminals with_useful_nonterminals;
end;

definition
 let nt be NonTerminal of PeanoNat,
      t be Element of TS PeanoNat;
 redefine func nt-tree t -> Element of TS PeanoNat;
end;

definition
 let x be FinSequence of NAT such that
 x <> {};
 func plus-one x -> Nat means
:: DTCONSTR:def 10
  ex n being Nat st it = n+1 & x.1 = n;
end;

definition
 func PN-to-NAT -> Function of TS(PeanoNat), NAT means
:: DTCONSTR:def 11
  (for t being Symbol of PeanoNat st t in Terminals PeanoNat
         holds it.(root-tree t) = 0) &
  (for nt being Symbol of PeanoNat,
       ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
         holds it.(nt-tree ts) = plus-one(it * ts));
end;

definition
 let x be Element of TS(PeanoNat);
 func PNsucc x -> Element of TS(PeanoNat) equals
:: DTCONSTR:def 12
  1-tree <*x*>;
end;

definition
 func NAT-to-PN -> Function of NAT, TS(PeanoNat) means
:: DTCONSTR:def 13
   it.0 = root-tree 0 &
  for n being Nat holds it.(n+1) = PNsucc it.n;
end;

theorem :: DTCONSTR:11
  for pn being Element of TS(PeanoNat) holds pn = NAT-to-PN.(PN-to-NAT.pn);

theorem :: DTCONSTR:12
  for n being Nat holds n = PN-to-NAT.(NAT-to-PN.n);

begin

:: Tree traversals and terminal language :::::::::::::::::::::::::::::::::::

definition
 let D be set, F be FinSequence of D*;
 func FlattenSeq F -> Element of D* means
:: DTCONSTR:def 14
  ex g being BinOp of D* st
   (for p, q being Element of D* holds g.(p,q) = p^q) &
     it = g "**" F;
end;

theorem :: DTCONSTR:13
 for D being set, d be Element of D* holds FlattenSeq <*d*> = d;

definition
 let G be non empty DTConstrStr, tsg be DecoratedTree of the carrier of G;
 assume
 tsg in TS G;
 func TerminalString tsg -> FinSequence of Terminals G means
:: DTCONSTR:def 15
   ex f being Function of (TS G), (Terminals G)* st
    it = f.tsg &
     (for t being Symbol of G st t in Terminals G
         holds f.(root-tree t) = <*t*>) &
     (for nt being Symbol of G,
       ts being FinSequence of TS(G) st nt ==> roots ts
             holds f.(nt-tree ts) = FlattenSeq(f * ts));
 func PreTraversal tsg -> FinSequence of the carrier of G means
:: DTCONSTR:def 16
 ex f being Function of (TS G), (the carrier of G)* st
    it = f.tsg &
     (for t being Symbol of G st t in Terminals G
         holds f.(root-tree t) = <*t*>) &
     (for nt being Symbol of G,
       ts being FinSequence of TS(G),
      rts being FinSequence st rts = roots ts & nt ==> rts
         for x being FinSequence of (the carrier of G)* st x = f * ts
             holds f.(nt-tree ts) = <*nt*>^FlattenSeq(x));
 func PostTraversal tsg -> FinSequence of the carrier of G means
:: DTCONSTR:def 17
 ex f being Function of (TS G), (the carrier of G)* st
    it = f.tsg &
     (for t being Symbol of G st t in Terminals G
         holds f.(root-tree t) = <*t*>) &
     (for nt being Symbol of G,
       ts being FinSequence of TS(G),
      rts being FinSequence st rts = roots ts & nt ==> rts
         for x being FinSequence of (the carrier of G)* st x = f * ts
             holds f.(nt-tree ts) = FlattenSeq(x)^<*nt*>);
end;

definition
 let G be with_nonterminals non empty (non empty DTConstrStr),
       nt be Symbol of G;
 func TerminalLanguage nt -> Subset of (Terminals G)* equals
:: DTCONSTR:def 18
     { TerminalString tsg
                     where tsg is Element of FinTrees the carrier of G :
            tsg in TS G & tsg.{} = nt };
 func PreTraversalLanguage nt -> Subset of (the carrier of G)* equals
:: DTCONSTR:def 19
  { PreTraversal tsg
                  where tsg is Element of FinTrees the carrier of G :
                  tsg in TS G & tsg.{} = nt };
 func PostTraversalLanguage nt -> Subset of (the carrier of G)* equals
:: DTCONSTR:def 20
  { PostTraversal tsg
                  where tsg is Element of FinTrees the carrier of G :
                  tsg in TS G & tsg.{} = nt };
end;

theorem :: DTCONSTR:14
for t being DecoratedTree of the carrier of PeanoNat
  st t in TS PeanoNat holds TerminalString t = <*0*>;

theorem :: DTCONSTR:15
for nt being Symbol of PeanoNat holds
          TerminalLanguage nt = {<*0*>};

theorem :: DTCONSTR:16
for t being Element of TS PeanoNat
  holds PreTraversal t = ((height dom t) |-> 1)^<*0*>;

theorem :: DTCONSTR:17
for nt being Symbol of PeanoNat holds
          (nt = 0 implies PreTraversalLanguage nt = {<*0*>}) &
          (nt = 1 implies PreTraversalLanguage nt = { (n|->1)^<*0*>
                                                  where n is Nat : n <> 0 });

theorem :: DTCONSTR:18
for t being Element of TS PeanoNat
  holds PostTraversal t = <*0*>^((height dom t) |-> 1);

theorem :: DTCONSTR:19
for nt being Symbol of PeanoNat holds
          (nt = 0 implies PostTraversalLanguage nt = {<*0*>}) &
          (nt = 1 implies PostTraversalLanguage nt = { <*0*>^(n|->1)
                                                  where n is Nat : n <> 0 });

:: What remains to be done, but in another article:
::
:: - partial trees (grown from the root towards the leaves)
:: - phrases