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

Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II"
by H. Rubin and J.E. Rubin, 1985.

Axiom AC0 comes from "Axiomatic Set Theory" by P. Suppes, 1972.

Some Isabelle proofs of equivalences of these axioms are formalizations of
proofs presented by the Rubins.  The others are based on the Rubins' proofs,
but slightly changed.
*)

theory AC_Equiv
imports ZF
begin (*obviously not ZFC*)

(* Well Ordering Theorems *)

definition  
    "WO1 ≡ ∀A. ∃R. well_ord(A,R)"

definition  
    "WO2 ≡ ∀A. ∃a. Ord(a) ∧ A≈a"

definition  
    "WO3 ≡ ∀A. ∃a. Ord(a) ∧ (∃b. b ⊆ a ∧ A≈b)"

definition  
    "WO4(m) ≡ ∀A. ∃a f. Ord(a) ∧ domain(f)=a ∧
                         (∪b<a. f`b) = A ∧ (∀b<a. f`b < m)"

definition  
    "WO5 ≡ ∃m ∈ nat. 1≤m ∧ WO4(m)"

definition  
    "WO6 ≡ ∀A. ∃m ∈ nat. 1≤m ∧ (∃a f. Ord(a) ∧ domain(f)=a
                               ∧ (∪b<a. f`b) = A ∧ (∀b<a. f`b < m))"

definition  
    "WO7 ≡ ∀A. Finite(A) ⟷ (∀R. well_ord(A,R) ⟶ well_ord(A,converse(R)))"

definition  
    "WO8 ≡ ∀A. (∃f. f ∈ (∏X ∈ A. X)) ⟶ (∃R. well_ord(A,R))"


definition
(* Auxiliary concepts needed below *)
  pairwise_disjoint :: "i → o"  where
    "pairwise_disjoint(A) ≡ ∀A1 ∈ A. ∀A2 ∈ A. A1 ∩ A2 ≠ 0 ⟶ A1=A2"

definition
  sets_of_size_between :: "[i, i, i] → o"  where
    "sets_of_size_between(A,m,n) ≡ ∀B ∈ A. m < B ∧ B < n"


(* Axioms of Choice *)  
definition
    "AC0 ≡ ∀A. ∃f. f ∈ (∏X ∈ Pow(A)-{0}. X)"

definition
    "AC1 ≡ ∀A. 0∉A ⟶ (∃f. f ∈ (∏X ∈ A. X))"

definition
    "AC2 ≡ ∀A. 0∉A ∧ pairwise_disjoint(A)
                   ⟶ (∃C. ∀B ∈ A. ∃y. B ∩ C = {y})"
definition
    "AC3 ≡ ∀A B. ∀f ∈ A->B. ∃g. g ∈ (∏x ∈ {a ∈ A. f`a≠0}. f`x)"

definition
    "AC4 ≡ ∀R A B. (R ⊆ A*B ⟶ (∃f. f ∈ (∏x ∈ domain(R). R``{x})))"

definition
    "AC5 ≡ ∀A B. ∀f ∈ A->B. ∃g ∈ range(f)->A. ∀x ∈ domain(g). f`(g`x) = x"

definition
    "AC6 ≡ ∀A. 0∉A ⟶ (∏B ∈ A. B)≠0"

definition
    "AC7 ≡ ∀A. 0∉A ∧ (∀B1 ∈ A. ∀B2 ∈ A. B1≈B2) ⟶ (∏B ∈ A. B) ≠ 0"

definition
    "AC8 ≡ ∀A. (∀B ∈ A. ∃B1 B2. B=⟨B1,B2⟩ ∧ B1≈B2)
                   ⟶ (∃f. ∀B ∈ A. f`B ∈ bij(fst(B),snd(B)))"

definition
    "AC9 ≡ ∀A. (∀B1 ∈ A. ∀B2 ∈ A. B1≈B2) ⟶
                   (∃f. ∀B1 ∈ A. ∀B2 ∈ A. f`⟨B1,B2⟩ ∈ bij(B1,B2))"

definition
    "AC10(n) ≡ ∀A. (∀B ∈ A. ¬Finite(B)) ⟶
                   (∃f. ∀B ∈ A. (pairwise_disjoint(f`B) ∧
                   sets_of_size_between(f`B, 2, succ(n)) ∧ ∪(f`B)=B))"

definition
    "AC11 ≡ ∃n ∈ nat. 1≤n ∧ AC10(n)"

definition
    "AC12 ≡ ∀A. (∀B ∈ A. ¬Finite(B)) ⟶
                 (∃n ∈ nat. 1≤n ∧ (∃f. ∀B ∈ A. (pairwise_disjoint(f`B) ∧
                      sets_of_size_between(f`B, 2, succ(n)) ∧ ∪(f`B)=B)))"

definition
    "AC13(m) ≡ ∀A. 0∉A ⟶ (∃f. ∀B ∈ A. f`B≠0 ∧ f`B ⊆ B ∧ f`B < m)"

definition
    "AC14 ≡ ∃m ∈ nat. 1≤m ∧ AC13(m)"

definition
    "AC15 ≡ ∀A. 0∉A ⟶
                 (∃m ∈ nat. 1≤m ∧ (∃f. ∀B ∈ A. f`B≠0 ∧ f`B ⊆ B ∧ f`B < m))"

definition
    "AC16(n, k) ≡
       ∀A. ¬Finite(A) ⟶
           (∃T. T ⊆ {X ∈ Pow(A). X≈succ(n)} ∧
           (∀X ∈ {X ∈ Pow(A). X≈succ(k)}. ∃! Y. Y ∈ T ∧ X ⊆ Y))"

definition
    "AC17 ≡ ∀A. ∀g ∈ (Pow(A)-{0} -> A) -> Pow(A)-{0}.
                   ∃f ∈ Pow(A)-{0} -> A. f`(g`f) ∈ g`f"

locale AC18 =
  assumes AC18: "A≠0 ∧ (∀a ∈ A. B(a) ≠ 0) ⟶
    ((∩a ∈ A. ∪b ∈ B(a). X(a,b)) =
      (∪f ∈ ∏a ∈ A. B(a). ∩a ∈ A. X(a, f`a)))"
  ― ‹AC18 cannot be expressed within the object-logic›

definition
    "AC19 ≡ ∀A. A≠0 ∧ 0∉A ⟶ ((∩a ∈ A. ∪b ∈ a. b) =
                   (∪f ∈ (∏B ∈ A. B). ∩a ∈ A. f`a))"



(* ********************************************************************** *)
(*                    Theorems concerning ordinals                        *)
(* ********************************************************************** *)

(* lemma for ordertype_Int *)
lemma rvimage_id: "rvimage(A,id(A),r) = r ∩ A*A"
  unfolding rvimage_def
apply (rule equalityI, safe)
apply (drule_tac P = "λa. <id (A) `xb,a>:r" in id_conv [THEN subst],
       assumption)
apply (drule_tac P = "λa. ⟨a,ya⟩:r" in id_conv [THEN subst], (assumption+))
apply (fast intro: id_conv [THEN ssubst])
done

(* used only in Hartog.ML *)
lemma ordertype_Int:
     "well_ord(A,r) ==> ordertype(A, r ∩ A*A) = ordertype(A,r)"
apply (rule_tac P = "λa. ordertype (A,a) =ordertype (A,r) " in rvimage_id [THEN subst])
apply (erule id_bij [THEN bij_ordertype_vimage])
done

lemma lam_sing_bij: "(λx ∈ A. {x}) ∈ bij(A, {{x}. x ∈ A})"
apply (rule_tac d = "λz. THE x. z={x}" in lam_bijective)
apply (auto simp add: the_equality)
done

lemma inj_strengthen_type: 
     "[f ∈ inj(A, B); ∧a. a ∈ A ==> f`a ∈ C] ==> f ∈ inj(A,C)"
by (unfold inj_def, blast intro: Pi_type) 

(* ********************************************************************** *)
(* Another elimination rule for \<exists>!                                       *)
(* ********************************************************************** *)

lemma ex1_two_eq: "[∃! x. P(x); P(x); P(y)] ==> x=y"
by blast

(* ********************************************************************** *)
(* Lemmas used in the proofs like WO? \<Longrightarrow> AC?                             *)
(* ********************************************************************** *)

lemma first_in_B:
     "[well_ord(∪(A),r); 0 ∉ A; B ∈ A] ==> (THE b. first(b,B,r)) ∈ B"
by (blast dest!: well_ord_imp_ex1_first
                    [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])

lemma ex_choice_fun: "[well_ord(∪(A), R); 0 ∉ A] ==> ∃f. f ∈ (∏X ∈ A. X)"
by (fast elim!: first_in_B intro!: lam_type)

lemma ex_choice_fun_Pow: "well_ord(A, R) ==> ∃f. f ∈ (∏X ∈ Pow(A)-{0}. X)"
by (fast elim!: well_ord_subset [THEN ex_choice_fun])


(* ********************************************************************** *)
(* Lemmas needed to state when a finite relation is a function.           *)
(*     The criteria are cardinalities of the relation and its domain.     *)
(*     Used in WO6WO1.ML                                                  *)
(* ********************************************************************** *)

(*Using AC we could trivially prove, for all u, domain(u) \<lesssim> u*)
lemma lepoll_m_imp_domain_lepoll_m: 
     "[m ∈ nat; u < m] ==> domain(u) < m"
  unfolding lepoll_def
apply (erule exE)
apply (rule_tac x = "λx ∈ domain(u). μ i. ∃y. ⟨x,y⟩ ∈ u ∧ f`⟨x,y⟩ = i" 
       in exI)
apply (rule_tac d = "λy. fst (converse(f) ` y) " in lam_injective)
apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord] 
                           inj_is_fun [THEN apply_type])
apply (erule domainE)
apply (frule inj_is_fun [THEN apply_type], assumption)
apply (rule LeastI2)
apply (auto elim!: nat_into_Ord [THEN Ord_in_Ord])
done

lemma rel_domain_ex1: 
    "[succ(m) < domain(r); r < succ(m); m ∈ nat] ==> function(r)"
apply (unfold function_def, safe)
apply (rule ccontr) 
apply (fast elim!: lepoll_trans [THEN succ_lepoll_natE] 
                   lepoll_m_imp_domain_lepoll_m [OF _ Diff_sing_lepoll]
            elim: domain_Diff_eq [OF _ not_sym, THEN subst])
done

lemma rel_is_fun:
     "[succ(m) < domain(r); r < succ(m); m ∈ nat;
         r ⊆ A*B; A=domain(r)] ==> r ∈ A->B"
by (simp add: Pi_iff rel_domain_ex1)

end