:: On Defining Functions on Binary Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received December 30, 1993
:: Copyright (c) 1993-2018 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;