:: Sets and Functions of Trees and Joining Operations of Trees
:: by Grzegorz Bancerek
::
:: Received November 27, 1992
:: Copyright (c) 1992-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, SUBSET_1, FINSEQ_1, FUNCT_1, XXREAL_0, ORDINAL4,
RELAT_1, TREES_1, XBOOLE_0, FINSET_1, TARSKI, TREES_2, FUNCT_2, CARD_1,
FINSEQ_2, FUNCOP_1, FUNCT_6, ZFMISC_1, PARTFUN1, MCART_1, NAT_1, ARYTM_3,
TREES_A, ARYTM_1, TREES_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, DOMAIN_1, FUNCOP_1,
RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, FUNCT_3, FINSEQ_2, TREES_1,
TREES_2, FUNCT_6, XXREAL_0;
constructors PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_3, SQUARE_1, NAT_1, FINSEQ_2,
FUNCT_6, TREES_2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, CARD_1,
RELSET_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Finite sets
reserve x,y,z for object, X,Y for set,
i,k,n for Nat,
p,q,r,s for FinSequence,
w for FinSequence of NAT,
f for Function;
begin :: Sets of trees
definition
func Trees -> set means
:: TREES_3:def 1
x in it iff x is Tree;
end;
registration
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;
registration
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;
registration
cluster empty ->
constituted-Trees constituted-FinTrees constituted-DTrees for set;
end;
theorem :: TREES_3:12
{x} is constituted-Trees iff x is Tree;
theorem :: TREES_3:13
for x being object holds
{x} is constituted-FinTrees iff x is finite Tree;
theorem :: TREES_3:14
{x} is constituted-DTrees iff x is DecoratedTree;
theorem :: TREES_3:15
{x,y} is constituted-Trees iff x is Tree & y is Tree;
theorem :: TREES_3:16
{x,y} is constituted-FinTrees iff x is finite Tree & y is finite Tree;
theorem :: TREES_3:17
{x,y} is constituted-DTrees iff x is DecoratedTree & y is DecoratedTree;
theorem :: TREES_3:18
X is constituted-Trees & Y c= X implies Y is constituted-Trees;
theorem :: TREES_3:19
X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees;
theorem :: TREES_3:20
X is constituted-DTrees & Y c= X implies Y is constituted-DTrees;
registration
cluster finite constituted-Trees constituted-FinTrees non empty for set;
cluster finite constituted-DTrees non empty for set;
end;
registration
cluster constituted-FinTrees -> constituted-Trees for set;
end;
registration
let X be constituted-Trees set;
cluster -> constituted-Trees for Subset of X;
end;
registration
let X be constituted-FinTrees set;
cluster -> constituted-FinTrees for Subset of X;
end;
registration
let X be constituted-DTrees set;
cluster -> constituted-DTrees for Subset of X;
end;
registration
let D be constituted-Trees non empty set;
cluster -> non empty Tree-like for Element of D;
end;
registration
let D be constituted-FinTrees non empty set;
cluster -> finite for Element of D;
end;
registration
cluster constituted-DTrees -> functional for set;
end;
registration
let D be constituted-DTrees non empty set;
cluster -> DecoratedTree-like for Element of D;
end;
registration
cluster Trees -> constituted-Trees;
end;
registration
cluster FinTrees -> constituted-FinTrees;
end;
registration
cluster constituted-FinTrees non empty for Subset of Trees;
end;
definition
let D be non empty set;
mode DTree-set of D -> non empty set means
:: TREES_3:def 6
for x st x in it holds x is DecoratedTree of D;
end;
registration
let D be non empty set;
cluster -> constituted-DTrees for DTree-set of D;
end;
registration
let D be non empty set;
cluster finite non empty for DTree-set of D;
end;
registration
let D be non empty set, E be non empty DTree-set of D;
cluster -> D-valued for Element of E;
end;
definition
let T be Tree, D be non empty set;
redefine func Funcs(T,D) -> non empty DTree-set of D;
end;
registration
let T be Tree, D be non empty set;
cluster -> DecoratedTree-like for 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;
registration
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;
theorem :: TREES_3:21
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;
registration
cluster empty -> Tree-yielding FinTree-yielding DTree-yielding for Function;
end;
theorem :: TREES_3:22
f is Tree-yielding iff for x st x in dom f holds f.x is Tree;
theorem :: TREES_3:23
f is FinTree-yielding iff for x st x in dom f holds f.x is finite Tree;
theorem :: TREES_3:24
f is DTree-yielding iff for x st x in dom f holds f.x is DecoratedTree;
theorem :: TREES_3:25
p is Tree-yielding & q is Tree-yielding iff p^q is Tree-yielding;
theorem :: TREES_3:26
p is FinTree-yielding & q is FinTree-yielding iff p^q is FinTree-yielding;
theorem :: TREES_3:27
p is DTree-yielding & q is DTree-yielding iff p^q is DTree-yielding;
theorem :: TREES_3:28
<*x*> is Tree-yielding iff x is Tree;
theorem :: TREES_3:29
for x being object holds
<*x*> is FinTree-yielding iff x is finite Tree;
theorem :: TREES_3:30
<*x*> is DTree-yielding iff x is DecoratedTree;
theorem :: TREES_3:31
<*x,y*> is Tree-yielding iff x is Tree & y is Tree;
theorem :: TREES_3:32
<*x,y*> is FinTree-yielding iff x is finite Tree & y is finite Tree;
theorem :: TREES_3:33
<*x,y*> is DTree-yielding iff x is DecoratedTree & y is DecoratedTree;
theorem :: TREES_3:34
i <> 0 implies (i |-> x is Tree-yielding iff x is Tree);
theorem :: TREES_3:35
i <> 0 implies (i |-> x is FinTree-yielding iff x is finite Tree);
theorem :: TREES_3:36
i <> 0 implies (i |-> x is DTree-yielding iff x is DecoratedTree);
registration
cluster Tree-yielding FinTree-yielding non empty for FinSequence;
cluster DTree-yielding non empty for FinSequence;
end;
registration
cluster Tree-yielding FinTree-yielding non empty for Function;
cluster DTree-yielding non empty for Function;
end;
registration
cluster FinTree-yielding -> Tree-yielding for Function;
end;
registration
let D be constituted-Trees non empty set;
cluster -> Tree-yielding for FinSequence of D;
end;
registration
let p,q be Tree-yielding FinSequence;
cluster p^q -> Tree-yielding;
end;
registration
let D be constituted-FinTrees non empty set;
cluster -> FinTree-yielding for FinSequence of D;
end;
registration
let p,q be FinTree-yielding FinSequence;
cluster p^q -> FinTree-yielding;
end;
registration
let D be constituted-DTrees non empty set;
cluster -> DTree-yielding for FinSequence of D;
end;
registration
let p,q be DTree-yielding FinSequence;
cluster p^q -> DTree-yielding;
end;
registration
let T be Tree;
cluster <*T*> -> Tree-yielding non empty;
let S be Tree;
cluster <*T,S*> -> Tree-yielding non empty;
end;
registration
let n be Nat, T be Tree;
cluster n |-> T -> Tree-yielding;
end;
registration
let T be finite Tree;
cluster <*T*> -> FinTree-yielding;
let S be finite Tree;
cluster <*T,S*> -> FinTree-yielding;
end;
registration
let n be Nat, T be finite Tree;
cluster n |-> T -> FinTree-yielding;
end;
registration
let T be DecoratedTree;
cluster <*T*> -> DTree-yielding non empty;
let S be DecoratedTree;
cluster <*T,S*> -> DTree-yielding non empty;
end;
registration
let n be Nat, T be DecoratedTree;
cluster n |-> T -> DTree-yielding;
end;
registration
cluster DTree-yielding -> Function-yielding for Function;
end;
theorem :: TREES_3:37
for f being DTree-yielding Function holds dom doms f = dom f &
doms f is Tree-yielding;
registration
let p be DTree-yielding FinSequence;
cluster doms p -> Tree-yielding FinSequence-like;
end;
theorem :: TREES_3:38
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;
registration
let T1,T2 be DecoratedTree;
cluster <:T1,T2:> -> DecoratedTree-like;
end;
registration
let D1,D2 be non empty set;
let T1 be DecoratedTree of D1;
let T2 be DecoratedTree of D2;
cluster <:T1,T2:> -> [:D1,D2:]-valued;
end;
registration
let D,E be non empty set;
let T be DecoratedTree of D;
let f be Function of D,E;
cluster f*T -> DecoratedTree-like;
end;
definition
let D1,D2 be non empty set;
redefine func pr1(D1,D2) -> Function of [:D1,D2:], D1;
redefine 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:39
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:40
for D1,D2 being non empty set, T being DecoratedTree of D1,D2 holds
<:T`1,T`2:> = T;
registration
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;
registration
let T be finite Tree;
cluster finite for T-Substitution of T;
end;
definition
let n;
mode T-Substitution of n is T-Substitution of elementary_tree n;
end;
theorem :: TREES_3:41
for T being Tree holds T is T-Substitution of 0;
theorem :: TREES_3:42
for T1, T2 being Tree st T1-level 1 c= T2-level 1 &
for n being Element of NAT st <*n*> in T1 holds T1|<*n*> = T2|<*n*>
holds T1 c= T2;
begin :: Joining of trees
theorem :: TREES_3:43
for T,T9 being Tree, p being FinSequence of NAT st
p in Leaves T holds T c= T with-replacement (p,T9);
theorem :: TREES_3:44
for T,T9 being DecoratedTree, p being Element of dom T holds
(T with-replacement (p,T9)).p = T9.{};
theorem :: TREES_3:45
for T,T9 being DecoratedTree, p,q being Element of dom T st
not p is_a_prefix_of q holds (T with-replacement (p,T9)).q = T.q;
theorem :: TREES_3:46
for T,T9 being DecoratedTree, p being Element of dom T,
q being Element of dom T9 holds (T with-replacement (p,T9)).(p^q) = T9.q;
registration
let T1,T2 be Tree;
cluster T1 \/ T2 -> non empty Tree-like;
end;
theorem :: TREES_3:47
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:48
p is Tree-yielding implies (<*n*>^q in tree(p) iff n < len p & q in p.(n+ 1
) );
theorem :: TREES_3:49
p is Tree-yielding implies tree(p)-level 1 = {<*n*>: n < len p} &
for n being Element of NAT st n < len p holds (tree(p))|<*n*> = p.(n+1);
theorem :: TREES_3:50
for p,q being Tree-yielding FinSequence st tree(p) = tree(q) holds p = q;
theorem :: TREES_3:51
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:52
tree({}) = elementary_tree 0;
theorem :: TREES_3:53
p is Tree-yielding implies elementary_tree len p c= tree(p);
theorem :: TREES_3:54
elementary_tree i = tree(i|->elementary_tree 0);
theorem :: TREES_3:55
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:56
for p being Tree-yielding FinSequence holds
tree(p^<*elementary_tree 0*>) = tree(p) \/ elementary_tree (len p + 1);
theorem :: TREES_3:57
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);
definition
let n be Nat;
redefine func <*n*> -> FinSequence of NAT;
end;
theorem :: TREES_3:58
for T being Tree holds ^T = elementary_tree 1 with-replacement(<*0*>, T);
theorem :: TREES_3:59
for T1,T2 being Tree holds
tree(T1,T2) = (elementary_tree 2 with-replacement(<*0*>,T1))
with-replacement (<*1*>, T2);
registration
let p be FinTree-yielding FinSequence;
cluster tree(p) -> finite;
end;
registration
let T be finite Tree;
cluster ^T -> finite;
end;
registration
let T1,T2 be finite Tree;
cluster tree(T1,T2) -> finite;
end;
theorem :: TREES_3:60
for T being Tree, x being object holds x in ^T iff x = {} or
ex p st p in T & x = <*0*>^p;
theorem :: TREES_3:61
for T being Tree, p being FinSequence holds p in T iff <*0*>^p in ^T;
theorem :: TREES_3:62
for T being Tree holds elementary_tree 1 c= ^T;
theorem :: TREES_3:63
for T1,T2 being Tree st T1 c= T2 holds ^T1 c= ^T2;
theorem :: TREES_3:64
for T1,T2 being Tree st ^T1 = ^T2 holds T1 = T2;
theorem :: TREES_3:65
for T being Tree holds (^T)|<*0*> = T;
theorem :: TREES_3:66
for T1,T2 being Tree holds ^T1 with-replacement (<*0*>,T2) = ^T2;
theorem :: TREES_3:67
^elementary_tree 0 = elementary_tree 1;
theorem :: TREES_3:68
for T1,T2 being Tree, x being object 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:69
for T1,T2 being Tree, p being FinSequence holds
p in T1 iff <*0*>^p in tree(T1,T2);
theorem :: TREES_3:70
for T1,T2 being Tree, p being FinSequence holds
p in T2 iff <*1*>^p in tree(T1,T2);
theorem :: TREES_3:71
for T1,T2 being Tree holds elementary_tree 2 c= tree(T1,T2);
theorem :: TREES_3:72
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:73
for T1,T2, W1,W2 being Tree st tree(T1,T2) = tree(W1,W2) holds
T1 = W1 & T2 = W2;
theorem :: TREES_3:74
for T1,T2 being Tree holds tree(T1,T2)|<*0*> = T1 & tree(T1,T2)|<*1*> = T2;
theorem :: TREES_3:75
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:76
tree(elementary_tree 0, elementary_tree 0) = elementary_tree 2;
reserve w for FinTree-yielding FinSequence;
theorem :: TREES_3:77
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:78
for t being finite Tree st t in rng w holds height tree(w) > height t;
theorem :: TREES_3:79
for t being finite Tree st t in rng w &
for t9 being finite Tree st t9 in rng w holds height t9 <= height t holds
height tree(w) = (height t) + 1;
theorem :: TREES_3:80
for T being finite Tree holds height ^T = (height T) + 1;
theorem :: TREES_3:81
for T1,T2 being finite Tree holds
height tree(T1,T2) = max(height T1, height T2)+1;
begin :: Addenda
:: from DTCONSTR
registration
let D be non empty set, t be Element of FinTrees D;
cluster dom t -> finite;
end;
definition
let p be FinSequence such that
p is DTree-yielding;
func roots p -> FinSequence means
:: TREES_3:def 18
dom it = dom p & for i being Element of NAT st i in dom p
ex T being DecoratedTree st T = p.i & it.i = T.{};
end;