Theory AC7_AC9

theory AC7_AC9
imports AC_Equiv
(*  Title:      ZF/AC/AC7_AC9.thy
    Author:     Krzysztof Grabczewski

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

theory AC7_AC9
imports AC_Equiv
begin

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

lemma Sigma_fun_space_not0: "[| 0∉A; B ∈ A |] ==> (nat->\<Union>(A)) * B ≠ 0"
by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1])

lemma inj_lemma: 
        "C ∈ A ==> (λg ∈ (nat->\<Union>(A))*C.   
                (λn ∈ nat. if(n=0, snd(g), fst(g)`(n #- 1))))   
                ∈ inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
apply (unfold inj_def)
apply (rule CollectI)
apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) 
apply (rule fun_extension, assumption+)
apply (drule lam_eqE [OF _ nat_succI], assumption, simp) 
apply (drule lam_eqE [OF _ nat_0I], simp) 
done

lemma Sigma_fun_space_eqpoll:
     "[| C ∈ A; 0∉A |] ==> (nat->\<Union>(A)) * C ≈ (nat->\<Union>(A))"
apply (rule eqpollI)
apply (simp add: lepoll_def)
apply (fast intro!: inj_lemma)
apply (fast elim!: prod_lepoll_self not_sym [THEN not_emptyE] subst_elem 
            elim: swap)
done


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

lemma AC6_AC7: "AC6 ==> AC7"
by (unfold AC6_def AC7_def, blast)

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

lemma lemma1_1: "y ∈ (Π B ∈ A. Y*B) ==> (λB ∈ A. snd(y`B)) ∈ (Π B ∈ A. B)"
by (fast intro!: lam_type snd_type apply_type)

lemma lemma1_2:
     "y ∈ (Π B ∈ {Y*C. C ∈ A}. B) ==> (λB ∈ A. y`(Y*B)) ∈ (Π B ∈ A. Y*B)"
apply (fast intro!: lam_type apply_type)
done

lemma AC7_AC6_lemma1:
     "(Π B ∈ {(nat->\<Union>(A))*C. C ∈ A}. B) ≠ 0 ==> (Π B ∈ A. B) ≠ 0"
by (fast intro!: equals0I lemma1_1 lemma1_2)

lemma AC7_AC6_lemma2: "0 ∉ A ==> 0 ∉ {(nat -> \<Union>(A)) * C. C ∈ A}"
by (blast dest: Sigma_fun_space_not0)

lemma AC7_AC6: "AC7 ==> AC6"
apply (unfold AC6_def AC7_def)
apply (rule allI)
apply (rule impI)
apply (case_tac "A=0", simp)
apply (rule AC7_AC6_lemma1)
apply (erule allE) 
apply (blast del: notI
             intro!: AC7_AC6_lemma2 intro: eqpoll_sym eqpoll_trans 
                    Sigma_fun_space_eqpoll)
done


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

lemma AC1_AC8_lemma1: 
        "∀B ∈ A. ∃B1 B2. B=<B1,B2> & B1 ≈ B2   
        ==> 0 ∉ { bij(fst(B),snd(B)). B ∈ A }"
apply (unfold eqpoll_def, auto)
done

lemma AC1_AC8_lemma2:
     "[| f ∈ (Π X ∈ RepFun(A,p). X); D ∈ A |] ==> (λx ∈ A. f`p(x))`D ∈ p(D)" 
apply (simp, fast elim!: apply_type)
done

lemma AC1_AC8: "AC1 ==> AC8"
apply (unfold AC1_def AC8_def)
apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2)
done


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

lemma AC8_AC9_lemma:
     "∀B1 ∈ A. ∀B2 ∈ A. B1 ≈ B2 
      ==> ∀B ∈ A*A. ∃B1 B2. B=<B1,B2> & B1 ≈ B2"
by fast

lemma AC8_AC9: "AC8 ==> AC9"
apply (unfold AC8_def AC9_def)
apply (intro allI impI)
apply (erule allE)
apply (erule impE, erule AC8_AC9_lemma, force) 
done


(* ********************************************************************** *)
(* 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) ∪ {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.     *)
(* ********************************************************************** *)

lemma snd_lepoll_SigmaI: "b ∈ B ==> X \<lesssim> B × X"
by (blast intro: lepoll_trans prod_lepoll_self eqpoll_imp_lepoll 
                 prod_commute_eqpoll) 

lemma nat_lepoll_lemma:
     "[|0 ∉ A; B ∈ A|] ==> nat \<lesssim> ((nat -> \<Union>(A)) × B) × nat"
by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI)

lemma AC9_AC1_lemma1:
     "[| 0∉A;  A≠0;   
         C = {((nat->\<Union>(A))*B)*nat. B ∈ A}  ∪  
             {cons(0,((nat->\<Union>(A))*B)*nat). B ∈ A};  
         B1 ∈ C;  B2 ∈ C |]   
      ==> B1 ≈ B2"
by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll
                     nat_cons_eqpoll [THEN eqpoll_trans] 
                     prod_eqpoll_cong [OF _ eqpoll_refl]
             intro: eqpoll_trans eqpoll_sym )

lemma AC9_AC1_lemma2:
     "∀B1 ∈ {(F*B)*N. B ∈ A} ∪ {cons(0,(F*B)*N). B ∈ A}.   
      ∀B2 ∈ {(F*B)*N. B ∈ A} ∪ {cons(0,(F*B)*N). B ∈ A}.   
        f`<B1,B2> ∈ bij(B1, B2)   
      ==> (λB ∈ A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) ∈ (Π X ∈ A. X)"
apply (intro lam_type snd_type fst_type)
apply (rule apply_type [OF _ consI1]) 
apply (fast intro!: fun_weaken_type bij_is_fun)
done

lemma AC9_AC1: "AC9 ==> AC1"
apply (unfold AC1_def AC9_def)
apply (intro allI impI)
apply (erule allE)
apply (case_tac "A≠0")
apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force) 
done

end