The Mizar abstract of TREES

Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users
The abstract of the Mizar article:: K\"onig's Lemma
by
Grzegorz Bancerek
Received January 10, 1991
MML identifier: TREES_2
[ Mizar article, MML identifier index ]
environ

 vocabulary TREES_1, FUNCT_1, FINSEQ_1, ZFMISC_1, RELAT_1, BOOLE, ORDERS_1,
      ORDINAL1, TARSKI, FINSET_1, CARD_1, ARYTM_1, FUNCOP_1, TREES_2, HAHNBAN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XREAL_0, RELAT_1,
      FUNCT_1, REAL_1, NAT_1, NUMBERS, FINSEQ_1, FINSET_1, CARD_1, FUNCT_2,
      FUNCOP_1, TREES_1;
 constructors WELLORD2, REAL_1, NAT_1, FUNCOP_1, TREES_1, XREAL_0, MEMBERED,
      XBOOLE_0;
 clusters SUBSET_1, RELSET_1, FINSEQ_1, CARD_1, TREES_1, FINSET_1, FUNCOP_1,
      RELAT_1, NAT_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 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,w' for Element of W,
         f for Function,
         D,D' 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;

canceled;

theorem :: TREES_2:4
  len v1 = k+1 implies ex v2,x st v1 = v2^<*x*> & len v2 = k;

canceled;

theorem :: TREES_2:6
  ProperPrefixes (v^<*x*>) = ProperPrefixes v \/ {v};

scheme TreeStruct_Ind { 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:7
  (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:8
   p in W implies W = W with-replacement (p,W|p);

theorem :: TREES_2:9
  p in W & q in W & not p is_a_prefix_of q implies
   q in W with-replacement (p,W1);

theorem :: TREES_2:10
   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;

definition
 cluster finite-order 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 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:11
   for L being Level of W holds L is AntiChain_of_Prefixes of W;

theorem :: TREES_2:12
   succ w is AntiChain_of_Prefixes of W;

theorem :: TREES_2:13
   for A being AntiChain_of_Prefixes of W, C being Chain of W
   ex w st A /\ C c= {w};

definition let W,n;
 func W-level n -> Level of W equals
:: TREES_2:def 6

    { w: len w = n };
end;

theorem :: TREES_2:14
  w^<*n*> in succ w iff w^<*n*> in W;

theorem :: TREES_2:15
   w = {} implies W-level 1 = succ w;

theorem :: TREES_2:16
    W = union { W-level n: not contradiction };

theorem :: TREES_2:17
   for W being finite Tree holds W = union { W-level n: n <= height W };

theorem :: TREES_2:18
   for L being Level of W ex n st L = W-level n;

scheme FraenkelCard { A() ->non empty set, X() -> set, F(set) -> set }:
 Card { F(w) where w is Element of A(): w in X() } <=` Card X();

scheme 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:19
  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:20
  W is finite-order implies succ w is finite;

definition let W be finite-order Tree;
 let w be Element of W;
  cluster succ w -> finite;
end;

theorem :: TREES_2:21
  {} is Chain of W;

theorem :: TREES_2:22
  {{}} is Chain of W;

definition let W;
 cluster non empty 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;

definition let W;
 cluster Branch-like Chain of W;
end;

definition let W;
 mode Branch of W is Branch-like Chain of W;
end;

definition let W;
 cluster Branch-like -> non empty Chain of W;
end;

 reserve C for Chain of W, B for Branch of W;

theorem :: TREES_2:23
  v1 in C & v2 in C implies v1 in
 ProperPrefixes v2 or v2 is_a_prefix_of v1;

theorem :: TREES_2:24
  v1 in C & v2 in C & v is_a_prefix_of v2 implies
   v1 in ProperPrefixes v or v is_a_prefix_of v1;

definition let W;
 cluster finite Chain of W;
end;

theorem :: TREES_2:25
  for C being finite Chain of W st card C > n
     ex p st p in C & len p >= n;

theorem :: TREES_2:26
  for C holds { w: ex p st p in C & w is_a_prefix_of p } is Chain of W;

theorem :: TREES_2:27
  p is_a_prefix_of q & q in B implies p in B;

theorem :: TREES_2:28
  {} in B;

theorem :: TREES_2:29
  p in C & q in C & len p <= len q implies p is_a_prefix_of q;

theorem :: TREES_2:30
  ex B st C c= B;

scheme FuncExOfMinNat { P[set,Nat], X()->set }:
 ex f st dom f = X() & for x 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 st x in X() ex n st P[x,n];

scheme InfiniteChain { X()->set, a()->set, Q[set], P[set,set] }:
 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 st x in X() & Q[x] ex y st y in X() & P[x,y] & Q[y];

theorem :: TREES_2:31
 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;

theorem :: TREES_2:32
   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;

definition
 cluster DecoratedTree-like Function;
end;

definition
 mode DecoratedTree is DecoratedTree-like Function;
end;

 reserve T,T1,T2 for DecoratedTree;

definition let T;
 cluster dom T -> non empty Tree-like;
end;

definition let X be set;
 mode ParametrizedSubset of X -> Relation means
:: TREES_2:def 9
 rng it c= X;
end;

definition let D;
 cluster DecoratedTree-like Function-like ParametrizedSubset of D;
end;

definition let D;
 mode DecoratedTree of D is
    DecoratedTree-like Function-like ParametrizedSubset of D;
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:33
 dom T1 = dom T2 & (for p st p in dom T1 holds T1.p = T2.p) implies T1 = T2;

scheme DTreeEx { T() -> Tree, P[set,set] }:
 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 DTreeLambda { T() -> Tree, f(set) -> 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 10

  T.:Leaves dom T;
 let p;
 func T|p -> DecoratedTree means
:: TREES_2:def 11

  dom it = (dom T)|p & for q st q in (dom T)|p holds it.q = T.(p^q);
end;

theorem :: TREES_2:34
  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;
 let p be Element of dom T;
 func T|p -> DecoratedTree of D;
end;

definition let T,p,T1;
 assume
   p in dom T;
 func T with-replacement (p,T1) -> DecoratedTree means
:: TREES_2:def 12
    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;

definition let W,x;
 cluster W --> x -> DecoratedTree-like;
end;

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

theorem :: TREES_2:35
  (for x st x in D holds x is Tree) implies union D is Tree;

theorem :: TREES_2:36
  (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:37
  (for x st x in D holds x is DecoratedTree) & D is c=-linear
   implies union D is DecoratedTree;

theorem :: TREES_2:38
  (for x st x in D' holds x is DecoratedTree of D) &
   D' is c=-linear implies
    union D' is DecoratedTree of D;

scheme 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,x st x = T.t & n in F(x) holds T.(t^<*n*>) = S().[x,n]
  provided
 for d being Element of D(), k1,k2 st k1 <= k2 & k2 in F(d) holds k1 in F(d);

scheme 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,x st x = T.t & n < F(x) holds T.(t^<*n*>) = S().[x,n];
The abstract of the Mizar article:

K\"onig's Lemma
