:: K\"onig's Lemma
:: by Grzegorz Bancerek
::
:: Received January 10, 1991
:: Copyright (c) 1991-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_1, SUBSET_1, FUNCT_1, XBOOLE_0, FINSEQ_1,
ORDINAL4, XXREAL_0, ARYTM_3, RELAT_1, TARSKI, CARD_1, NAT_1, ORDINAL1,
FINSET_1, REAL_1, ARYTM_1, ZFMISC_1, FUNCOP_1, TREES_2, AMISTD_3,
FINSEQ_2, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, XCMPLX_0,
FUNCT_1, PARTFUN1, XREAL_0, REAL_1, NAT_1, CARD_1, NUMBERS, FINSEQ_1,
FINSEQ_2, FINSET_1, RELSET_1, BINOP_1, FUNCT_2, FUNCOP_1, TREES_1,
XXREAL_0;
constructors WELLORD2, BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, TREES_1,
RELSET_1, FINSEQ_2, XREAL_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, TREES_1, CARD_1,
FINSEQ_2, PARTFUN1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
reserve x,y,z,a,b,c,X,X1,X2,Y,Z for set,
W,W1,W2 for Tree,
w,w9 for Element of W,
f for Function,
D,D9 for non empty set,
i,k,k1,k2,l,m,n for Nat,
v,v1,v2 for FinSequence,
p,q,r,r1,r2 for FinSequence of NAT;
theorem :: TREES_2:1
for v1,v2,v st v1 is_a_prefix_of v & v2 is_a_prefix_of v
holds v1,v2 are_c=-comparable;
theorem :: TREES_2:2
for v1,v2,v st v1 is_a_proper_prefix_of v & v2 is_a_prefix_of v holds
v1,v2 are_c=-comparable;
theorem :: TREES_2:3
len v1 = k+1 implies ex v2,x st v1 = v2^<*x*> & len v2 = k;
theorem :: TREES_2:4
ProperPrefixes (v^<*x*>) = ProperPrefixes v \/ {v};
scheme :: TREES_2:sch 1
TreeStructInd { T()->Tree, P[set] }:
for t being Element of T() holds P[t]
provided
P[{}] and
for t being Element of T(), n st P[t] & t^<*n*> in T() holds P[t^<*n*>];
theorem :: TREES_2:5
(for p holds p in W1 iff p in W2) implies W1 = W2;
definition
let W1,W2;
redefine pred W1 = W2 means
:: TREES_2:def 1
for p holds p in W1 iff p in W2;
end;
theorem :: TREES_2:6
p in W implies W = W with-replacement (p,W|p);
theorem :: TREES_2:7
p in W & q in W & not p is_a_prefix_of q implies
q in W with-replacement (p,W1);
theorem :: TREES_2:8
p in W & q in W & not p,q are_c=-comparable implies
(W with-replacement (p,W1)) with-replacement (q,W2) =
(W with-replacement (q,W2)) with-replacement (p,W1);
definition
let IT be Tree;
attr IT is finite-order means
:: TREES_2:def 2
ex n st for t being Element of IT holds not t^<*n*> in IT;
end;
registration
cluster finite-order for Tree;
end;
definition
let W;
mode Chain of W -> Subset of W means
:: TREES_2:def 3
for p,q st p in it & q in it holds p,q are_c=-comparable;
mode Level of W -> Subset of W means
:: TREES_2:def 4
ex n being Nat st it = { w: len w = n};
let w;
func succ w -> Subset of W equals
:: TREES_2:def 5
{ w^<*n*>: w^<*n*> in W };
end;
theorem :: TREES_2:9
for L being Level of W holds L is AntiChain_of_Prefixes of W;
theorem :: TREES_2:10
succ w is AntiChain_of_Prefixes of W;
theorem :: TREES_2:11
for A being AntiChain_of_Prefixes of W, C being Chain of W
ex w st A /\ C c= {w};
definition
let W;
let n be Nat;
func W-level n -> Level of W equals
:: TREES_2:def 6
{ w: len w = n };
end;
theorem :: TREES_2:12
w^<*n*> in succ w iff w^<*n*> in W;
theorem :: TREES_2:13
w = {} implies W-level 1 = succ w;
theorem :: TREES_2:14
W = union the set of all W-level n;
theorem :: TREES_2:15
for W being finite Tree holds W = union { W-level n: n <= height W };
theorem :: TREES_2:16
for L being Level of W ex n st L = W-level n;
scheme :: TREES_2:sch 2
FraenkelCard { A() ->non empty set, X() -> set, F(object) -> set }:
card { F(w) where w is Element of A(): w in X() } c= card X();
scheme :: TREES_2:sch 3
FraenkelFinCard { A() ->non empty set,
X,Y() -> finite set, F(set) -> set }: card Y() <= card X()
provided
Y() = { F(w) where w is Element of A(): w in X() };
theorem :: TREES_2:17
W is finite-order implies ex n st for w holds
ex B being finite set st B = succ w & card B <= n;
theorem :: TREES_2:18
W is finite-order implies succ w is finite;
registration
let W be finite-order Tree;
let w be Element of W;
cluster succ w -> finite;
end;
theorem :: TREES_2:19
{} is Chain of W;
theorem :: TREES_2:20
{{}} is Chain of W;
registration
let W;
cluster non empty for Chain of W;
end;
definition
let W;
let IT be Chain of W;
attr IT is Branch-like means
:: TREES_2:def 7
(for p st p in IT holds ProperPrefixes p c= IT) &
not ex p st p in W & for q st q in IT holds q is_a_proper_prefix_of p;
end;
registration
let W;
cluster Branch-like for Chain of W;
end;
definition
let W;
mode Branch of W is Branch-like Chain of W;
end;
registration
let W;
cluster Branch-like -> non empty for Chain of W;
end;
reserve C for Chain of W,
B for Branch of W;
theorem :: TREES_2:21
v1 in C & v2 in C implies v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1;
theorem :: TREES_2:22
v1 in C & v2 in C & v is_a_prefix_of v2 implies
v1 in ProperPrefixes v or v is_a_prefix_of v1;
registration
let W;
cluster finite for Chain of W;
end;
theorem :: TREES_2:23
for C being finite Chain of W st card C > n ex p st p in C & len p >= n;
theorem :: TREES_2:24
for C holds { w: ex p st p in C & w is_a_prefix_of p } is Chain of W;
theorem :: TREES_2:25
p is_a_prefix_of q & q in B implies p in B;
theorem :: TREES_2:26
{} in B;
theorem :: TREES_2:27
p in C & q in C & len p <= len q implies p is_a_prefix_of q;
theorem :: TREES_2:28
ex B st C c= B;
scheme :: TREES_2:sch 4
FuncExOfMinNat { P[object,Nat], X()->set }:
ex f st dom f = X() &
for x being object st x in X() ex n st f.x = n & P[x,n] &
for m st P[x,m] holds n <= m
provided
for x being object st x in X() ex n st P[x,n];
scheme :: TREES_2:sch 5
InfiniteChain{X()->set, a()->object, Q[object], P[object,object]}:
ex f st dom f = NAT & rng f c= X() & f.0 = a() &
for k holds P[f.k,f.(k+1)] & Q[f.k]
provided
a() in X() & Q[a()] and
for x being object st x in X() & Q[x]
ex y being object st y in X() & P[x,y] & Q[y];
theorem :: TREES_2:29
for T being Tree st (for n ex C being finite Chain of T st card C = n) &
for t being Element of T holds succ t is finite
ex B being Chain of T st not B is finite;
::$N Koenig Lemma
theorem :: TREES_2:30
for T being finite-order Tree st
for n ex C being finite Chain of T st card C = n
ex B being Chain of T st not B is finite;
definition
let IT be Relation;
attr IT is DecoratedTree-like means
:: TREES_2:def 8
dom IT is Tree;
end;
registration
cluster DecoratedTree-like for Function;
end;
definition
mode DecoratedTree is DecoratedTree-like Function;
end;
reserve T,T1,T2 for DecoratedTree;
registration
let T;
cluster dom T -> non empty Tree-like;
end;
registration
let D;
cluster DecoratedTree-like D-valued for Function;
end;
definition
let D;
mode DecoratedTree of D is D-valued DecoratedTree;
end;
definition
let D be non empty set, T be DecoratedTree of D, t be Element of dom T;
redefine func T.t -> Element of D;
end;
theorem :: TREES_2:31
dom T1 = dom T2 & (for p st p in dom T1 holds T1.p = T2.p) implies T1 = T2;
scheme :: TREES_2:sch 6
DTreeEx { T() -> Tree, P[object,object] }:
ex T st dom T = T() & for p st p in T() holds P[p,T.p]
provided
for p st p in T() ex x st P[p,x];
scheme :: TREES_2:sch 7
DTreeLambda { T() -> Tree, f(object) -> set }:
ex T st dom T = T() & for p st p in T() holds T.p = f(p);
definition
let T;
func Leaves T -> set equals
:: TREES_2:def 9
T.:Leaves dom T;
let p;
func T|p -> DecoratedTree means
:: TREES_2:def 10
dom it = (dom T)|p & for q st q in (dom T)|p holds it.q = T.(p^q);
end;
theorem :: TREES_2:32
p in dom T implies rng (T|p) c= rng T;
definition
let D;
let T be DecoratedTree of D;
redefine func Leaves T -> Subset of D;
end;
registration
let D;
let T be DecoratedTree of D;
let p be Element of dom T;
cluster T|p -> D-valued;
end;
definition
let T,p,T1;
assume
p in dom T;
func T with-replacement (p,T1) -> DecoratedTree means
:: TREES_2:def 11
dom it = dom T with-replacement (p,dom T1) &
for q st q in dom T with-replacement (p,dom T1) holds
not p is_a_prefix_of q & it.q = T.q or
ex r st r in dom T1 & q = p^r & it.q = T1.r;
end;
registration
let W,x;
cluster W --> x -> DecoratedTree-like;
end;
theorem :: TREES_2:33
(for x st x in D holds x is Tree) implies union D is Tree;
theorem :: TREES_2:34
(for x st x in X holds x is Function) & X is c=-linear implies
union X is Relation-like Function-like;
theorem :: TREES_2:35
(for x st x in D holds x is DecoratedTree) & D is c=-linear
implies union D is DecoratedTree;
theorem :: TREES_2:36
(for x st x in D9 holds x is DecoratedTree of D) & D9 is c=-linear implies
union D9 is DecoratedTree of D;
scheme :: TREES_2:sch 8
DTreeStructEx
{ D() -> non empty set, d() -> Element of D(), F(set) -> set,
S() -> Function of [:D(),NAT:],D()}:
ex T being DecoratedTree of D() st T.{} = d() &
for t being Element of dom T holds succ t = { t^<*k*>: k in F(T.t)} &
for n st n in F(T.t) holds T.(t^<*n*>) = S().(T.t,n)
provided
for d being Element of D(), k1,k2 st k1 <= k2 & k2 in F(d) holds k1 in F(d);
scheme :: TREES_2:sch 9
DTreeStructFinEx
{ D() -> non empty set, d() -> Element of D(), F(set) -> Nat,
S() -> Function of [:D(),NAT:],D()}:
ex T being DecoratedTree of D() st T.{} = d() &
for t being Element of dom T holds succ t = { t^<*k*>: k < F(T.t)} &
for n st n < F(T.t) holds T.(t^<*n*>) = S().(T.t,n);
begin :: Addenda
:: from PRELAMB
registration
let Tr be finite Tree, v be Element of Tr;
cluster succ v -> finite;
end;
definition
let Tr be finite Tree, v be Element of Tr;
func branchdeg v -> set equals
:: TREES_2:def 12
card succ v;
end;
registration
cluster finite for DecoratedTree;
end;
registration
let D be non empty set;
cluster finite for DecoratedTree of D;
end;
registration
let a,b be non empty set;
cluster non empty for Relation of a,b;
end;
:: from MODAL_1, 2007.03.14, A.T.
reserve x1,x2 for set,
w for FinSequence of NAT;
theorem :: TREES_2:37
for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2),w being Element of Z2
st v = p^w holds succ v,succ w are_equipotent;
scheme :: TREES_2:sch 10
DTreeStructEx
{ D() -> non empty set, d() -> Element of D(), Q[set,set],
S() -> Function of [:D(),NAT:],D()}:
ex T being DecoratedTree of D() st T.{} = d() &
for t being Element of dom T holds succ t = { t^<*k*>: Q[k,T.t]} &
for n st Q[n,T.t] holds T.(t^<*n*>) = S().(T.t,n)
provided
for d being Element of D(), k1,k2 st k1 <= k2 & Q[k2,d] holds Q[k1,d];
:: from AMISTD_3, 2010.01.10, A.T.
theorem :: TREES_2:38
for T1, T2 being Tree st
for n being Nat holds T1-level n = T2-level n
holds T1 = T2;
theorem :: TREES_2:39
for n being Nat holds TrivialInfiniteTree-level n = { n |-> 0 };
theorem :: TREES_2:40
for X,Y being set for B being c=-linear Subset of PFuncs(X,Y)
holds union B in PFuncs(X,Y);