# Theory AC7_AC9

Up to index of Isabelle/ZF/AC

theory AC7_AC9
imports AC_Equiv
begin

    (*  Title:      ZF/AC/AC7_AC9.thy
        ID:         $Id: AC7_AC9.thy,v 1.3 2005/06/17 14:15:10 haftmann Exp $
        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) 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.     *)
    (* ********************************************************************** *)

    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}  Un
                 {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} Un {cons(0,(F*B)*N). B ∈ A}.
          ∀B2 ∈ {(F*B)*N. B ∈ A} Un {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

lemma Sigma_fun_space_not0:

      [| 0 ∉ A; B ∈ A |] ==> (nat -> \<Union>A) × B ≠ 0

lemma inj_lemma:

      C ∈ A
      ==> (λg∈(nat -> \<Union>A) × C.
              λn∈nat. if n = 0 then snd(g) else fst(g) ` (n #- 1)) ∈
          inj((nat -> \<Union>A) × C, nat -> \<Union>A)

lemma Sigma_fun_space_eqpoll:

      [| C ∈ A; 0 ∉ A |] ==> (nat -> \<Union>A) × C ≈ nat -> \<Union>A

lemma AC6_AC7:

      AC6 ==> AC7

lemma lemma1_1:

      y ∈ (ΠB∈A. Y × B) ==> (λB∈A. snd(y ` B)) ∈ (ΠB∈A. B)

lemma lemma1_2:

      y ∈ (ΠB∈{Y × C . C ∈ A}. B) ==> (λB∈A. y ` (Y × B)) ∈ (ΠB∈A. Y × B)

lemma AC7_AC6_lemma1:

      (ΠB∈{(nat -> \<Union>A) × C . C ∈ A}. B) ≠ 0 ==> (ΠB∈A. B) ≠ 0

lemma AC7_AC6_lemma2:

      0 ∉ A ==> 0 ∉ {(nat -> \<Union>A) × C . C ∈ A}

lemma AC7_AC6:

      AC7 ==> AC6

lemma AC1_AC8_lemma1:

      ∀B∈A. ∃B1 B2. B = ⟨B1, B2⟩ ∧ B1 ≈ B2 ==> 0 ∉ {bij(fst(B), snd(B)) . B ∈ A}

lemma AC1_AC8_lemma2:

      [| f ∈ (ΠX∈RepFun(A, p). X); D ∈ A |] ==> (λx∈A. f ` p(x)) ` D ∈ p(D)

lemma AC1_AC8:

      AC1 ==> AC8

lemma AC8_AC9_lemma:

      ∀B1∈A. ∀B2∈A. B1 ≈ B2 ==> ∀B∈A × A. ∃B1 B2. B = ⟨B1, B2⟩ ∧ B1 ≈ B2

lemma AC8_AC9:

      AC8 ==> AC9

lemma snd_lepoll_SigmaI:

      b ∈ B ==> X lepoll B × X

lemma nat_lepoll_lemma:

      [| 0 ∉ A; B ∈ A |] ==> nat lepoll ((nat -> \<Union>A) × B) × nat

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.0 ∈ C; B2.0 ∈ C |]
      ==> B1.0 ≈ B2.0

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)

lemma AC9_AC1:

      AC9 ==> AC1