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