Theory AC17_AC1
theory AC17_AC1
imports HH
begin
lemma AC0_AC1_lemma: "⟦f:(∏X ∈ A. X); D ⊆ A⟧ ⟹ ∃g. g:(∏X ∈ D. X)"
by (fast intro!: lam_type apply_type)
lemma AC0_AC1: "AC0 ⟹ AC1"
unfolding AC0_def AC1_def
apply (blast intro: AC0_AC1_lemma)
done
lemma AC1_AC0: "AC1 ⟹ AC0"
by (unfold AC0_def AC1_def, blast)
lemma AC1_AC17_lemma: "f ∈ (∏X ∈ Pow(A) - {0}. X) ⟹ f ∈ (Pow(A) - {0} -> A)"
apply (rule Pi_type, assumption)
apply (drule apply_type, assumption, fast)
done
lemma AC1_AC17: "AC1 ⟹ AC17"
unfolding AC1_def AC17_def
apply (rule allI)
apply (rule ballI)
apply (erule_tac x = "Pow (A) -{0}" in allE)
apply (erule impE, fast)
apply (erule exE)
apply (rule bexI)
apply (erule_tac [2] AC1_AC17_lemma)
apply (rule apply_type, assumption)
apply (fast dest!: AC1_AC17_lemma elim!: apply_type)
done
lemma UN_eq_imp_well_ord:
"⟦x - (⋃j ∈ μ i. HH(λX ∈ Pow(x)-{0}. {f`X}, x, i) = {x}.
HH(λX ∈ Pow(x)-{0}. {f`X}, x, j)) = 0;
f ∈ Pow(x)-{0} -> x⟧
⟹ ∃r. well_ord(x,r)"
apply (rule exI)
apply (erule well_ord_rvimage
[OF bij_Least_HH_x [THEN bij_converse_bij, THEN bij_is_inj]
Ord_Least [THEN well_ord_Memrel]], assumption)
done
lemma not_AC1_imp_ex:
"¬AC1 ⟹ ∃A. ∀f ∈ Pow(A)-{0} -> A. ∃u ∈ Pow(A)-{0}. f`u ∉ u"
unfolding AC1_def
apply (erule swap)
apply (rule allI)
apply (erule swap)
apply (rule_tac x = "⋃(A)" in exI)
apply (blast intro: lam_type)
done
lemma AC17_AC1_aux1:
"⟦∀f ∈ Pow(x) - {0} -> x. ∃u ∈ Pow(x) - {0}. f`u∉u;
∃f ∈ Pow(x)-{0}->x.
x - (⋃a ∈ (μ i. HH(λX ∈ Pow(x)-{0}. {f`X},x,i)={x}).
HH(λX ∈ Pow(x)-{0}. {f`X},x,a)) = 0⟧
⟹ P"
apply (erule bexE)
apply (erule UN_eq_imp_well_ord [THEN exE], assumption)
apply (erule ex_choice_fun_Pow [THEN exE])
apply (erule ballE)
apply (fast intro: apply_type del: DiffE)
apply (erule notE)
apply (rule Pi_type, assumption)
apply (blast dest: apply_type)
done
lemma AC17_AC1_aux2:
"¬ (∃f ∈ Pow(x)-{0}->x. x - F(f) = 0)
⟹ (λf ∈ Pow(x)-{0}->x . x - F(f))
∈ (Pow(x) -{0} -> x) -> Pow(x) - {0}"
by (fast intro!: lam_type dest!: Diff_eq_0_iff [THEN iffD1])
lemma AC17_AC1_aux3:
"⟦f`Z ∈ Z; Z ∈ Pow(x)-{0}⟧
⟹ (λX ∈ Pow(x)-{0}. {f`X})`Z ∈ Pow(Z)-{0}"
by auto
lemma AC17_AC1_aux4:
"∃f ∈ F. f`((λf ∈ F. Q(f))`f) ∈ (λf ∈ F. Q(f))`f
⟹ ∃f ∈ F. f`Q(f) ∈ Q(f)"
by simp
lemma AC17_AC1: "AC17 ⟹ AC1"
unfolding AC17_def
apply (rule classical)
apply (erule not_AC1_imp_ex [THEN exE])
apply (case_tac
"∃f ∈ Pow(x)-{0} -> x.
x - (⋃a ∈ (μ i. HH (λX ∈ Pow (x) -{0}. {f`X},x,i) ={x}) . HH (λX ∈ Pow (x) -{0}. {f`X},x,a)) = 0")
apply (erule AC17_AC1_aux1, assumption)
apply (drule AC17_AC1_aux2)
apply (erule allE)
apply (drule bspec, assumption)
apply (drule AC17_AC1_aux4)
apply (erule bexE)
apply (drule apply_type, assumption)
apply (simp add: HH_Least_eq_x del: Diff_iff )
apply (drule AC17_AC1_aux3, assumption)
apply (fast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]]
f_subset_imp_HH_subset elim!: mem_irrefl)
done
lemma AC1_AC2_aux1:
"⟦f:(∏X ∈ A. X); B ∈ A; 0∉A⟧ ⟹ {f`B} ⊆ B ∩ {f`C. C ∈ A}"
by (fast elim!: apply_type)
lemma AC1_AC2_aux2:
"⟦pairwise_disjoint(A); B ∈ A; C ∈ A; D ∈ B; D ∈ C⟧ ⟹ f`B = f`C"
by (unfold pairwise_disjoint_def, fast)
lemma AC1_AC2: "AC1 ⟹ AC2"
unfolding AC1_def AC2_def
apply (rule allI)
apply (rule impI)
apply (elim asm_rl conjE allE exE impE, assumption)
apply (intro exI ballI equalityI)
prefer 2 apply (rule AC1_AC2_aux1, assumption+)
apply (fast elim!: AC1_AC2_aux2 elim: apply_type)
done
lemma AC2_AC1_aux1: "0∉A ⟹ 0 ∉ {B*{B}. B ∈ A}"
by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]])
lemma AC2_AC1_aux2: "⟦X*{X} ∩ C = {y}; X ∈ A⟧
⟹ (THE y. X*{X} ∩ C = {y}): X*A"
apply (rule subst_elem [of y])
apply (blast elim!: equalityE)
apply (auto simp add: singleton_eq_iff)
done
lemma AC2_AC1_aux3:
"∀D ∈ {E*{E}. E ∈ A}. ∃y. D ∩ C = {y}
⟹ (λx ∈ A. fst(THE z. (x*{x} ∩ C = {z}))) ∈ (∏X ∈ A. X)"
apply (rule lam_type)
apply (drule bspec, blast)
apply (blast intro: AC2_AC1_aux2 fst_type)
done
lemma AC2_AC1: "AC2 ⟹ AC1"
unfolding AC1_def AC2_def pairwise_disjoint_def
apply (intro allI impI)
apply (elim allE impE)
prefer 2 apply (fast elim!: AC2_AC1_aux3)
apply (blast intro!: AC2_AC1_aux1)
done
lemma empty_notin_images: "0 ∉ {R``{x}. x ∈ domain(R)}"
by blast
lemma AC1_AC4: "AC1 ⟹ AC4"
unfolding AC1_def AC4_def
apply (intro allI impI)
apply (drule spec, drule mp [OF _ empty_notin_images])
apply (best intro!: lam_type elim!: apply_type)
done
lemma AC4_AC3_aux1: "f ∈ A->B ⟹ (⋃z ∈ A. {z}*f`z) ⊆ A*⋃(B)"
by (fast dest!: apply_type)
lemma AC4_AC3_aux2: "domain(⋃z ∈ A. {z}*f(z)) = {a ∈ A. f(a)≠0}"
by blast
lemma AC4_AC3_aux3: "x ∈ A ⟹ (⋃z ∈ A. {z}*f(z))``{x} = f(x)"
by fast
lemma AC4_AC3: "AC4 ⟹ AC3"
unfolding AC3_def AC4_def
apply (intro allI ballI)
apply (elim allE impE)
apply (erule AC4_AC3_aux1)
apply (simp add: AC4_AC3_aux2 AC4_AC3_aux3 cong add: Pi_cong)
done
lemma AC3_AC1_lemma:
"b∉A ⟹ (∏x ∈ {a ∈ A. id(A)`a≠b}. id(A)`x) = (∏x ∈ A. x)"
apply (simp add: id_def cong add: Pi_cong)
apply (rule_tac b = A in subst_context, fast)
done
lemma AC3_AC1: "AC3 ⟹ AC1"
unfolding AC1_def AC3_def
apply (fast intro!: id_type elim: AC3_AC1_lemma [THEN subst])
done
lemma AC4_AC5: "AC4 ⟹ AC5"
unfolding range_def AC4_def AC5_def
apply (intro allI ballI)
apply (elim allE impE)
apply (erule fun_is_rel [THEN converse_type])
apply (erule exE)
apply (rename_tac g)
apply (rule_tac x=g in bexI)
apply (blast dest: apply_equality range_type)
apply (blast intro: Pi_type dest: apply_type fun_is_rel)
done
lemma AC5_AC4_aux1: "R ⊆ A*B ⟹ (λx ∈ R. fst(x)) ∈ R -> A"
by (fast intro!: lam_type fst_type)
lemma AC5_AC4_aux2: "R ⊆ A*B ⟹ range(λx ∈ R. fst(x)) = domain(R)"
by (unfold lam_def, force)
lemma AC5_AC4_aux3: "⟦∃f ∈ A->C. P(f,domain(f)); A=B⟧ ⟹ ∃f ∈ B->C. P(f,B)"
apply (erule bexE)
apply (frule domain_of_fun, fast)
done
lemma AC5_AC4_aux4: "⟦R ⊆ A*B; g ∈ C->R; ∀x ∈ C. (λz ∈ R. fst(z))` (g`x) = x⟧
⟹ (λx ∈ C. snd(g`x)): (∏x ∈ C. R``{x})"
apply (rule lam_type)
apply (force dest: apply_type)
done
lemma AC5_AC4: "AC5 ⟹ AC4"
apply (unfold AC4_def AC5_def, clarify)
apply (elim allE ballE)
apply (drule AC5_AC4_aux3 [OF _ AC5_AC4_aux2], assumption)
apply (fast elim!: AC5_AC4_aux4)
apply (blast intro: AC5_AC4_aux1)
done
lemma AC1_iff_AC6: "AC1 ⟷ AC6"
by (unfold AC1_def AC6_def, blast)
end