Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

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

Back to top