:: On Defining Functions on Trees :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received October 12, 1993 :: Copyright (c) 1993-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, CARD_1, XBOOLE_0, FINSEQ_1, TREES_3, SUBSET_1, RELAT_1, FUNCT_1, TARSKI, TREES_2, TREES_4, ZFMISC_1, MCART_1, LANG1, STRUCT_0, TDGROUP, CARD_3, ARYTM_3, NAT_1, XXREAL_0, FINSET_1, TREES_1, TREES_A, FUNCT_6, PRE_POLY, ORDINAL4, FINSEQ_2, DTCONSTR; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELSET_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSET_1, XTUPLE_0, MCART_1, CARD_3, DOMAIN_1, LANG1, TREES_1, TREES_2, FINSEQ_4, TREES_3, TREES_4, FINSEQOP, XXREAL_0, NAT_1, PRE_POLY; constructors PARTFUN1, BINOP_1, DOMAIN_1, SETWISEO, XXREAL_0, XREAL_0, NAT_1, CARD_3, FINSEQOP, FINSEQ_4, FINSOP_1, TREES_4, LANG1, RELSET_1, PRE_POLY, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, TREES_3, STRUCT_0, LANG1, FINSET_1, CARD_1, FINSEQ_2, TREES_4, VALUED_0, XTUPLE_0; 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; registration let D be non empty set, T be DTree-set of D; cluster -> DTree-yielding for 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 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 X, Y be set, f be FinSequence of [:X, Y:]; redefine func pr1 f -> FinSequence of X; redefine func pr2 f -> FinSequence of Y; end; theorem :: DTCONSTR:7 pr1 {} = {} & pr2 {} = {}; begin registration let A be non empty set, R be Relation of A,A*; cluster DTConstrStr(#A,R#) -> non empty; end; scheme :: DTCONSTR:sch 1 DTConstrStrEx { S() -> non empty set, P[object,object] }: 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 :: DTCONSTR:sch 2 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 :: DTCONSTR:sch 3 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 :: DTCONSTR:sch 4 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 :: DTCONSTR:sch 5 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 :: DTCONSTR:sch 6 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 1 (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 :: DTCONSTR:sch 7 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 :: DTCONSTR:sch 8 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 :: DTCONSTR:sch 9 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 2 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 3 Terminals G <> {}; attr G is with_nonterminals means :: DTCONSTR:def 4 NonTerminals G <> {}; attr G is with_useful_nonterminals means :: DTCONSTR:def 5 for nt being Symbol of G st nt in NonTerminals G ex p being FinSequence of TS(G) st nt ==> roots p; end; registration cluster with_terminals with_nonterminals with_useful_nonterminals strict for non empty DTConstrStr; end; definition let G be with_terminals non empty DTConstrStr; redefine func Terminals G -> non empty Subset of G; end; registration let G be with_terminals non empty DTConstrStr; cluster TS G -> non empty; end; registration 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 6 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 registration 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; func plus-one x -> Element of NAT equals :: DTCONSTR:def 7 (x.1) + 1; end; definition func PN-to-NAT -> Function of TS(PeanoNat), NAT means :: DTCONSTR:def 8 (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 9 1-tree <*x*>; end; definition func NAT-to-PN -> sequence of TS(PeanoNat) means :: DTCONSTR:def 10 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 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 11 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 12 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 13 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 14 { 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 15 { 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 16 { PostTraversal tsg where tsg is Element of FinTrees the carrier of G : tsg in TS G & tsg.{} = nt }; end; theorem :: DTCONSTR:13 for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds TerminalString t = <*0*>; theorem :: DTCONSTR:14 for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>}; theorem :: DTCONSTR:15 for t being Element of TS PeanoNat holds PreTraversal t = ((height dom t) |-> 1)^<*0*>; theorem :: DTCONSTR:16 for nt being Symbol of PeanoNat holds (nt = 0 implies PreTraversalLanguage nt = {<*0*>}) & (nt = 1 implies PreTraversalLanguage nt = { (n|->1)^<*0*> where n is Element of NAT : n <> 0 }); theorem :: DTCONSTR:17 for t being Element of TS PeanoNat holds PostTraversal t = <*0*>^((height dom t) |-> 1); theorem :: DTCONSTR:18 for nt being Symbol of PeanoNat holds (nt = 0 implies PostTraversalLanguage nt = {<*0*>}) & (nt = 1 implies PostTraversalLanguage nt = { <*0*>^(n|->1) where n is Element of NAT : n <> 0 }); :: What remains to be done, but in another article: :: :: - partial trees (grown from the root towards the leaves) :: - phrases