:: On Defining Functions on Binary Trees :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received December 30, 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, XBOOLE_0, TREES_2, SUBSET_1, FUNCT_1, TREES_4, TREES_3, FINSEQ_1, TREES_1, ORDINAL1, ORDINAL4, CARD_1, XXREAL_0, ARYTM_3, FINSET_1, RELAT_1, TARSKI, TREES_A, LANG1, TDGROUP, DTCONSTR, STRUCT_0, ZFMISC_1, FUNCT_2, BINTREE1, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, RELAT_1, STRUCT_0, MCART_1, DOMAIN_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, FINSET_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR, PRE_POLY, XXREAL_0; constructors DOMAIN_1, FINSEQOP, DTCONSTR, RELSET_1, PRE_POLY, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, MEMBERED, FINSEQ_1, TREES_2, TREES_3, STRUCT_0, DTCONSTR, FINSET_1, TREES_4, TREES_1, RELSET_1, XXREAL_0; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin definition let D be non empty set, t be DecoratedTree of D; func root-label t -> Element of D equals :: BINTREE1:def 1 t.{}; end; theorem :: BINTREE1:1 for D being non empty set, t being DecoratedTree of D holds roots <*t *> = <*root-label t*>; theorem :: BINTREE1:2 for D being non empty set, t1, t2 being DecoratedTree of D holds roots <*t1, t2*> = <*root-label t1, root-label t2*>; definition let IT be Tree; attr IT is binary means :: BINTREE1:def 2 for t being Element of IT st not t in Leaves IT holds succ t = { t^<*0*>, t^<*1*> }; end; theorem :: BINTREE1:3 :: LeavesDef3: for T being Tree, t being Element of T holds succ t = {} iff t in Leaves T; registration cluster elementary_tree 0 -> binary; cluster elementary_tree 2 -> binary; end; theorem :: BINTREE1:4 elementary_tree 0 is binary; theorem :: BINTREE1:5 elementary_tree 2 is binary; registration cluster binary finite for Tree; end; definition let IT be DecoratedTree; attr IT is binary means :: BINTREE1:def 3 dom IT is binary; end; registration let D be non empty set; cluster binary finite for DecoratedTree of D; end; registration cluster binary finite for DecoratedTree; end; registration cluster binary -> finite-order for Tree; end; theorem :: BINTREE1:6 for T0,T1 being Tree, t being Element of tree(T0,T1) holds (for p being Element of T0 st t = <*0*>^p holds t in Leaves tree(T0,T1) iff p in Leaves T0) & for p being Element of T1 st t = <*1*>^p holds t in Leaves tree(T0 ,T1) iff p in Leaves T1; theorem :: BINTREE1:7 for T0,T1 being Tree, t being Element of tree(T0,T1) holds (t = {} implies succ t = { t^<*0*>, t^<*1*> }) & (for p being Element of T0 st t = <*0*>^p for sp being FinSequence holds sp in succ p iff <*0*>^sp in succ t) & for p being Element of T1 st t = <*1*>^p for sp being FinSequence holds sp in succ p iff <*1*>^sp in succ t; theorem :: BINTREE1:8 for T1,T2 being Tree holds T1 is binary & T2 is binary iff tree( T1,T2) is binary; theorem :: BINTREE1:9 for T1,T2 being DecoratedTree, x being set holds T1 is binary & T2 is binary iff x-tree (T1,T2) is binary; registration let D be non empty set, x be Element of D, T1, T2 be binary finite DecoratedTree of D; cluster x-tree (T1,T2) -> binary finite D-valued; end; definition let IT be non empty DTConstrStr; attr IT is binary means :: BINTREE1:def 4 for s being Symbol of IT, p being FinSequence st s ==> p ex x1, x2 being Symbol of IT st p = <* x1, x2 *>; end; registration cluster binary with_terminals with_nonterminals with_useful_nonterminals strict for non empty DTConstrStr; end; scheme :: BINTREE1:sch 1 BinDTConstrStrEx { S() -> non empty set, P[set, set, set] }: ex G be binary strict non empty DTConstrStr st the carrier of G = S() & for x, y, z being Symbol of G holds x ==> <*y,z*> iff P[x, y, z]; theorem :: BINTREE1:10 for G being binary with_terminals with_nonterminals non empty DTConstrStr, ts being FinSequence of TS G, nt being Symbol of G st nt ==> roots ts holds nt is NonTerminal of G & dom ts = {1, 2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st roots ts = <*root-label tl, root-label tr*> & tl = ts.1 & tr = ts.2 & nt-tree ts = nt-tree (tl, tr) & tl in rng ts & tr in rng ts; scheme :: BINTREE1:sch 2 BinDTConstrInd { G() -> binary with_terminals with_nonterminals non empty DTConstrStr, P[set] }: for t being Element of TS(G()) holds P[t] provided for s being Terminal of G() holds P[root-tree s] and for nt being NonTerminal of G(), tl, tr being Element of TS(G()) st nt ==> <*root-label tl, root-label tr*> & P[tl] & P[tr] holds P[nt-tree(tl, tr) ]; scheme :: BINTREE1:sch 3 BinDTConstrIndDef { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr, D()->non empty set, TermVal( set) -> Element of D(), NTermVal(set, set, set, set, set) -> Element of D() }: ex f being Function of TS(G()), D() st (for t being Terminal of G() holds f.( root-tree t) = TermVal(t)) & for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of D() st xl = f .tl & xr = f.tr holds f.(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr); scheme :: BINTREE1:sch 4 BinDTConstrUniqDef { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr, D()->non empty set, f1, f2() -> Function of TS(G()), D(), TermVal(set) -> Element of D(), NTermVal(set, set, set, set, set) -> Element of D() }: f1() = f2() provided (for t being Terminal of G() holds f1().(root-tree t) = TermVal(t)) & for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of D() st xl = f1().tl & xr = f1().tr holds f1().(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr) and (for t being Terminal of G() holds f2().(root-tree t) = TermVal(t)) & for nt being NonTerminal of G(), tl, tr being Element of TS(G()), rtl, rtr being Symbol of G() st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of D() st xl = f2().tl & xr = f2().tr holds f2().(nt-tree (tl, tr)) = NTermVal(nt, rtl, rtr, xl, xr); scheme :: BINTREE1:sch 5 BinDTCDefLambda { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr, A, B() -> non empty set, F( set, set) -> Element of B(), H(set, set, set, set) -> Element of B() }: ex f being Function of TS G(), Funcs(A(), B()) st (for t being Terminal of G() ex g being Function of A(), B() st g = f.(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & for nt being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex g, f1, f2 being Function of A(), B() st g = f.(nt -tree (t1, t2)) & f1 = f.t1 & f2 = f.t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a); scheme :: BINTREE1:sch 6 BinDTCDefLambdaUniq { G() -> binary with_terminals with_nonterminals with_useful_nonterminals non empty DTConstrStr, A, B() -> non empty set, f1, f2() -> Function of TS G(), Funcs (A(), B()), F(set, set) -> Element of B(), H( set, set, set, set) -> Element of B() }: f1() = f2() provided (for t being Terminal of G() ex g being Function of A(), B() st g = f1().(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & for nt being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex g, f1, f2 being Function of A(), B() st g = f1().(nt-tree (t1, t2)) & f1 = f1() .t1 & f2 = f1().t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a) and (for t being Terminal of G() ex g being Function of A(), B() st g = f2().(root-tree t) & for a being Element of A() holds g.a = F(t, a)) & for nt being NonTerminal of G(), t1, t2 being Element of TS G(), rtl, rtr being Symbol of G() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *> ex g, f1, f2 being Function of A(), B() st g = f2().(nt-tree (t1, t2)) & f1 = f2() .t1 & f2 = f2().t2 & for a being Element of A() holds g.a = H(nt, f1, f2, a); registration let G be binary with_terminals with_nonterminals non empty DTConstrStr; cluster -> binary for Element of TS G; end;