src/ZF/AC/AC16_WO4.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 46822 95f1e700b712
child 59788 6f7b6adac439
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*  Title:      ZF/AC/AC16_WO4.thy
     2     Author:     Krzysztof Grabczewski
     3 
     4 The proof of AC16(n, k) ==> WO4(n-k)
     5 
     6 Tidied (using locales) by LCP
     7 *)
     8 
     9 theory AC16_WO4
    10 imports AC16_lemmas
    11 begin
    12 
    13 (* ********************************************************************** *)
    14 (* The case of finite set                                                 *)
    15 (* ********************************************************************** *)
    16 
    17 lemma lemma1:
    18      "[| Finite(A); 0<m; m \<in> nat |] 
    19       ==> \<exists>a f. Ord(a) & domain(f) = a &   
    20                 (\<Union>b<a. f`b) = A & (\<forall>b<a. f`b \<lesssim> m)"
    21 apply (unfold Finite_def)
    22 apply (erule bexE)
    23 apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
    24 apply (erule exE)
    25 apply (rule_tac x = n in exI)
    26 apply (rule_tac x = "\<lambda>i \<in> n. {f`i}" in exI)
    27 apply (simp add: ltD bij_def surj_def)
    28 apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun] 
    29                singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
    30                     nat_1_lepoll_iff [THEN iffD2]
    31           elim!: apply_type ltE)
    32 done
    33 
    34 (* ********************************************************************** *)
    35 (* The case of infinite set                                               *)
    36 (* ********************************************************************** *)
    37 
    38 (* well_ord(x,r) ==> well_ord({{y,z}. y \<in> x}, Something(x,z))  **)
    39 lemmas well_ord_paired = paired_bij [THEN bij_is_inj, THEN well_ord_rvimage]
    40 
    41 lemma lepoll_trans1: "[| A \<lesssim> B; ~ A \<lesssim> C |] ==> ~ B \<lesssim> C"
    42 by (blast intro: lepoll_trans)
    43 
    44 (* ********************************************************************** *)
    45 (* There exists a well ordered set y such that ...                        *)
    46 (* ********************************************************************** *)
    47 
    48 lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]
    49 
    50 lemma lemma2: "\<exists>y R. well_ord(y,R) & x \<inter> y = 0 & ~y \<lesssim> z & ~Finite(y)"
    51 apply (rule_tac x = "{{a,x}. a \<in> nat \<union> Hartog (z) }" in exI)
    52 apply (rule well_ord_Un [OF Ord_nat [THEN well_ord_Memrel] 
    53                          Ord_Hartog [THEN well_ord_Memrel], THEN exE])
    54 apply (blast intro!: Ord_Hartog well_ord_Memrel well_ord_paired
    55                       lepoll_trans1 [OF _ not_Hartog_lepoll_self]
    56                       lepoll_trans [OF subset_imp_lepoll lepoll_paired]
    57        elim!: nat_not_Finite [THEN notE]
    58        elim: mem_asym 
    59        dest!: Un_upper1 [THEN subset_imp_lepoll, THEN lepoll_Finite]
    60               lepoll_paired [THEN lepoll_Finite])
    61 done
    62 
    63 lemma infinite_Un: "~Finite(B) ==> ~Finite(A \<union> B)"
    64 by (blast intro: subset_Finite)
    65 
    66 (* ********************************************************************** *)
    67 (* There is a v \<in> s(u) such that k \<lesssim> x \<inter> y (in our case succ(k))    *)
    68 (* The idea of the proof is the following \<in>                               *)
    69 (* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y   *)
    70 (* Thence y is less than or equipollent to {v \<in> Pow(x). v \<approx> n#-k}      *)
    71 (*   We have obtained this result in two steps \<in>                          *)
    72 (*   1. y is less than or equipollent to {v \<in> s(u). a \<subseteq> v}                  *)
    73 (*      where a is certain k-2 element subset of y                        *)
    74 (*   2. {v \<in> s(u). a \<subseteq> v} is less than or equipollent                       *)
    75 (*      to {v \<in> Pow(x). v \<approx> n-k}                                       *)
    76 (* ********************************************************************** *)
    77 
    78 (*Proof simplified by LCP*)
    79 lemma succ_not_lepoll_lemma:
    80      "[| ~(\<exists>x \<in> A. f`x=y); f \<in> inj(A, B); y \<in> B |]   
    81       ==> (\<lambda>a \<in> succ(A). if(a=A, y, f`a)) \<in> inj(succ(A), B)"
    82 apply (rule_tac d = "%z. if (z=y, A, converse (f) `z) " in lam_injective)
    83 apply (force simp add: inj_is_fun [THEN apply_type])
    84 (*this preliminary simplification prevents looping somehow*)
    85 apply (simp (no_asm_simp))
    86 apply force
    87 done
    88 
    89 lemma succ_not_lepoll_imp_eqpoll: "[| ~A \<approx> B; A \<lesssim> B |] ==> succ(A) \<lesssim> B"
    90 apply (unfold lepoll_def eqpoll_def bij_def surj_def)
    91 apply (fast elim!: succ_not_lepoll_lemma inj_is_fun)
    92 done
    93 
    94 
    95 (* ********************************************************************** *)
    96 (* There is a k-2 element subset of y                                     *)
    97 (* ********************************************************************** *)
    98 
    99 lemmas ordertype_eqpoll =
   100        ordermap_bij [THEN exI [THEN eqpoll_def [THEN def_imp_iff, THEN iffD2]]]
   101 
   102 lemma cons_cons_subset:
   103      "[| a \<subseteq> y; b \<in> y-a; u \<in> x |] ==> cons(b, cons(u, a)) \<in> Pow(x \<union> y)"
   104 by fast
   105 
   106 lemma cons_cons_eqpoll:
   107      "[| a \<approx> k; a \<subseteq> y; b \<in> y-a; u \<in> x; x \<inter> y = 0 |]    
   108       ==> cons(b, cons(u, a)) \<approx> succ(succ(k))"
   109 by (fast intro!: cons_eqpoll_succ)
   110 
   111 lemma set_eq_cons:
   112      "[| succ(k) \<approx> A; k \<approx> B; B \<subseteq> A; a \<in> A-B; k \<in> nat |] ==> A = cons(a, B)"
   113 apply (rule equalityI)
   114 prefer 2 apply fast
   115 apply (rule Diff_eq_0_iff [THEN iffD1])
   116 apply (rule equals0I)
   117 apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
   118 apply (drule eqpoll_sym [THEN cons_eqpoll_succ], fast)
   119 apply (drule cons_eqpoll_succ, fast)
   120 apply (fast elim!: lepoll_trans [THEN lepoll_trans, THEN succ_lepoll_natE,
   121          OF eqpoll_sym [THEN eqpoll_imp_lepoll] subset_imp_lepoll])
   122 done
   123 
   124 lemma cons_eqE: "[| cons(x,a) = cons(y,a); x \<notin> a |] ==> x = y "
   125 by (fast elim!: equalityE)
   126 
   127 lemma eq_imp_Int_eq: "A = B ==> A \<inter> C = B \<inter> C"
   128 by blast
   129 
   130 (* ********************************************************************** *)
   131 (* some arithmetic                                                        *)
   132 (* ********************************************************************** *)
   133 
   134 lemma eqpoll_sum_imp_Diff_lepoll_lemma [rule_format]:
   135      "[| k \<in> nat; m \<in> nat |] 
   136       ==> \<forall>A B. A \<approx> k #+ m & k \<lesssim> B & B \<subseteq> A \<longrightarrow> A-B \<lesssim> m"
   137 apply (induct_tac "k")
   138 apply (simp add: add_0)
   139 apply (blast intro: eqpoll_imp_lepoll lepoll_trans
   140                     Diff_subset [THEN subset_imp_lepoll])
   141 apply (intro allI impI)
   142 apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], fast)
   143 apply (erule_tac x = "A - {xa}" in allE)
   144 apply (erule_tac x = "B - {xa}" in allE)
   145 apply (erule impE)
   146 apply (simp add: add_succ)
   147 apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing) 
   148 apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
   149 apply blast 
   150 done
   151 
   152 lemma eqpoll_sum_imp_Diff_lepoll:
   153      "[| A \<approx> succ(k #+ m); B \<subseteq> A; succ(k) \<lesssim> B;  k \<in> nat; m \<in> nat |]   
   154       ==> A-B \<lesssim> m"
   155 apply (simp only: add_succ [symmetric]) 
   156 apply (blast intro: eqpoll_sum_imp_Diff_lepoll_lemma) 
   157 done
   158 
   159 (* ********************************************************************** *)
   160 (* similar properties for \<approx>                                          *)
   161 (* ********************************************************************** *)
   162 
   163 lemma eqpoll_sum_imp_Diff_eqpoll_lemma [rule_format]:
   164      "[| k \<in> nat; m \<in> nat |] 
   165       ==> \<forall>A B. A \<approx> k #+ m & k \<approx> B & B \<subseteq> A \<longrightarrow> A-B \<approx> m"
   166 apply (induct_tac "k")
   167 apply (force dest!: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_0_is_0])
   168 apply (intro allI impI)
   169 apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE])
   170 apply (fast elim!: eqpoll_imp_lepoll)
   171 apply (erule_tac x = "A - {xa}" in allE)
   172 apply (erule_tac x = "B - {xa}" in allE)
   173 apply (erule impE)
   174 apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll)
   175 apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
   176 apply blast 
   177 done
   178 
   179 lemma eqpoll_sum_imp_Diff_eqpoll:
   180      "[| A \<approx> succ(k #+ m); B \<subseteq> A; succ(k) \<approx> B; k \<in> nat; m \<in> nat |]   
   181       ==> A-B \<approx> m"
   182 apply (simp only: add_succ [symmetric]) 
   183 apply (blast intro: eqpoll_sum_imp_Diff_eqpoll_lemma) 
   184 done
   185 
   186 
   187 (* ********************************************************************** *)
   188 (* LL can be well ordered                                                 *)
   189 (* ********************************************************************** *)
   190 
   191 lemma subsets_lepoll_0_eq_unit: "{x \<in> Pow(X). x \<lesssim> 0} = {0}"
   192 by (fast dest!: lepoll_0_is_0 intro!: lepoll_refl)
   193 
   194 lemma subsets_lepoll_succ:
   195      "n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> succ(n)} =   
   196                   {z \<in> Pow(y). z \<lesssim> n} \<union> {z \<in> Pow(y). z \<approx> succ(n)}"
   197 by (blast intro: leI le_imp_lepoll nat_into_Ord 
   198                     lepoll_trans eqpoll_imp_lepoll
   199           dest!: lepoll_succ_disj)
   200 
   201 lemma Int_empty:
   202      "n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> n} \<inter> {z \<in> Pow(y). z \<approx> succ(n)} = 0"
   203 by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
   204                  succ_lepoll_natE)
   205 
   206 locale AC16 =
   207   fixes x and y and k and l and m and t_n and R and MM and LL and GG and s 
   208   defines k_def:     "k   == succ(l)"
   209       and MM_def:    "MM  == {v \<in> t_n. succ(k) \<lesssim> v \<inter> y}"
   210       and LL_def:    "LL  == {v \<inter> y. v \<in> MM}"
   211       and GG_def:    "GG  == \<lambda>v \<in> LL. (THE w. w \<in> MM & v \<subseteq> w) - v"
   212       and s_def:     "s(u) == {v \<in> t_n. u \<in> v & k \<lesssim> v \<inter> y}"
   213   assumes all_ex:    "\<forall>z \<in> {z \<in> Pow(x \<union> y) . z \<approx> succ(k)}.
   214                        \<exists>! w. w \<in> t_n & z \<subseteq> w "
   215     and disjoint[iff]:  "x \<inter> y = 0"
   216     and "includes":  "t_n \<subseteq> {v \<in> Pow(x \<union> y). v \<approx> succ(k #+ m)}"
   217     and WO_R[iff]:      "well_ord(y,R)"
   218     and lnat[iff]:      "l \<in> nat"
   219     and mnat[iff]:      "m \<in> nat"
   220     and mpos[iff]:      "0<m"
   221     and Infinite[iff]:  "~ Finite(y)"
   222     and noLepoll:  "~ y \<lesssim> {v \<in> Pow(x). v \<approx> m}"
   223 
   224 lemma (in AC16) knat [iff]: "k \<in> nat"
   225 by (simp add: k_def)
   226 
   227 
   228 (* ********************************************************************** *)
   229 (*   1. y is less than or equipollent to {v \<in> s(u). a \<subseteq> v}                *)
   230 (*      where a is certain k-2 element subset of y                        *)
   231 (* ********************************************************************** *)
   232 
   233 lemma (in AC16) Diff_Finite_eqpoll: "[| l \<approx> a; a \<subseteq> y |] ==> y - a \<approx> y"
   234 apply (insert WO_R Infinite lnat)
   235 apply (rule eqpoll_trans) 
   236 apply (rule Diff_lesspoll_eqpoll_Card) 
   237 apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])
   238 apply (blast intro: lesspoll_trans1
   239             intro!: Card_cardinal  
   240                     Card_cardinal [THEN Card_is_Ord, THEN nat_le_infinite_Ord,
   241                                    THEN le_imp_lepoll] 
   242             dest: well_ord_cardinal_eqpoll 
   243                    eqpoll_sym  eqpoll_imp_lepoll
   244                    n_lesspoll_nat [THEN lesspoll_trans2]
   245                    well_ord_cardinal_eqpoll [THEN eqpoll_sym, 
   246                           THEN eqpoll_imp_lepoll, THEN lepoll_infinite])+
   247 done
   248 
   249 
   250 lemma (in AC16) s_subset: "s(u) \<subseteq> t_n"
   251 by (unfold s_def, blast)
   252 
   253 lemma (in AC16) sI: 
   254       "[| w \<in> t_n; cons(b,cons(u,a)) \<subseteq> w; a \<subseteq> y; b \<in> y-a; l \<approx> a |] 
   255        ==> w \<in> s(u)"
   256 apply (unfold s_def succ_def k_def)
   257 apply (blast intro!: eqpoll_imp_lepoll [THEN cons_lepoll_cong]
   258              intro: subset_imp_lepoll lepoll_trans)
   259 done
   260 
   261 lemma (in AC16) in_s_imp_u_in: "v \<in> s(u) ==> u \<in> v"
   262 by (unfold s_def, blast)
   263 
   264 
   265 lemma (in AC16) ex1_superset_a:
   266      "[| l \<approx> a;  a \<subseteq> y;  b \<in> y - a;  u \<in> x |]   
   267       ==> \<exists>! c. c \<in> s(u) & a \<subseteq> c & b \<in> c"
   268 apply (rule all_ex [simplified k_def, THEN ballE])
   269  apply (erule ex1E)
   270  apply (rule_tac a = w in ex1I, blast intro: sI)
   271  apply (blast dest: s_subset [THEN subsetD] in_s_imp_u_in)
   272 apply (blast del: PowI 
   273              intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll])
   274 done
   275 
   276 lemma (in AC16) the_eq_cons:
   277      "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;   
   278          l \<approx> a;  a \<subseteq> y;  b \<in> y - a;  u \<in> x |]    
   279       ==> (THE c. c \<in> s(u) & a \<subseteq> c & b \<in> c) \<inter> y = cons(b, a)"
   280 apply (frule ex1_superset_a [THEN theI], assumption+)
   281 apply (rule set_eq_cons)
   282 apply (fast+)
   283 done
   284 
   285 lemma (in AC16) y_lepoll_subset_s:
   286      "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;   
   287          l \<approx> a;  a \<subseteq> y;  u \<in> x |]   
   288       ==> y \<lesssim> {v \<in> s(u). a \<subseteq> v}"
   289 apply (rule Diff_Finite_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, 
   290                                 THEN lepoll_trans],  fast+)
   291 apply (rule_tac  f3 = "\<lambda>b \<in> y-a. THE c. c \<in> s (u) & a \<subseteq> c & b \<in> c" 
   292         in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
   293 apply (simp add: inj_def)
   294 apply (rule conjI)
   295 apply (rule lam_type)
   296 apply (frule ex1_superset_a [THEN theI], fast+, clarify)
   297 apply (rule cons_eqE [of _ a])
   298 apply (drule_tac A = "THE c. ?P (c) " and C = y in eq_imp_Int_eq)
   299 apply (simp_all add: the_eq_cons)
   300 done
   301 
   302 
   303 (* ********************************************************************** *)
   304 (* back to the second part                                                *)
   305 (* ********************************************************************** *)
   306 
   307 
   308 (*relies on the disjointness of x, y*)
   309 lemma (in AC16) x_imp_not_y [dest]: "a \<in> x ==> a \<notin> y"
   310 by (blast dest:  disjoint [THEN equalityD1, THEN subsetD, OF IntI])
   311 
   312 lemma (in AC16) w_Int_eq_w_Diff:
   313      "w \<subseteq> x \<union> y ==> w \<inter> (x - {u}) = w - cons(u, w \<inter> y)" 
   314 by blast
   315 
   316 lemma (in AC16) w_Int_eqpoll_m:
   317      "[| w \<in> {v \<in> s(u). a \<subseteq> v};   
   318          l \<approx> a;  u \<in> x;   
   319          \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y |] 
   320       ==> w \<inter> (x - {u}) \<approx> m"
   321 apply (erule CollectE)
   322 apply (subst w_Int_eq_w_Diff)
   323 apply (fast dest!: s_subset [THEN subsetD] 
   324                    "includes" [simplified k_def, THEN subsetD])
   325 apply (blast dest: s_subset [THEN subsetD] 
   326                    "includes" [simplified k_def, THEN subsetD] 
   327              dest: eqpoll_sym [THEN cons_eqpoll_succ, THEN eqpoll_sym] 
   328                    in_s_imp_u_in
   329             intro!: eqpoll_sum_imp_Diff_eqpoll)
   330 done
   331 
   332 
   333 (* ********************************************************************** *)
   334 (*   2. {v \<in> s(u). a \<subseteq> v} is less than or equipollent                       *)
   335 (*      to {v \<in> Pow(x). v \<approx> n-k}                                       *)
   336 (* ********************************************************************** *)
   337 
   338 lemma (in AC16) eqpoll_m_not_empty: "a \<approx> m ==> a \<noteq> 0"
   339 apply (insert mpos)
   340 apply (fast elim!: zero_lt_natE dest!: eqpoll_succ_imp_not_empty)
   341 done
   342 
   343 lemma (in AC16) cons_cons_in:
   344      "[| z \<in> xa \<inter> (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x |]   
   345       ==> \<exists>! w. w \<in> t_n & cons(z, cons(u, a)) \<subseteq> w"
   346 apply (rule all_ex [THEN bspec])
   347 apply (unfold k_def)
   348 apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym)
   349 done
   350 
   351 lemma (in AC16) subset_s_lepoll_w:
   352      "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y; a \<subseteq> y; l \<approx> a; u \<in> x |]   
   353       ==> {v \<in> s(u). a \<subseteq> v} \<lesssim> {v \<in> Pow(x). v \<approx> m}"
   354 apply (rule_tac f3 = "\<lambda>w \<in> {v \<in> s (u) . a \<subseteq> v}. w \<inter> (x - {u})" 
   355        in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
   356 apply (simp add: inj_def)
   357 apply (intro conjI lam_type CollectI)
   358   apply fast
   359  apply (blast intro: w_Int_eqpoll_m) 
   360 apply (intro ballI impI)
   361 (** LEVEL 8 **)
   362 apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE])
   363 apply (blast, assumption+)
   364 apply (drule equalityD1 [THEN subsetD], assumption)
   365 apply (frule cons_cons_in, assumption+)
   366 apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+
   367 done
   368 
   369 
   370 (* ********************************************************************** *)
   371 (* well_ord_subsets_lepoll_n                                              *)
   372 (* ********************************************************************** *)
   373 
   374 lemma (in AC16) well_ord_subsets_eqpoll_n:
   375      "n \<in> nat ==> \<exists>S. well_ord({z \<in> Pow(y) . z \<approx> succ(n)}, S)"
   376 apply (rule WO_R [THEN well_ord_infinite_subsets_eqpoll_X,
   377                   THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
   378 apply (fast intro: bij_is_inj [THEN well_ord_rvimage])+
   379 done
   380 
   381 lemma (in AC16) well_ord_subsets_lepoll_n:
   382      "n \<in> nat ==> \<exists>R. well_ord({z \<in> Pow(y). z \<lesssim> n}, R)"
   383 apply (induct_tac "n")
   384 apply (force intro!: well_ord_unit simp add: subsets_lepoll_0_eq_unit)
   385 apply (erule exE)
   386 apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption)
   387 apply (simp add: subsets_lepoll_succ)
   388 apply (drule well_ord_radd, assumption)
   389 apply (erule Int_empty [THEN disj_Un_eqpoll_sum,
   390                   THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
   391 apply (fast elim!: bij_is_inj [THEN well_ord_rvimage])
   392 done
   393 
   394 
   395 lemma (in AC16) LL_subset: "LL \<subseteq> {z \<in> Pow(y). z \<lesssim> succ(k #+ m)}"
   396 apply (unfold LL_def MM_def)
   397 apply (insert "includes")
   398 apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
   399 done
   400 
   401 lemma (in AC16) well_ord_LL: "\<exists>S. well_ord(LL,S)"
   402 apply (rule well_ord_subsets_lepoll_n [THEN exE, of "succ(k#+m)"])
   403 apply simp 
   404 apply (blast intro: well_ord_subset [OF _ LL_subset])
   405 done
   406 
   407 (* ********************************************************************** *)
   408 (* every element of LL is a contained in exactly one element of MM        *)
   409 (* ********************************************************************** *)
   410 
   411 lemma (in AC16) unique_superset_in_MM:
   412      "v \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> w"
   413 apply (unfold MM_def LL_def, safe, fast)
   414 apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
   415 apply (rule_tac x = x in all_ex [THEN ballE]) 
   416 apply (blast intro: eqpoll_sym)+
   417 done
   418 
   419 
   420 (* ********************************************************************** *)
   421 (* The function GG satisfies the conditions of WO4                        *)
   422 (* ********************************************************************** *)
   423 
   424 (* ********************************************************************** *)
   425 (* The union of appropriate values is the whole x                         *)
   426 (* ********************************************************************** *)
   427 
   428 lemma (in AC16) Int_in_LL: "w \<in> MM ==> w \<inter> y \<in> LL"
   429 by (unfold LL_def, fast)
   430 
   431 lemma (in AC16) in_LL_eq_Int: 
   432      "v \<in> LL ==> v = (THE x. x \<in> MM & v \<subseteq> x) \<inter> y"
   433 apply (unfold LL_def, clarify)
   434 apply (subst unique_superset_in_MM [THEN the_equality2])
   435 apply (auto simp add: Int_in_LL)
   436 done
   437 
   438 lemma (in AC16) unique_superset1: "a \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> a \<subseteq> x) \<in> MM"
   439 by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]) 
   440 
   441 lemma (in AC16) the_in_MM_subset:
   442      "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x \<union> y"
   443 apply (drule unique_superset1)
   444 apply (unfold MM_def)
   445 apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
   446 done
   447 
   448 lemma (in AC16) GG_subset: "v \<in> LL ==> GG ` v \<subseteq> x"
   449 apply (unfold GG_def)
   450 apply (frule the_in_MM_subset)
   451 apply (frule in_LL_eq_Int)
   452 apply (force elim: equalityE)
   453 done
   454 
   455 lemma (in AC16) nat_lepoll_ordertype: "nat \<lesssim> ordertype(y, R)"
   456 apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll]) 
   457  apply (rule Ord_ordertype [OF WO_R]) 
   458 apply (rule ordertype_eqpoll [THEN eqpoll_imp_lepoll, THEN lepoll_infinite]) 
   459  apply (rule WO_R) 
   460 apply (rule Infinite) 
   461 done
   462 
   463 lemma (in AC16) ex_subset_eqpoll_n: "n \<in> nat ==> \<exists>z. z \<subseteq> y & n \<approx> z"
   464 apply (erule nat_lepoll_imp_ex_eqpoll_n)
   465 apply (rule lepoll_trans [OF nat_lepoll_ordertype]) 
   466 apply (rule ordertype_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]) 
   467 apply (rule WO_R) 
   468 done
   469 
   470 
   471 lemma (in AC16) exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v \<inter> y"
   472 apply (rule ccontr)
   473 apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v \<inter> y")
   474 prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
   475 apply (unfold k_def)
   476 apply (insert all_ex "includes" lnat)
   477 apply (rule ex_subset_eqpoll_n [THEN exE], assumption)
   478 apply (rule noLepoll [THEN notE])
   479 apply (blast intro: lepoll_trans [OF y_lepoll_subset_s subset_s_lepoll_w])
   480 done
   481 
   482 lemma (in AC16) exists_in_MM: "u \<in> x ==> \<exists>w \<in> MM. u \<in> w"
   483 apply (erule exists_proper_in_s [THEN bexE])
   484 apply (unfold MM_def s_def, fast)
   485 done
   486 
   487 lemma (in AC16) exists_in_LL: "u \<in> x ==> \<exists>w \<in> LL. u \<in> GG`w"
   488 apply (rule exists_in_MM [THEN bexE], assumption)
   489 apply (rule bexI)
   490 apply (erule_tac [2] Int_in_LL)
   491 apply (unfold GG_def)
   492 apply (simp add: Int_in_LL)
   493 apply (subst unique_superset_in_MM [THEN the_equality2])
   494 apply (fast elim!: Int_in_LL)+
   495 done
   496 
   497 lemma (in AC16) OUN_eq_x: "well_ord(LL,S) ==>       
   498       (\<Union>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x"
   499 apply (rule equalityI)
   500 apply (rule subsetI)
   501 apply (erule OUN_E)
   502 apply (rule GG_subset [THEN subsetD])
   503 prefer 2 apply assumption
   504 apply (blast intro: ltD  ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun,
   505                                        THEN apply_type])
   506 apply (rule subsetI)
   507 apply (erule exists_in_LL [THEN bexE])
   508 apply (force intro: ltI [OF _ Ord_ordertype]
   509                     ordermap_type [THEN apply_type]
   510              simp add: ordermap_bij [THEN bij_is_inj, THEN left_inverse])
   511 done
   512 
   513 (* ********************************************************************** *)
   514 (* Every element of the family is less than or equipollent to n-k (m)     *)
   515 (* ********************************************************************** *)
   516 
   517 lemma (in AC16) in_MM_eqpoll_n: "w \<in> MM ==> w \<approx> succ(k #+ m)"
   518 apply (unfold MM_def)
   519 apply (fast dest: "includes" [THEN subsetD])
   520 done
   521 
   522 lemma (in AC16) in_LL_eqpoll_n: "w \<in> LL ==> succ(k) \<lesssim> w"
   523 by (unfold LL_def MM_def, fast)
   524 
   525 lemma (in AC16) in_LL: "w \<in> LL ==> w \<subseteq> (THE x. x \<in> MM \<and> w \<subseteq> x)"
   526 by (erule subset_trans [OF in_LL_eq_Int [THEN equalityD1] Int_lower1])
   527 
   528 lemma (in AC16) all_in_lepoll_m: 
   529       "well_ord(LL,S) ==>       
   530        \<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) \<lesssim> m"
   531 apply (unfold GG_def)
   532 apply (rule oallI)
   533 apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type])
   534 apply (insert "includes")
   535 apply (rule eqpoll_sum_imp_Diff_lepoll)
   536 apply (blast del: subsetI
   537              dest!: ltD 
   538              intro!: eqpoll_sum_imp_Diff_lepoll in_LL_eqpoll_n
   539              intro: in_LL   unique_superset1 [THEN in_MM_eqpoll_n] 
   540                     ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, 
   541                                   THEN apply_type])+
   542 done
   543 
   544 lemma (in AC16) conclusion:
   545      "\<exists>a f. Ord(a) & domain(f) = a & (\<Union>b<a. f ` b) = x & (\<forall>b<a. f ` b \<lesssim> m)"
   546 apply (rule well_ord_LL [THEN exE])
   547 apply (rename_tac S)
   548 apply (rule_tac x = "ordertype (LL,S)" in exI)
   549 apply (rule_tac x = "\<lambda>b \<in> ordertype(LL,S). 
   550                       GG ` (converse (ordermap (LL,S)) ` b)"  in exI)
   551 apply (simp add: ltD)
   552 apply (blast intro: lam_funtype [THEN domain_of_fun] 
   553                     Ord_ordertype  OUN_eq_x  all_in_lepoll_m [THEN ospec])
   554 done
   555 
   556 
   557 (* ********************************************************************** *)
   558 (* The main theorem AC16(n, k) ==> WO4(n-k)                               *)
   559 (* ********************************************************************** *)
   560 
   561 term AC16
   562 
   563 theorem AC16_WO4: 
   564      "[| AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat |] ==> WO4(m)"
   565 apply (unfold AC_Equiv.AC16_def WO4_def)
   566 apply (rule allI)
   567 apply (case_tac "Finite (A)")
   568 apply (rule lemma1, assumption+)
   569 apply (cut_tac lemma2)
   570 apply (elim exE conjE)
   571 apply (erule_tac x = "A \<union> y" in allE)
   572 apply (frule infinite_Un, drule mp, assumption)
   573 apply (erule zero_lt_natE, assumption, clarify)
   574 apply (blast intro: AC16.conclusion [OF AC16.intro])
   575 done
   576 
   577 end