Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

Joining of Decorated Trees

by
Grzegorz Bancerek

MML identifier: TREES_4
[ Mizar article, MML identifier index ]

environ

vocabulary TREES_2, RELAT_1, FINSEQ_1, FUNCT_1, TREES_1, BOOLE, FUNCOP_1,
TREES_3, FINSEQ_2, FUNCT_6, FINSEQ_4, FINSET_1, MCART_1, FUNCT_3,
PARTFUN1, TREES_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
RELAT_1, FUNCT_1, FINSET_1, DOMAIN_1, FUNCOP_1, FUNCT_3, FINSEQ_1,
FINSEQ_2, TREES_1, TREES_2, FUNCT_6, TREES_3;
constructors FINSEQ_2, NAT_1, DOMAIN_1, FUNCT_6, TREES_3, XREAL_0, MEMBERED,
XBOOLE_0;
clusters SUBSET_1, TREES_2, TREES_3, FINSEQ_1, RELSET_1, ARYTM_3, MEMBERED,
ZFMISC_1, XBOOLE_0, ORDINAL2;
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 set, 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;
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
j < i implies (elementary_tree i)|<*j*> = elementary_tree 0;

theorem :: TREES_4:9
i < len p implies (x-flat_tree p)|<*i*> = root-tree (p.(i+1));

definition let x, 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 st n < len p holds it|<*n*> = p.(n+1);
end;

definition let x; let T be DecoratedTree;
func x-tree T -> DecoratedTree equals
:: TREES_4:def 5

x-tree <*T*>;
end;

definition let x; 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);

definition
let D be non empty set, d be Element of D, p be FinSequence of D;
redefine func d-flat_tree(p) -> DecoratedTree of D;
end;

definition
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;
redefine func d-tree(p) -> DecoratedTree of D;
end;

definition
let D be non empty set, d be Element of D, T be DecoratedTree of D;
redefine func d-tree T -> DecoratedTree of D;
end;

definition
let D be non empty set, d be Element of D, T1, T2 be DecoratedTree of D;
redefine func d-tree(T1, T2) -> DecoratedTree of D;
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;

definition let D be non empty constituted-DTrees set;
let X be Subset of D;
cluster -> DTree-yielding FinSequence of X;
end;

begin :: Expanding of decoreted tree by substitution

scheme 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,T' be DecoratedTree;
let x be set;
func (T,x) <- T' -> 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 T' 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 T' st
p in Leaves dom T & T.p = x holds it.(p^q) = T'.q);
end;

definition let D be non empty set;
let T,T' be DecoratedTree of D;
let x be set;
redefine func (T,x) <- T' -> DecoratedTree of D;
end;

reserve T,T' for DecoratedTree, x,y for set;

theorem :: TREES_4:23
not x in rng T or not x in Leaves T implies (T,x) <- T' = 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;