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