src/ZF/AC/AC7_AC9.ML

Krzysztof Grabczewski's (nearly) complete AC proofs

(*  Title: 	ZF/AC/AC7-AC9.ML
    ID:         $Id$
    Author: 	Krzysztof Gr`abczewski

The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous
instances of AC.
*)

(* ********************************************************************** *)
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1		  *)
(*  - Sigma_fun_space_not0						  *)
(*  - all_eqpoll_imp_pair_eqpoll					  *)
(*  - Sigma_fun_space_eqpoll						  *)
(* ********************************************************************** *)

goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
by (fast_tac ZF_cs 1);
val mem_not_eq_not_mem = result();

goal thy "!!A. [| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
by (fast_tac (ZF_cs addSDs [Sigma_empty_iff RS iffD1]
		addDs [fun_space_emptyD, mem_not_eq_not_mem]
		addEs [equals0D]
		addSIs [equals0I,UnionI]) 1);
val Sigma_fun_space_not0 = result();

goal thy "!!A C. (ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
by (REPEAT (resolve_tac [ballI] 1));
by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
	THEN REPEAT (atac 1));
val all_eqpoll_imp_pair_eqpoll = result();

goal thy "!!A. [| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A   \
\	|] ==> P(b)=R(b)";
by (dresolve_tac [bspec] 1 THEN (atac 1));
by (asm_full_simp_tac ZF_ss 1);
val if_eqE1 = result();

goal thy "!!A. ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a))  \
\	==> ALL a:A. a~=b --> Q(a)=S(a)";
by (resolve_tac [ballI] 1);
by (resolve_tac [impI] 1);
by (dresolve_tac [bspec] 1 THEN (atac 1));
by (asm_full_simp_tac ZF_ss 1);
val if_eqE2 = result();

goal thy "!!A. [| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
by (fast_tac (ZF_cs addDs [subsetD]
		addSIs [lamI]
		addEs [equalityE, lamE]) 1);
val lam_eqE = result();

goalw thy [inj_def]
	"!!A. C:A ==> (lam g:(nat->Union(A))*C.  \
\		(lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1))))  \
\		: inj((nat->Union(A))*C, (nat->Union(A)) ) ";
by (resolve_tac [CollectI] 1);
by (fast_tac (ZF_cs addSIs [lam_type,RepFunI,if_type,snd_type,apply_type,
				fst_type,diff_type,nat_succI,nat_0I]) 1);
by (REPEAT (resolve_tac [ballI, impI] 1));
by (asm_full_simp_tac ZF_ss 1);
by (REPEAT (eresolve_tac [SigmaE] 1));
by (REPEAT (hyp_subst_tac 1));
by (asm_full_simp_tac ZF_ss 1);
by (resolve_tac [conjI] 1);
by (dresolve_tac [nat_0I RSN (2, lam_eqE)] 2);
by (asm_full_simp_tac AC_ss 2);
by (resolve_tac [fun_extension] 1 THEN  REPEAT (atac 1));
by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (atac 1));
by (asm_full_simp_tac (AC_ss addsimps [succ_not_0 RS if_not_P]) 1);
by (fast_tac (AC_cs addSEs [diff_succ_succ RS (diff_0 RSN (2, trans)) RS subst]
		addSIs [nat_0I]) 1);
val lemma = result();

goal thy "!!A. [| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))";
by (resolve_tac [eqpollI] 1);
by (fast_tac (ZF_cs addSEs [prod_lepoll_self, not_sym RS not_emptyE,
		subst_elem] addEs [swap]) 2);
by (rewrite_goals_tac [lepoll_def]);
by (fast_tac (ZF_cs addSIs [lemma]) 1);
val Sigma_fun_space_eqpoll = result();


(* ********************************************************************** *)
(* AC6 ==> AC7								  *)
(* ********************************************************************** *)

goalw thy AC_defs "!!Z. AC6 ==> AC7";
by (fast_tac ZF_cs 1);
result();

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

goal thy "!!y. y: (PROD B:A. Y*B) ==> (lam B:A. snd(y`B)): (PROD B:A. B)";
by (fast_tac (ZF_cs addSIs [lam_type, snd_type, apply_type]) 1);
val lemma1_1 = result();

goal thy "!!A. y: (PROD B:{Y*C. C:A}. B)  \
\		==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
by (fast_tac (ZF_cs addSIs [lam_type, apply_type]) 1);
val lemma1_2 = result();

goal thy "!!A. (PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0  \
\		==> (PROD B:A. B) ~= 0";
by (fast_tac (ZF_cs addSIs [equals0I,lemma1_1, lemma1_2]
		addSEs [equals0D]) 1);
val lemma1 = result();

goal thy "!!A. 0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
by (fast_tac (ZF_cs addEs [RepFunE,
		Sigma_fun_space_not0 RS not_sym RS notE]) 1);
val lemma2 = result();

goalw thy AC_defs "!!Z. AC7 ==> AC6";
by (resolve_tac [allI] 1);
by (resolve_tac [impI] 1);
by (excluded_middle_tac "A=0" 1);
by (fast_tac (ZF_cs addSIs [not_emptyI, empty_fun]) 2);
by (resolve_tac [lemma1] 1);
by (eresolve_tac [allE] 1);
by (eresolve_tac [impE] 1 THEN (atac 2));
by (fast_tac (AC_cs addSEs [RepFunE]
	addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
		Sigma_fun_space_eqpoll]) 1);
result();


(* ********************************************************************** *)
(* AC1 ==> AC8								  *)
(* ********************************************************************** *)

goalw thy [eqpoll_def]
	"!!A. ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2  \
\	==> 0 ~: { bij(fst(B),snd(B)). B:A }";
by (resolve_tac [notI] 1);
by (eresolve_tac [RepFunE] 1);
by (dresolve_tac [bspec] 1 THEN (atac 1));
by (REPEAT (eresolve_tac [exE,conjE] 1));
by (hyp_subst_tac 1);
by (asm_full_simp_tac AC_ss 1);
by (fast_tac (AC_cs addSEs [sym RS equals0D]) 1);
val lemma1 = result();

goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |]  \
\		==> (lam x:A. f`p(x))`D : p(D)";
by (resolve_tac [beta RS ssubst] 1 THEN (atac 1));
by (fast_tac (AC_cs addSEs [apply_type]) 1);
val lemma2 = result();

goalw thy AC_defs "!!Z. AC1 ==> AC8";
by (resolve_tac [allI] 1);
by (eresolve_tac [allE] 1);
by (resolve_tac [impI] 1);
by (eresolve_tac [impE] 1);
by (eresolve_tac [lemma1] 1);
by (fast_tac (AC_cs addSEs [lemma2]) 1);
result();


(* ********************************************************************** *)
(* AC8 ==> AC9								  *)
(*  - this proof replaces the following two from Rubin & Rubin:		  *)
(*    AC8 ==> AC1 and AC1 ==> AC9					  *)
(* ********************************************************************** *)

goal thy "!!A. ALL B1:A. ALL B2:A. B1 eqpoll B2 ==>  \
\		ALL B:A*A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2";
by (fast_tac ZF_cs 1);
val lemma1 = result();

goal thy "!!f. f:bij(fst(<a,b>),snd(<a,b>)) ==> f:bij(a,b)";
by (asm_full_simp_tac AC_ss 1);
val lemma2 = result();

goalw thy AC_defs "!!Z. AC8 ==> AC9";
by (resolve_tac [allI] 1);
by (resolve_tac [impI] 1);
by (eresolve_tac [allE] 1);
by (eresolve_tac [impE] 1);
by (eresolve_tac [lemma1] 1);
by (fast_tac (AC_cs addSEs [lemma2]) 1);
result();


(* ********************************************************************** *)
(* AC9 ==> AC1								  *)
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to	  *)
(* (x * y) Un {0} when y is a set of total functions acting from nat to	  *)
(* Union(A) -- therefore we have used the set (y * nat) instead of y.	  *)
(* ********************************************************************** *)

(* Rules nedded to prove lemma1 *)
val snd_lepoll_SigmaI = prod_lepoll_self RS 
        ((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
val lemma1_cs = FOL_cs addSEs [UnE, RepFunE]
		addSIs [all_eqpoll_imp_pair_eqpoll, ballI,
			nat_cons_eqpoll RS eqpoll_trans]
		addEs [Sigma_fun_space_not0 RS not_emptyE]
		addIs [snd_lepoll_SigmaI, eqpoll_refl RSN 
			(2, prod_eqpoll_cong), Sigma_fun_space_eqpoll];

goal thy "!!A. [| 0~:A; A~=0 |]  \
\	==> ALL B1: ({((nat->Union(A))*B)*nat. B:A}  \
\		Un {cons(0,((nat->Union(A))*B)*nat). B:A}).  \
\	ALL B2: ({((nat->Union(A))*B)*nat. B:A}  \
\		Un {cons(0,((nat->Union(A))*B)*nat). B:A}).  \
\	B1 eqpoll B2";
by (fast_tac lemma1_cs 1);
val lemma1 = result();

goal thy "!!A. ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}.  \
\	ALL B2:{(F*B)*N. B:A}  \
\	Un {cons(0,(F*B)*N). B:A}. f`<B1,B2> : bij(B1, B2)  \
\	==> (lam B:A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) :  \
\		(PROD X:A. X)";
by (resolve_tac [lam_type] 1);
by (resolve_tac [snd_type] 1);
by (resolve_tac [fst_type] 1);
by (resolve_tac [consI1 RSN (2, apply_type)] 1);
by (fast_tac (ZF_cs addSIs [fun_weaken_type, bij_is_fun]) 1);
val lemma2 = result();

val prems = goalw thy AC_defs "!!Z. AC9 ==> AC1";
by (resolve_tac [allI] 1);
by (resolve_tac [impI] 1);
by (eresolve_tac [allE] 1);
by (excluded_middle_tac "A=0" 1);
by (fast_tac (FOL_cs addSIs [empty_fun]) 2);
by (eresolve_tac [impE] 1);
by (resolve_tac [lemma1] 1 THEN (REPEAT (atac 1)));
by (fast_tac (AC_cs addSEs [lemma2]) 1);
result();