src/ZF/AC/WO2_AC16.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 46954 d8b3412cdb99
child 59788 6f7b6adac439
permissions -rw-r--r--
eliminated spurious semicolons;
paulson@12776
     1
(*  Title:      ZF/AC/WO2_AC16.thy
paulson@12776
     2
    Author:     Krzysztof Grabczewski
paulson@12776
     3
wenzelm@32960
     4
The proof of WO2 ==> AC16(k #+ m, k)
paulson@12776
     5
  
wenzelm@32960
     6
The main part of the proof is the inductive reasoning concerning
wenzelm@32960
     7
properties of constructed family T_gamma.
wenzelm@32960
     8
The proof deals with three cases for ordinals: 0, succ and limit ordinal.
wenzelm@32960
     9
The first instance is trivial, the third not difficult, but the second
wenzelm@32960
    10
is very complicated requiring many lemmas.
wenzelm@32960
    11
We also need to prove that at any stage gamma the set 
paulson@46822
    12
(s - \<Union>(...) - k_gamma)   (Rubin & Rubin page 15)
wenzelm@32960
    13
contains m distinct elements (in fact is equipollent to s)
paulson@12776
    14
*)
paulson@12776
    15
haftmann@16417
    16
theory WO2_AC16 imports AC_Equiv AC16_lemmas Cardinal_aux begin
paulson@12776
    17
paulson@12776
    18
(**** A recursive definition used in the proof of WO2 ==> AC16 ****)
paulson@12776
    19
wenzelm@24893
    20
definition
wenzelm@24893
    21
  recfunAC16 :: "[i,i,i,i] => i"  where
paulson@12776
    22
    "recfunAC16(f,h,i,a) == 
paulson@12776
    23
         transrec2(i, 0, 
paulson@12776
    24
              %g r. if (\<exists>y \<in> r. h`g \<subseteq> y) then r
paulson@46822
    25
                    else r \<union> {f`(LEAST i. h`g \<subseteq> f`i & 
paulson@46822
    26
                         (\<forall>b<a. (h`b \<subseteq> f`i \<longrightarrow> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})"
paulson@12776
    27
paulson@12776
    28
(* ********************************************************************** *)
paulson@12776
    29
(* Basic properties of recfunAC16                                         *)
paulson@12776
    30
(* ********************************************************************** *)
paulson@12776
    31
paulson@12776
    32
lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0"
paulson@12820
    33
by (simp add: recfunAC16_def)
paulson@12776
    34
paulson@12776
    35
lemma recfunAC16_succ: 
paulson@12776
    36
     "recfunAC16(f,h,succ(i),a) =   
paulson@12776
    37
      (if (\<exists>y \<in> recfunAC16(f,h,i,a). h ` i \<subseteq> y) then recfunAC16(f,h,i,a)  
paulson@46822
    38
       else recfunAC16(f,h,i,a) \<union>  
paulson@12776
    39
            {f ` (LEAST j. h ` i \<subseteq> f ` j &   
paulson@12776
    40
             (\<forall>b<a. (h`b \<subseteq> f`j   
paulson@46822
    41
              \<longrightarrow> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
paulson@12820
    42
apply (simp add: recfunAC16_def)
paulson@12776
    43
done
paulson@12776
    44
paulson@12776
    45
lemma recfunAC16_Limit: "Limit(i)   
paulson@12776
    46
        ==> recfunAC16(f,h,i,a) = (\<Union>j<i. recfunAC16(f,h,j,a))"
paulson@13339
    47
by (simp add: recfunAC16_def transrec2_Limit)
paulson@12776
    48
paulson@12776
    49
(* ********************************************************************** *)
paulson@12776
    50
(* Monotonicity of transrec2                                              *)
paulson@12776
    51
(* ********************************************************************** *)
paulson@12776
    52
paulson@12776
    53
lemma transrec2_mono_lemma [rule_format]:
paulson@12776
    54
     "[| !!g r. r \<subseteq> B(g,r);  Ord(i) |]   
paulson@46822
    55
      ==> j<i \<longrightarrow> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
paulson@12820
    56
apply (erule trans_induct)
paulson@12820
    57
apply (rule Ord_cases, assumption+, fast)
paulson@12776
    58
apply (simp (no_asm_simp))
paulson@12820
    59
apply (blast elim!: leE) 
paulson@12820
    60
apply (simp add: transrec2_Limit) 
paulson@12776
    61
apply (blast intro: OUN_I ltI Ord_in_Ord [THEN le_refl]
paulson@12776
    62
             elim!: Limit_has_succ [THEN ltE])
paulson@12776
    63
done
paulson@12776
    64
paulson@12776
    65
lemma transrec2_mono:
paulson@12776
    66
     "[| !!g r. r \<subseteq> B(g,r); j\<le>i |] 
paulson@12776
    67
      ==> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
paulson@12820
    68
apply (erule leE)
paulson@12776
    69
apply (rule transrec2_mono_lemma)
paulson@12820
    70
apply (auto intro: lt_Ord2 ) 
paulson@12776
    71
done
paulson@12776
    72
paulson@12776
    73
(* ********************************************************************** *)
paulson@12776
    74
(* Monotonicity of recfunAC16                                             *)
paulson@12776
    75
(* ********************************************************************** *)
paulson@12776
    76
paulson@12776
    77
lemma recfunAC16_mono: 
paulson@12776
    78
       "i\<le>j ==> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)"
paulson@12776
    79
apply (unfold recfunAC16_def)
paulson@12820
    80
apply (rule transrec2_mono, auto) 
paulson@12776
    81
done
paulson@12776
    82
paulson@12776
    83
(* ********************************************************************** *)
paulson@12776
    84
(* case of limit ordinal                                                  *)
paulson@12776
    85
(* ********************************************************************** *)
paulson@12776
    86
paulson@12776
    87
paulson@12776
    88
lemma lemma3_1:
paulson@46822
    89
    "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
paulson@46822
    90
        \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); j\<le>i; i<x; z<a;
paulson@12776
    91
        V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]   
paulson@12776
    92
     ==> V = W"
paulson@12776
    93
apply (erule asm_rl allE impE)+
paulson@12820
    94
apply (drule subsetD, assumption, blast) 
paulson@12776
    95
done
paulson@12776
    96
paulson@12776
    97
paulson@12776
    98
lemma lemma3:
paulson@46822
    99
    "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
paulson@46822
   100
        \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); i<x; j<x; z<a;   
paulson@12776
   101
        V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]   
paulson@12776
   102
     ==> V = W"
paulson@12776
   103
apply (rule_tac j=j in Ord_linear_le [OF lt_Ord lt_Ord], assumption+)
paulson@12776
   104
apply (erule lemma3_1 [symmetric], assumption+)
paulson@12776
   105
apply (erule lemma3_1, assumption+)
paulson@12776
   106
done
paulson@12776
   107
paulson@12776
   108
lemma lemma4:
paulson@12776
   109
     "[| \<forall>y<x. F(y) \<subseteq> X &   
paulson@46822
   110
                (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>   
paulson@12776
   111
                 (\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y)); 
paulson@12776
   112
         x < a |]   
paulson@46822
   113
      ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) \<longrightarrow>   
paulson@12776
   114
                       (\<exists>! Y. Y \<in> F(y) & h(z) \<subseteq> Y)"
paulson@12776
   115
apply (intro oallI impI)
paulson@12820
   116
apply (drule ospec, assumption, clarify)
paulson@12776
   117
apply (blast elim!: oallE ) 
paulson@12776
   118
done
paulson@12776
   119
paulson@12776
   120
lemma lemma5:
paulson@12776
   121
     "[| \<forall>y<x. F(y) \<subseteq> X &   
paulson@46822
   122
               (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>   
paulson@12776
   123
                (\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y));  
paulson@46822
   124
         x < a; Limit(x); \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |]   
paulson@12776
   125
      ==> (\<Union>x<x. F(x)) \<subseteq> X &   
paulson@12776
   126
          (\<forall>xa<a. xa < x | (\<exists>x \<in> \<Union>x<x. F(x). h(xa) \<subseteq> x)   
paulson@46822
   127
                \<longrightarrow> (\<exists>! Y. Y \<in> (\<Union>x<x. F(x)) & h(xa) \<subseteq> Y))"
paulson@12776
   128
apply (rule conjI)
paulson@12776
   129
apply (rule subsetI)
paulson@12776
   130
apply (erule OUN_E)
paulson@12820
   131
apply (drule ospec, assumption, fast)
paulson@12776
   132
apply (drule lemma4, assumption)
paulson@12776
   133
apply (rule oallI)
paulson@12776
   134
apply (rule impI)
paulson@12776
   135
apply (erule disjE)
paulson@12776
   136
apply (frule ospec, erule Limit_has_succ, assumption) 
paulson@13339
   137
apply (drule_tac A = a and x = xa in ospec, assumption)
paulson@12776
   138
apply (erule impE, rule le_refl [THEN disjI1], erule lt_Ord) 
paulson@12776
   139
apply (blast intro: lemma3 Limit_has_succ) 
paulson@12776
   140
apply (blast intro: lemma3) 
paulson@12776
   141
done
paulson@12776
   142
paulson@12776
   143
(* ********************************************************************** *)
paulson@12776
   144
(* case of successor ordinal                                              *)
paulson@12776
   145
(* ********************************************************************** *)
paulson@12776
   146
paulson@12776
   147
(*
paulson@12776
   148
  First quite complicated proof of the fact used in the recursive construction
paulson@12776
   149
  of the family T_gamma (WO2 ==> AC16(k #+ m, k)) - the fact that at any stage
paulson@46822
   150
  gamma the set (s - \<Union>(...) - k_gamma) is equipollent to s
paulson@12776
   151
  (Rubin & Rubin page 15).
paulson@12776
   152
*)
paulson@12776
   153
paulson@12776
   154
(* ********************************************************************** *)
paulson@12776
   155
(* dbl_Diff_eqpoll_Card                                                   *)
paulson@12776
   156
(* ********************************************************************** *)
paulson@12776
   157
paulson@12776
   158
paulson@12776
   159
lemma dbl_Diff_eqpoll_Card:
paulson@12776
   160
      "[| A\<approx>a; Card(a); ~Finite(a); B\<prec>a; C\<prec>a |] ==> A - B - C\<approx>a"
paulson@12776
   161
by (blast intro: Diff_lesspoll_eqpoll_Card) 
paulson@12776
   162
paulson@12776
   163
(* ********************************************************************** *)
paulson@12776
   164
(* Case of finite ordinals                                                *)
paulson@12776
   165
(* ********************************************************************** *)
paulson@12776
   166
paulson@12776
   167
paulson@12776
   168
lemma Finite_lesspoll_infinite_Ord: 
paulson@12776
   169
      "[| Finite(X); ~Finite(a); Ord(a) |] ==> X\<prec>a"
paulson@12776
   170
apply (unfold lesspoll_def)
paulson@12776
   171
apply (rule conjI)
paulson@12776
   172
apply (drule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption)
paulson@12776
   173
apply (unfold Finite_def)
paulson@12776
   174
apply (blast intro: leI [THEN le_imp_subset, THEN subset_imp_lepoll]
paulson@12776
   175
                    ltI eqpoll_imp_lepoll lepoll_trans) 
paulson@12776
   176
apply (blast intro: eqpoll_sym [THEN eqpoll_trans])
paulson@12776
   177
done
paulson@12776
   178
paulson@12776
   179
lemma Union_lesspoll:
paulson@46954
   180
     "[| \<forall>x \<in> X. x \<lesssim> n & x \<subseteq> T; well_ord(T, R); X \<lesssim> b;   
paulson@12776
   181
         b<a; ~Finite(a); Card(a); n \<in> nat |]   
paulson@46822
   182
      ==> \<Union>(X)\<prec>a"
paulson@12776
   183
apply (case_tac "Finite (X)")
paulson@12776
   184
apply (blast intro: Card_is_Ord Finite_lesspoll_infinite_Ord 
paulson@12776
   185
                    lepoll_nat_imp_Finite Finite_Union)
paulson@12776
   186
apply (drule lepoll_imp_ex_le_eqpoll) 
paulson@12776
   187
apply (erule lt_Ord) 
paulson@12776
   188
apply (elim exE conjE)
paulson@12776
   189
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
paulson@12776
   190
apply (erule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1],
paulson@12776
   191
                         THEN exE])
paulson@12776
   192
apply (frule bij_is_surj [THEN surj_image_eq])
paulson@12776
   193
apply (drule image_fun [OF bij_is_fun subset_refl])
paulson@12776
   194
apply (drule sym [THEN trans], assumption)
paulson@12776
   195
apply (blast intro: lt_Ord UN_lepoll lt_Card_imp_lesspoll
paulson@12776
   196
                    lt_trans1 lesspoll_trans1)
paulson@12776
   197
done
paulson@12776
   198
paulson@12776
   199
(* ********************************************************************** *)
paulson@12776
   200
(* recfunAC16_lepoll_index                                                *)
paulson@12776
   201
(* ********************************************************************** *)
paulson@12776
   202
paulson@46822
   203
lemma Un_sing_eq_cons: "A \<union> {a} = cons(a, A)"
paulson@12776
   204
by fast
paulson@12776
   205
paulson@46954
   206
lemma Un_lepoll_succ: "A \<lesssim> B ==> A \<union> {a} \<lesssim> succ(B)"
paulson@12776
   207
apply (simp add: Un_sing_eq_cons succ_def)
paulson@12776
   208
apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
paulson@12776
   209
done
paulson@12776
   210
paulson@12776
   211
lemma Diff_UN_succ_empty: "Ord(a) ==> F(a) - (\<Union>b<succ(a). F(b)) = 0"
paulson@12776
   212
by (fast intro!: le_refl)
paulson@12776
   213
paulson@46822
   214
lemma Diff_UN_succ_subset: "Ord(a) ==> F(a) \<union> X - (\<Union>b<succ(a). F(b)) \<subseteq> X"
paulson@12776
   215
by blast
paulson@12776
   216
paulson@12776
   217
lemma recfunAC16_Diff_lepoll_1:
paulson@12776
   218
     "Ord(x) 
paulson@46954
   219
      ==> recfunAC16(f, g, x, a) - (\<Union>i<x. recfunAC16(f, g, i, a)) \<lesssim> 1"
paulson@12776
   220
apply (erule Ord_cases)
paulson@12776
   221
  apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll])
paulson@12776
   222
(*Limit case*)
paulson@12776
   223
prefer 2 apply (simp add: recfunAC16_Limit Diff_cancel 
paulson@12776
   224
                          empty_subsetI [THEN subset_imp_lepoll])
paulson@12776
   225
(*succ case*)
paulson@12776
   226
apply (simp add: recfunAC16_succ
paulson@12776
   227
                 Diff_UN_succ_empty [of _ "%j. recfunAC16(f,g,j,a)"]
paulson@12776
   228
                 empty_subsetI [THEN subset_imp_lepoll])
paulson@12776
   229
apply (best intro: Diff_UN_succ_subset [THEN subset_imp_lepoll]
paulson@12776
   230
                   singleton_eqpoll_1 [THEN eqpoll_imp_lepoll] lepoll_trans)
paulson@12776
   231
done
paulson@12776
   232
paulson@12776
   233
lemma in_Least_Diff:
paulson@12776
   234
     "[| z \<in> F(x); Ord(x) |]   
paulson@12776
   235
      ==> z \<in> F(LEAST i. z \<in> F(i)) - (\<Union>j<(LEAST i. z \<in> F(i)). F(j))"
paulson@13339
   236
by (fast elim: less_LeastE elim!: LeastI)
paulson@12776
   237
paulson@12776
   238
lemma Least_eq_imp_ex:
paulson@12776
   239
     "[| (LEAST i. w \<in> F(i)) = (LEAST i. z \<in> F(i));   
paulson@12776
   240
         w \<in> (\<Union>i<a. F(i)); z \<in> (\<Union>i<a. F(i)) |]   
paulson@12776
   241
      ==> \<exists>b<a. w \<in> (F(b) - (\<Union>c<b. F(c))) & z \<in> (F(b) - (\<Union>c<b. F(c)))"
paulson@12776
   242
apply (elim OUN_E)
paulson@12776
   243
apply (drule in_Least_Diff, erule lt_Ord) 
paulson@12776
   244
apply (frule in_Least_Diff, erule lt_Ord) 
paulson@12776
   245
apply (rule oexI, force) 
paulson@12776
   246
apply (blast intro: lt_Ord Least_le [THEN lt_trans1]) 
paulson@12776
   247
done
paulson@12776
   248
paulson@12776
   249
paulson@46954
   250
lemma two_in_lepoll_1: "[| A \<lesssim> 1; a \<in> A; b \<in> A |] ==> a=b"
paulson@12776
   251
by (fast dest!: lepoll_1_is_sing)
paulson@12776
   252
paulson@12776
   253
paulson@12776
   254
lemma UN_lepoll_index:
paulson@46954
   255
     "[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) \<lesssim> 1; Limit(a) |]   
paulson@46954
   256
      ==> (\<Union>x<a. F(x)) \<lesssim> a"
paulson@12776
   257
apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
paulson@12776
   258
apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). LEAST i. z \<in> F (i) " in exI)
paulson@12776
   259
apply (unfold inj_def)
paulson@12776
   260
apply (rule CollectI)
paulson@12776
   261
apply (rule lam_type)
paulson@12776
   262
apply (erule OUN_E)
paulson@12776
   263
apply (erule Least_in_Ord)
paulson@12776
   264
apply (erule ltD)
paulson@12776
   265
apply (erule lt_Ord2)
paulson@12776
   266
apply (intro ballI)
paulson@12776
   267
apply (simp (no_asm_simp))
paulson@12776
   268
apply (rule impI)
paulson@12776
   269
apply (drule Least_eq_imp_ex, assumption+)
paulson@12776
   270
apply (fast elim!: two_in_lepoll_1)
paulson@12776
   271
done
paulson@12776
   272
paulson@12776
   273
paulson@46954
   274
lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) \<lesssim> y"
paulson@12776
   275
apply (erule trans_induct3)
paulson@12776
   276
(*0 case*)
paulson@12776
   277
apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl)
paulson@12776
   278
(*succ case*)
paulson@12776
   279
apply (simp (no_asm_simp) add: recfunAC16_succ)
paulson@12776
   280
apply (blast dest!: succI1 [THEN rev_bspec] 
paulson@12776
   281
             intro: subset_succI [THEN subset_imp_lepoll] Un_lepoll_succ  
paulson@12776
   282
                    lepoll_trans)
paulson@12776
   283
apply (simp (no_asm_simp) add: recfunAC16_Limit)
paulson@12776
   284
apply (blast intro: lt_Ord [THEN recfunAC16_Diff_lepoll_1] UN_lepoll_index)
paulson@12776
   285
done
paulson@12776
   286
lcp@1196
   287
paulson@12776
   288
lemma Union_recfunAC16_lesspoll:
paulson@12776
   289
     "[| recfunAC16(f,g,y,a) \<subseteq> {X \<in> Pow(A). X\<approx>n};   
paulson@12776
   290
         A\<approx>a;  y<a;  ~Finite(a);  Card(a);  n \<in> nat |]   
paulson@46822
   291
      ==> \<Union>(recfunAC16(f,g,y,a))\<prec>a"
paulson@12776
   292
apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE])
paulson@13339
   293
apply (rule_tac T=A in Union_lesspoll, simp_all)
paulson@12776
   294
apply (blast intro!: eqpoll_imp_lepoll)
paulson@12776
   295
apply (blast intro: bij_is_inj Card_is_Ord [THEN well_ord_Memrel]
paulson@12776
   296
                    well_ord_rvimage)
paulson@12776
   297
apply (erule lt_Ord [THEN recfunAC16_lepoll_index])
paulson@12776
   298
done
paulson@12776
   299
paulson@12776
   300
lemma dbl_Diff_eqpoll:
paulson@12776
   301
     "[| recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)};   
wenzelm@32960
   302
         Card(a); ~ Finite(a); A\<approx>a;   
wenzelm@32960
   303
         k \<in> nat;  y<a;   
wenzelm@32960
   304
         h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)}) |]   
paulson@46822
   305
      ==> A - \<Union>(recfunAC16(f, h, y, a)) - h`y\<approx>a"
paulson@12776
   306
apply (rule dbl_Diff_eqpoll_Card, simp_all)
paulson@12776
   307
apply (simp add: Union_recfunAC16_lesspoll)
paulson@12776
   308
apply (rule Finite_lesspoll_infinite_Ord) 
paulson@12776
   309
apply (rule Finite_def [THEN def_imp_iff, THEN iffD2]) 
paulson@12820
   310
apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)  
paulson@12776
   311
apply (blast intro: Card_is_Ord) 
wenzelm@58860
   312
done
paulson@12776
   313
paulson@12776
   314
(* back to the proof *)
paulson@12776
   315
paulson@12776
   316
lemmas disj_Un_eqpoll_nat_sum = 
paulson@12776
   317
    eqpoll_trans [THEN eqpoll_trans, 
wenzelm@58860
   318
                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum]
paulson@12776
   319
paulson@12776
   320
paulson@12776
   321
lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;   
paulson@12776
   322
        h \<in> bij(a, {x \<in> Pow(A) . x\<approx>k}); i<a; k \<in> nat; m \<in> nat |]   
paulson@46822
   323
        ==> h ` i \<union> x \<in> {x \<in> Pow(A) . x\<approx>k #+ m}"
paulson@12776
   324
by (blast intro: disj_Un_eqpoll_nat_sum
paulson@12776
   325
          dest:  ltD bij_is_fun [THEN apply_type])
paulson@12776
   326
paulson@12776
   327
paulson@12776
   328
(* ********************************************************************** *)
paulson@12776
   329
(* Lemmas simplifying assumptions                                         *)
paulson@12776
   330
(* ********************************************************************** *)
paulson@12776
   331
paulson@12776
   332
lemma lemma6:
paulson@46822
   333
     "[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) \<longrightarrow> Q(x,y)); succ(j)<a |]
paulson@46822
   334
      ==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j))"
paulson@13339
   335
by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]) 
paulson@12776
   336
paulson@12776
   337
paulson@12776
   338
lemma lemma7:
paulson@46822
   339
     "[| \<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j);  succ(j)<a |]   
paulson@46822
   340
      ==> P(j,j) \<longrightarrow> (\<forall>x<a. x\<le>j | P(x,j) \<longrightarrow> Q(x,j))"
paulson@12776
   341
by (fast elim!: leE)
paulson@12776
   342
paulson@12776
   343
(* ********************************************************************** *)
paulson@12776
   344
(* Lemmas needed to prove ex_next_set, which means that for any successor *)
paulson@12776
   345
(* ordinal there is a set satisfying certain properties                   *)
paulson@12776
   346
(* ********************************************************************** *)
paulson@12776
   347
paulson@12776
   348
lemma ex_subset_eqpoll:
paulson@12776
   349
     "[| A\<approx>a; ~ Finite(a); Ord(a); m \<in> nat |] ==> \<exists>X \<in> Pow(A). X\<approx>m"
paulson@12776
   350
apply (rule lepoll_imp_eqpoll_subset [of m A, THEN exE]) 
paulson@12776
   351
 apply (rule lepoll_trans, rule leI [THEN le_imp_lepoll])
paulson@12776
   352
  apply (blast intro: lt_trans2 [OF ltI nat_le_infinite_Ord] Ord_nat)
paulson@12776
   353
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 
paulson@12776
   354
apply (fast elim!: eqpoll_sym)
paulson@12776
   355
done
paulson@12776
   356
paulson@46822
   357
lemma subset_Un_disjoint: "[| A \<subseteq> B \<union> C; A \<inter> C = 0 |] ==> A \<subseteq> B"
paulson@12776
   358
by blast
paulson@12776
   359
paulson@12776
   360
paulson@12776
   361
lemma Int_empty:
paulson@46822
   362
     "[| X \<in> Pow(A - \<Union>(B) -C); T \<in> B; F \<subseteq> T |] ==> F \<inter> X = 0"
paulson@12776
   363
by blast
paulson@12776
   364
paulson@12776
   365
paulson@12776
   366
(* ********************************************************************** *)
paulson@12776
   367
(* equipollent subset (and finite) is the whole set                       *)
paulson@12776
   368
(* ********************************************************************** *)
paulson@12776
   369
paulson@12776
   370
paulson@12776
   371
lemma subset_imp_eq_lemma:
paulson@46954
   372
     "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m \<lesssim> A & B \<lesssim> m \<longrightarrow> A=B"
paulson@12776
   373
apply (induct_tac "m")
paulson@12776
   374
apply (fast dest!: lepoll_0_is_0)
paulson@12776
   375
apply (intro allI impI)
paulson@12776
   376
apply (elim conjE)
paulson@12776
   377
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], assumption)
paulson@12776
   378
apply (frule subsetD [THEN Diff_sing_lepoll], assumption+)
paulson@12776
   379
apply (frule lepoll_Diff_sing)
paulson@12776
   380
apply (erule allE impE)+
paulson@12776
   381
apply (rule conjI)
paulson@12776
   382
prefer 2 apply fast
paulson@12776
   383
apply fast
paulson@12776
   384
apply (blast elim: equalityE) 
paulson@12776
   385
done
paulson@12776
   386
paulson@12776
   387
paulson@46954
   388
lemma subset_imp_eq: "[| A \<subseteq> B; m \<lesssim> A; B \<lesssim> m; m \<in> nat |] ==> A=B"
paulson@12776
   389
by (blast dest!: subset_imp_eq_lemma)
paulson@12776
   390
paulson@12776
   391
paulson@12776
   392
lemma bij_imp_arg_eq:
paulson@12776
   393
     "[| f \<in> bij(a, {Y \<in> X. Y\<approx>succ(k)}); k \<in> nat; f`b \<subseteq> f`y; b<a; y<a |] 
paulson@12776
   394
      ==> b=y"
paulson@12776
   395
apply (drule subset_imp_eq)
paulson@12776
   396
apply (erule_tac [3] nat_succI)
paulson@12776
   397
apply (unfold bij_def inj_def)
paulson@12776
   398
apply (blast intro: eqpoll_sym eqpoll_imp_lepoll
paulson@12776
   399
             dest:  ltD apply_type)+
paulson@12776
   400
done
paulson@12776
   401
paulson@12776
   402
paulson@12776
   403
lemma ex_next_set:
paulson@12776
   404
     "[| recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)};   
paulson@12776
   405
         Card(a); ~ Finite(a); A\<approx>a;   
paulson@12776
   406
         k \<in> nat; m \<in> nat; y<a;   
paulson@12776
   407
         h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)});   
paulson@12776
   408
         ~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |]   
paulson@12776
   409
      ==> \<exists>X \<in> {Y \<in> Pow(A). Y\<approx>succ(k #+ m)}. h`y \<subseteq> X &   
paulson@46822
   410
                (\<forall>b<a. h`b \<subseteq> X \<longrightarrow>   
paulson@12776
   411
                (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))"
paulson@12776
   412
apply (erule_tac m1=m in dbl_Diff_eqpoll [THEN ex_subset_eqpoll, THEN bexE], 
paulson@12776
   413
       assumption+)
paulson@12776
   414
apply (erule Card_is_Ord, assumption)
paulson@12776
   415
apply (frule Un_in_Collect, (erule asm_rl nat_succI)+) 
paulson@12776
   416
apply (erule CollectE)
paulson@12776
   417
apply (rule rev_bexI, simp)
paulson@12776
   418
apply (rule conjI, blast) 
paulson@12776
   419
apply (intro ballI impI oallI notI)
paulson@12776
   420
apply (drule subset_Un_disjoint, rule Int_empty, assumption+)
paulson@12776
   421
apply (blast dest: bij_imp_arg_eq) 
paulson@12776
   422
done
paulson@12776
   423
paulson@12776
   424
(* ********************************************************************** *)
paulson@12776
   425
(* Lemma ex_next_Ord states that for any successor                        *)
paulson@12776
   426
(* ordinal there is a number of the set satisfying certain properties     *)
paulson@12776
   427
(* ********************************************************************** *)
paulson@12776
   428
paulson@12776
   429
lemma ex_next_Ord:
paulson@12776
   430
     "[| recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)};   
wenzelm@32960
   431
         Card(a); ~ Finite(a); A\<approx>a;   
wenzelm@32960
   432
         k \<in> nat; m \<in> nat; y<a;   
wenzelm@32960
   433
         h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)});   
wenzelm@32960
   434
         f \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k #+ m)});   
wenzelm@32960
   435
         ~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |]   
paulson@12776
   436
      ==> \<exists>c<a. h`y \<subseteq> f`c &   
paulson@46822
   437
                (\<forall>b<a. h`b \<subseteq> f`c \<longrightarrow>   
wenzelm@32960
   438
                (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))"
paulson@12776
   439
apply (drule ex_next_set, assumption+)
paulson@12776
   440
apply (erule bexE)
paulson@15481
   441
apply (rule_tac x="converse(f)`X" in oexI)
paulson@15481
   442
apply (simp add: right_inverse_bij)
paulson@12776
   443
apply (blast intro: bij_converse_bij bij_is_fun [THEN apply_type] ltI
paulson@12776
   444
                    Card_is_Ord)
paulson@12776
   445
done
paulson@12776
   446
paulson@12776
   447
paulson@12776
   448
(* ********************************************************************** *)
paulson@12776
   449
(* Lemma simplifying assumptions                                          *)
paulson@12776
   450
(* ********************************************************************** *)
paulson@12776
   451
paulson@12776
   452
lemma lemma8:
paulson@12776
   453
     "[| \<forall>x<a. x<j | (\<exists>xa \<in> F(j). P(x, xa))   
paulson@46822
   454
         \<longrightarrow> (\<exists>! Y. Y \<in> F(j) & P(x, Y)); F(j) \<subseteq> X;   
paulson@46822
   455
         L \<in> X; P(j, L) & (\<forall>x<a. P(x, L) \<longrightarrow> (\<forall>xa \<in> F(j). ~P(x, xa))) |]   
paulson@46822
   456
      ==> F(j) \<union> {L} \<subseteq> X &   
paulson@46822
   457
          (\<forall>x<a. x\<le>j | (\<exists>xa \<in> (F(j) \<union> {L}). P(x, xa)) \<longrightarrow>   
paulson@46822
   458
                 (\<exists>! Y. Y \<in> (F(j) \<union> {L}) & P(x, Y)))"
paulson@12776
   459
apply (rule conjI)
paulson@12776
   460
apply (fast intro!: singleton_subsetI)
paulson@12776
   461
apply (rule oallI)
paulson@12776
   462
apply (blast elim!: leE oallE)
paulson@12776
   463
done
paulson@12776
   464
paulson@12776
   465
(* ********************************************************************** *)
paulson@12776
   466
(* The main part of the proof: inductive proof of the property of T_gamma *)
paulson@12776
   467
(* lemma main_induct                                                      *)
paulson@12776
   468
(* ********************************************************************** *)
paulson@12776
   469
paulson@12776
   470
lemma main_induct:
paulson@12776
   471
     "[| b < a; f \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k #+ m)});   
paulson@12776
   472
         h \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k)});   
paulson@12776
   473
         ~Finite(a); Card(a); A\<approx>a; k \<in> nat; m \<in> nat |]   
paulson@12776
   474
      ==> recfunAC16(f, h, b, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)} &   
paulson@46822
   475
          (\<forall>x<a. x < b | (\<exists>Y \<in> recfunAC16(f, h, b, a). h ` x \<subseteq> Y) \<longrightarrow>   
paulson@12776
   476
          (\<exists>! Y. Y \<in> recfunAC16(f, h, b, a) & h ` x \<subseteq> Y))"
paulson@12776
   477
apply (erule lt_induct)
paulson@12776
   478
apply (frule lt_Ord)
paulson@12776
   479
apply (erule Ord_cases)
paulson@12776
   480
(* case 0 *)
paulson@12776
   481
apply (simp add: recfunAC16_0)
paulson@12776
   482
(* case Limit *)
paulson@12776
   483
prefer 2  apply (simp add: recfunAC16_Limit)
paulson@12776
   484
          apply (rule lemma5, assumption+)
paulson@12776
   485
          apply (blast dest!: recfunAC16_mono)
paulson@12776
   486
(* case succ *)
paulson@12776
   487
apply clarify 
paulson@12776
   488
apply (erule lemma6 [THEN conjE], assumption)
paulson@12776
   489
apply (simp (no_asm_simp) split del: split_if add: recfunAC16_succ)
paulson@12776
   490
apply (rule conjI [THEN split_if [THEN iffD2]])
paulson@12776
   491
 apply (simp, erule lemma7, assumption)
paulson@12776
   492
apply (rule impI)
paulson@12776
   493
apply (rule ex_next_Ord [THEN oexE], 
paulson@12776
   494
       assumption+, rule le_refl [THEN lt_trans], assumption+) 
paulson@12776
   495
apply (erule lemma8, assumption)
paulson@12776
   496
 apply (rule bij_is_fun [THEN apply_type], assumption)
paulson@12776
   497
 apply (erule Least_le [THEN lt_trans2, THEN ltD])
paulson@12776
   498
  apply (erule lt_Ord) 
paulson@12776
   499
 apply (erule succ_leI)
paulson@12776
   500
apply (erule LeastI) 
paulson@12776
   501
apply (erule lt_Ord) 
paulson@12776
   502
done
paulson@12776
   503
paulson@12776
   504
(* ********************************************************************** *)
paulson@12776
   505
(* Lemma to simplify the inductive proof                                  *)
paulson@12776
   506
(*   - the desired property is a consequence of the inductive assumption  *)
paulson@12776
   507
(* ********************************************************************** *)
paulson@12776
   508
paulson@12776
   509
lemma lemma_simp_induct:
paulson@46822
   510
     "[| \<forall>b. b<a \<longrightarrow> F(b) \<subseteq> S & (\<forall>x<a. (x<b | (\<exists>Y \<in> F(b). f`x \<subseteq> Y))  
paulson@46822
   511
                                   \<longrightarrow> (\<exists>! Y. Y \<in> F(b) & f`x \<subseteq> Y));
paulson@12776
   512
         f \<in> a->f``(a); Limit(a); 
paulson@46822
   513
         \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |]   
paulson@12776
   514
        ==> (\<Union>j<a. F(j)) \<subseteq> S &   
paulson@12776
   515
            (\<forall>x \<in> f``a. \<exists>! Y. Y \<in> (\<Union>j<a. F(j)) & x \<subseteq> Y)"
paulson@12776
   516
apply (rule conjI)
paulson@12776
   517
apply (rule subsetI)
paulson@12776
   518
apply (erule OUN_E, blast) 
paulson@12776
   519
apply (rule ballI)
paulson@12776
   520
apply (erule imageE)
paulson@12776
   521
apply (drule ltI, erule Limit_is_Ord) 
paulson@12776
   522
apply (drule Limit_has_succ, assumption) 
paulson@12820
   523
apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption)
paulson@12776
   524
apply (erule conjE)
paulson@12776
   525
apply (drule ospec) 
paulson@12776
   526
(** LEVEL 10 **)
paulson@12776
   527
apply (erule leI [THEN succ_leE])
paulson@12776
   528
apply (erule impE)
paulson@12776
   529
apply (fast elim!: leI [THEN succ_leE, THEN lt_Ord, THEN le_refl])
paulson@12776
   530
apply (drule apply_equality, assumption) 
paulson@12776
   531
apply (elim conjE ex1E)
paulson@12776
   532
(** LEVEL 15 **)
paulson@12776
   533
apply (rule ex1I, blast) 
paulson@12776
   534
apply (elim conjE OUN_E)
paulson@12776
   535
apply (erule_tac i="succ(xa)" and j=aa 
paulson@12776
   536
       in Ord_linear_le [OF lt_Ord lt_Ord], assumption)
paulson@12776
   537
prefer 2 
paulson@12776
   538
apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
paulson@12776
   539
(** LEVEL 20 **)
paulson@13339
   540
apply (drule_tac x1=aa in spec [THEN mp], assumption)
paulson@12776
   541
apply (frule succ_leE)
paulson@12776
   542
apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
paulson@12776
   543
done
paulson@12776
   544
paulson@12776
   545
(* ********************************************************************** *)
paulson@12776
   546
(* The target theorem                                                     *)
paulson@12776
   547
(* ********************************************************************** *)
paulson@12776
   548
paulson@12776
   549
theorem WO2_AC16: "[| WO2; 0<m; k \<in> nat; m \<in> nat |] ==> AC16(k #+ m,k)"
paulson@12776
   550
apply (unfold AC16_def)
paulson@12776
   551
apply (rule allI)
paulson@12776
   552
apply (rule impI)
paulson@12776
   553
apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
paulson@12820
   554
apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp, simp) 
paulson@12776
   555
apply (frule WO2_imp_ex_Card)
paulson@12776
   556
apply (elim exE conjE)
paulson@12776
   557
apply (drule eqpoll_trans [THEN eqpoll_sym, 
paulson@12776
   558
                           THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
paulson@12776
   559
       assumption)
paulson@12776
   560
apply (drule eqpoll_trans [THEN eqpoll_sym, 
paulson@12776
   561
                           THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]], 
paulson@12776
   562
       assumption+)
paulson@12776
   563
apply (elim exE)
paulson@12776
   564
apply (rename_tac h)
paulson@12776
   565
apply (rule_tac x = "\<Union>j<a. recfunAC16 (h,f,j,a) " in exI)
paulson@12776
   566
apply (rule_tac P="%z. ?Y & (\<forall>x \<in> z. ?Z (x))" 
paulson@12776
   567
       in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
paulson@12776
   568
apply (rule lemma_simp_induct)
paulson@12776
   569
apply (blast del: conjI notI
wenzelm@32960
   570
             intro!: main_induct eqpoll_imp_lepoll [THEN lepoll_infinite] ) 
paulson@12776
   571
apply (blast intro: bij_is_fun [THEN surj_image, THEN surj_is_fun])
paulson@12776
   572
apply (erule eqpoll_imp_lepoll [THEN lepoll_infinite, 
paulson@12776
   573
                                THEN infinite_Card_is_InfCard, 
paulson@12776
   574
                                THEN InfCard_is_Limit], 
paulson@12776
   575
       assumption+)
paulson@12776
   576
apply (blast dest!: recfunAC16_mono)
paulson@12776
   577
done
paulson@12776
   578
paulson@12776
   579
end