Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

Sets and Functions of Trees and Joining Operations of Trees

by
Grzegorz Bancerek

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

environ

vocabulary FINSEQ_1, FUNCT_1, RELAT_1, FINSET_1, MCART_1, TREES_1, TREES_2,
BOOLE, FUNCT_2, TARSKI, FINSEQ_2, FUNCOP_1, FUNCT_6, PARTFUN1, FUNCT_3,
ARYTM_1, SQUARE_1, TREES_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, DOMAIN_1, SQUARE_1,
FUNCOP_1, RELSET_1, FUNCT_2, FUNCT_3, FINSEQ_2, TREES_1, TREES_2,
FUNCT_6;
constructors FUNCT_5, NAT_1, DOMAIN_1, SQUARE_1, FUNCT_3, FINSEQ_2, TREES_2,
FUNCT_6, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FINSEQ_1, TREES_1, TREES_2, FINSET_1, RELSET_1, CARD_1,
XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin :: Finite sets

reserve x,y,z for set, i,k,n for Nat, p,q,r,s for FinSequence,
w for FinSequence of NAT, X,Y for set, f for Function;

begin :: Sets of trees

definition
func Trees -> set means
:: TREES_3:def 1
x in it iff x is Tree;
end;

definition
cluster Trees -> non empty;
end;

definition
func FinTrees -> Subset of Trees means
:: TREES_3:def 2

x in it iff x is finite Tree;
end;

definition
cluster FinTrees -> non empty;
end;

definition let IT be set;
attr IT is constituted-Trees means
:: TREES_3:def 3

for x st x in IT holds x is Tree;
attr IT is constituted-FinTrees means
:: TREES_3:def 4

for x st x in IT holds x is finite Tree;
attr IT is constituted-DTrees means
:: TREES_3:def 5

for x st x in IT holds x is DecoratedTree;
end;

theorem :: TREES_3:1
X is constituted-Trees iff X c= Trees;

theorem :: TREES_3:2
X is constituted-FinTrees iff X c= FinTrees;

theorem :: TREES_3:3
X is constituted-Trees & Y is constituted-Trees iff X \/
Y is constituted-Trees;

theorem :: TREES_3:4
X is constituted-Trees & Y is constituted-Trees implies
X \+\ Y is constituted-Trees;

theorem :: TREES_3:5
X is constituted-Trees implies X /\ Y is constituted-Trees &
Y /\ X is constituted-Trees & X \ Y is constituted-Trees;

theorem :: TREES_3:6
X is constituted-FinTrees & Y is constituted-FinTrees iff
X \/ Y is constituted-FinTrees;

theorem :: TREES_3:7
X is constituted-FinTrees & Y is constituted-FinTrees implies
X \+\ Y is constituted-FinTrees;

theorem :: TREES_3:8
X is constituted-FinTrees implies X /\ Y is constituted-FinTrees &
Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees;

theorem :: TREES_3:9
X is constituted-DTrees & Y is constituted-DTrees iff
X \/ Y is constituted-DTrees;

theorem :: TREES_3:10
X is constituted-DTrees & Y is constituted-DTrees implies
X \+\ Y is constituted-DTrees;

theorem :: TREES_3:11
X is constituted-DTrees implies X /\ Y is constituted-DTrees &
Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees;

theorem :: TREES_3:12
{} is constituted-Trees constituted-FinTrees constituted-DTrees;

theorem :: TREES_3:13
{x} is constituted-Trees iff x is Tree;

theorem :: TREES_3:14
{x} is constituted-FinTrees iff x is finite Tree;

theorem :: TREES_3:15
{x} is constituted-DTrees iff x is DecoratedTree;

theorem :: TREES_3:16
{x,y} is constituted-Trees iff x is Tree & y is Tree;

theorem :: TREES_3:17
{x,y} is constituted-FinTrees iff x is finite Tree & y is finite Tree;

theorem :: TREES_3:18
{x,y} is constituted-DTrees iff x is DecoratedTree & y is DecoratedTree;

theorem :: TREES_3:19
X is constituted-Trees & Y c= X implies Y is constituted-Trees;

theorem :: TREES_3:20
X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees;

theorem :: TREES_3:21
X is constituted-DTrees & Y c= X implies Y is constituted-DTrees;

definition
cluster finite constituted-Trees constituted-FinTrees non empty set;
cluster finite constituted-DTrees non empty set;
end;

definition
cluster constituted-FinTrees -> constituted-Trees set;
end;

definition let X be constituted-Trees set;
cluster -> constituted-Trees Subset of X;
end;

definition let X be constituted-FinTrees set;
cluster -> constituted-FinTrees Subset of X;
end;

definition let X be constituted-DTrees set;
cluster -> constituted-DTrees Subset of X;
end;

definition
let D be constituted-Trees non empty set;
redefine mode Element of D -> Tree;
end;

definition
let D be constituted-FinTrees non empty set;
redefine mode Element of D -> finite Tree;
end;

definition
let D be constituted-DTrees non empty set;
redefine mode Element of D -> DecoratedTree;
end;

definition
cluster Trees -> constituted-Trees;
end;

definition
cluster constituted-FinTrees non empty Subset of Trees;
end;

definition
cluster FinTrees -> constituted-FinTrees;
end;

definition let D be non empty set;
mode DTree-set of D -> set means
:: TREES_3:def 6

for x st x in it holds x is DecoratedTree of D;
end;

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

definition let D be non empty set;
cluster finite non empty DTree-set of D;
end;

definition let D be non empty set, E be non empty DTree-set of D;
redefine mode Element of E -> DecoratedTree of D;
end;

definition let T be Tree, D be non empty set;
redefine func Funcs(T,D) -> non empty DTree-set of D;
mode Relation of T,D -> ParametrizedSubset of D;
end;

definition let T be Tree, D be non empty set;
cluster -> DecoratedTree-like Function of T,D;
end;

definition
let D be non empty set;
func Trees(D) -> DTree-set of D means
:: TREES_3:def 7

for T being DecoratedTree of D holds T in it;
end;

definition
let D be non empty set;
cluster Trees(D) -> non empty;
end;

definition let D be non empty set;
func FinTrees(D) -> DTree-set of D means
:: TREES_3:def 8
for T being DecoratedTree of D holds dom T is finite iff T in it;
end;

definition let D be non empty set;
cluster FinTrees D -> non empty;
end;

theorem :: TREES_3:22
for D being non empty set holds FinTrees D c= Trees D;

begin :: Functions yielding trees

definition let IT be Function;
attr IT is Tree-yielding means
:: TREES_3:def 9

rng IT is constituted-Trees;
attr IT is FinTree-yielding means
:: TREES_3:def 10

rng IT is constituted-FinTrees;
attr IT is DTree-yielding means
:: TREES_3:def 11

rng IT is constituted-DTrees;
end;

theorem :: TREES_3:23
{} is Tree-yielding FinTree-yielding DTree-yielding;

theorem :: TREES_3:24
f is Tree-yielding iff for x st x in dom f holds f.x is Tree;

theorem :: TREES_3:25
f is FinTree-yielding iff for x st x in dom f holds f.x is finite Tree;

theorem :: TREES_3:26
f is DTree-yielding iff for x st x in dom f holds f.x is DecoratedTree;

theorem :: TREES_3:27
p is Tree-yielding & q is Tree-yielding iff p^q is Tree-yielding;

theorem :: TREES_3:28
p is FinTree-yielding & q is FinTree-yielding iff p^q is FinTree-yielding;

theorem :: TREES_3:29
p is DTree-yielding & q is DTree-yielding iff p^q is DTree-yielding;

theorem :: TREES_3:30
<*x*> is Tree-yielding iff x is Tree;

theorem :: TREES_3:31
<*x*> is FinTree-yielding iff x is finite Tree;

theorem :: TREES_3:32
<*x*> is DTree-yielding iff x is DecoratedTree;

theorem :: TREES_3:33
<*x,y*> is Tree-yielding iff x is Tree & y is Tree;

theorem :: TREES_3:34
<*x,y*> is FinTree-yielding iff x is finite Tree & y is finite Tree;

theorem :: TREES_3:35
<*x,y*> is DTree-yielding iff x is DecoratedTree & y is DecoratedTree;

theorem :: TREES_3:36
i <> 0 implies (i |-> x is Tree-yielding iff x is Tree);

theorem :: TREES_3:37
i <> 0 implies (i |-> x is FinTree-yielding iff x is finite Tree);

theorem :: TREES_3:38
i <> 0 implies (i |-> x is DTree-yielding iff x is DecoratedTree);

definition
cluster Tree-yielding FinTree-yielding non empty FinSequence;
cluster DTree-yielding non empty FinSequence;
end;

definition
cluster Tree-yielding FinTree-yielding non empty Function;
cluster DTree-yielding non empty Function;
end;

definition
cluster FinTree-yielding -> Tree-yielding Function;
end;

definition
let D be constituted-Trees non empty set;
cluster -> Tree-yielding FinSequence of D;
end;

definition let p,q be Tree-yielding FinSequence;
cluster p^q -> Tree-yielding;
end;

definition
let D be constituted-FinTrees non empty set;
cluster -> FinTree-yielding FinSequence of D;
end;

definition let p,q be FinTree-yielding FinSequence;
cluster p^q -> FinTree-yielding;
end;

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

definition let p,q be DTree-yielding FinSequence;
cluster p^q -> DTree-yielding;
end;

definition let T be Tree;
cluster <*T*> -> Tree-yielding non empty;
let S be Tree;
cluster <*T,S*> -> Tree-yielding non empty;
end;

definition let n be Nat, T be Tree;
cluster n |-> T -> Tree-yielding;
end;

definition let T be finite Tree;
cluster <*T*> -> FinTree-yielding;
let S be finite Tree;
cluster <*T,S*> -> FinTree-yielding;
end;

definition let n be Nat, T be finite Tree;
cluster n |-> T -> FinTree-yielding;
end;

definition let T be DecoratedTree;
cluster <*T*> -> DTree-yielding non empty;
let S be DecoratedTree;
cluster <*T,S*> -> DTree-yielding non empty;
end;

definition let n be Nat, T be DecoratedTree;
cluster n |-> T -> DTree-yielding;
end;

theorem :: TREES_3:39
for f being DTree-yielding Function holds dom doms f = dom f &
doms f is Tree-yielding;

definition let p be DTree-yielding FinSequence;
cluster doms p -> Tree-yielding FinSequence-like;
end;

theorem :: TREES_3:40
for p being DTree-yielding FinSequence holds len doms p = len p;

begin :: Trees decorated by Cartesian product and structure of substitution

definition let D,E be non empty set;
mode DecoratedTree of D,E is DecoratedTree of [:D,E:];
mode DTree-set of D,E is DTree-set of [:D,E:];
end;

definition let T1,T2 be DecoratedTree;
cluster <:T1,T2:> -> DecoratedTree-like;
end;

definition let D1,D2 be non empty set;
let T1 be DecoratedTree of D1;
let T2 be DecoratedTree of D2;
redefine func <:T1,T2:> -> DecoratedTree of D1,D2;
end;

definition let D,E be non empty set;
let T be DecoratedTree of D;
let f be Function of D,E;
redefine func f*T -> DecoratedTree of E;
end;

definition let D1,D2 be non empty set; redefine
func pr1(D1,D2) -> Function of [:D1,D2:], D1;
func pr2(D1,D2) -> Function of [:D1,D2:], D2;
end;

definition let D1,D2 be non empty set, T be DecoratedTree of D1,D2;
func T`1 -> DecoratedTree of D1 equals
:: TREES_3:def 12
pr1(D1,D2)*T;
func T`2 -> DecoratedTree of D2 equals
:: TREES_3:def 13
pr2(D1,D2)*T;
end;

theorem :: TREES_3:41
for D1,D2 being non empty set, T being DecoratedTree of D1,D2,
t being Element of dom T holds (T.t)`1 = T`1.t & T`2.t = (T.t)`2;

theorem :: TREES_3:42
for D1,D2 being non empty set, T being DecoratedTree of D1,D2 holds
<:T`1,T`2:> = T;

definition let T be finite Tree;
cluster Leaves T -> finite non empty;
end;

definition let T be Tree, S be non empty Subset of T;
redefine mode Element of S -> Element of T;
end;

definition let T be finite Tree;
redefine mode Leaf of T -> Element of Leaves T;
end;

definition
let T be finite Tree;
mode T-Substitution of T -> Tree means
:: TREES_3:def 14

for t being Element of it holds t in T or
ex l being Leaf of T st l is_a_proper_prefix_of t;
end;

definition let T be finite Tree, t be Leaf of T, S be Tree;
redefine func T with-replacement (t,S) -> T-Substitution of T;
end;

definition let T be finite Tree;
cluster finite T-Substitution of T;
end;

definition let n;
mode T-Substitution of n is T-Substitution of elementary_tree n;
end;

theorem :: TREES_3:43
for T being Tree holds T is T-Substitution of 0;

theorem :: TREES_3:44
for T1, T2 being Tree st T1-level 1 c= T2-level 1 &
for n st <*n*> in T1 holds T1|<*n*> = T2|<*n*> holds T1 c= T2;

begin :: Joining of trees

canceled;

theorem :: TREES_3:46
for T,T' being Tree, p being FinSequence of NAT st
p in Leaves T holds T c= T with-replacement (p,T');

theorem :: TREES_3:47
for T,T' being DecoratedTree, p being Element of dom T holds
(T with-replacement (p,T')).p = T'.{};

theorem :: TREES_3:48
for T,T' being DecoratedTree, p,q being Element of dom T st
not p is_a_prefix_of q holds (T with-replacement (p,T')).q = T.q;

theorem :: TREES_3:49
for T,T' being DecoratedTree, p being Element of dom T,
q being Element of dom T' holds (T with-replacement (p,T')).(p^q) = T'.q;

definition let T1,T2 be Tree;
cluster T1 \/ T2 -> non empty Tree-like;
end;

theorem :: TREES_3:50
for T1,T2 being Tree, p being Element of T1 \/ T2 holds
(p in T1 & p in T2 implies (T1 \/ T2)|p = (T1|p) \/ (T2|p)) &
(not p in T1 implies (T1 \/ T2)|p = T2|p) &
(not p in T2 implies (T1 \/ T2)|p = T1|p);

definition let p such that
p is Tree-yielding;
func tree p -> Tree means
:: TREES_3:def 15

x in it iff x = {} or ex n,q st n < len p & q in p.(n+1) & x = <*n*>^q;
end;

definition let T be Tree;
func ^T -> Tree equals
:: TREES_3:def 16

tree<*T*>;
end;

definition let T1,T2 be Tree;
func tree(T1,T2) -> Tree equals
:: TREES_3:def 17

tree(<*T1,T2*>);
end;

theorem :: TREES_3:51
p is Tree-yielding implies (<*n*>^q in tree(p) iff n < len p & q in p.(n+1))
;

theorem :: TREES_3:52
p is Tree-yielding implies
tree(p)-level 1 = {<*n*>: n < len p} &
for n st n < len p holds (tree(p))|<*n*> = p.(n+1);

theorem :: TREES_3:53
for p,q being Tree-yielding FinSequence st tree(p) = tree(q) holds p = q;

theorem :: TREES_3:54
for p1,p2 being Tree-yielding FinSequence, T being Tree holds
p in T iff <*len p1*>^p in tree(p1^<*T*>^p2);

theorem :: TREES_3:55
tree({}) = elementary_tree 0;

theorem :: TREES_3:56
p is Tree-yielding implies elementary_tree len p c= tree(p);

theorem :: TREES_3:57
elementary_tree i = tree(i|->elementary_tree 0);

theorem :: TREES_3:58
for T being Tree, p being Tree-yielding FinSequence holds
tree(p^<*T*>) = (tree(p) \/ elementary_tree (len p + 1))
with-replacement (<*len p*>, T);

theorem :: TREES_3:59
for p being Tree-yielding FinSequence holds
tree(p^<*elementary_tree 0*>) = tree(p) \/ elementary_tree (len p + 1);

theorem :: TREES_3:60
for p, q being Tree-yielding FinSequence for T1,T2 be Tree holds
tree(p^<*T1*>^q) = tree(p^<*T2*>^q) with-replacement(<*len p*>,T1);

theorem :: TREES_3:61
for T being Tree holds ^T = elementary_tree 1 with-replacement(<*0*>, T);

theorem :: TREES_3:62
for T1,T2 being Tree holds
tree(T1,T2) = (elementary_tree 2 with-replacement(<*0*>,T1))
with-replacement (<*1*>, T2);

definition let p be FinTree-yielding FinSequence;
cluster tree(p) -> finite;
end;

definition let T be finite Tree;
cluster ^T -> finite;
end;

definition let T1,T2 be finite Tree;
cluster tree(T1,T2) -> finite;
end;

theorem :: TREES_3:63
for T being Tree, x being set holds x in ^T iff x = {} or
ex p st p in T & x = <*0*>^p;

theorem :: TREES_3:64
for T being Tree, p being FinSequence holds p in T iff <*0*>^p in ^T;

theorem :: TREES_3:65
for T being Tree holds elementary_tree 1 c= ^T;

theorem :: TREES_3:66
for T1,T2 being Tree st T1 c= T2 holds ^T1 c= ^T2;

theorem :: TREES_3:67
for T1,T2 being Tree st ^T1 = ^T2 holds T1 = T2;

theorem :: TREES_3:68
for T being Tree holds (^T)|<*0*> = T;

theorem :: TREES_3:69
for T1,T2 being Tree holds ^T1 with-replacement (<*0*>,T2) = ^T2;

theorem :: TREES_3:70
^elementary_tree 0 = elementary_tree 1;

theorem :: TREES_3:71
for T1,T2 being Tree, x being set holds x in tree(T1,T2) iff x = {} or
ex p st p in T1 & x = <*0*>^p or p in T2 & x = <*1*>^p;

theorem :: TREES_3:72
for T1,T2 being Tree, p being FinSequence holds
p in T1 iff <*0*>^p in tree(T1,T2);

theorem :: TREES_3:73
for T1,T2 being Tree, p being FinSequence holds
p in T2 iff <*1*>^p in tree(T1,T2);

theorem :: TREES_3:74
for T1,T2 being Tree holds elementary_tree 2 c= tree(T1,T2);

theorem :: TREES_3:75
for T1,T2, W1,W2 being Tree st T1 c= W1 & T2 c= W2 holds
tree(T1,T2) c= tree(W1,W2);

theorem :: TREES_3:76
for T1,T2, W1,W2 being Tree st tree(T1,T2) = tree(W1,W2) holds
T1 = W1 & T2 = W2;

theorem :: TREES_3:77
for T1,T2 being Tree holds tree(T1,T2)|<*0*> = T1 & tree(T1,T2)|<*1*> = T2;

theorem :: TREES_3:78
for T,T1,T2 being Tree holds
tree(T1,T2) with-replacement (<*0*>, T) = tree(T,T2) &
tree(T1,T2) with-replacement (<*1*>, T) = tree(T1,T);

theorem :: TREES_3:79
tree(elementary_tree 0, elementary_tree 0) = elementary_tree 2;

reserve w for FinTree-yielding FinSequence;

theorem :: TREES_3:80
for w st for t being finite Tree st t in rng w holds height t <= n holds
height tree(w) <= n+1;

theorem :: TREES_3:81
for t being finite Tree st t in rng w holds height tree(w) > height t;

theorem :: TREES_3:82
for t being finite Tree st t in rng w &
for t' being finite Tree st t' in rng w holds height t' <= height t holds
height tree(w) = (height t) + 1;

theorem :: TREES_3:83
for T being finite Tree holds height ^T = (height T) + 1;

theorem :: TREES_3:84
for T1,T2 being finite Tree holds
height tree(T1,T2) = max(height T1, height T2)+1;