author | wenzelm |
Wed, 30 Dec 2015 17:45:18 +0100 | |
changeset 61980 | 6b780867d426 |
parent 46822 | 95f1e700b712 |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
12787 | 1 |
(* Title: ZF/AC/AC7_AC9.thy |
2 |
Author: Krzysztof Grabczewski |
|
3 |
||
4 |
The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous |
|
5 |
instances of AC. |
|
6 |
*) |
|
7 |
||
27678 | 8 |
theory AC7_AC9 |
9 |
imports AC_Equiv |
|
10 |
begin |
|
12787 | 11 |
|
12 |
(* ********************************************************************** *) |
|
13 |
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *) |
|
14 |
(* - Sigma_fun_space_not0 *) |
|
15 |
(* - Sigma_fun_space_eqpoll *) |
|
16 |
(* ********************************************************************** *) |
|
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 | 19 |
by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1]) |
20 |
||
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 | 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 | 25 |
apply (unfold inj_def) |
26 |
apply (rule CollectI) |
|
27 |
apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) |
|
28 |
apply (rule fun_extension, assumption+) |
|
29 |
apply (drule lam_eqE [OF _ nat_succI], assumption, simp) |
|
30 |
apply (drule lam_eqE [OF _ nat_0I], simp) |
|
31 |
done |
|
32 |
||
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 | 35 |
apply (rule eqpollI) |
36 |
apply (simp add: lepoll_def) |
|
37 |
apply (fast intro!: inj_lemma) |
|
38 |
apply (fast elim!: prod_lepoll_self not_sym [THEN not_emptyE] subst_elem |
|
39 |
elim: swap) |
|
40 |
done |
|
41 |
||
42 |
||
43 |
(* ********************************************************************** *) |
|
44 |
(* AC6 ==> AC7 *) |
|
45 |
(* ********************************************************************** *) |
|
46 |
||
47 |
lemma AC6_AC7: "AC6 ==> AC7" |
|
48 |
by (unfold AC6_def AC7_def, blast) |
|
49 |
||
50 |
(* ********************************************************************** *) |
|
51 |
(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *) |
|
52 |
(* The case of the empty family of sets added in order to complete *) |
|
53 |
(* the proof. *) |
|
54 |
(* ********************************************************************** *) |
|
55 |
||
61980 | 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 | 57 |
by (fast intro!: lam_type snd_type apply_type) |
58 |
||
59 |
lemma lemma1_2: |
|
61980 | 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 | 61 |
apply (fast intro!: lam_type apply_type) |
62 |
done |
|
63 |
||
64 |
lemma AC7_AC6_lemma1: |
|
61980 | 65 |
"(\<Prod>B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Prod>B \<in> A. B) \<noteq> 0" |
12787 | 66 |
by (fast intro!: equals0I lemma1_1 lemma1_2) |
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 | 69 |
by (blast dest: Sigma_fun_space_not0) |
70 |
||
71 |
lemma AC7_AC6: "AC7 ==> AC6" |
|
72 |
apply (unfold AC6_def AC7_def) |
|
73 |
apply (rule allI) |
|
74 |
apply (rule impI) |
|
75 |
apply (case_tac "A=0", simp) |
|
76 |
apply (rule AC7_AC6_lemma1) |
|
77 |
apply (erule allE) |
|
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 | 80 |
Sigma_fun_space_eqpoll) |
81 |
done |
|
82 |
||
83 |
||
84 |
(* ********************************************************************** *) |
|
85 |
(* AC1 ==> AC8 *) |
|
86 |
(* ********************************************************************** *) |
|
87 |
||
88 |
lemma AC1_AC8_lemma1: |
|
89 |
"\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1 \<approx> B2 |
|
90 |
==> 0 \<notin> { bij(fst(B),snd(B)). B \<in> A }" |
|
91 |
apply (unfold eqpoll_def, auto) |
|
92 |
done |
|
93 |
||
94 |
lemma AC1_AC8_lemma2: |
|
61980 | 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 | 96 |
apply (simp, fast elim!: apply_type) |
97 |
done |
|
98 |
||
99 |
lemma AC1_AC8: "AC1 ==> AC8" |
|
100 |
apply (unfold AC1_def AC8_def) |
|
101 |
apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2) |
|
102 |
done |
|
103 |
||
104 |
||
105 |
(* ********************************************************************** *) |
|
106 |
(* AC8 ==> AC9 *) |
|
107 |
(* - this proof replaces the following two from Rubin & Rubin: *) |
|
108 |
(* AC8 ==> AC1 and AC1 ==> AC9 *) |
|
109 |
(* ********************************************************************** *) |
|
110 |
||
111 |
lemma AC8_AC9_lemma: |
|
112 |
"\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1 \<approx> B2 |
|
113 |
==> \<forall>B \<in> A*A. \<exists>B1 B2. B=<B1,B2> & B1 \<approx> B2" |
|
114 |
by fast |
|
115 |
||
116 |
lemma AC8_AC9: "AC8 ==> AC9" |
|
117 |
apply (unfold AC8_def AC9_def) |
|
118 |
apply (intro allI impI) |
|
119 |
apply (erule allE) |
|
120 |
apply (erule impE, erule AC8_AC9_lemma, force) |
|
121 |
done |
|
122 |
||
123 |
||
124 |
(* ********************************************************************** *) |
|
125 |
(* AC9 ==> AC1 *) |
|
126 |
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *) |
|
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 | 130 |
(* ********************************************************************** *) |
131 |
||
132 |
lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X" |
|
133 |
by (blast intro: lepoll_trans prod_lepoll_self eqpoll_imp_lepoll |
|
134 |
prod_commute_eqpoll) |
|
135 |
||
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 | 138 |
by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI) |
139 |
||
140 |
lemma AC9_AC1_lemma1: |
|
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 | 144 |
B1 \<in> C; B2 \<in> C |] |
145 |
==> B1 \<approx> B2" |
|
146 |
by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll |
|
147 |
nat_cons_eqpoll [THEN eqpoll_trans] |
|
148 |
prod_eqpoll_cong [OF _ eqpoll_refl] |
|
149 |
intro: eqpoll_trans eqpoll_sym ) |
|
150 |
||
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 | 154 |
f`<B1,B2> \<in> bij(B1, B2) |
61980 | 155 |
==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Prod>X \<in> A. X)" |
12787 | 156 |
apply (intro lam_type snd_type fst_type) |
157 |
apply (rule apply_type [OF _ consI1]) |
|
158 |
apply (fast intro!: fun_weaken_type bij_is_fun) |
|
159 |
done |
|
160 |
||
161 |
lemma AC9_AC1: "AC9 ==> AC1" |
|
162 |
apply (unfold AC1_def AC9_def) |
|
163 |
apply (intro allI impI) |
|
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 | 166 |
apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force) |
167 |
done |
|
168 |
||
169 |
end |