src/ZF/Cardinal.thy
author paulson
Tue, 09 Jul 2002 23:05:26 +0200
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
permissions -rw-r--r--
better document preparation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/Cardinal.thy
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     5
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     6
*)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
     7
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     8
header{*Cardinal Numbers Without the Axiom of Choice*}
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     9
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
    10
theory Cardinal = OrderType + Finite + Nat + Sum:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    11
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    12
(*** The following really belong in upair ***)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    13
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    14
lemma eq_imp_not_mem: "a=A ==> a ~: A"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    15
by (blast intro: elim: mem_irrefl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    16
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    17
constdefs
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    18
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    19
  (*least ordinal operator*)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    20
   Least    :: "(i=>o) => i"    (binder "LEAST " 10)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    21
     "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    22
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    23
  eqpoll   :: "[i,i] => o"     (infixl "eqpoll" 50)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    24
    "A eqpoll B == EX f. f: bij(A,B)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    25
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    26
  lepoll   :: "[i,i] => o"     (infixl "lepoll" 50)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    27
    "A lepoll B == EX f. f: inj(A,B)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    28
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    29
  lesspoll :: "[i,i] => o"     (infixl "lesspoll" 50)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    30
    "A lesspoll B == A lepoll B & ~(A eqpoll B)"
832
ad50a9e74eaf Added Krzysztof's constants lesspoll and Finite
lcp
parents: 753
diff changeset
    31
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    32
  cardinal :: "i=>i"           ("|_|")
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    33
    "|A| == LEAST i. i eqpoll A"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    34
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    35
  Finite   :: "i=>o"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    36
    "Finite(A) == EX n:nat. A eqpoll n"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    37
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    38
  Card     :: "i=>o"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    39
    "Card(i) == (i = |i|)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    40
9683
f87c8c449018 added some xsymbols, and tidied
paulson
parents: 1478
diff changeset
    41
syntax (xsymbols)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    42
  "eqpoll"      :: "[i,i] => o"       (infixl "\<approx>" 50)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    43
  "lepoll"      :: "[i,i] => o"       (infixl "\<lesssim>" 50)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    44
  "lesspoll"    :: "[i,i] => o"       (infixl "\<prec>" 50)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    45
  "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    46
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    47
(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    48
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    49
(** Lemma: Banach's Decomposition Theorem **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    50
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    51
lemma decomp_bnd_mono: "bnd_mono(X, %W. X - g``(Y - f``W))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    52
by (rule bnd_monoI, blast+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    53
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    54
lemma Banach_last_equation:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    55
    "g: Y->X
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    56
     ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =        
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    57
	 X - lfp(X, %W. X - g``(Y - f``W))" 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    58
apply (rule_tac P = "%u. ?v = X-u" 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    59
       in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    60
apply (simp add: double_complement  fun_is_rel [THEN image_subset])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    61
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    62
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    63
lemma decomposition:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    64
     "[| f: X->Y;  g: Y->X |] ==>    
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    65
      EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &     
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    66
                      (YA Int YB = 0) & (YA Un YB = Y) &     
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    67
                      f``XA=YA & g``YB=XB"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    68
apply (intro exI conjI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    69
apply (rule_tac [6] Banach_last_equation)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    70
apply (rule_tac [5] refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    71
apply (assumption | 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    72
       rule  Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    73
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    74
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    75
lemma schroeder_bernstein:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    76
    "[| f: inj(X,Y);  g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    77
apply (insert decomposition [of f X Y g]) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    78
apply (simp add: inj_is_fun)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    79
apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    80
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    81
   is forced by the context!! *)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    82
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    83
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    84
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    85
(** Equipollence is an equivalence relation **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    86
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    87
lemma bij_imp_eqpoll: "f: bij(A,B) ==> A \<approx> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    88
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    89
apply (erule exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    90
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    91
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    92
(*A eqpoll A*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    93
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, standard, simp]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    94
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    95
lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    96
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    97
apply (blast intro: bij_converse_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    98
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    99
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   100
lemma eqpoll_trans: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   101
    "[| X \<approx> Y;  Y \<approx> Z |] ==> X \<approx> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   102
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   103
apply (blast intro: comp_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   104
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   105
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   106
(** Le-pollence is a partial ordering **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   107
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   108
lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   109
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   110
apply (rule exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   111
apply (erule id_subset_inj)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   112
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   113
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   114
lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, standard, simp]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   115
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   116
lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll, standard]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   117
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   118
lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   119
by (unfold eqpoll_def bij_def lepoll_def, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   120
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   121
lemma lepoll_trans: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   122
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   123
apply (blast intro: comp_inj)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   124
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   125
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   126
(*Asymmetry law*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   127
lemma eqpollI: "[| X \<lesssim> Y;  Y \<lesssim> X |] ==> X \<approx> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   128
apply (unfold lepoll_def eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   129
apply (elim exE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   130
apply (rule schroeder_bernstein, assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   131
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   132
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   133
lemma eqpollE:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   134
    "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   135
by (blast intro: eqpoll_imp_lepoll eqpoll_sym) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   136
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   137
lemma eqpoll_iff: "X \<approx> Y <-> X \<lesssim> Y & Y \<lesssim> X"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   138
by (blast intro: eqpollI elim!: eqpollE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   139
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   140
lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   141
apply (unfold lepoll_def inj_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   142
apply (blast dest: apply_type)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   143
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   144
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   145
(*0 \<lesssim> Y*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   146
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   147
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   148
lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   149
by (blast intro: lepoll_0_is_0 lepoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   150
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   151
lemma Un_lepoll_Un: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   152
    "[| A \<lesssim> B; C \<lesssim> D; B Int D = 0 |] ==> A Un C \<lesssim> B Un D"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   153
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   154
apply (blast intro: inj_disjoint_Un)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   155
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   156
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   157
(*A eqpoll 0 ==> A=0*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   158
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0, standard]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   159
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   160
lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   161
by (blast intro: eqpoll_0_is_0 eqpoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   162
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   163
lemma eqpoll_disjoint_Un: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   164
    "[| A \<approx> B;  C \<approx> D;  A Int C = 0;  B Int D = 0 |]   
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   165
     ==> A Un C \<approx> B Un D"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   166
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   167
apply (blast intro: bij_disjoint_Un)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   168
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   169
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   170
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   171
(*** lesspoll: contributions by Krzysztof Grabczewski ***)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   172
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   173
lemma lesspoll_not_refl: "~ (i \<prec> i)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   174
by (simp add: lesspoll_def) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   175
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   176
lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   177
by (simp add: lesspoll_def) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   178
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   179
lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   180
by (unfold lesspoll_def, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   181
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   182
lemma lepoll_well_ord: "[| A \<lesssim> B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   183
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   184
apply (blast intro: well_ord_rvimage)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   185
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   186
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   187
lemma lepoll_iff_leqpoll: "A \<lesssim> B <-> A \<prec> B | A \<approx> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   188
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   189
apply (blast intro!: eqpollI elim!: eqpollE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   190
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   191
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   192
lemma inj_not_surj_succ: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   193
  "[| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   194
apply (unfold inj_def surj_def) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   195
apply (safe del: succE) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   196
apply (erule swap, rule exI) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   197
apply (rule_tac a = "lam z:A. if f`z=m then y else f`z" in CollectI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   198
txt{*the typing condition*}
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   199
 apply (best intro!: if_type [THEN lam_type] elim: apply_funtype [THEN succE])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   200
txt{*Proving it's injective*}
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   201
apply simp
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   202
apply blast 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   203
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   204
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   205
(** Variations on transitivity **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   206
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   207
lemma lesspoll_trans: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   208
      "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   209
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   210
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   211
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   212
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   213
lemma lesspoll_trans1: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   214
      "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   215
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   216
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   217
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   218
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   219
lemma lesspoll_trans2: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   220
      "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   221
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   222
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   223
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   224
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   225
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   226
(** LEAST -- the least number operator [from HOL/Univ.ML] **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   227
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   228
lemma Least_equality: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   229
    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   230
apply (unfold Least_def) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   231
apply (rule the_equality, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   232
apply (elim conjE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   233
apply (erule Ord_linear_lt, assumption, blast+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   234
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   235
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   236
lemma LeastI: "[| P(i);  Ord(i) |] ==> P(LEAST x. P(x))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   237
apply (erule rev_mp)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   238
apply (erule_tac i=i in trans_induct) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   239
apply (rule impI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   240
apply (rule classical)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   241
apply (blast intro: Least_equality [THEN ssubst]  elim!: ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   242
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   243
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   244
(*Proof is almost identical to the one above!*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   245
lemma Least_le: "[| P(i);  Ord(i) |] ==> (LEAST x. P(x)) le i"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   246
apply (erule rev_mp)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   247
apply (erule_tac i=i in trans_induct) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   248
apply (rule impI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   249
apply (rule classical)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   250
apply (subst Least_equality, assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   251
apply (erule_tac [2] le_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   252
apply (blast elim: ltE intro: leI ltI lt_trans1)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   253
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   254
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   255
(*LEAST really is the smallest*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   256
lemma less_LeastE: "[| P(i);  i < (LEAST x. P(x)) |] ==> Q"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   257
apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   258
apply (simp add: lt_Ord) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   259
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   260
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   261
(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   262
lemma LeastI2:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   263
    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   264
by (blast intro: LeastI ) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   265
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   266
(*If there is no such P then LEAST is vacuously 0*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   267
lemma Least_0: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   268
    "[| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   269
apply (unfold Least_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   270
apply (rule the_0, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   271
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   272
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   273
lemma Ord_Least: "Ord(LEAST x. P(x))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   274
apply (rule_tac P = "EX i. Ord(i) & P(i)" in case_split_thm)  
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   275
    (*case_tac method not available yet; needs "inductive"*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   276
apply safe
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   277
apply (rule Least_le [THEN ltE])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   278
prefer 3 apply assumption+
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   279
apply (erule Least_0 [THEN ssubst])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   280
apply (rule Ord_0)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   281
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   282
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   283
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   284
(** Basic properties of cardinals **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   285
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   286
(*Not needed for simplification, but helpful below*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   287
lemma Least_cong:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   288
     "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   289
by simp
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   290
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   291
(*Need AC to get X \<lesssim> Y ==> |X| le |Y|;  see well_ord_lepoll_imp_Card_le
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   292
  Converse also requires AC, but see well_ord_cardinal_eqE*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   293
lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   294
apply (unfold eqpoll_def cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   295
apply (rule Least_cong)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   296
apply (blast intro: comp_bij bij_converse_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   297
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   298
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   299
(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   300
lemma well_ord_cardinal_eqpoll: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   301
    "well_ord(A,r) ==> |A| \<approx> A"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   302
apply (unfold cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   303
apply (rule LeastI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   304
apply (erule_tac [2] Ord_ordertype)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   305
apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_imp_eqpoll])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   306
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   307
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   308
(* Ord(A) ==> |A| \<approx> A *)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   309
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   310
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   311
lemma well_ord_cardinal_eqE:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   312
     "[| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X \<approx> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   313
apply (rule eqpoll_sym [THEN eqpoll_trans])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   314
apply (erule well_ord_cardinal_eqpoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   315
apply (simp (no_asm_simp) add: well_ord_cardinal_eqpoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   316
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   317
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   318
lemma well_ord_cardinal_eqpoll_iff:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   319
     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X \<approx> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   320
by (blast intro: cardinal_cong well_ord_cardinal_eqE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   321
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   322
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   323
(** Observations from Kunen, page 28 **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   324
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   325
lemma Ord_cardinal_le: "Ord(i) ==> |i| le i"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   326
apply (unfold cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   327
apply (erule eqpoll_refl [THEN Least_le])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   328
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   329
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   330
lemma Card_cardinal_eq: "Card(K) ==> |K| = K"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   331
apply (unfold Card_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   332
apply (erule sym)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   333
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   334
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   335
(* Could replace the  ~(j \<approx> i)  by  ~(i \<lesssim> j) *)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   336
lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   337
apply (unfold Card_def cardinal_def) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   338
apply (subst Least_equality)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   339
apply (blast intro: eqpoll_refl )+
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   340
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   341
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   342
lemma Card_is_Ord: "Card(i) ==> Ord(i)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   343
apply (unfold Card_def cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   344
apply (erule ssubst)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   345
apply (rule Ord_Least)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   346
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   347
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   348
lemma Card_cardinal_le: "Card(K) ==> K le |K|"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   349
apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   350
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   351
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   352
lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   353
apply (unfold cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   354
apply (rule Ord_Least)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   355
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   356
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   357
(*The cardinals are the initial ordinals*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   358
lemma Card_iff_initial: "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j \<approx> K)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   359
apply (safe intro!: CardI Card_is_Ord)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   360
 prefer 2 apply blast
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   361
apply (unfold Card_def cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   362
apply (rule less_LeastE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   363
apply (erule_tac [2] subst, assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   364
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   365
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   366
lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   367
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   368
apply (drule Card_iff_initial [THEN iffD1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   369
apply (blast intro!: leI [THEN le_imp_lepoll])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   370
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   371
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   372
lemma Card_0: "Card(0)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   373
apply (rule Ord_0 [THEN CardI])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   374
apply (blast elim!: ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   375
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   376
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   377
lemma Card_Un: "[| Card(K);  Card(L) |] ==> Card(K Un L)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   378
apply (rule Ord_linear_le [of K L])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   379
apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_is_Ord le_imp_subset
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   380
                     subset_Un_iff2 [THEN iffD1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   381
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   382
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   383
(*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   384
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   385
lemma Card_cardinal: "Card(|A|)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   386
apply (unfold cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   387
apply (rule_tac P =  "EX i. Ord (i) & i \<approx> A" in case_split_thm)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   388
 txt{*degenerate case*}
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   389
 prefer 2 apply (erule Least_0 [THEN ssubst], rule Card_0)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   390
txt{*real case: A is isomorphic to some ordinal*}
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   391
apply (rule Ord_Least [THEN CardI], safe)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   392
apply (rule less_LeastE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   393
prefer 2 apply assumption
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   394
apply (erule eqpoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   395
apply (best intro: LeastI ) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   396
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   397
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   398
(*Kunen's Lemma 10.5*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   399
lemma cardinal_eq_lemma: "[| |i| le j;  j le i |] ==> |j| = |i|"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   400
apply (rule eqpollI [THEN cardinal_cong])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   401
apply (erule le_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   402
apply (rule lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   403
apply (erule_tac [2] le_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   404
apply (rule eqpoll_sym [THEN eqpoll_imp_lepoll])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   405
apply (rule Ord_cardinal_eqpoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   406
apply (elim ltE Ord_succD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   407
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   408
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   409
lemma cardinal_mono: "i le j ==> |i| le |j|"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   410
apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   411
apply (safe intro!: Ord_cardinal le_eqI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   412
apply (rule cardinal_eq_lemma)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   413
prefer 2 apply assumption
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   414
apply (erule le_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   415
apply (erule ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   416
apply (erule Ord_cardinal_le)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   417
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   418
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   419
(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   420
lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   421
apply (rule Ord_linear2 [of i j], assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   422
apply (erule lt_trans2 [THEN lt_irrefl])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   423
apply (erule cardinal_mono)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   424
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   425
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   426
lemma Card_lt_imp_lt: "[| |i| < K;  Ord(i);  Card(K) |] ==> i < K"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   427
apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   428
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   429
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   430
lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) <-> (i < K)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   431
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   432
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   433
lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K le |i|) <-> (K le i)"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13244
diff changeset
   434
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   435
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   436
(*Can use AC or finiteness to discharge first premise*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   437
lemma well_ord_lepoll_imp_Card_le:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   438
     "[| well_ord(B,r);  A \<lesssim> B |] ==> |A| le |B|"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   439
apply (rule_tac i = "|A|" and j = "|B|" in Ord_linear_le)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   440
apply (safe intro!: Ord_cardinal le_eqI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   441
apply (rule eqpollI [THEN cardinal_cong], assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   442
apply (rule lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   443
apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll], assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   444
apply (erule le_imp_lepoll [THEN lepoll_trans])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   445
apply (rule eqpoll_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   446
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   447
apply (erule exE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   448
apply (rule well_ord_cardinal_eqpoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   449
apply (erule well_ord_rvimage, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   450
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   451
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   452
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   453
lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| le i"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   454
apply (rule le_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   455
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   456
apply (erule Ord_cardinal_le)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   457
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   458
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   459
lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   460
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   461
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   462
lemma lesspoll_imp_eqpoll: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   463
     "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   464
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   465
apply (blast intro: lepoll_Ord_imp_eqpoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   466
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   467
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   468
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   469
(*** The finite cardinals ***)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   470
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   471
lemma cons_lepoll_consD: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   472
 "[| cons(u,A) \<lesssim> cons(v,B);  u~:A;  v~:B |] ==> A \<lesssim> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   473
apply (unfold lepoll_def inj_def, safe)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   474
apply (rule_tac x = "lam x:A. if f`x=v then f`u else f`x" in exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   475
apply (rule CollectI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   476
(*Proving it's in the function space A->B*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   477
apply (rule if_type [THEN lam_type])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   478
apply (blast dest: apply_funtype)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   479
apply (blast elim!: mem_irrefl dest: apply_funtype)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   480
(*Proving it's injective*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   481
apply (simp (no_asm_simp))
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   482
apply blast
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   483
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   484
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   485
lemma cons_eqpoll_consD: "[| cons(u,A) \<approx> cons(v,B);  u~:A;  v~:B |] ==> A \<approx> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   486
apply (simp add: eqpoll_iff)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   487
apply (blast intro: cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   488
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   489
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   490
(*Lemma suggested by Mike Fourman*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   491
lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   492
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   493
apply (erule cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   494
apply (rule mem_not_refl)+
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   495
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   496
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   497
lemma nat_lepoll_imp_le [rule_format]:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   498
     "m:nat ==> ALL n: nat. m \<lesssim> n --> m le n"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   499
apply (induct_tac m)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   500
apply (blast intro!: nat_0_le)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   501
apply (rule ballI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   502
apply (erule_tac n = "n" in natE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   503
apply (simp (no_asm_simp) add: lepoll_def inj_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   504
apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   505
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   506
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   507
lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   508
apply (rule iffI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   509
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   510
apply (simp add: eqpoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   511
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   512
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   513
(*The object of all this work: every natural number is a (finite) cardinal*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   514
lemma nat_into_Card: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   515
    "n: nat ==> Card(n)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   516
apply (unfold Card_def cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   517
apply (subst Least_equality)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   518
apply (rule eqpoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   519
apply (erule nat_into_Ord) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   520
apply (simp (no_asm_simp) add: lt_nat_in_nat [THEN nat_eqpoll_iff])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   521
apply (blast elim!: lt_irrefl)+
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   522
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   523
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   524
lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   525
lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   526
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   527
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   528
(*Part of Kunen's Lemma 10.6*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   529
lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n:nat |] ==> P"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   530
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   531
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   532
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   533
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   534
apply (fast elim!: Ord_nat [THEN [2] ltI [THEN leI, THEN le_imp_lepoll]]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   535
                   eqpoll_sym [THEN eqpoll_imp_lepoll] 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   536
    intro: Ord_nat [THEN [2] nat_succI [THEN ltI], THEN leI, 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   537
                 THEN le_imp_lepoll, THEN lepoll_trans, THEN succ_lepoll_natE])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   538
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   539
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   540
lemma nat_lepoll_imp_ex_eqpoll_n: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   541
     "[| n \<in> nat;  nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   542
apply (unfold lepoll_def eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   543
apply (fast del: subsetI subsetCE
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   544
            intro!: subset_SIs
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   545
            dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   546
            elim!: restrict_bij 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   547
                   inj_is_fun [THEN fun_is_rel, THEN image_subset])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   548
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   549
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   550
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   551
(** lepoll, \<prec> and natural numbers **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   552
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   553
lemma lepoll_imp_lesspoll_succ: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   554
     "[| A \<lesssim> m; m:nat |] ==> A \<prec> succ(m)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   555
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   556
apply (rule conjI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   557
apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   558
apply (rule notI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   559
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   560
apply (drule lepoll_trans, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   561
apply (erule succ_lepoll_natE, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   562
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   563
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   564
lemma lesspoll_succ_imp_lepoll: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   565
     "[| A \<prec> succ(m); m:nat |] ==> A \<lesssim> m"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   566
apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def, clarify)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   567
apply (blast intro!: inj_not_surj_succ)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   568
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   569
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   570
lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) <-> A \<lesssim> m"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   571
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   572
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   573
lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   574
apply (rule disjCI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   575
apply (rule lesspoll_succ_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   576
prefer 2 apply assumption
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   577
apply (simp (no_asm_simp) add: lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   578
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   579
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   580
lemma lesspoll_cardinal_lt: "[| A \<prec> i; Ord(i) |] ==> |A| < i"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   581
apply (unfold lesspoll_def, clarify)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   582
apply (frule lepoll_cardinal_le, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   583
apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   584
             dest: lepoll_well_ord  elim!: leE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   585
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   586
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   587
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   588
(*** The first infinite cardinal: Omega, or nat ***)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   589
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   590
(*This implies Kunen's Lemma 10.6*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   591
lemma lt_not_lepoll: "[| n<i;  n:nat |] ==> ~ i \<lesssim> n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   592
apply (rule notI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   593
apply (rule succ_lepoll_natE [of n])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   594
apply (rule lepoll_trans [of _ i])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   595
apply (erule ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   596
apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   597
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   598
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   599
lemma Ord_nat_eqpoll_iff: "[| Ord(i);  n:nat |] ==> i \<approx> n <-> i=n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   600
apply (rule iffI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   601
 prefer 2 apply (simp add: eqpoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   602
apply (rule Ord_linear_lt [of i n])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   603
apply (simp_all add: nat_into_Ord)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   604
apply (erule lt_nat_in_nat [THEN nat_eqpoll_iff, THEN iffD1], assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   605
apply (rule lt_not_lepoll [THEN notE], assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   606
apply (erule eqpoll_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   607
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   608
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   609
lemma Card_nat: "Card(nat)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   610
apply (unfold Card_def cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   611
apply (subst Least_equality)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   612
apply (rule eqpoll_refl) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   613
apply (rule Ord_nat) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   614
apply (erule ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   615
apply (simp_all add: eqpoll_iff lt_not_lepoll ltI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   616
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   617
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   618
(*Allows showing that |i| is a limit cardinal*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   619
lemma nat_le_cardinal: "nat le i ==> nat le |i|"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   620
apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   621
apply (erule cardinal_mono)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   622
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   623
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   624
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   625
(*** Towards Cardinal Arithmetic ***)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   626
(** Congruence laws for successor, cardinal addition and multiplication **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   627
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   628
(*Congruence law for  cons  under equipollence*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   629
lemma cons_lepoll_cong: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   630
    "[| A \<lesssim> B;  b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   631
apply (unfold lepoll_def, safe)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   632
apply (rule_tac x = "lam y: cons (a,A) . if y=a then b else f`y" in exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   633
apply (rule_tac d = "%z. if z:B then converse (f) `z else a" in lam_injective)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   634
apply (safe elim!: consE') 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   635
   apply simp_all
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   636
apply (blast intro: inj_is_fun [THEN apply_type])+ 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   637
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   638
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   639
lemma cons_eqpoll_cong:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   640
     "[| A \<approx> B;  a ~: A;  b ~: B |] ==> cons(a,A) \<approx> cons(b,B)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   641
by (simp add: eqpoll_iff cons_lepoll_cong)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   642
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   643
lemma cons_lepoll_cons_iff:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   644
     "[| a ~: A;  b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B)  <->  A \<lesssim> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   645
by (blast intro: cons_lepoll_cong cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   646
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   647
lemma cons_eqpoll_cons_iff:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   648
     "[| a ~: A;  b ~: B |] ==> cons(a,A) \<approx> cons(b,B)  <->  A \<approx> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   649
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   650
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   651
lemma singleton_eqpoll_1: "{a} \<approx> 1"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   652
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   653
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   654
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   655
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   656
lemma cardinal_singleton: "|{a}| = 1"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   657
apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   658
apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   659
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   660
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   661
lemma not_0_is_lepoll_1: "A ~= 0 ==> 1 \<lesssim> A"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   662
apply (erule not_emptyE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   663
apply (rule_tac a = "cons (x, A-{x}) " in subst)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   664
apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A-{x})" in subst)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   665
prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   666
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   667
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   668
(*Congruence law for  succ  under equipollence*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   669
lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   670
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   671
apply (simp add: cons_eqpoll_cong mem_not_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   672
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   673
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   674
(*Congruence law for + under equipollence*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   675
lemma sum_eqpoll_cong: "[| A \<approx> C;  B \<approx> D |] ==> A+B \<approx> C+D"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   676
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   677
apply (blast intro!: sum_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   678
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   679
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   680
(*Congruence law for * under equipollence*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   681
lemma prod_eqpoll_cong: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   682
    "[| A \<approx> C;  B \<approx> D |] ==> A*B \<approx> C*D"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   683
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   684
apply (blast intro!: prod_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   685
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   686
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   687
lemma inj_disjoint_eqpoll: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   688
    "[| f: inj(A,B);  A Int B = 0 |] ==> A Un (B - range(f)) \<approx> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   689
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   690
apply (rule exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   691
apply (rule_tac c = "%x. if x:A then f`x else x" 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   692
            and d = "%y. if y: range (f) then converse (f) `y else y" 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   693
       in lam_bijective)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   694
apply (blast intro!: if_type inj_is_fun [THEN apply_type])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   695
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   696
apply (safe elim!: UnE') 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   697
   apply (simp_all add: inj_is_fun [THEN apply_rangeI])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   698
apply (blast intro: inj_converse_fun [THEN apply_type])+ 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   699
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   700
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   701
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   702
(*** Lemmas by Krzysztof Grabczewski.  New proofs using cons_lepoll_cons.
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   703
     Could easily generalise from succ to cons. ***)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   704
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   705
(*If A has at most n+1 elements and a:A then A-{a} has at most n.*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   706
lemma Diff_sing_lepoll: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   707
      "[| a:A;  A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   708
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   709
apply (rule cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   710
apply (rule_tac [3] mem_not_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   711
apply (erule cons_Diff [THEN ssubst], safe)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   712
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   713
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   714
(*If A has at least n+1 elements then A-{a} has at least n.*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   715
lemma lepoll_Diff_sing: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   716
      "[| succ(n) \<lesssim> A |] ==> n \<lesssim> A - {a}"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   717
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   718
apply (rule cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   719
apply (rule_tac [2] mem_not_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   720
prefer 2 apply blast
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   721
apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   722
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   723
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   724
lemma Diff_sing_eqpoll: "[| a:A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   725
by (blast intro!: eqpollI 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   726
          elim!: eqpollE 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   727
          intro: Diff_sing_lepoll lepoll_Diff_sing)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   728
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   729
lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a:A |] ==> A = {a}"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   730
apply (frule Diff_sing_lepoll, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   731
apply (drule lepoll_0_is_0)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   732
apply (blast elim: equalityE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   733
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   734
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   735
lemma Un_lepoll_sum: "A Un B \<lesssim> A+B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   736
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   737
apply (rule_tac x = "lam x: A Un B. if x:A then Inl (x) else Inr (x) " in exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   738
apply (rule_tac d = "%z. snd (z) " in lam_injective)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   739
apply force 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   740
apply (simp add: Inl_def Inr_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   741
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   742
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   743
lemma well_ord_Un:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   744
     "[| well_ord(X,R); well_ord(Y,S) |] ==> EX T. well_ord(X Un Y, T)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   745
by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]], 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   746
    assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   747
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   748
(*Krzysztof Grabczewski*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   749
lemma disj_Un_eqpoll_sum: "A Int B = 0 ==> A Un B \<approx> A + B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   750
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   751
apply (rule_tac x = "lam a:A Un B. if a:A then Inl (a) else Inr (a) " in exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   752
apply (rule_tac d = "%z. case (%x. x, %x. x, z) " in lam_bijective)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   753
apply auto
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   754
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   755
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   756
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   757
subsection {*Finite and infinite sets*}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   758
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   759
lemma Finite_0 [simp]: "Finite(0)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   760
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   761
apply (blast intro!: eqpoll_refl nat_0I)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   762
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   763
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   764
lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n;  n:nat |] ==> Finite(A)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   765
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   766
apply (erule rev_mp)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   767
apply (erule nat_induct)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   768
apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   769
apply (blast dest!: lepoll_succ_disj)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   770
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   771
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   772
lemma lesspoll_nat_is_Finite: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   773
     "A \<prec> nat ==> Finite(A)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   774
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   775
apply (blast dest: ltD lesspoll_cardinal_lt 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   776
                   lesspoll_imp_eqpoll [THEN eqpoll_sym])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   777
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   778
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   779
lemma lepoll_Finite: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   780
     "[| Y \<lesssim> X;  Finite(X) |] ==> Finite(Y)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   781
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   782
apply (blast elim!: eqpollE
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   783
             intro: lepoll_trans [THEN lepoll_nat_imp_Finite
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   784
                                       [unfolded Finite_def]])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   785
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   786
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   787
lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   788
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   789
lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   790
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   791
lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   792
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   793
apply (rule_tac P =  "y:x" in case_split_thm)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   794
apply (simp add: cons_absorb)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   795
apply (erule bexE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   796
apply (rule bexI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   797
apply (erule_tac [2] nat_succI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   798
apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   799
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   800
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   801
lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   802
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   803
apply (erule Finite_cons)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   804
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   805
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13244
diff changeset
   806
lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   807
by (blast intro: Finite_cons subset_Finite)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   808
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13244
diff changeset
   809
lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   810
by (simp add: succ_def)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   811
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   812
lemma nat_le_infinite_Ord: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   813
      "[| Ord(i);  ~ Finite(i) |] ==> nat le i"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   814
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   815
apply (erule Ord_nat [THEN [2] Ord_linear2])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   816
prefer 2 apply assumption
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   817
apply (blast intro!: eqpoll_refl elim!: ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   818
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   819
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   820
lemma Finite_imp_well_ord: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   821
    "Finite(A) ==> EX r. well_ord(A,r)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   822
apply (unfold Finite_def eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   823
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   824
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   825
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   826
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   827
by (fast dest!: lepoll_0_is_0)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   828
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   829
lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   830
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   831
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   832
lemma Finite_Fin_lemma [rule_format]:
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   833
     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   834
apply (induct_tac n)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   835
apply (rule allI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   836
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   837
apply (rule allI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   838
apply (rule impI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   839
apply (erule conjE)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   840
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   841
apply (frule Diff_sing_eqpoll, assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   842
apply (erule allE)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   843
apply (erule impE, fast)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   844
apply (drule subsetD, assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   845
apply (drule Fin.consI, assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   846
apply (simp add: cons_Diff)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   847
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   848
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   849
lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   850
by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   851
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   852
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   853
apply (unfold Finite_def) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   854
apply (blast intro: eqpoll_trans eqpoll_sym) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   855
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   856
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   857
lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   858
apply (induct_tac n)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   859
apply (simp add: eqpoll_0_iff, clarify)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   860
apply (subgoal_tac "EX u. u:A")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   861
apply (erule exE)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   862
apply (rule Diff_sing_eqpoll [THEN revcut_rl])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   863
prefer 2 apply assumption
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   864
apply assumption
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   865
apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   866
apply (rule Fin.consI, blast)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   867
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   868
(*Now for the lemma assumed above*)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   869
apply (unfold eqpoll_def)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   870
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   871
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   872
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   873
lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   874
apply (unfold Finite_def)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   875
apply (blast intro: Fin_lemma)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   876
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   877
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   878
lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   879
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   880
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   881
lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   882
by (blast intro: Finite_into_Fin Fin_into_Finite)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   883
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   884
lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   885
by (blast intro!: Fin_into_Finite Fin_UnI 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   886
          dest!: Finite_into_Fin
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   887
          intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   888
                 Un_upper2 [THEN Fin_mono, THEN subsetD])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   889
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   890
lemma Finite_Union: "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   891
apply (simp add: Finite_Fin_iff)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   892
apply (rule Fin_UnionI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   893
apply (erule Fin_induct, simp)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   894
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   895
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   896
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   897
(* Induction principle for Finite(A), by Sidi Ehmety *)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   898
lemma Finite_induct:
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   899
"[| Finite(A); P(0);
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   900
    !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   901
 ==> P(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   902
apply (erule Finite_into_Fin [THEN Fin_induct]) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   903
apply (blast intro: Fin_into_Finite)+
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   904
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   905
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   906
(*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   907
lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   908
apply (unfold Finite_def)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   909
apply (case_tac "a:A")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   910
apply (subgoal_tac [2] "A-{a}=A", auto)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   911
apply (rule_tac x = "succ (n) " in bexI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   912
apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   913
apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   914
apply (auto dest: mem_irrefl)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   915
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   916
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   917
(*Sidi Ehmety.  And the contrapositive of this says
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   918
   [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   919
lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   920
apply (erule Finite_induct, auto)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   921
apply (case_tac "x:A")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   922
 apply (subgoal_tac [2] "A-cons (x, B) = A - B")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   923
apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   924
apply (rotate_tac -1, simp)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   925
apply (drule Diff_sing_Finite, auto)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   926
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   927
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   928
lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   929
by (erule Finite_induct, simp_all)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   930
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   931
lemma Finite_RepFun_iff_lemma [rule_format]:
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   932
     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   933
      ==> \<forall>A. x = RepFun(A,f) --> Finite(A)" 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   934
apply (erule Finite_induct)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   935
 apply clarify 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   936
 apply (case_tac "A=0", simp)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   937
 apply (blast del: allE, clarify) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   938
apply (subgoal_tac "\<exists>z\<in>A. x = f(z)") 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   939
 prefer 2 apply (blast del: allE elim: equalityE, clarify) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   940
apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   941
 apply (blast intro: Diff_sing_Finite) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   942
apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)") 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   943
apply (rule equalityI) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   944
 apply (blast intro: elim: equalityE) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   945
apply (blast intro: elim: equalityCE) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   946
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   947
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   948
text{*I don't know why, but if the premise is expressed using meta-connectives
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   949
then  the simplifier cannot prove it automatically in conditional rewriting.*}
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   950
lemma Finite_RepFun_iff:
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   951
     "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   952
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f]) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   953
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   954
lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   955
apply (erule Finite_induct) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   956
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   957
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   958
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   959
lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   960
apply (subgoal_tac "Finite({{x} . x \<in> A})")
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   961
 apply (simp add: Finite_RepFun_iff ) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   962
apply (blast intro: subset_Finite) 
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   963
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   964
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   965
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   966
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   967
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   968
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   969
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   970
(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   971
  set is well-ordered.  Proofs simplified by lcp. *)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   972
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   973
lemma nat_wf_on_converse_Memrel: "n:nat ==> wf[n](converse(Memrel(n)))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   974
apply (erule nat_induct)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   975
apply (blast intro: wf_onI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   976
apply (rule wf_onI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   977
apply (simp add: wf_on_def wf_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   978
apply (rule_tac P =  "x:Z" in case_split_thm)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   979
 txt{*x:Z case*}
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   980
 apply (drule_tac x = x in bspec, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   981
 apply (blast elim: mem_irrefl mem_asym)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   982
txt{*other case*} 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   983
apply (drule_tac x = "Z" in spec, blast) 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   984
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   985
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   986
lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   987
apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   988
apply (unfold well_ord_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   989
apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   990
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   991
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   992
lemma well_ord_converse:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   993
     "[|well_ord(A,r);      
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   994
        well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   995
      ==> well_ord(A,converse(r))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   996
apply (rule well_ord_Int_iff [THEN iffD1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   997
apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   998
apply (simp add: rvimage_converse converse_Int converse_prod
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   999
                 ordertype_ord_iso [THEN ord_iso_rvimage_eq])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1000
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1001
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1002
lemma ordertype_eq_n:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1003
     "[| well_ord(A,r);  A \<approx> n;  n:nat |] ==> ordertype(A,r)=n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1004
apply (rule Ord_ordertype [THEN Ord_nat_eqpoll_iff, THEN iffD1], assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1005
apply (rule eqpoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1006
 prefer 2 apply assumption
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1007
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1008
apply (blast intro!: ordermap_bij [THEN bij_converse_bij])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1009
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1010
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1011
lemma Finite_well_ord_converse: 
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1012
    "[| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1013
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1014
apply (rule well_ord_converse, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1015
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1016
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1017
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1018
lemma nat_into_Finite: "n:nat ==> Finite(n)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1019
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1020
apply (fast intro!: eqpoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1021
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1022
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1023
ML
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1024
{*
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1025
val Least_def = thm "Least_def";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1026
val eqpoll_def = thm "eqpoll_def";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1027
val lepoll_def = thm "lepoll_def";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1028
val lesspoll_def = thm "lesspoll_def";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1029
val cardinal_def = thm "cardinal_def";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1030
val Finite_def = thm "Finite_def";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1031
val Card_def = thm "Card_def";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1032
val eq_imp_not_mem = thm "eq_imp_not_mem";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1033
val decomp_bnd_mono = thm "decomp_bnd_mono";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1034
val Banach_last_equation = thm "Banach_last_equation";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1035
val decomposition = thm "decomposition";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1036
val schroeder_bernstein = thm "schroeder_bernstein";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1037
val bij_imp_eqpoll = thm "bij_imp_eqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1038
val eqpoll_refl = thm "eqpoll_refl";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1039
val eqpoll_sym = thm "eqpoll_sym";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1040
val eqpoll_trans = thm "eqpoll_trans";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1041
val subset_imp_lepoll = thm "subset_imp_lepoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1042
val lepoll_refl = thm "lepoll_refl";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1043
val le_imp_lepoll = thm "le_imp_lepoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1044
val eqpoll_imp_lepoll = thm "eqpoll_imp_lepoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1045
val lepoll_trans = thm "lepoll_trans";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1046
val eqpollI = thm "eqpollI";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1047
val eqpollE = thm "eqpollE";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1048
val eqpoll_iff = thm "eqpoll_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1049
val lepoll_0_is_0 = thm "lepoll_0_is_0";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1050
val empty_lepollI = thm "empty_lepollI";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1051
val lepoll_0_iff = thm "lepoll_0_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1052
val Un_lepoll_Un = thm "Un_lepoll_Un";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1053
val eqpoll_0_is_0 = thm "eqpoll_0_is_0";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1054
val eqpoll_0_iff = thm "eqpoll_0_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1055
val eqpoll_disjoint_Un = thm "eqpoll_disjoint_Un";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1056
val lesspoll_not_refl = thm "lesspoll_not_refl";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1057
val lesspoll_irrefl = thm "lesspoll_irrefl";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1058
val lesspoll_imp_lepoll = thm "lesspoll_imp_lepoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1059
val lepoll_well_ord = thm "lepoll_well_ord";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1060
val lepoll_iff_leqpoll = thm "lepoll_iff_leqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1061
val inj_not_surj_succ = thm "inj_not_surj_succ";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1062
val lesspoll_trans = thm "lesspoll_trans";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1063
val lesspoll_trans1 = thm "lesspoll_trans1";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1064
val lesspoll_trans2 = thm "lesspoll_trans2";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1065
val Least_equality = thm "Least_equality";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1066
val LeastI = thm "LeastI";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1067
val Least_le = thm "Least_le";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1068
val less_LeastE = thm "less_LeastE";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1069
val LeastI2 = thm "LeastI2";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1070
val Least_0 = thm "Least_0";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1071
val Ord_Least = thm "Ord_Least";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1072
val Least_cong = thm "Least_cong";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1073
val cardinal_cong = thm "cardinal_cong";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1074
val well_ord_cardinal_eqpoll = thm "well_ord_cardinal_eqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1075
val Ord_cardinal_eqpoll = thm "Ord_cardinal_eqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1076
val well_ord_cardinal_eqE = thm "well_ord_cardinal_eqE";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1077
val well_ord_cardinal_eqpoll_iff = thm "well_ord_cardinal_eqpoll_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1078
val Ord_cardinal_le = thm "Ord_cardinal_le";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1079
val Card_cardinal_eq = thm "Card_cardinal_eq";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1080
val CardI = thm "CardI";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1081
val Card_is_Ord = thm "Card_is_Ord";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1082
val Card_cardinal_le = thm "Card_cardinal_le";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1083
val Ord_cardinal = thm "Ord_cardinal";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1084
val Card_iff_initial = thm "Card_iff_initial";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1085
val lt_Card_imp_lesspoll = thm "lt_Card_imp_lesspoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1086
val Card_0 = thm "Card_0";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1087
val Card_Un = thm "Card_Un";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1088
val Card_cardinal = thm "Card_cardinal";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1089
val cardinal_mono = thm "cardinal_mono";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1090
val cardinal_lt_imp_lt = thm "cardinal_lt_imp_lt";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1091
val Card_lt_imp_lt = thm "Card_lt_imp_lt";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1092
val Card_lt_iff = thm "Card_lt_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1093
val Card_le_iff = thm "Card_le_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1094
val well_ord_lepoll_imp_Card_le = thm "well_ord_lepoll_imp_Card_le";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1095
val lepoll_cardinal_le = thm "lepoll_cardinal_le";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1096
val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1097
val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1098
val cons_lepoll_consD = thm "cons_lepoll_consD";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1099
val cons_eqpoll_consD = thm "cons_eqpoll_consD";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1100
val succ_lepoll_succD = thm "succ_lepoll_succD";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1101
val nat_lepoll_imp_le = thm "nat_lepoll_imp_le";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1102
val nat_eqpoll_iff = thm "nat_eqpoll_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1103
val nat_into_Card = thm "nat_into_Card";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1104
val cardinal_0 = thm "cardinal_0";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1105
val cardinal_1 = thm "cardinal_1";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1106
val succ_lepoll_natE = thm "succ_lepoll_natE";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1107
val n_lesspoll_nat = thm "n_lesspoll_nat";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1108
val nat_lepoll_imp_ex_eqpoll_n = thm "nat_lepoll_imp_ex_eqpoll_n";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1109
val lepoll_imp_lesspoll_succ = thm "lepoll_imp_lesspoll_succ";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1110
val lesspoll_succ_imp_lepoll = thm "lesspoll_succ_imp_lepoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1111
val lesspoll_succ_iff = thm "lesspoll_succ_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1112
val lepoll_succ_disj = thm "lepoll_succ_disj";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1113
val lesspoll_cardinal_lt = thm "lesspoll_cardinal_lt";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1114
val lt_not_lepoll = thm "lt_not_lepoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1115
val Ord_nat_eqpoll_iff = thm "Ord_nat_eqpoll_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1116
val Card_nat = thm "Card_nat";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1117
val nat_le_cardinal = thm "nat_le_cardinal";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1118
val cons_lepoll_cong = thm "cons_lepoll_cong";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1119
val cons_eqpoll_cong = thm "cons_eqpoll_cong";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1120
val cons_lepoll_cons_iff = thm "cons_lepoll_cons_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1121
val cons_eqpoll_cons_iff = thm "cons_eqpoll_cons_iff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1122
val singleton_eqpoll_1 = thm "singleton_eqpoll_1";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1123
val cardinal_singleton = thm "cardinal_singleton";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1124
val not_0_is_lepoll_1 = thm "not_0_is_lepoll_1";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1125
val succ_eqpoll_cong = thm "succ_eqpoll_cong";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1126
val sum_eqpoll_cong = thm "sum_eqpoll_cong";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1127
val prod_eqpoll_cong = thm "prod_eqpoll_cong";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1128
val inj_disjoint_eqpoll = thm "inj_disjoint_eqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1129
val Diff_sing_lepoll = thm "Diff_sing_lepoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1130
val lepoll_Diff_sing = thm "lepoll_Diff_sing";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1131
val Diff_sing_eqpoll = thm "Diff_sing_eqpoll";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1132
val lepoll_1_is_sing = thm "lepoll_1_is_sing";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1133
val Un_lepoll_sum = thm "Un_lepoll_sum";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1134
val well_ord_Un = thm "well_ord_Un";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1135
val disj_Un_eqpoll_sum = thm "disj_Un_eqpoll_sum";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1136
val Finite_0 = thm "Finite_0";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1137
val lepoll_nat_imp_Finite = thm "lepoll_nat_imp_Finite";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1138
val lesspoll_nat_is_Finite = thm "lesspoll_nat_is_Finite";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1139
val lepoll_Finite = thm "lepoll_Finite";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1140
val subset_Finite = thm "subset_Finite";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1141
val Finite_Diff = thm "Finite_Diff";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1142
val Finite_cons = thm "Finite_cons";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1143
val Finite_succ = thm "Finite_succ";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1144
val nat_le_infinite_Ord = thm "nat_le_infinite_Ord";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1145
val Finite_imp_well_ord = thm "Finite_imp_well_ord";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1146
val nat_wf_on_converse_Memrel = thm "nat_wf_on_converse_Memrel";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1147
val nat_well_ord_converse_Memrel = thm "nat_well_ord_converse_Memrel";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1148
val well_ord_converse = thm "well_ord_converse";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1149
val ordertype_eq_n = thm "ordertype_eq_n";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1150
val Finite_well_ord_converse = thm "Finite_well_ord_converse";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1151
val nat_into_Finite = thm "nat_into_Finite";
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1152
*}
9683
f87c8c449018 added some xsymbols, and tidied
paulson
parents: 1478
diff changeset
  1153
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
  1154
end