src/ZF/AC/AC7_AC9.thy
author wenzelm
Wed, 30 Dec 2015 17:45:18 +0100
changeset 61980 6b780867d426
parent 46822 95f1e700b712
child 76213 e44d86131648
permissions -rw-r--r--
clarified syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
     1
(*  Title:      ZF/AC/AC7_AC9.thy
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
     2
    Author:     Krzysztof Grabczewski
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
     3
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
     4
The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
     5
instances of AC.
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
     6
*)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
     7
27678
85ea2be46c71 dropped locale (open)
haftmann
parents: 16417
diff changeset
     8
theory AC7_AC9
85ea2be46c71 dropped locale (open)
haftmann
parents: 16417
diff changeset
     9
imports AC_Equiv
85ea2be46c71 dropped locale (open)
haftmann
parents: 16417
diff changeset
    10
begin
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    11
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    12
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    13
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1                  *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    14
(*  - Sigma_fun_space_not0                                                *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    15
(*  - Sigma_fun_space_eqpoll                                              *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    16
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    17
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    18
lemma Sigma_fun_space_not0: "[| 0\<notin>A; B \<in> A |] ==> (nat->\<Union>(A)) * B \<noteq> 0"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    19
by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1])
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    20
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    21
lemma inj_lemma: 
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    22
        "C \<in> A ==> (\<lambda>g \<in> (nat->\<Union>(A))*C.   
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    23
                (\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1))))   
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    24
                \<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    25
apply (unfold inj_def)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    26
apply (rule CollectI)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    27
apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    28
apply (rule fun_extension, assumption+)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    29
apply (drule lam_eqE [OF _ nat_succI], assumption, simp) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    30
apply (drule lam_eqE [OF _ nat_0I], simp) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    31
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    32
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    33
lemma Sigma_fun_space_eqpoll:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    34
     "[| C \<in> A; 0\<notin>A |] ==> (nat->\<Union>(A)) * C \<approx> (nat->\<Union>(A))"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    35
apply (rule eqpollI)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    36
apply (simp add: lepoll_def)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    37
apply (fast intro!: inj_lemma)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    38
apply (fast elim!: prod_lepoll_self not_sym [THEN not_emptyE] subst_elem 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    39
            elim: swap)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    40
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    41
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    42
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    43
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    44
(* AC6 ==> AC7                                                            *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    45
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    46
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    47
lemma AC6_AC7: "AC6 ==> AC7"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    48
by (unfold AC6_def AC7_def, blast)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    49
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    50
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    51
(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8                          *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    52
(* The case of the empty family of sets added in order to complete        *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    53
(* the proof.                                                             *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    54
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    55
61980
6b780867d426 clarified syntax;
wenzelm
parents: 46822
diff changeset
    56
lemma lemma1_1: "y \<in> (\<Prod>B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Prod>B \<in> A. B)"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    57
by (fast intro!: lam_type snd_type apply_type)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    58
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    59
lemma lemma1_2:
61980
6b780867d426 clarified syntax;
wenzelm
parents: 46822
diff changeset
    60
     "y \<in> (\<Prod>B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Prod>B \<in> A. Y*B)"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    61
apply (fast intro!: lam_type apply_type)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    62
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    63
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    64
lemma AC7_AC6_lemma1:
61980
6b780867d426 clarified syntax;
wenzelm
parents: 46822
diff changeset
    65
     "(\<Prod>B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Prod>B \<in> A. B) \<noteq> 0"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    66
by (fast intro!: equals0I lemma1_1 lemma1_2)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    67
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    68
lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> \<Union>(A)) * C. C \<in> A}"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    69
by (blast dest: Sigma_fun_space_not0)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    70
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    71
lemma AC7_AC6: "AC7 ==> AC6"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    72
apply (unfold AC6_def AC7_def)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    73
apply (rule allI)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    74
apply (rule impI)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    75
apply (case_tac "A=0", simp)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    76
apply (rule AC7_AC6_lemma1)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    77
apply (erule allE) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    78
apply (blast del: notI
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27678
diff changeset
    79
             intro!: AC7_AC6_lemma2 intro: eqpoll_sym eqpoll_trans 
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    80
                    Sigma_fun_space_eqpoll)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    81
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    82
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    83
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    84
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    85
(* AC1 ==> AC8                                                            *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    86
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    87
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    88
lemma AC1_AC8_lemma1: 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    89
        "\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1 \<approx> B2   
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    90
        ==> 0 \<notin> { bij(fst(B),snd(B)). B \<in> A }"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    91
apply (unfold eqpoll_def, auto)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    92
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    93
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    94
lemma AC1_AC8_lemma2:
61980
6b780867d426 clarified syntax;
wenzelm
parents: 46822
diff changeset
    95
     "[| f \<in> (\<Prod>X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)" 
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    96
apply (simp, fast elim!: apply_type)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    97
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    98
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
    99
lemma AC1_AC8: "AC1 ==> AC8"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   100
apply (unfold AC1_def AC8_def)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   101
apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   102
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   103
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   104
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   105
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   106
(* AC8 ==> AC9                                                            *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   107
(*  - this proof replaces the following two from Rubin & Rubin:           *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   108
(*    AC8 ==> AC1 and AC1 ==> AC9                                         *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   109
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   110
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   111
lemma AC8_AC9_lemma:
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   112
     "\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1 \<approx> B2 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   113
      ==> \<forall>B \<in> A*A. \<exists>B1 B2. B=<B1,B2> & B1 \<approx> B2"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   114
by fast
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   115
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   116
lemma AC8_AC9: "AC8 ==> AC9"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   117
apply (unfold AC8_def AC9_def)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   118
apply (intro allI impI)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   119
apply (erule allE)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   120
apply (erule impE, erule AC8_AC9_lemma, force) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   121
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   122
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   123
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   124
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   125
(* AC9 ==> AC1                                                            *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   126
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   127
(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to        *)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   128
(* (x * y) \<union> {0} when y is a set of total functions acting from nat to   *)
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   129
(* \<Union>(A) -- therefore we have used the set (y * nat) instead of y.     *)
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   130
(* ********************************************************************** *)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   131
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   132
lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   133
by (blast intro: lepoll_trans prod_lepoll_self eqpoll_imp_lepoll 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   134
                 prod_commute_eqpoll) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   135
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   136
lemma nat_lepoll_lemma:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   137
     "[|0 \<notin> A; B \<in> A|] ==> nat \<lesssim> ((nat \<rightarrow> \<Union>(A)) \<times> B) \<times> nat"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   138
by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   139
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   140
lemma AC9_AC1_lemma1:
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   141
     "[| 0\<notin>A;  A\<noteq>0;   
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   142
         C = {((nat->\<Union>(A))*B)*nat. B \<in> A}  \<union>  
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   143
             {cons(0,((nat->\<Union>(A))*B)*nat). B \<in> A};  
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   144
         B1 \<in> C;  B2 \<in> C |]   
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   145
      ==> B1 \<approx> B2"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   146
by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   147
                     nat_cons_eqpoll [THEN eqpoll_trans] 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   148
                     prod_eqpoll_cong [OF _ eqpoll_refl]
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   149
             intro: eqpoll_trans eqpoll_sym )
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   150
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   151
lemma AC9_AC1_lemma2:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   152
     "\<forall>B1 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   153
      \<forall>B2 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   154
        f`<B1,B2> \<in> bij(B1, B2)   
61980
6b780867d426 clarified syntax;
wenzelm
parents: 46822
diff changeset
   155
      ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Prod>X \<in> A. X)"
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   156
apply (intro lam_type snd_type fst_type)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   157
apply (rule apply_type [OF _ consI1]) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   158
apply (fast intro!: fun_weaken_type bij_is_fun)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   159
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   160
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   161
lemma AC9_AC1: "AC9 ==> AC1"
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   162
apply (unfold AC1_def AC9_def)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   163
apply (intro allI impI)
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   164
apply (erule allE)
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   165
apply (case_tac "A\<noteq>0")
12787
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   166
apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force) 
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   167
done
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   168
3ecbc37befab mistakenly deleted this theory
paulson
parents:
diff changeset
   169
end