author  paulson 
Thu, 10 Sep 1998 17:42:44 +0200  
changeset 5470  855654b691db 
parent 5325  f7a5e06adea1 
child 9683  f87c8c449018 
permissions  rwrr 
1461  1 
(* Title: ZF/AC/AC7AC9.ML 
1123  2 
ID: $Id$ 
1461  3 
Author: Krzysztof Grabczewski 
1123  4 

5 
The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous 

6 
instances of AC. 

7 
*) 

8 

9 
(* ********************************************************************** *) 

1461  10 
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *) 
11 
(*  Sigma_fun_space_not0 *) 

12 
(*  all_eqpoll_imp_pair_eqpoll *) 

13 
(*  Sigma_fun_space_eqpoll *) 

1123  14 
(* ********************************************************************** *) 
15 

5137  16 
Goal "[ 0~:A; B:A ] ==> (nat>Union(A))*B ~= 0"; 
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5265
diff
changeset

17 
by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1, 
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5265
diff
changeset

18 
Union_empty_iff RS iffD1] 
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5265
diff
changeset

19 
addDs [fun_space_emptyD]) 1); 
3731  20 
qed "Sigma_fun_space_not0"; 
1123  21 

5137  22 
Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)"; 
1207  23 
by (REPEAT (rtac ballI 1)); 
1123  24 
by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1 
1461  25 
THEN REPEAT (assume_tac 1)); 
3731  26 
qed "all_eqpoll_imp_pair_eqpoll"; 
1123  27 

5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

28 
Goal "[ ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A ] \ 
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

29 
\ ==> P(b)=R(b)"; 
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

30 
by Auto_tac; 
3731  31 
qed "if_eqE1"; 
1123  32 

5137  33 
Goal "ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \ 
1461  34 
\ ==> ALL a:A. a~=b > Q(a)=S(a)"; 
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

35 
by Auto_tac; 
3731  36 
qed "if_eqE2"; 
1123  37 

5137  38 
Goal "[ (lam x:A. f(x))=(lam x:A. g(x)); a:A ] ==> f(a)=g(a)"; 
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

39 
by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1); 
3731  40 
qed "lam_eqE"; 
1123  41 

5068  42 
Goalw [inj_def] 
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset

43 
"C:A ==> (lam g:(nat>Union(A))*C. \ 
1461  44 
\ (lam n:nat. if(n=0, snd(g), fst(g)`(n # 1)))) \ 
45 
\ : inj((nat>Union(A))*C, (nat>Union(A)) ) "; 

1207  46 
by (rtac CollectI 1); 
4091  47 
by (fast_tac (claset() addSIs [lam_type,RepFunI,if_type,snd_type,apply_type, 
1461  48 
fst_type,diff_type,nat_succI,nat_0I]) 1); 
1123  49 
by (REPEAT (resolve_tac [ballI, impI] 1)); 
2469  50 
by (Asm_full_simp_tac 1); 
1207  51 
by (REPEAT (etac SigmaE 1)); 
1123  52 
by (REPEAT (hyp_subst_tac 1)); 
2469  53 
by (Asm_full_simp_tac 1); 
1207  54 
by (rtac conjI 1); 
1123  55 
by (dresolve_tac [nat_0I RSN (2, lam_eqE)] 2); 
2469  56 
by (Asm_full_simp_tac 2); 
1207  57 
by (rtac fun_extension 1 THEN REPEAT (assume_tac 1)); 
1196  58 
by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (assume_tac 1)); 
4091  59 
by (asm_full_simp_tac (simpset() addsimps [succ_not_0 RS if_not_P]) 1); 
1123  60 
val lemma = result(); 
61 

5137  62 
Goal "[ C:A; 0~:A ] ==> (nat>Union(A)) * C eqpoll (nat>Union(A))"; 
1207  63 
by (rtac eqpollI 1); 
4091  64 
by (fast_tac (claset() addSEs [prod_lepoll_self, not_sym RS not_emptyE, 
1461  65 
subst_elem] addEs [swap]) 2); 
1207  66 
by (rewtac lepoll_def); 
4091  67 
by (fast_tac (claset() addSIs [lemma]) 1); 
3731  68 
qed "Sigma_fun_space_eqpoll"; 
1123  69 

70 

71 
(* ********************************************************************** *) 

1461  72 
(* AC6 ==> AC7 *) 
1123  73 
(* ********************************************************************** *) 
74 

5137  75 
Goalw AC_defs "AC6 ==> AC7"; 
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

76 
by (Blast_tac 1); 
1196  77 
qed "AC6_AC7"; 
1123  78 

79 
(* ********************************************************************** *) 

1461  80 
(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *) 
81 
(* The case of the empty family of sets added in order to complete *) 

82 
(* the proof. *) 

1123  83 
(* ********************************************************************** *) 
84 

5137  85 
Goal "y: (PROD B:A. Y*B) ==> (lam B:A. snd(y`B)): (PROD B:A. B)"; 
4091  86 
by (fast_tac (claset() addSIs [lam_type, snd_type, apply_type]) 1); 
1123  87 
val lemma1_1 = result(); 
88 

5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

89 
Goal "y: (PROD B:{Y*C. C:A}. B) ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)"; 
4091  90 
by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); 
1123  91 
val lemma1_2 = result(); 
92 

5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset

93 
Goal "(PROD B:{(nat>Union(A))*C. C:A}. B) ~= 0 ==> (PROD B:A. B) ~= 0"; 
5470  94 
by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]) 1); 
1123  95 
val lemma1 = result(); 
96 

5137  97 
Goal "0 ~: A ==> 0 ~: {(nat > Union(A)) * C. C:A}"; 
5241  98 
by (fast_tac (claset() addEs [Sigma_fun_space_not0 RS not_sym RS notE]) 1); 
1123  99 
val lemma2 = result(); 
100 

5137  101 
Goalw AC_defs "AC7 ==> AC6"; 
1207  102 
by (rtac allI 1); 
103 
by (rtac impI 1); 

1123  104 
by (excluded_middle_tac "A=0" 1); 
4091  105 
by (fast_tac (claset() addSIs [not_emptyI, empty_fun]) 2); 
1207  106 
by (rtac lemma1 1); 
107 
by (etac allE 1); 

108 
by (etac impE 1 THEN (assume_tac 2)); 

5241  109 
by (fast_tac (claset() addSIs [lemma2, all_eqpoll_imp_pair_eqpoll, 
110 
Sigma_fun_space_eqpoll]) 1); 

1196  111 
qed "AC7_AC6"; 
1123  112 

113 

114 
(* ********************************************************************** *) 

1461  115 
(* AC1 ==> AC8 *) 
1123  116 
(* ********************************************************************** *) 
117 

5068  118 
Goalw [eqpoll_def] 
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset

119 
"ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2 \ 
1461  120 
\ ==> 0 ~: { bij(fst(B),snd(B)). B:A }"; 
5241  121 
by Auto_tac; 
1123  122 
val lemma1 = result(); 
123 

5241  124 
Goal "[ f: (PROD X:RepFun(A,p). X); D:A ] ==> (lam x:A. f`p(x))`D : p(D)"; 
1196  125 
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); 
4091  126 
by (fast_tac (claset() addSEs [apply_type]) 1); 
1123  127 
val lemma2 = result(); 
128 

5137  129 
Goalw AC_defs "AC1 ==> AC8"; 
5241  130 
by (Clarify_tac 1); 
131 
by (dtac lemma1 1); 

4091  132 
by (fast_tac (claset() addSEs [lemma2]) 1); 
1196  133 
qed "AC1_AC8"; 
1123  134 

135 

136 
(* ********************************************************************** *) 

1461  137 
(* AC8 ==> AC9 *) 
138 
(*  this proof replaces the following two from Rubin & Rubin: *) 

139 
(* AC8 ==> AC1 and AC1 ==> AC9 *) 

1123  140 
(* ********************************************************************** *) 
141 

5137  142 
Goal "ALL B1:A. ALL B2:A. B1 eqpoll B2 ==> \ 
1461  143 
\ ALL B:A*A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2"; 
2469  144 
by (Fast_tac 1); 
1123  145 
val lemma1 = result(); 
146 

5137  147 
Goal "f:bij(fst(<a,b>),snd(<a,b>)) ==> f:bij(a,b)"; 
2469  148 
by (Asm_full_simp_tac 1); 
1123  149 
val lemma2 = result(); 
150 

5137  151 
Goalw AC_defs "AC8 ==> AC9"; 
1207  152 
by (rtac allI 1); 
153 
by (rtac impI 1); 

154 
by (etac allE 1); 

155 
by (etac impE 1); 

156 
by (etac lemma1 1); 

4091  157 
by (fast_tac (claset() addSEs [lemma2]) 1); 
1196  158 
qed "AC8_AC9"; 
1123  159 

160 

161 
(* ********************************************************************** *) 

1461  162 
(* AC9 ==> AC1 *) 
1123  163 
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *) 
1461  164 
(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *) 
165 
(* (x * y) Un {0} when y is a set of total functions acting from nat to *) 

166 
(* Union(A)  therefore we have used the set (y * nat) instead of y. *) 

1123  167 
(* ********************************************************************** *) 
168 

169 
(* Rules nedded to prove lemma1 *) 

170 
val snd_lepoll_SigmaI = prod_lepoll_self RS 

171 
((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans)); 

2469  172 

1123  173 

5137  174 
Goal "[ 0~:A; A~=0 ] \ 
1461  175 
\ ==> ALL B1: ({((nat>Union(A))*B)*nat. B:A} \ 
176 
\ Un {cons(0,((nat>Union(A))*B)*nat). B:A}). \ 

177 
\ ALL B2: ({((nat>Union(A))*B)*nat. B:A} \ 

178 
\ Un {cons(0,((nat>Union(A))*B)*nat). B:A}). \ 

179 
\ B1 eqpoll B2"; 

4091  180 
by (fast_tac (claset() addSIs [all_eqpoll_imp_pair_eqpoll, ballI, 
2469  181 
nat_cons_eqpoll RS eqpoll_trans] 
182 
addEs [Sigma_fun_space_not0 RS not_emptyE] 

183 
addIs [snd_lepoll_SigmaI, eqpoll_refl RSN 

184 
(2, prod_eqpoll_cong), Sigma_fun_space_eqpoll]) 1); 

1123  185 
val lemma1 = result(); 
186 

5137  187 
Goal "ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}. \ 
1461  188 
\ ALL B2:{(F*B)*N. B:A} \ 
189 
\ Un {cons(0,(F*B)*N). B:A}. f`<B1,B2> : bij(B1, B2) \ 

190 
\ ==> (lam B:A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) : \ 

191 
\ (PROD X:A. X)"; 

1207  192 
by (rtac lam_type 1); 
193 
by (rtac snd_type 1); 

194 
by (rtac fst_type 1); 

1123  195 
by (resolve_tac [consI1 RSN (2, apply_type)] 1); 
4091  196 
by (fast_tac (claset() addSIs [fun_weaken_type, bij_is_fun]) 1); 
1123  197 
val lemma2 = result(); 
198 

5137  199 
Goalw AC_defs "AC9 ==> AC1"; 
1207  200 
by (rtac allI 1); 
201 
by (rtac impI 1); 

202 
by (etac allE 1); 

1123  203 
by (excluded_middle_tac "A=0" 1); 
1207  204 
by (etac impE 1); 
205 
by (rtac lemma1 1 THEN (REPEAT (assume_tac 1))); 

4091  206 
by (fast_tac (claset() addSEs [lemma2]) 1); 
207 
by (fast_tac (claset() addSIs [empty_fun]) 1); 

1196  208 
qed "AC9_AC1"; 