:: Joining of Decorated Trees
:: by Grzegorz Bancerek
::
:: Received October 8, 1993
:: Copyright (c) 1993-2016 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, TREES_2, SUBSET_1, RELAT_1, FINSEQ_1, FUNCT_1, TARSKI,
TREES_1, XXREAL_0, ARYTM_3, CARD_1, FUNCOP_1, XBOOLE_0, TREES_3,
ZFMISC_1, NAT_1, FINSEQ_2, TREES_A, ORDINAL4, FUNCT_6, FINSEQ_4, MCART_1,
PARTFUN1, TREES_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, DOMAIN_1, FUNCOP_1, FUNCT_3, FINSEQ_1, FINSEQ_2,
TREES_1, TREES_2, FUNCT_6, TREES_3, XXREAL_0;
constructors BINOP_1, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FUNCT_5, FINSEQ_2,
FUNCT_6, TREES_3, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0,
FINSEQ_1, TREES_2, TREES_3, CARD_1, FINSEQ_2, FUNCOP_1, TREES_1,
XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Joining of decorated trees
definition
let T be DecoratedTree;
mode Node of T is Element of dom T;
end;
reserve x, y, z for object,
i, j, n for Nat,
p, q, r for FinSequence,
v for FinSequence of NAT;
definition
let T1, T2 be DecoratedTree;
redefine pred T1 = T2 means
:: TREES_4:def 1
dom T1 = dom T2 & for p being Node of T1 holds T1.p = T2.p;
end;
theorem :: TREES_4:1
for i,j being Nat
st elementary_tree i c= elementary_tree j holds i <= j;
theorem :: TREES_4:2
for i,j being Nat
st elementary_tree i = elementary_tree j holds i = j;
definition
let x be object;
func root-tree x -> DecoratedTree equals
:: TREES_4:def 2
(elementary_tree 0) --> x;
end;
definition
let D be non empty set, d be Element of D;
redefine func root-tree d -> Element of FinTrees D;
end;
theorem :: TREES_4:3
dom root-tree x = elementary_tree 0 & (root-tree x).{} = x;
theorem :: TREES_4:4
root-tree x = root-tree y implies x = y;
theorem :: TREES_4:5
for T being DecoratedTree st dom T = elementary_tree 0 holds
T = root-tree (T.{});
theorem :: TREES_4:6
root-tree x = {[{},x]};
definition
let x;
let p be FinSequence;
func x-flat_tree(p) -> DecoratedTree means
:: TREES_4:def 3
dom it = elementary_tree len p & it.{} = x &
for n st n < len p holds it.<*n*> = p.(n+1);
end;
theorem :: TREES_4:7
x-flat_tree p = y-flat_tree q implies x = y & p = q;
theorem :: TREES_4:8
for j being Element of NAT st j < i
holds (elementary_tree i)|<*j*> = elementary_tree 0;
theorem :: TREES_4:9
for i being Element of NAT st i < len p
holds (x-flat_tree p)|<*i*> = root-tree (p.(i+1));
definition
let x be object, p such that
p is DTree-yielding;
func x-tree(p) -> DecoratedTree means
:: TREES_4:def 4
( ex q being DTree-yielding FinSequence st p = q & dom it = tree(doms q)) &
it.{} = x &
for n being Nat st n < len p holds it|<*n*> = p.(n+1);
end;
definition
let x be object;
let T be DecoratedTree;
func x-tree T -> DecoratedTree equals
:: TREES_4:def 5
x-tree <*T*>;
end;
definition
let x be object;
let T1, T2 be DecoratedTree;
func x-tree (T1,T2) -> DecoratedTree equals
:: TREES_4:def 6
x-tree <*T1,T2*>;
end;
theorem :: TREES_4:10
for p being DTree-yielding FinSequence holds dom (x-tree(p)) = tree(doms p);
theorem :: TREES_4:11
for p being DTree-yielding FinSequence holds
y in dom (x-tree(p)) iff y = {} or
ex i being Nat, T being DecoratedTree, q being Node of T st
i < len p & T = p.(i+1) & y = <*i*>^q;
theorem :: TREES_4:12
for p being DTree-yielding FinSequence for i being Nat,
T being DecoratedTree, q being Node of T st i < len p &
T = p.(i+1) holds (x-tree p).(<*i*>^q) = T.q;
theorem :: TREES_4:13
for T being DecoratedTree holds dom (x-tree T) = ^dom T;
theorem :: TREES_4:14
for T1, T2 being DecoratedTree holds
dom (x-tree (T1,T2)) = tree(dom T1, dom T2);
theorem :: TREES_4:15
for p,q being DTree-yielding FinSequence st x-tree p = y-tree q holds
x = y & p = q;
theorem :: TREES_4:16
root-tree x = y-flat_tree p implies x = y & p = {};
theorem :: TREES_4:17
root-tree x = y-tree p & p is DTree-yielding implies x = y & p = {};
theorem :: TREES_4:18
x-flat_tree p = y-tree q & q is DTree-yielding implies x = y &
len p = len q & for i st i in dom p holds q.i = root-tree (p.i);
theorem :: TREES_4:19
for p being DTree-yielding FinSequence, n being Nat,
q being FinSequence st <*n*>^q in dom (x-tree(p)) holds
(x-tree(p)).(<*n*>^q) = p..(n+1,q);
theorem :: TREES_4:20
x-flat_tree({}) = root-tree x & x-tree({}) = root-tree x;
theorem :: TREES_4:21
x-flat_tree(<*y*>) =
((elementary_tree 1) --> x) with-replacement (<*0*>, root-tree y);
theorem :: TREES_4:22
for T being DecoratedTree holds
x-tree(<*T*>) = ((elementary_tree 1) --> x) with-replacement (<*0*>, T);
registration
let D be non empty set, d be Element of D, p be FinSequence of D;
cluster d-flat_tree(p) -> D-valued;
end;
registration
let D be non empty set, F be non empty DTree-set of D;
let d be Element of D, p be FinSequence of F;
cluster d-tree(p) -> D-valued;
end;
registration
let D be non empty set, d be Element of D, T be DecoratedTree of D;
cluster d-tree T -> D-valued;
end;
registration
let D be non empty set, d be Element of D, T1, T2 be DecoratedTree of D;
cluster d-tree(T1, T2) -> D-valued;
end;
definition
let D be non empty set;
let p be FinSequence of FinTrees D;
redefine func doms p -> FinSequence of FinTrees;
end;
definition
let D be non empty set;
let d be Element of D, p be FinSequence of FinTrees D;
redefine func d-tree p -> Element of FinTrees D;
end;
definition
let D be non empty set, x be Subset of D;
redefine mode FinSequence of x -> FinSequence of D;
end;
registration
let D be non empty constituted-DTrees set;
let X be Subset of D;
cluster -> DTree-yielding for FinSequence of X;
end;
begin :: Expanding of decoreted tree by substitution
scheme :: TREES_4:sch 1
ExpandTree{T1() -> Tree, T2() -> Tree, P[set]}: ex T being Tree st
for p holds p in T iff p in T1() or
ex q being Element of T1(), r being Element of T2() st P[q] & p = q^r;
definition
let T,T9 be DecoratedTree;
let x be set;
func (T,x) <- T9 -> DecoratedTree means
:: TREES_4:def 7
(for p holds p in dom it iff p in dom T or
ex q being Node of T, r being Node of T9 st
q in Leaves dom T & T.q = x & p = q^r) & (for p being Node of T st
not p in Leaves dom T or T.p <> x holds it.p = T.p) &
for p being Node of T, q being Node of T9 st
p in Leaves dom T & T.p = x holds it.(p^q) = T9.q;
end;
registration
let D be non empty set;
let T,T9 be DecoratedTree of D;
let x be set;
cluster (T,x) <- T9 -> D-valued;
end;
reserve T,T9 for DecoratedTree,
x,y for set;
theorem :: TREES_4:23
not x in rng T or not x in Leaves T implies (T,x) <- T9 = T;
begin :: Double decoreted trees
reserve D1, D2 for non empty set,
T for DecoratedTree of D1,D2,
d1 for Element of D1,
d2 for Element of D2,
F for non empty DTree-set of D1,D2,
F1 for non empty (DTree-set of D1),
F2 for non empty DTree-set of D2;
theorem :: TREES_4:24
for D1, D2, T holds dom T`1 = dom T & dom T`2 = dom T;
theorem :: TREES_4:25
(root-tree [d1,d2])`1 = root-tree d1 & (root-tree [d1,d2])`2 = root-tree d2;
theorem :: TREES_4:26
<:root-tree x, root-tree y:> = root-tree [x,y];
theorem :: TREES_4:27
for D1,D2, d1,d2, F,F1
for p being FinSequence of F, p1 being FinSequence of F1 st dom p1 = dom p &
for i st i in dom p for T st T = p.i holds p1.i = T`1
holds ([d1,d2]-tree p)`1 = d1-tree p1;
theorem :: TREES_4:28
for D1,D2, d1,d2, F,F2
for p being FinSequence of F, p2 being FinSequence of F2 st dom p2 = dom p &
for i st i in dom p for T st T = p.i holds p2.i = T`2
holds ([d1,d2]-tree p)`2 = d2-tree p2;
theorem :: TREES_4:29
for D1,D2, d1,d2, F for p being FinSequence of F
ex p1 being FinSequence of Trees D1 st dom p1 = dom p &
(for i st i in dom p ex T being Element of F st T = p.i & p1.i = T`1) &
([d1,d2]-tree p)`1 = d1-tree p1;
theorem :: TREES_4:30
for D1,D2, d1,d2, F for p being FinSequence of F
ex p2 being FinSequence of Trees D2 st dom p2 = dom p &
(for i st i in dom p ex T being Element of F st T = p.i & p2.i = T`2) &
([d1,d2]-tree p)`2 = d2-tree p2;
theorem :: TREES_4:31
for D1,D2, d1,d2 for p being FinSequence of FinTrees [:D1,D2:]
ex p1 being FinSequence of FinTrees D1 st dom p1 = dom p &
(for i st i in dom p ex T being Element of FinTrees [:D1,D2:] st
T = p.i & p1.i = T`1) & ([d1,d2]-tree p)`1 = d1-tree p1;
theorem :: TREES_4:32
for D1,D2, d1,d2 for p being FinSequence of FinTrees [:D1,D2:]
ex p2 being FinSequence of FinTrees D2 st dom p2 = dom p &
(for i st i in dom p ex T being Element of FinTrees [:D1,D2:] st
T = p.i & p2.i = T`2) & ([d1,d2]-tree p)`2 = d2-tree p2;