1461
|
1 |
(* Title: ZF/AC/AC2_AC6.ML
|
1123
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Krzysztof Grabczewski
|
1123
|
4 |
|
1196
|
5 |
The proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent
|
|
6 |
to AC0 and AC1:
|
1123
|
7 |
AC1 ==> AC2 ==> AC1
|
|
8 |
AC1 ==> AC4 ==> AC3 ==> AC1
|
|
9 |
AC4 ==> AC5 ==> AC4
|
|
10 |
AC1 <-> AC6
|
|
11 |
*)
|
|
12 |
|
|
13 |
(* ********************************************************************** *)
|
1461
|
14 |
(* AC1 ==> AC2 *)
|
1123
|
15 |
(* ********************************************************************** *)
|
|
16 |
|
|
17 |
goal thy "!!B. [| B:A; f:(PROD X:A. X); 0~:A |] \
|
1461
|
18 |
\ ==> {f`B} <= B Int {f`C. C:A}";
|
1123
|
19 |
by (fast_tac (AC_cs addSEs [singletonE, apply_type, RepFunI]) 1);
|
|
20 |
val lemma1 = result();
|
|
21 |
|
|
22 |
goalw thy [pairwise_disjoint_def]
|
1461
|
23 |
"!!A. [| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C";
|
1123
|
24 |
by (fast_tac (ZF_cs addSEs [equals0D]) 1);
|
|
25 |
val lemma2 = result();
|
|
26 |
|
|
27 |
goalw thy AC_defs "!!Z. AC1 ==> AC2";
|
1206
|
28 |
by (rtac allI 1);
|
|
29 |
by (rtac impI 1);
|
1123
|
30 |
by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1));
|
|
31 |
by (REPEAT (resolve_tac [exI,ballI,equalityI] 1));
|
1206
|
32 |
by (rtac lemma1 2 THEN (REPEAT (assume_tac 2)));
|
1123
|
33 |
by (fast_tac (AC_cs addSEs [RepFunE, lemma2] addEs [apply_type]) 1);
|
1196
|
34 |
qed "AC1_AC2";
|
1123
|
35 |
|
|
36 |
|
|
37 |
(* ********************************************************************** *)
|
1461
|
38 |
(* AC2 ==> AC1 *)
|
1123
|
39 |
(* ********************************************************************** *)
|
|
40 |
|
|
41 |
goal thy "!!A. 0~:A ==> 0 ~: {B*{B}. B:A}";
|
|
42 |
by (fast_tac (AC_cs addSDs [sym RS (Sigma_empty_iff RS iffD1)]
|
1461
|
43 |
addSEs [RepFunE, equals0D]) 1);
|
1123
|
44 |
val lemma1 = result();
|
|
45 |
|
|
46 |
goal thy "!!A. [| X*{X} Int C = {y}; X:A |] \
|
1461
|
47 |
\ ==> (THE y. X*{X} Int C = {y}): X*A";
|
1206
|
48 |
by (rtac subst_elem 1);
|
1123
|
49 |
by (fast_tac (ZF_cs addSIs [the_equality]
|
1461
|
50 |
addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2);
|
1123
|
51 |
by (fast_tac (AC_cs addSEs [equalityE, make_elim singleton_subsetD]) 1);
|
|
52 |
val lemma2 = result();
|
|
53 |
|
|
54 |
goal thy "!!A. ALL D:{E*{E}. E:A}. EX y. D Int C = {y} \
|
1461
|
55 |
\ ==> (lam x:A. fst(THE z. (x*{x} Int C = {z}))) : \
|
|
56 |
\ (PROD X:A. X) ";
|
1123
|
57 |
by (fast_tac (FOL_cs addSEs [lemma2]
|
1461
|
58 |
addSIs [lam_type, RepFunI, fst_type]
|
|
59 |
addSDs [bspec]) 1);
|
1123
|
60 |
val lemma3 = result();
|
|
61 |
|
|
62 |
goalw thy (AC_defs@AC_aux_defs) "!!Z. AC2 ==> AC1";
|
|
63 |
by (REPEAT (resolve_tac [allI, impI] 1));
|
|
64 |
by (REPEAT (eresolve_tac [allE, impE] 1));
|
|
65 |
by (fast_tac (AC_cs addSEs [lemma3]) 2);
|
|
66 |
by (fast_tac (AC_cs addSIs [lemma1, equals0I]) 1);
|
1196
|
67 |
qed "AC2_AC1";
|
1123
|
68 |
|
|
69 |
|
|
70 |
(* ********************************************************************** *)
|
1461
|
71 |
(* AC1 ==> AC4 *)
|
1123
|
72 |
(* ********************************************************************** *)
|
|
73 |
|
|
74 |
goal thy "!!R. 0 ~: {R``{x}. x:domain(R)}";
|
|
75 |
by (fast_tac (AC_cs addSEs [RepFunE, domainE, sym RS equals0D]) 1);
|
|
76 |
val lemma = result();
|
|
77 |
|
|
78 |
goalw thy AC_defs "!!Z. AC1 ==> AC4";
|
|
79 |
by (REPEAT (resolve_tac [allI, impI] 1));
|
|
80 |
by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
|
|
81 |
by (fast_tac (AC_cs addSIs [lam_type, RepFunI] addSEs [apply_type]) 1);
|
1196
|
82 |
qed "AC1_AC4";
|
1123
|
83 |
|
|
84 |
|
|
85 |
(* ********************************************************************** *)
|
1461
|
86 |
(* AC4 ==> AC3 *)
|
1123
|
87 |
(* ********************************************************************** *)
|
|
88 |
|
|
89 |
goal thy "!!f. f:A->B ==> (UN z:A. {z}*f`z) <= A*Union(B)";
|
|
90 |
by (fast_tac (ZF_cs addSDs [apply_type] addSEs [UN_E, singletonE]) 1);
|
|
91 |
val lemma1 = result();
|
|
92 |
|
|
93 |
goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
|
|
94 |
by (fast_tac (ZF_cs addIs [equalityI]
|
1461
|
95 |
addSEs [not_emptyE]
|
|
96 |
addSIs [singletonI, not_emptyI]
|
|
97 |
addDs [range_type]) 1);
|
1123
|
98 |
val lemma2 = result();
|
|
99 |
|
|
100 |
goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
|
|
101 |
by (fast_tac (ZF_cs addIs [equalityI] addSIs [singletonI, UN_I] addSEs [singletonE, UN_E]) 1);
|
|
102 |
val lemma3 = result();
|
|
103 |
|
|
104 |
goalw thy AC_defs "!!Z. AC4 ==> AC3";
|
|
105 |
by (REPEAT (resolve_tac [allI,ballI] 1));
|
|
106 |
by (REPEAT (eresolve_tac [allE,impE] 1));
|
1206
|
107 |
by (etac lemma1 1);
|
1123
|
108 |
by (asm_full_simp_tac (AC_ss addsimps [lemma2, lemma3]
|
1461
|
109 |
addcongs [Pi_cong]) 1);
|
1196
|
110 |
qed "AC4_AC3";
|
1123
|
111 |
|
|
112 |
(* ********************************************************************** *)
|
1461
|
113 |
(* AC3 ==> AC1 *)
|
1123
|
114 |
(* ********************************************************************** *)
|
|
115 |
|
|
116 |
goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)";
|
|
117 |
by (asm_full_simp_tac (AC_ss addsimps [id_def] addcongs [Pi_cong]) 1);
|
|
118 |
by (res_inst_tac [("b","A")] subst_context 1);
|
|
119 |
by (fast_tac (AC_cs addSIs [equalityI]) 1);
|
|
120 |
val lemma = result();
|
|
121 |
|
|
122 |
goalw thy AC_defs "!!Z. AC3 ==> AC1";
|
|
123 |
by (REPEAT (resolve_tac [allI, impI] 1));
|
|
124 |
by (REPEAT (eresolve_tac [allE, ballE] 1));
|
|
125 |
by (fast_tac (AC_cs addSIs [id_type]) 2);
|
|
126 |
by (fast_tac (AC_cs addEs [lemma RS subst]) 1);
|
1196
|
127 |
qed "AC3_AC1";
|
1123
|
128 |
|
|
129 |
(* ********************************************************************** *)
|
1461
|
130 |
(* AC4 ==> AC5 *)
|
1123
|
131 |
(* ********************************************************************** *)
|
|
132 |
|
|
133 |
goalw thy (range_def::AC_defs) "!!Z. AC4 ==> AC5";
|
|
134 |
by (REPEAT (resolve_tac [allI,ballI] 1));
|
|
135 |
by (REPEAT (eresolve_tac [allE,impE] 1));
|
|
136 |
by (eresolve_tac [fun_is_rel RS converse_type] 1);
|
1206
|
137 |
by (etac exE 1);
|
|
138 |
by (rtac bexI 1);
|
|
139 |
by (rtac Pi_type 2 THEN (assume_tac 2));
|
1123
|
140 |
by (fast_tac (ZF_cs addSDs [apply_type]
|
1461
|
141 |
addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2);
|
1206
|
142 |
by (rtac ballI 1);
|
|
143 |
by (rtac apply_equality 1 THEN (assume_tac 2));
|
|
144 |
by (etac domainE 1);
|
1196
|
145 |
by (forward_tac [range_type] 1 THEN (assume_tac 1));
|
1123
|
146 |
by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1);
|
1196
|
147 |
qed "AC4_AC5";
|
1123
|
148 |
|
|
149 |
|
|
150 |
(* ********************************************************************** *)
|
1461
|
151 |
(* AC5 ==> AC4, Rubin & Rubin, p. 11 *)
|
1123
|
152 |
(* ********************************************************************** *)
|
|
153 |
|
|
154 |
goal thy "!!A. R <= A*B ==> (lam x:R. fst(x)) : R -> A";
|
|
155 |
by (fast_tac (ZF_cs addSIs [lam_type, fst_type]) 1);
|
|
156 |
val lemma1 = result();
|
|
157 |
|
|
158 |
goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
|
1206
|
159 |
by (rtac equalityI 1);
|
1123
|
160 |
by (fast_tac (AC_cs addSEs [lamE, Pair_inject]
|
1461
|
161 |
addEs [subst_elem]
|
|
162 |
addSDs [converseD, Pair_fst_snd_eq]) 1);
|
1206
|
163 |
by (rtac subsetI 1);
|
|
164 |
by (etac domainE 1);
|
|
165 |
by (rtac domainI 1);
|
1123
|
166 |
by (fast_tac (AC_cs addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1);
|
|
167 |
val lemma2 = result();
|
|
168 |
|
|
169 |
goal thy "!!A. [| EX f: A->C. P(f,domain(f)); A=B |] ==> EX f: B->C. P(f,B)";
|
1206
|
170 |
by (etac bexE 1);
|
1123
|
171 |
by (forward_tac [domain_of_fun] 1);
|
|
172 |
by (fast_tac ZF_cs 1);
|
|
173 |
val lemma3 = result();
|
|
174 |
|
|
175 |
goal thy "!!g. [| R <= A*B; g: C->R; ALL x:C. (lam z:R. fst(z))` (g`x) = x |] \
|
1461
|
176 |
\ ==> (lam x:C. snd(g`x)): (PROD x:C. R``{x})";
|
1206
|
177 |
by (rtac lam_type 1);
|
|
178 |
by (dtac apply_type 1 THEN (assume_tac 1));
|
|
179 |
by (dtac bspec 1 THEN (assume_tac 1));
|
|
180 |
by (rtac imageI 1);
|
1123
|
181 |
by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1
|
1461
|
182 |
THEN (REPEAT (assume_tac 1)));
|
1123
|
183 |
by (asm_full_simp_tac AC_ss 1);
|
|
184 |
val lemma4 = result();
|
|
185 |
|
|
186 |
goalw thy AC_defs "!!Z. AC5 ==> AC4";
|
|
187 |
by (REPEAT (resolve_tac [allI,impI] 1));
|
|
188 |
by (REPEAT (eresolve_tac [allE,ballE] 1));
|
1196
|
189 |
by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2));
|
|
190 |
by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1));
|
1123
|
191 |
by (fast_tac (AC_cs addSEs [lemma4]) 1);
|
1196
|
192 |
qed "AC5_AC4";
|
1123
|
193 |
|
|
194 |
|
|
195 |
(* ********************************************************************** *)
|
1461
|
196 |
(* AC1 <-> AC6 *)
|
1123
|
197 |
(* ********************************************************************** *)
|
|
198 |
|
|
199 |
goalw thy AC_defs "AC1 <-> AC6";
|
|
200 |
by (fast_tac (ZF_cs addDs [equals0D] addSEs [not_emptyE]) 1);
|
1196
|
201 |
qed "AC1_iff_AC6";
|
|
202 |
|