author | paulson |
Thu, 10 Sep 1998 17:42:44 +0200 | |
changeset 5470 | 855654b691db |
parent 5265 | 9d1d4c43c76d |
child 7499 | 23e090051cb8 |
permissions | -rw-r--r-- |
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 |
||
5137 | 17 |
Goal "[| B:A; f:(PROD X:A. X); 0~:A |] \ |
1461 | 18 |
\ ==> {f`B} <= B Int {f`C. C:A}"; |
4091 | 19 |
by (fast_tac (claset() addSEs [apply_type]) 1); |
1123 | 20 |
val lemma1 = result(); |
21 |
||
5068 | 22 |
Goalw [pairwise_disjoint_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
23 |
"[| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
24 |
by (Fast_tac 1); |
1123 | 25 |
val lemma2 = result(); |
26 |
||
5137 | 27 |
Goalw AC_defs "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))); |
5241 | 33 |
by (fast_tac (claset() addSEs [lemma2] addEs [apply_type]) 1); |
1196 | 34 |
qed "AC1_AC2"; |
1123 | 35 |
|
36 |
||
37 |
(* ********************************************************************** *) |
|
1461 | 38 |
(* AC2 ==> AC1 *) |
1123 | 39 |
(* ********************************************************************** *) |
40 |
||
5137 | 41 |
Goal "0~:A ==> 0 ~: {B*{B}. B:A}"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
42 |
by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]) 1); |
1123 | 43 |
val lemma1 = result(); |
44 |
||
5137 | 45 |
Goal "[| X*{X} Int C = {y}; X:A |] \ |
1461 | 46 |
\ ==> (THE y. X*{X} Int C = {y}): X*A"; |
1206 | 47 |
by (rtac subst_elem 1); |
4091 | 48 |
by (fast_tac (claset() addSIs [the_equality] |
1461 | 49 |
addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2); |
4091 | 50 |
by (fast_tac (claset() addSEs [equalityE, make_elim singleton_subsetD]) 1); |
1123 | 51 |
val lemma2 = result(); |
52 |
||
5137 | 53 |
Goal "ALL D:{E*{E}. E:A}. EX y. D Int C = {y} \ |
1461 | 54 |
\ ==> (lam x:A. fst(THE z. (x*{x} Int C = {z}))) : \ |
55 |
\ (PROD X:A. X) "; |
|
4091 | 56 |
by (fast_tac (claset() addSEs [lemma2] |
1461 | 57 |
addSIs [lam_type, RepFunI, fst_type] |
58 |
addSDs [bspec]) 1); |
|
1123 | 59 |
val lemma3 = result(); |
60 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
61 |
Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1"; |
1123 | 62 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
63 |
by (REPEAT (eresolve_tac [allE, impE] 1)); |
|
4091 | 64 |
by (fast_tac (claset() addSEs [lemma3]) 2); |
65 |
by (fast_tac (claset() addSIs [lemma1, equals0I]) 1); |
|
1196 | 66 |
qed "AC2_AC1"; |
1123 | 67 |
|
68 |
||
69 |
(* ********************************************************************** *) |
|
1461 | 70 |
(* AC1 ==> AC4 *) |
1123 | 71 |
(* ********************************************************************** *) |
72 |
||
5137 | 73 |
Goal "0 ~: {R``{x}. x:domain(R)}"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
74 |
by (Blast_tac 1); |
1123 | 75 |
val lemma = result(); |
76 |
||
5137 | 77 |
Goalw AC_defs "AC1 ==> AC4"; |
1123 | 78 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
79 |
by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1)); |
|
4091 | 80 |
by (best_tac (claset() addSIs [lam_type] addSEs [apply_type]) 1); |
1196 | 81 |
qed "AC1_AC4"; |
1123 | 82 |
|
83 |
||
84 |
(* ********************************************************************** *) |
|
1461 | 85 |
(* AC4 ==> AC3 *) |
1123 | 86 |
(* ********************************************************************** *) |
87 |
||
5137 | 88 |
Goal "f:A->B ==> (UN z:A. {z}*f`z) <= A*Union(B)"; |
4091 | 89 |
by (fast_tac (claset() addSDs [apply_type]) 1); |
1123 | 90 |
val lemma1 = result(); |
91 |
||
5137 | 92 |
Goal "domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}"; |
4091 | 93 |
by (fast_tac (claset() addSIs [not_emptyI] addDs [range_type]) 1); |
1123 | 94 |
val lemma2 = result(); |
95 |
||
5137 | 96 |
Goal "x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)"; |
2496 | 97 |
by (Fast_tac 1); |
1123 | 98 |
val lemma3 = result(); |
99 |
||
5137 | 100 |
Goalw AC_defs "AC4 ==> AC3"; |
1123 | 101 |
by (REPEAT (resolve_tac [allI,ballI] 1)); |
102 |
by (REPEAT (eresolve_tac [allE,impE] 1)); |
|
1206 | 103 |
by (etac lemma1 1); |
4091 | 104 |
by (asm_full_simp_tac (simpset() addsimps [lemma2, lemma3] |
1461 | 105 |
addcongs [Pi_cong]) 1); |
1196 | 106 |
qed "AC4_AC3"; |
1123 | 107 |
|
108 |
(* ********************************************************************** *) |
|
1461 | 109 |
(* AC3 ==> AC1 *) |
1123 | 110 |
(* ********************************************************************** *) |
111 |
||
5137 | 112 |
Goal "b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)"; |
4091 | 113 |
by (asm_full_simp_tac (simpset() addsimps [id_def] addcongs [Pi_cong]) 1); |
1123 | 114 |
by (res_inst_tac [("b","A")] subst_context 1); |
2496 | 115 |
by (Fast_tac 1); |
1123 | 116 |
val lemma = result(); |
117 |
||
5137 | 118 |
Goalw AC_defs "AC3 ==> AC1"; |
1123 | 119 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
120 |
by (REPEAT (eresolve_tac [allE, ballE] 1)); |
|
4091 | 121 |
by (fast_tac (claset() addSIs [id_type]) 2); |
122 |
by (fast_tac (claset() addEs [lemma RS subst]) 1); |
|
1196 | 123 |
qed "AC3_AC1"; |
1123 | 124 |
|
125 |
(* ********************************************************************** *) |
|
1461 | 126 |
(* AC4 ==> AC5 *) |
1123 | 127 |
(* ********************************************************************** *) |
128 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
129 |
Goalw (range_def::AC_defs) "AC4 ==> AC5"; |
1123 | 130 |
by (REPEAT (resolve_tac [allI,ballI] 1)); |
131 |
by (REPEAT (eresolve_tac [allE,impE] 1)); |
|
132 |
by (eresolve_tac [fun_is_rel RS converse_type] 1); |
|
1206 | 133 |
by (etac exE 1); |
134 |
by (rtac bexI 1); |
|
135 |
by (rtac Pi_type 2 THEN (assume_tac 2)); |
|
4091 | 136 |
by (fast_tac (claset() addSDs [apply_type] |
1461 | 137 |
addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2); |
1206 | 138 |
by (rtac ballI 1); |
139 |
by (rtac apply_equality 1 THEN (assume_tac 2)); |
|
140 |
by (etac domainE 1); |
|
1196 | 141 |
by (forward_tac [range_type] 1 THEN (assume_tac 1)); |
4091 | 142 |
by (fast_tac (claset() addDs [apply_equality]) 1); |
1196 | 143 |
qed "AC4_AC5"; |
1123 | 144 |
|
145 |
||
146 |
(* ********************************************************************** *) |
|
1461 | 147 |
(* AC5 ==> AC4, Rubin & Rubin, p. 11 *) |
1123 | 148 |
(* ********************************************************************** *) |
149 |
||
5137 | 150 |
Goal "R <= A*B ==> (lam x:R. fst(x)) : R -> A"; |
4091 | 151 |
by (fast_tac (claset() addSIs [lam_type, fst_type]) 1); |
1123 | 152 |
val lemma1 = result(); |
153 |
||
5137 | 154 |
Goalw [range_def] "R <= A*B ==> range(lam x:R. fst(x)) = domain(R)"; |
1206 | 155 |
by (rtac equalityI 1); |
4091 | 156 |
by (fast_tac (claset() addSEs [lamE] |
1461 | 157 |
addEs [subst_elem] |
1932
cc9f1ba8f29a
Tidying: removing redundant args in classical reasoner calls
paulson
parents:
1924
diff
changeset
|
158 |
addSDs [Pair_fst_snd_eq]) 1); |
1206 | 159 |
by (rtac subsetI 1); |
160 |
by (etac domainE 1); |
|
161 |
by (rtac domainI 1); |
|
4091 | 162 |
by (fast_tac (claset() addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1); |
1123 | 163 |
val lemma2 = result(); |
164 |
||
5137 | 165 |
Goal "[| EX f: A->C. P(f,domain(f)); A=B |] ==> EX f: B->C. P(f,B)"; |
1206 | 166 |
by (etac bexE 1); |
1123 | 167 |
by (forward_tac [domain_of_fun] 1); |
2469 | 168 |
by (Fast_tac 1); |
1123 | 169 |
val lemma3 = result(); |
170 |
||
5137 | 171 |
Goal "[| R <= A*B; g: C->R; ALL x:C. (lam z:R. fst(z))` (g`x) = x |] \ |
1461 | 172 |
\ ==> (lam x:C. snd(g`x)): (PROD x:C. R``{x})"; |
1206 | 173 |
by (rtac lam_type 1); |
174 |
by (dtac apply_type 1 THEN (assume_tac 1)); |
|
175 |
by (dtac bspec 1 THEN (assume_tac 1)); |
|
176 |
by (rtac imageI 1); |
|
1123 | 177 |
by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1 |
1461 | 178 |
THEN (REPEAT (assume_tac 1))); |
2469 | 179 |
by (Asm_full_simp_tac 1); |
1123 | 180 |
val lemma4 = result(); |
181 |
||
5137 | 182 |
Goalw AC_defs "AC5 ==> AC4"; |
1123 | 183 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
184 |
by (REPEAT (eresolve_tac [allE,ballE] 1)); |
|
1196 | 185 |
by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2)); |
186 |
by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1)); |
|
4091 | 187 |
by (fast_tac (claset() addSEs [lemma4]) 1); |
1196 | 188 |
qed "AC5_AC4"; |
1123 | 189 |
|
190 |
||
191 |
(* ********************************************************************** *) |
|
1461 | 192 |
(* AC1 <-> AC6 *) |
1123 | 193 |
(* ********************************************************************** *) |
194 |
||
5068 | 195 |
Goalw AC_defs "AC1 <-> AC6"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
196 |
by (Blast_tac 1); |
1196 | 197 |
qed "AC1_iff_AC6"; |
198 |