author  paulson 
Tue, 04 Mar 1997 10:42:28 +0100  
changeset 2717  b29c45ef3d86 
parent 2496  40efb87985b5 
child 4091  771b1f6422a8 
permissions  rwrr 
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}"; 
2469  19 
by (fast_tac (!claset addSEs [apply_type]) 1); 
1123  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"; 
2469  24 
by (fast_tac (!claset addSEs [equals0D]) 1); 
1123  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))); 
2469  33 
by (fast_tac (!claset 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}"; 

2469  42 
by (fast_tac (!claset 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); 
2469  49 
by (fast_tac (!claset addSIs [the_equality] 
1461  50 
addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2); 
2469  51 
by (fast_tac (!claset addSEs [equalityE, make_elim singleton_subsetD]) 1); 
1123  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) "; 

2469  57 
by (fast_tac (!claset 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)); 

2469  65 
by (fast_tac (!claset addSEs [lemma3]) 2); 
66 
by (fast_tac (!claset 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)}"; 

2469  75 
by (fast_tac (!claset addEs [sym RS equals0D]) 1); 
1123  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)); 

2717
b29c45ef3d86
best_tac avoids looping with change to RepFun_eqI in claset
paulson
parents:
2496
diff
changeset

81 
by (best_tac (!claset addSIs [lam_type] 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)"; 

2469  90 
by (fast_tac (!claset addSDs [apply_type]) 1); 
1123  91 
val lemma1 = result(); 
92 

93 
goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}"; 

2496  94 
by (fast_tac (!claset addSIs [not_emptyI] addDs [range_type]) 1); 
1123  95 
val lemma2 = result(); 
96 

97 
goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)"; 

2496  98 
by (Fast_tac 1); 
1123  99 
val lemma3 = result(); 
100 

101 
goalw thy AC_defs "!!Z. AC4 ==> AC3"; 

102 
by (REPEAT (resolve_tac [allI,ballI] 1)); 

103 
by (REPEAT (eresolve_tac [allE,impE] 1)); 

1206  104 
by (etac lemma1 1); 
2469  105 
by (asm_full_simp_tac (!simpset addsimps [lemma2, lemma3] 
1461  106 
addcongs [Pi_cong]) 1); 
1196  107 
qed "AC4_AC3"; 
1123  108 

109 
(* ********************************************************************** *) 

1461  110 
(* AC3 ==> AC1 *) 
1123  111 
(* ********************************************************************** *) 
112 

113 
goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)"; 

2469  114 
by (asm_full_simp_tac (!simpset addsimps [id_def] addcongs [Pi_cong]) 1); 
1123  115 
by (res_inst_tac [("b","A")] subst_context 1); 
2496  116 
by (Fast_tac 1); 
1123  117 
val lemma = result(); 
118 

119 
goalw thy AC_defs "!!Z. AC3 ==> AC1"; 

120 
by (REPEAT (resolve_tac [allI, impI] 1)); 

121 
by (REPEAT (eresolve_tac [allE, ballE] 1)); 

2469  122 
by (fast_tac (!claset addSIs [id_type]) 2); 
123 
by (fast_tac (!claset addEs [lemma RS subst]) 1); 

1196  124 
qed "AC3_AC1"; 
1123  125 

126 
(* ********************************************************************** *) 

1461  127 
(* AC4 ==> AC5 *) 
1123  128 
(* ********************************************************************** *) 
129 

130 
goalw thy (range_def::AC_defs) "!!Z. AC4 ==> AC5"; 

131 
by (REPEAT (resolve_tac [allI,ballI] 1)); 

132 
by (REPEAT (eresolve_tac [allE,impE] 1)); 

133 
by (eresolve_tac [fun_is_rel RS converse_type] 1); 

1206  134 
by (etac exE 1); 
135 
by (rtac bexI 1); 

136 
by (rtac Pi_type 2 THEN (assume_tac 2)); 

2469  137 
by (fast_tac (!claset addSDs [apply_type] 
1461  138 
addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2); 
1206  139 
by (rtac ballI 1); 
140 
by (rtac apply_equality 1 THEN (assume_tac 2)); 

141 
by (etac domainE 1); 

1196  142 
by (forward_tac [range_type] 1 THEN (assume_tac 1)); 
2469  143 
by (fast_tac (!claset addDs [apply_equality]) 1); 
1196  144 
qed "AC4_AC5"; 
1123  145 

146 

147 
(* ********************************************************************** *) 

1461  148 
(* AC5 ==> AC4, Rubin & Rubin, p. 11 *) 
1123  149 
(* ********************************************************************** *) 
150 

151 
goal thy "!!A. R <= A*B ==> (lam x:R. fst(x)) : R > A"; 

2469  152 
by (fast_tac (!claset addSIs [lam_type, fst_type]) 1); 
1123  153 
val lemma1 = result(); 
154 

155 
goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)"; 

1206  156 
by (rtac equalityI 1); 
2469  157 
by (fast_tac (!claset addSEs [lamE] 
1461  158 
addEs [subst_elem] 
1932
cc9f1ba8f29a
Tidying: removing redundant args in classical reasoner calls
paulson
parents:
1924
diff
changeset

159 
addSDs [Pair_fst_snd_eq]) 1); 
1206  160 
by (rtac subsetI 1); 
161 
by (etac domainE 1); 

162 
by (rtac domainI 1); 

2469  163 
by (fast_tac (!claset addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1); 
1123  164 
val lemma2 = result(); 
165 

166 
goal thy "!!A. [ EX f: A>C. P(f,domain(f)); A=B ] ==> EX f: B>C. P(f,B)"; 

1206  167 
by (etac bexE 1); 
1123  168 
by (forward_tac [domain_of_fun] 1); 
2469  169 
by (Fast_tac 1); 
1123  170 
val lemma3 = result(); 
171 

172 
goal thy "!!g. [ R <= A*B; g: C>R; ALL x:C. (lam z:R. fst(z))` (g`x) = x ] \ 

1461  173 
\ ==> (lam x:C. snd(g`x)): (PROD x:C. R``{x})"; 
1206  174 
by (rtac lam_type 1); 
175 
by (dtac apply_type 1 THEN (assume_tac 1)); 

176 
by (dtac bspec 1 THEN (assume_tac 1)); 

177 
by (rtac imageI 1); 

1123  178 
by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1 
1461  179 
THEN (REPEAT (assume_tac 1))); 
2469  180 
by (Asm_full_simp_tac 1); 
1123  181 
val lemma4 = result(); 
182 

183 
goalw thy AC_defs "!!Z. AC5 ==> AC4"; 

184 
by (REPEAT (resolve_tac [allI,impI] 1)); 

185 
by (REPEAT (eresolve_tac [allE,ballE] 1)); 

1196  186 
by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2)); 
187 
by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1)); 

2469  188 
by (fast_tac (!claset addSEs [lemma4]) 1); 
1196  189 
qed "AC5_AC4"; 
1123  190 

191 

192 
(* ********************************************************************** *) 

1461  193 
(* AC1 <> AC6 *) 
1123  194 
(* ********************************************************************** *) 
195 

196 
goalw thy AC_defs "AC1 <> AC6"; 

2469  197 
by (fast_tac (!claset addDs [equals0D] addSEs [not_emptyE]) 1); 
1196  198 
qed "AC1_iff_AC6"; 
199 