Theory AC_Equiv
theory AC_Equiv
imports ZF
begin
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
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"
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)))"
definition
"AC19 ≡ ∀A. A≠0 ∧ 0∉A ⟶ ((⋂a ∈ A. ⋃b ∈ a. b) =
(⋃f ∈ (∏B ∈ A. B). ⋂a ∈ A. f`a))"
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
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)
lemma ex1_two_eq: "⟦∃! x. P(x); P(x); P(y)⟧ ⟹ x=y"
by blast
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])
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