src/ZF/AC/AC17_AC1.thy
author wenzelm
Fri Feb 18 16:22:27 2011 +0100 (2011-02-18)
changeset 41777 1f7cbe39d425
parent 32960 69916a850301
child 46822 95f1e700b712
permissions -rw-r--r--
more precise headers;
wenzelm@41777
     1
(*  Title:      ZF/AC/AC17_AC1.thy
paulson@12776
     2
    Author:     Krzysztof Grabczewski
paulson@12776
     3
paulson@12776
     4
The equivalence of AC0, AC1 and AC17
paulson@12776
     5
paulson@12776
     6
Also, the proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent
paulson@12776
     7
to AC0 and AC1.
paulson@12776
     8
*)
paulson@12776
     9
haftmann@27678
    10
theory AC17_AC1
haftmann@27678
    11
imports HH
haftmann@27678
    12
begin
paulson@12776
    13
paulson@12776
    14
paulson@12776
    15
(** AC0 is equivalent to AC1.  
paulson@12776
    16
    AC0 comes from Suppes, AC1 from Rubin & Rubin **)
paulson@12776
    17
skalberg@14171
    18
lemma AC0_AC1_lemma: "[| f:(\<Pi> X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi> X \<in> D. X)"
paulson@12891
    19
by (fast intro!: lam_type apply_type)
paulson@12776
    20
paulson@12776
    21
lemma AC0_AC1: "AC0 ==> AC1"
paulson@12776
    22
apply (unfold AC0_def AC1_def)
paulson@12776
    23
apply (blast intro: AC0_AC1_lemma)
paulson@12776
    24
done
paulson@12776
    25
paulson@12776
    26
lemma AC1_AC0: "AC1 ==> AC0"
paulson@12776
    27
by (unfold AC0_def AC1_def, blast)
paulson@12776
    28
paulson@12776
    29
paulson@12776
    30
(**** The proof of AC1 ==> AC17 ****)
paulson@12776
    31
skalberg@14171
    32
lemma AC1_AC17_lemma: "f \<in> (\<Pi> X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
paulson@12776
    33
apply (rule Pi_type, assumption)
paulson@12776
    34
apply (drule apply_type, assumption, fast)
paulson@12776
    35
done
paulson@12776
    36
paulson@12776
    37
lemma AC1_AC17: "AC1 ==> AC17"
paulson@12776
    38
apply (unfold AC1_def AC17_def)
paulson@12776
    39
apply (rule allI)
paulson@12776
    40
apply (rule ballI)
paulson@12776
    41
apply (erule_tac x = "Pow (A) -{0}" in allE)
paulson@12776
    42
apply (erule impE, fast)
paulson@12776
    43
apply (erule exE)
paulson@12776
    44
apply (rule bexI)
paulson@12776
    45
apply (erule_tac [2] AC1_AC17_lemma)
paulson@12776
    46
apply (rule apply_type, assumption)
paulson@12776
    47
apply (fast dest!: AC1_AC17_lemma elim!: apply_type)
paulson@12776
    48
done
paulson@12776
    49
paulson@12776
    50
paulson@12776
    51
(**** The proof of AC17 ==> AC1 ****)
paulson@12776
    52
paulson@12776
    53
(* *********************************************************************** *)
paulson@12776
    54
(* more properties of HH                                                   *)
paulson@12776
    55
(* *********************************************************************** *)
paulson@12776
    56
paulson@12776
    57
lemma UN_eq_imp_well_ord:
paulson@12776
    58
     "[| x - (\<Union>j \<in> LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.  
paulson@12776
    59
        HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, j)) = 0;   
paulson@12776
    60
        f \<in> Pow(x)-{0} -> x |]   
paulson@12776
    61
        ==> \<exists>r. well_ord(x,r)"
paulson@12776
    62
apply (rule exI)
paulson@12776
    63
apply (erule well_ord_rvimage 
paulson@12776
    64
        [OF bij_Least_HH_x [THEN bij_converse_bij, THEN bij_is_inj] 
paulson@12776
    65
            Ord_Least [THEN well_ord_Memrel]], assumption)
paulson@12776
    66
done
paulson@12776
    67
paulson@12776
    68
(* *********************************************************************** *)
paulson@12776
    69
(* theorems closer to the proof                                            *)
paulson@12776
    70
(* *********************************************************************** *)
paulson@12776
    71
paulson@12776
    72
lemma not_AC1_imp_ex:
paulson@12776
    73
     "~AC1 ==> \<exists>A. \<forall>f \<in> Pow(A)-{0} -> A. \<exists>u \<in> Pow(A)-{0}. f`u \<notin> u"
paulson@12776
    74
apply (unfold AC1_def)
paulson@12776
    75
apply (erule swap)
paulson@12776
    76
apply (rule allI)
paulson@12776
    77
apply (erule swap)
paulson@12776
    78
apply (rule_tac x = "Union (A)" in exI)
paulson@12891
    79
apply (blast intro: lam_type)
paulson@12776
    80
done
paulson@12776
    81
wenzelm@13535
    82
lemma AC17_AC1_aux1:
paulson@12776
    83
     "[| \<forall>f \<in> Pow(x) - {0} -> x. \<exists>u \<in> Pow(x) - {0}. f`u\<notin>u;   
paulson@12776
    84
         \<exists>f \<in> Pow(x)-{0}->x.  
paulson@12776
    85
            x - (\<Union>a \<in> (LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).   
paulson@12776
    86
            HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,a)) = 0 |]  
paulson@12776
    87
        ==> P"
paulson@12776
    88
apply (erule bexE)
paulson@12776
    89
apply (erule UN_eq_imp_well_ord [THEN exE], assumption)
paulson@12776
    90
apply (erule ex_choice_fun_Pow [THEN exE])
paulson@12776
    91
apply (erule ballE) 
paulson@12776
    92
apply (fast intro: apply_type del: DiffE)
paulson@12776
    93
apply (erule notE)
paulson@12776
    94
apply (rule Pi_type, assumption)
paulson@12776
    95
apply (blast dest: apply_type) 
paulson@12776
    96
done
paulson@12776
    97
wenzelm@13535
    98
lemma AC17_AC1_aux2:
paulson@12776
    99
      "~ (\<exists>f \<in> Pow(x)-{0}->x. x - F(f) = 0)   
paulson@12776
   100
       ==> (\<lambda>f \<in> Pow(x)-{0}->x . x - F(f))   
paulson@12776
   101
           \<in> (Pow(x) -{0} -> x) -> Pow(x) - {0}"
paulson@12776
   102
by (fast intro!: lam_type dest!: Diff_eq_0_iff [THEN iffD1])
paulson@12776
   103
wenzelm@13535
   104
lemma AC17_AC1_aux3:
paulson@12776
   105
     "[| f`Z \<in> Z; Z \<in> Pow(x)-{0} |] 
paulson@12776
   106
      ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X})`Z \<in> Pow(Z)-{0}"
paulson@12776
   107
by auto
paulson@12776
   108
wenzelm@13535
   109
lemma AC17_AC1_aux4:
paulson@12776
   110
     "\<exists>f \<in> F. f`((\<lambda>f \<in> F. Q(f))`f) \<in> (\<lambda>f \<in> F. Q(f))`f   
paulson@12776
   111
      ==> \<exists>f \<in> F. f`Q(f) \<in> Q(f)"
paulson@12776
   112
by simp
paulson@12776
   113
paulson@12776
   114
lemma AC17_AC1: "AC17 ==> AC1"
paulson@12776
   115
apply (unfold AC17_def)
paulson@12776
   116
apply (rule classical)
paulson@12776
   117
apply (erule not_AC1_imp_ex [THEN exE])
paulson@12776
   118
apply (case_tac 
paulson@12776
   119
       "\<exists>f \<in> Pow(x)-{0} -> x. 
paulson@12776
   120
        x - (\<Union>a \<in> (LEAST i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
wenzelm@13535
   121
apply (erule AC17_AC1_aux1, assumption)
wenzelm@13535
   122
apply (drule AC17_AC1_aux2)
paulson@12776
   123
apply (erule allE)
paulson@12776
   124
apply (drule bspec, assumption)
wenzelm@13535
   125
apply (drule AC17_AC1_aux4)
paulson@12776
   126
apply (erule bexE)
paulson@12776
   127
apply (drule apply_type, assumption)
paulson@12776
   128
apply (simp add: HH_Least_eq_x del: Diff_iff ) 
wenzelm@13535
   129
apply (drule AC17_AC1_aux3, assumption) 
paulson@12776
   130
apply (fast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]]
paulson@12776
   131
                   f_subset_imp_HH_subset elim!: mem_irrefl)
paulson@12776
   132
done
paulson@12776
   133
paulson@12776
   134
paulson@12776
   135
(* **********************************************************************
paulson@12776
   136
    AC1 ==> AC2 ==> AC1
paulson@12776
   137
    AC1 ==> AC4 ==> AC3 ==> AC1
paulson@12776
   138
    AC4 ==> AC5 ==> AC4
paulson@12776
   139
    AC1 <-> AC6
paulson@12776
   140
************************************************************************* *)
paulson@12776
   141
paulson@12776
   142
(* ********************************************************************** *)
paulson@12776
   143
(* AC1 ==> AC2                                                            *)
paulson@12776
   144
(* ********************************************************************** *)
paulson@12776
   145
wenzelm@13535
   146
lemma AC1_AC2_aux1:
skalberg@14171
   147
     "[| f:(\<Pi> X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
paulson@12776
   148
by (fast elim!: apply_type)
lcp@1123
   149
wenzelm@13535
   150
lemma AC1_AC2_aux2: 
paulson@12776
   151
        "[| pairwise_disjoint(A); B \<in> A; C \<in> A; D \<in> B; D \<in> C |] ==> f`B = f`C"
paulson@12776
   152
by (unfold pairwise_disjoint_def, fast)
paulson@12776
   153
paulson@12776
   154
lemma AC1_AC2: "AC1 ==> AC2"
paulson@12776
   155
apply (unfold AC1_def AC2_def)
paulson@12776
   156
apply (rule allI)
paulson@12776
   157
apply (rule impI)  
paulson@12776
   158
apply (elim asm_rl conjE allE exE impE, assumption)
paulson@12776
   159
apply (intro exI ballI equalityI)
wenzelm@13535
   160
prefer 2 apply (rule AC1_AC2_aux1, assumption+)
wenzelm@13535
   161
apply (fast elim!: AC1_AC2_aux2 elim: apply_type)
paulson@12776
   162
done
paulson@12776
   163
paulson@12776
   164
paulson@12776
   165
(* ********************************************************************** *)
paulson@12776
   166
(* AC2 ==> AC1                                                            *)
paulson@12776
   167
(* ********************************************************************** *)
paulson@12776
   168
wenzelm@13535
   169
lemma AC2_AC1_aux1: "0\<notin>A ==> 0 \<notin> {B*{B}. B \<in> A}"
paulson@12776
   170
by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]])
paulson@12776
   171
wenzelm@13535
   172
lemma AC2_AC1_aux2: "[| X*{X} Int C = {y}; X \<in> A |]   
paulson@12776
   173
               ==> (THE y. X*{X} Int C = {y}): X*A"
paulson@12776
   174
apply (rule subst_elem [of y])
paulson@12776
   175
apply (blast elim!: equalityE)
paulson@12776
   176
apply (auto simp add: singleton_eq_iff) 
paulson@12776
   177
done
paulson@12776
   178
wenzelm@13535
   179
lemma AC2_AC1_aux3:
paulson@12776
   180
     "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D Int C = {y}   
skalberg@14171
   181
      ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi> X \<in> A. X)"
paulson@12776
   182
apply (rule lam_type)
paulson@12776
   183
apply (drule bspec, blast)
wenzelm@13535
   184
apply (blast intro: AC2_AC1_aux2 fst_type)
paulson@12776
   185
done
paulson@12776
   186
paulson@12776
   187
lemma AC2_AC1: "AC2 ==> AC1"
paulson@12776
   188
apply (unfold AC1_def AC2_def pairwise_disjoint_def)
paulson@12776
   189
apply (intro allI impI)
paulson@12776
   190
apply (elim allE impE)
wenzelm@13535
   191
prefer 2 apply (fast elim!: AC2_AC1_aux3) 
wenzelm@13535
   192
apply (blast intro!: AC2_AC1_aux1)
paulson@12776
   193
done
paulson@12776
   194
paulson@12776
   195
paulson@12776
   196
(* ********************************************************************** *)
paulson@12776
   197
(* AC1 ==> AC4                                                            *)
paulson@12776
   198
(* ********************************************************************** *)
paulson@12776
   199
paulson@12776
   200
lemma empty_notin_images: "0 \<notin> {R``{x}. x \<in> domain(R)}"
paulson@12776
   201
by blast
paulson@12776
   202
paulson@12776
   203
lemma AC1_AC4: "AC1 ==> AC4"
paulson@12776
   204
apply (unfold AC1_def AC4_def)
paulson@12776
   205
apply (intro allI impI)
paulson@12776
   206
apply (drule spec, drule mp [OF _ empty_notin_images]) 
paulson@12776
   207
apply (best intro!: lam_type elim!: apply_type)
paulson@12776
   208
done
paulson@12776
   209
paulson@12776
   210
paulson@12776
   211
(* ********************************************************************** *)
paulson@12776
   212
(* AC4 ==> AC3                                                            *)
paulson@12776
   213
(* ********************************************************************** *)
paulson@12776
   214
wenzelm@13535
   215
lemma AC4_AC3_aux1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*Union(B)"
paulson@12776
   216
by (fast dest!: apply_type)
paulson@12776
   217
wenzelm@13535
   218
lemma AC4_AC3_aux2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
paulson@12776
   219
by blast
paulson@12776
   220
wenzelm@13535
   221
lemma AC4_AC3_aux3: "x \<in> A ==> (\<Union>z \<in> A. {z}*f(z))``{x} = f(x)"
paulson@12776
   222
by fast
paulson@12776
   223
paulson@12776
   224
lemma AC4_AC3: "AC4 ==> AC3"
paulson@12776
   225
apply (unfold AC3_def AC4_def)
paulson@12776
   226
apply (intro allI ballI)
paulson@12776
   227
apply (elim allE impE)
wenzelm@13535
   228
apply (erule AC4_AC3_aux1)
wenzelm@13535
   229
apply (simp add: AC4_AC3_aux2 AC4_AC3_aux3 cong add: Pi_cong)
paulson@12776
   230
done
paulson@12776
   231
paulson@12776
   232
(* ********************************************************************** *)
paulson@12776
   233
(* AC3 ==> AC1                                                            *)
paulson@12776
   234
(* ********************************************************************** *)
paulson@12776
   235
paulson@12776
   236
lemma AC3_AC1_lemma:
skalberg@14171
   237
     "b\<notin>A ==> (\<Pi> x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi> x \<in> A. x)"
paulson@12776
   238
apply (simp add: id_def cong add: Pi_cong)
paulson@13339
   239
apply (rule_tac b = A in subst_context, fast)
paulson@12776
   240
done
paulson@12776
   241
paulson@12776
   242
lemma AC3_AC1: "AC3 ==> AC1"
paulson@12776
   243
apply (unfold AC1_def AC3_def)
paulson@12776
   244
apply (fast intro!: id_type elim: AC3_AC1_lemma [THEN subst])
paulson@12776
   245
done
paulson@12776
   246
paulson@12776
   247
(* ********************************************************************** *)
paulson@12776
   248
(* AC4 ==> AC5                                                            *)
paulson@12776
   249
(* ********************************************************************** *)
paulson@12776
   250
paulson@12776
   251
lemma AC4_AC5: "AC4 ==> AC5"
paulson@12776
   252
apply (unfold range_def AC4_def AC5_def)
paulson@12776
   253
apply (intro allI ballI)
paulson@12776
   254
apply (elim allE impE)
paulson@12776
   255
apply (erule fun_is_rel [THEN converse_type])
paulson@12776
   256
apply (erule exE)
paulson@12776
   257
apply (rename_tac g)
paulson@12776
   258
apply (rule_tac x=g in bexI)
paulson@12776
   259
apply (blast dest: apply_equality range_type) 
paulson@12776
   260
apply (blast intro: Pi_type dest: apply_type fun_is_rel)
paulson@12776
   261
done
paulson@12776
   262
paulson@12776
   263
paulson@12776
   264
(* ********************************************************************** *)
paulson@12776
   265
(* AC5 ==> AC4, Rubin & Rubin, p. 11                                      *)
paulson@12776
   266
(* ********************************************************************** *)
paulson@12776
   267
wenzelm@13535
   268
lemma AC5_AC4_aux1: "R \<subseteq> A*B ==> (\<lambda>x \<in> R. fst(x)) \<in> R -> A"
paulson@12776
   269
by (fast intro!: lam_type fst_type)
paulson@12776
   270
wenzelm@13535
   271
lemma AC5_AC4_aux2: "R \<subseteq> A*B ==> range(\<lambda>x \<in> R. fst(x)) = domain(R)"
paulson@12776
   272
by (unfold lam_def, force)
paulson@12776
   273
wenzelm@13535
   274
lemma AC5_AC4_aux3: "[| \<exists>f \<in> A->C. P(f,domain(f)); A=B |] ==>  \<exists>f \<in> B->C. P(f,B)"
paulson@12776
   275
apply (erule bexE)
paulson@12776
   276
apply (frule domain_of_fun, fast)
paulson@12776
   277
done
paulson@12776
   278
wenzelm@13535
   279
lemma AC5_AC4_aux4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]  
skalberg@14171
   280
                ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi> x \<in> C. R``{x})"
paulson@12776
   281
apply (rule lam_type)
paulson@12776
   282
apply (force dest: apply_type)
paulson@12776
   283
done
paulson@12776
   284
paulson@12776
   285
lemma AC5_AC4: "AC5 ==> AC4"
paulson@12776
   286
apply (unfold AC4_def AC5_def, clarify)
paulson@12776
   287
apply (elim allE ballE)
wenzelm@13535
   288
apply (drule AC5_AC4_aux3 [OF _ AC5_AC4_aux2], assumption)
wenzelm@13535
   289
apply (fast elim!: AC5_AC4_aux4)
wenzelm@13535
   290
apply (blast intro: AC5_AC4_aux1) 
paulson@12776
   291
done
paulson@12776
   292
paulson@12776
   293
paulson@12776
   294
(* ********************************************************************** *)
paulson@12776
   295
(* AC1 <-> AC6                                                            *)
paulson@12776
   296
(* ********************************************************************** *)
paulson@12776
   297
paulson@12776
   298
lemma AC1_iff_AC6: "AC1 <-> AC6"
paulson@12776
   299
by (unfold AC1_def AC6_def, blast)
paulson@12776
   300
paulson@12776
   301
end