Theory AC15_WO6
theory AC15_WO6
imports HH Cardinal_aux
begin
lemma lepoll_Sigma: "A≠0 ⟹ B ≲ A*B"
unfolding lepoll_def
apply (erule not_emptyE)
apply (rule_tac x = "λz ∈ B. ⟨x,z⟩" in exI)
apply (fast intro!: snd_conv lam_injective)
done
lemma cons_times_nat_not_Finite:
"0∉A ⟹ ∀B ∈ {cons(0,x*nat). x ∈ A}. ¬Finite(B)"
apply clarify
apply (rule nat_not_Finite [THEN notE] )
apply (subgoal_tac "x ≠ 0")
apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
done
lemma lemma1: "⟦⋃(C)=A; a ∈ A⟧ ⟹ ∃B ∈ C. a ∈ B ∧ B ⊆ A"
by fast
lemma lemma2:
"⟦pairwise_disjoint(A); B ∈ A; C ∈ A; a ∈ B; a ∈ C⟧ ⟹ B=C"
by (unfold pairwise_disjoint_def, blast)
lemma lemma3:
"∀B ∈ {cons(0, x*nat). x ∈ A}. pairwise_disjoint(f`B) ∧
sets_of_size_between(f`B, 2, n) ∧ ⋃(f`B)=B
⟹ ∀B ∈ A. ∃! u. u ∈ f`cons(0, B*nat) ∧ u ⊆ cons(0, B*nat) ∧
0 ∈ u ∧ 2 ≲ u ∧ u ≲ n"
unfolding sets_of_size_between_def
apply (rule ballI)
apply (erule_tac x="cons(0, B*nat)" in ballE)
apply (blast dest: lemma1 intro!: lemma2, blast)
done
lemma lemma4: "⟦A ≲ i; Ord(i)⟧ ⟹ {P(a). a ∈ A} ≲ i"
unfolding lepoll_def
apply (erule exE)
apply (rule_tac x = "λx ∈ RepFun(A,P). μ j. ∃a∈A. x=P(a) ∧ f`a=j"
in exI)
apply (rule_tac d = "λy. P (converse (f) `y) " in lam_injective)
apply (erule RepFunE)
apply (frule inj_is_fun [THEN apply_type], assumption)
apply (fast intro: LeastI2 elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
apply (erule RepFunE)
apply (rule LeastI2)
apply fast
apply (fast elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
apply (fast elim: sym left_inverse [THEN ssubst])
done
lemma lemma5_1:
"⟦B ∈ A; 2 ≲ u(B)⟧ ⟹ (λx ∈ A. {fst(x). x ∈ u(x)-{0}})`B ≠ 0"
apply simp
apply (fast dest: lepoll_Diff_sing
elim: lepoll_trans [THEN succ_lepoll_natE] ssubst
intro!: lepoll_refl)
done
lemma lemma5_2:
"⟦B ∈ A; u(B) ⊆ cons(0, B*nat)⟧
⟹ (λx ∈ A. {fst(x). x ∈ u(x)-{0}})`B ⊆ B"
apply auto
done
lemma lemma5_3:
"⟦n ∈ nat; B ∈ A; 0 ∈ u(B); u(B) ≲ succ(n)⟧
⟹ (λx ∈ A. {fst(x). x ∈ u(x)-{0}})`B ≲ n"
apply simp
apply (fast elim!: Diff_lepoll [THEN lemma4 [OF _ nat_into_Ord]])
done
lemma ex_fun_AC13_AC15:
"⟦∀B ∈ {cons(0, x*nat). x ∈ A}.
pairwise_disjoint(f`B) ∧
sets_of_size_between(f`B, 2, succ(n)) ∧ ⋃(f`B)=B;
n ∈ nat⟧
⟹ ∃f. ∀B ∈ A. f`B ≠ 0 ∧ f`B ⊆ B ∧ f`B ≲ n"
by (fast del: subsetI notI
dest!: lemma3 theI intro!: lemma5_1 lemma5_2 lemma5_3)
theorem AC10_AC11: "⟦n ∈ nat; 1≤n; AC10(n)⟧ ⟹ AC11"
by (unfold AC10_def AC11_def, blast)
theorem AC11_AC12: "AC11 ⟹ AC12"
by (unfold AC10_def AC11_def AC11_def AC12_def, blast)
theorem AC12_AC15: "AC12 ⟹ AC15"
unfolding AC12_def AC15_def
apply (blast del: ballI
intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
done
lemma OUN_eq_UN: "Ord(x) ⟹ (⋃a<x. F(a)) = (⋃a ∈ x. F(a))"
by (fast intro!: ltI dest!: ltD)
lemma AC15_WO6_aux1:
"∀x ∈ Pow(A)-{0}. f`x≠0 ∧ f`x ⊆ x ∧ f`x ≲ m
⟹ (⋃i<μ x. HH(f,A,x)={A}. HH(f,A,i)) = A"
apply (simp add: Ord_Least [THEN OUN_eq_UN])
apply (rule equalityI)
apply (fast dest!: less_Least_subset_x)
apply (blast del: subsetI
intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]])
done
lemma AC15_WO6_aux2:
"∀x ∈ Pow(A)-{0}. f`x≠0 ∧ f`x ⊆ x ∧ f`x ≲ m
⟹ ∀x < (μ x. HH(f,A,x)={A}). HH(f,A,x) ≲ m"
apply (rule oallI)
apply (drule ltD [THEN less_Least_subset_x])
apply (frule HH_subset_imp_eq)
apply (erule ssubst)
apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2])
done
theorem AC15_WO6: "AC15 ⟹ WO6"
unfolding AC15_def WO6_def
apply (rule allI)
apply (erule_tac x = "Pow (A) -{0}" in allE)
apply (erule impE, fast)
apply (elim bexE conjE exE)
apply (rule bexI)
apply (rule conjI, assumption)
apply (rule_tac x = "μ i. HH (f,A,i) ={A}" in exI)
apply (rule_tac x = "λj ∈ (μ i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
apply (simp_all add: ltD)
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2)
done
theorem AC10_AC13: "⟦n ∈ nat; 1≤n; AC10(n)⟧ ⟹ AC13(n)"
apply (unfold AC10_def AC13_def, safe)
apply (erule allE)
apply (erule impE [OF _ cons_times_nat_not_Finite], assumption)
apply (fast elim!: impE [OF _ cons_times_nat_not_Finite]
dest!: ex_fun_AC13_AC15)
done
lemma AC1_AC13: "AC1 ⟹ AC13(1)"
unfolding AC1_def AC13_def
apply (rule allI)
apply (erule allE)
apply (rule impI)
apply (drule mp, assumption)
apply (elim exE)
apply (rule_tac x = "λx ∈ A. {f`x}" in exI)
apply (simp add: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll])
done
lemma AC13_mono: "⟦m≤n; AC13(m)⟧ ⟹ AC13(n)"
unfolding AC13_def
apply (drule le_imp_lepoll)
apply (fast elim!: lepoll_trans)
done
theorem AC13_AC14: "⟦n ∈ nat; 1≤n; AC13(n)⟧ ⟹ AC14"
by (unfold AC13_def AC14_def, auto)
theorem AC14_AC15: "AC14 ⟹ AC15"
by (unfold AC13_def AC14_def AC15_def, fast)
lemma lemma_aux: "⟦A≠0; A ≲ 1⟧ ⟹ ∃a. A={a}"
by (fast elim!: not_emptyE lepoll_1_is_sing)
lemma AC13_AC1_lemma:
"∀B ∈ A. f(B)≠0 ∧ f(B)<=B ∧ f(B) ≲ 1
⟹ (λx ∈ A. THE y. f(x)={y}) ∈ (∏X ∈ A. X)"
apply (rule lam_type)
apply (drule bspec, assumption)
apply (elim conjE)
apply (erule lemma_aux [THEN exE], assumption)
apply (simp add: the_equality)
done
theorem AC13_AC1: "AC13(1) ⟹ AC1"
unfolding AC13_def AC1_def
apply (fast elim!: AC13_AC1_lemma)
done
theorem AC11_AC14: "AC11 ⟹ AC14"
unfolding AC11_def AC14_def
apply (fast intro!: AC10_AC13)
done
end