Theory WO2_AC16
theory WO2_AC16 imports AC_Equiv AC16_lemmas Cardinal_aux begin
definition
recfunAC16 :: "[i,i,i,i] ⇒ i" where
"recfunAC16(f,h,i,a) ≡
transrec2(i, 0,
λg r. if (∃y ∈ r. h`g ⊆ y) then r
else r ∪ {f`(μ i. h`g ⊆ f`i ∧
(∀b<a. (h`b ⊆ f`i ⟶ (∀t ∈ r. ¬ h`b ⊆ t))))})"
lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0"
by (simp add: recfunAC16_def)
lemma recfunAC16_succ:
"recfunAC16(f,h,succ(i),a) =
(if (∃y ∈ recfunAC16(f,h,i,a). h ` i ⊆ y) then recfunAC16(f,h,i,a)
else recfunAC16(f,h,i,a) ∪
{f ` (μ j. h ` i ⊆ f ` j ∧
(∀b<a. (h`b ⊆ f`j
⟶ (∀t ∈ recfunAC16(f,h,i,a). ¬ h`b ⊆ t))))})"
apply (simp add: recfunAC16_def)
done
lemma recfunAC16_Limit: "Limit(i)
⟹ recfunAC16(f,h,i,a) = (⋃j<i. recfunAC16(f,h,j,a))"
by (simp add: recfunAC16_def transrec2_Limit)
lemma transrec2_mono_lemma [rule_format]:
"⟦⋀g r. r ⊆ B(g,r); Ord(i)⟧
⟹ j<i ⟶ transrec2(j, 0, B) ⊆ transrec2(i, 0, B)"
apply (erule trans_induct)
apply (rule Ord_cases, assumption+, fast)
apply (simp (no_asm_simp))
apply (blast elim!: leE)
apply (simp add: transrec2_Limit)
apply (blast intro: OUN_I ltI Ord_in_Ord [THEN le_refl]
elim!: Limit_has_succ [THEN ltE])
done
lemma transrec2_mono:
"⟦⋀g r. r ⊆ B(g,r); j≤i⟧
⟹ transrec2(j, 0, B) ⊆ transrec2(i, 0, B)"
apply (erule leE)
apply (rule transrec2_mono_lemma)
apply (auto intro: lt_Ord2 )
done
lemma recfunAC16_mono:
"i≤j ⟹ recfunAC16(f, g, i, a) ⊆ recfunAC16(f, g, j, a)"
unfolding recfunAC16_def
apply (rule transrec2_mono, auto)
done
lemma lemma3_1:
"⟦∀y<x. ∀z<a. z<y | (∃Y ∈ F(y). f(z)<=Y) ⟶ (∃! Y. Y ∈ F(y) ∧ f(z)<=Y);
∀i j. i≤j ⟶ F(i) ⊆ F(j); j≤i; i<x; z<a;
V ∈ F(i); f(z)<=V; W ∈ F(j); f(z)<=W⟧
⟹ V = W"
apply (erule asm_rl allE impE)+
apply (drule subsetD, assumption, blast)
done
lemma lemma3:
"⟦∀y<x. ∀z<a. z<y | (∃Y ∈ F(y). f(z)<=Y) ⟶ (∃! Y. Y ∈ F(y) ∧ f(z)<=Y);
∀i j. i≤j ⟶ F(i) ⊆ F(j); i<x; j<x; z<a;
V ∈ F(i); f(z)<=V; W ∈ F(j); f(z)<=W⟧
⟹ V = W"
apply (rule_tac j=j in Ord_linear_le [OF lt_Ord lt_Ord], assumption+)
apply (erule lemma3_1 [symmetric], assumption+)
apply (erule lemma3_1, assumption+)
done
lemma lemma4:
"⟦∀y<x. F(y) ⊆ X ∧
(∀x<a. x < y | (∃Y ∈ F(y). h(x) ⊆ Y) ⟶
(∃! Y. Y ∈ F(y) ∧ h(x) ⊆ Y));
x < a⟧
⟹ ∀y<x. ∀z<a. z < y | (∃Y ∈ F(y). h(z) ⊆ Y) ⟶
(∃! Y. Y ∈ F(y) ∧ h(z) ⊆ Y)"
apply (intro oallI impI)
apply (drule ospec, assumption, clarify)
apply (blast elim!: oallE )
done
lemma lemma5:
"⟦∀y<x. F(y) ⊆ X ∧
(∀x<a. x < y | (∃Y ∈ F(y). h(x) ⊆ Y) ⟶
(∃! Y. Y ∈ F(y) ∧ h(x) ⊆ Y));
x < a; Limit(x); ∀i j. i≤j ⟶ F(i) ⊆ F(j)⟧
⟹ (⋃x<x. F(x)) ⊆ X ∧
(∀xa<a. xa < x | (∃x ∈ ⋃x<x. F(x). h(xa) ⊆ x)
⟶ (∃! Y. Y ∈ (⋃x<x. F(x)) ∧ h(xa) ⊆ Y))"
apply (rule conjI)
apply (rule subsetI)
apply (erule OUN_E)
apply (drule ospec, assumption, fast)
apply (drule lemma4, assumption)
apply (rule oallI)
apply (rule impI)
apply (erule disjE)
apply (frule ospec, erule Limit_has_succ, assumption)
apply (drule_tac A = a and x = xa in ospec, assumption)
apply (erule impE, rule le_refl [THEN disjI1], erule lt_Ord)
apply (blast intro: lemma3 Limit_has_succ)
apply (blast intro: lemma3)
done
lemma dbl_Diff_eqpoll_Card:
"⟦A≈a; Card(a); ¬Finite(a); B≺a; C≺a⟧ ⟹ A - B - C≈a"
by (blast intro: Diff_lesspoll_eqpoll_Card)
lemma Finite_lesspoll_infinite_Ord:
"⟦Finite(X); ¬Finite(a); Ord(a)⟧ ⟹ X≺a"
unfolding lesspoll_def
apply (rule conjI)
apply (drule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption)
unfolding Finite_def
apply (blast intro: leI [THEN le_imp_subset, THEN subset_imp_lepoll]
ltI eqpoll_imp_lepoll lepoll_trans)
apply (blast intro: eqpoll_sym [THEN eqpoll_trans])
done
lemma Union_lesspoll:
"⟦∀x ∈ X. x ≲ n ∧ x ⊆ T; well_ord(T, R); X ≲ b;
b<a; ¬Finite(a); Card(a); n ∈ nat⟧
⟹ ⋃(X)≺a"
apply (case_tac "Finite (X)")
apply (blast intro: Card_is_Ord Finite_lesspoll_infinite_Ord
lepoll_nat_imp_Finite Finite_Union)
apply (drule lepoll_imp_ex_le_eqpoll)
apply (erule lt_Ord)
apply (elim exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (erule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1],
THEN exE])
apply (frule bij_is_surj [THEN surj_image_eq])
apply (drule image_fun [OF bij_is_fun subset_refl])
apply (drule sym [THEN trans], assumption)
apply (blast intro: lt_Ord UN_lepoll lt_Card_imp_lesspoll
lt_trans1 lesspoll_trans1)
done
lemma Un_sing_eq_cons: "A ∪ {a} = cons(a, A)"
by fast
lemma Un_lepoll_succ: "A ≲ B ⟹ A ∪ {a} ≲ succ(B)"
apply (simp add: Un_sing_eq_cons succ_def)
apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
done
lemma Diff_UN_succ_empty: "Ord(a) ⟹ F(a) - (⋃b<succ(a). F(b)) = 0"
by (fast intro!: le_refl)
lemma Diff_UN_succ_subset: "Ord(a) ⟹ F(a) ∪ X - (⋃b<succ(a). F(b)) ⊆ X"
by blast
lemma recfunAC16_Diff_lepoll_1:
"Ord(x)
⟹ recfunAC16(f, g, x, a) - (⋃i<x. recfunAC16(f, g, i, a)) ≲ 1"
apply (erule Ord_cases)
apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll])
prefer 2 apply (simp add: recfunAC16_Limit Diff_cancel
empty_subsetI [THEN subset_imp_lepoll])
apply (simp add: recfunAC16_succ
Diff_UN_succ_empty [of _ "λj. recfunAC16(f,g,j,a)"]
empty_subsetI [THEN subset_imp_lepoll])
apply (best intro: Diff_UN_succ_subset [THEN subset_imp_lepoll]
singleton_eqpoll_1 [THEN eqpoll_imp_lepoll] lepoll_trans)
done
lemma in_Least_Diff:
"⟦z ∈ F(x); Ord(x)⟧
⟹ z ∈ F(μ i. z ∈ F(i)) - (⋃j<(μ i. z ∈ F(i)). F(j))"
by (fast elim: less_LeastE elim!: LeastI)
lemma Least_eq_imp_ex:
"⟦(μ i. w ∈ F(i)) = (μ i. z ∈ F(i));
w ∈ (⋃i<a. F(i)); z ∈ (⋃i<a. F(i))⟧
⟹ ∃b<a. w ∈ (F(b) - (⋃c<b. F(c))) ∧ z ∈ (F(b) - (⋃c<b. F(c)))"
apply (elim OUN_E)
apply (drule in_Least_Diff, erule lt_Ord)
apply (frule in_Least_Diff, erule lt_Ord)
apply (rule oexI, force)
apply (blast intro: lt_Ord Least_le [THEN lt_trans1])
done
lemma two_in_lepoll_1: "⟦A ≲ 1; a ∈ A; b ∈ A⟧ ⟹ a=b"
by (fast dest!: lepoll_1_is_sing)
lemma UN_lepoll_index:
"⟦∀i<a. F(i)-(⋃j<i. F(j)) ≲ 1; Limit(a)⟧
⟹ (⋃x<a. F(x)) ≲ a"
apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
apply (rule_tac x = "λz ∈ (⋃x<a. F (x)). μ i. z ∈ F (i) " in exI)
unfolding inj_def
apply (rule CollectI)
apply (rule lam_type)
apply (erule OUN_E)
apply (erule Least_in_Ord)
apply (erule ltD)
apply (erule lt_Ord2)
apply (intro ballI)
apply (simp (no_asm_simp))
apply (rule impI)
apply (drule Least_eq_imp_ex, assumption+)
apply (fast elim!: two_in_lepoll_1)
done
lemma recfunAC16_lepoll_index: "Ord(y) ⟹ recfunAC16(f, h, y, a) ≲ y"
apply (erule trans_induct3)
apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl)
apply (simp (no_asm_simp) add: recfunAC16_succ)
apply (blast dest!: succI1 [THEN rev_bspec]
intro: subset_succI [THEN subset_imp_lepoll] Un_lepoll_succ
lepoll_trans)
apply (simp (no_asm_simp) add: recfunAC16_Limit)
apply (blast intro: lt_Ord [THEN recfunAC16_Diff_lepoll_1] UN_lepoll_index)
done
lemma Union_recfunAC16_lesspoll:
"⟦recfunAC16(f,g,y,a) ⊆ {X ∈ Pow(A). X≈n};
A≈a; y<a; ¬Finite(a); Card(a); n ∈ nat⟧
⟹ ⋃(recfunAC16(f,g,y,a))≺a"
apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE])
apply (rule_tac T=A in Union_lesspoll, simp_all)
apply (blast intro!: eqpoll_imp_lepoll)
apply (blast intro: bij_is_inj Card_is_Ord [THEN well_ord_Memrel]
well_ord_rvimage)
apply (erule lt_Ord [THEN recfunAC16_lepoll_index])
done
lemma dbl_Diff_eqpoll:
"⟦recfunAC16(f, h, y, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)};
Card(a); ¬ Finite(a); A≈a;
k ∈ nat; y<a;
h ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k)})⟧
⟹ A - ⋃(recfunAC16(f, h, y, a)) - h`y≈a"
apply (rule dbl_Diff_eqpoll_Card, simp_all)
apply (simp add: Union_recfunAC16_lesspoll)
apply (rule Finite_lesspoll_infinite_Ord)
apply (rule Finite_def [THEN def_imp_iff, THEN iffD2])
apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)
apply (blast intro: Card_is_Ord)
done
lemmas disj_Un_eqpoll_nat_sum =
eqpoll_trans [THEN eqpoll_trans,
OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum]
lemma Un_in_Collect: "⟦x ∈ Pow(A - B - h`i); x≈m;
h ∈ bij(a, {x ∈ Pow(A) . x≈k}); i<a; k ∈ nat; m ∈ nat⟧
⟹ h ` i ∪ x ∈ {x ∈ Pow(A) . x≈k #+ m}"
by (blast intro: disj_Un_eqpoll_nat_sum
dest: ltD bij_is_fun [THEN apply_type])
lemma lemma6:
"⟦∀y<succ(j). F(y)<=X ∧ (∀x<a. x<y | P(x,y) ⟶ Q(x,y)); succ(j)<a⟧
⟹ F(j)<=X ∧ (∀x<a. x<j | P(x,j) ⟶ Q(x,j))"
by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl])
lemma lemma7:
"⟦∀x<a. x<j | P(x,j) ⟶ Q(x,j); succ(j)<a⟧
⟹ P(j,j) ⟶ (∀x<a. x≤j | P(x,j) ⟶ Q(x,j))"
by (fast elim!: leE)
lemma ex_subset_eqpoll:
"⟦A≈a; ¬ Finite(a); Ord(a); m ∈ nat⟧ ⟹ ∃X ∈ Pow(A). X≈m"
apply (rule lepoll_imp_eqpoll_subset [of m A, THEN exE])
apply (rule lepoll_trans, rule leI [THEN le_imp_lepoll])
apply (blast intro: lt_trans2 [OF ltI nat_le_infinite_Ord] Ord_nat)
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
apply (fast elim!: eqpoll_sym)
done
lemma subset_Un_disjoint: "⟦A ⊆ B ∪ C; A ∩ C = 0⟧ ⟹ A ⊆ B"
by blast
lemma Int_empty:
"⟦X ∈ Pow(A - ⋃(B) -C); T ∈ B; F ⊆ T⟧ ⟹ F ∩ X = 0"
by blast
lemma subset_imp_eq_lemma:
"m ∈ nat ⟹ ∀A B. A ⊆ B ∧ m ≲ A ∧ B ≲ m ⟶ A=B"
apply (induct_tac "m")
apply (fast dest!: lepoll_0_is_0)
apply (intro allI impI)
apply (elim conjE)
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], assumption)
apply (frule subsetD [THEN Diff_sing_lepoll], assumption+)
apply (frule lepoll_Diff_sing)
apply (erule allE impE)+
apply (rule conjI)
prefer 2 apply fast
apply fast
apply (blast elim: equalityE)
done
lemma subset_imp_eq: "⟦A ⊆ B; m ≲ A; B ≲ m; m ∈ nat⟧ ⟹ A=B"
by (blast dest!: subset_imp_eq_lemma)
lemma bij_imp_arg_eq:
"⟦f ∈ bij(a, {Y ∈ X. Y≈succ(k)}); k ∈ nat; f`b ⊆ f`y; b<a; y<a⟧
⟹ b=y"
apply (drule subset_imp_eq)
apply (erule_tac [3] nat_succI)
unfolding bij_def inj_def
apply (blast intro: eqpoll_sym eqpoll_imp_lepoll
dest: ltD apply_type)+
done
lemma ex_next_set:
"⟦recfunAC16(f, h, y, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)};
Card(a); ¬ Finite(a); A≈a;
k ∈ nat; m ∈ nat; y<a;
h ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k)});
¬ (∃Y ∈ recfunAC16(f, h, y, a). h`y ⊆ Y)⟧
⟹ ∃X ∈ {Y ∈ Pow(A). Y≈succ(k #+ m)}. h`y ⊆ X ∧
(∀b<a. h`b ⊆ X ⟶
(∀T ∈ recfunAC16(f, h, y, a). ¬ h`b ⊆ T))"
apply (erule_tac m1=m in dbl_Diff_eqpoll [THEN ex_subset_eqpoll, THEN bexE],
assumption+)
apply (erule Card_is_Ord, assumption)
apply (frule Un_in_Collect, (erule asm_rl nat_succI)+)
apply (erule CollectE)
apply (rule rev_bexI, simp)
apply (rule conjI, blast)
apply (intro ballI impI oallI notI)
apply (drule subset_Un_disjoint, rule Int_empty, assumption+)
apply (blast dest: bij_imp_arg_eq)
done
lemma ex_next_Ord:
"⟦recfunAC16(f, h, y, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)};
Card(a); ¬ Finite(a); A≈a;
k ∈ nat; m ∈ nat; y<a;
h ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k)});
f ∈ bij(a, {Y ∈ Pow(A). Y≈succ(k #+ m)});
¬ (∃Y ∈ recfunAC16(f, h, y, a). h`y ⊆ Y)⟧
⟹ ∃c<a. h`y ⊆ f`c ∧
(∀b<a. h`b ⊆ f`c ⟶
(∀T ∈ recfunAC16(f, h, y, a). ¬ h`b ⊆ T))"
apply (drule ex_next_set, assumption+)
apply (erule bexE)
apply (rule_tac x="converse(f)`X" in oexI)
apply (simp add: right_inverse_bij)
apply (blast intro: bij_converse_bij bij_is_fun [THEN apply_type] ltI
Card_is_Ord)
done
lemma lemma8:
"⟦∀x<a. x<j | (∃xa ∈ F(j). P(x, xa))
⟶ (∃! Y. Y ∈ F(j) ∧ P(x, Y)); F(j) ⊆ X;
L ∈ X; P(j, L) ∧ (∀x<a. P(x, L) ⟶ (∀xa ∈ F(j). ¬P(x, xa)))⟧
⟹ F(j) ∪ {L} ⊆ X ∧
(∀x<a. x≤j | (∃xa ∈ (F(j) ∪ {L}). P(x, xa)) ⟶
(∃! Y. Y ∈ (F(j) ∪ {L}) ∧ P(x, Y)))"
apply (rule conjI)
apply (fast intro!: singleton_subsetI)
apply (rule oallI)
apply (blast elim!: leE oallE)
done
lemma main_induct:
"⟦b < a; f ∈ bij(a, {Y ∈ Pow(A) . Y≈succ(k #+ m)});
h ∈ bij(a, {Y ∈ Pow(A) . Y≈succ(k)});
¬Finite(a); Card(a); A≈a; k ∈ nat; m ∈ nat⟧
⟹ recfunAC16(f, h, b, a) ⊆ {X ∈ Pow(A) . X≈succ(k #+ m)} ∧
(∀x<a. x < b | (∃Y ∈ recfunAC16(f, h, b, a). h ` x ⊆ Y) ⟶
(∃! Y. Y ∈ recfunAC16(f, h, b, a) ∧ h ` x ⊆ Y))"
apply (erule lt_induct)
apply (frule lt_Ord)
apply (erule Ord_cases)
apply (simp add: recfunAC16_0)
prefer 2 apply (simp add: recfunAC16_Limit)
apply (rule lemma5, assumption+)
apply (blast dest!: recfunAC16_mono)
apply clarify
apply (erule lemma6 [THEN conjE], assumption)
apply (simp (no_asm_simp) split del: split_if add: recfunAC16_succ)
apply (rule conjI [THEN split_if [THEN iffD2]])
apply (simp, erule lemma7, assumption)
apply (rule impI)
apply (rule ex_next_Ord [THEN oexE],
assumption+, rule le_refl [THEN lt_trans], assumption+)
apply (erule lemma8, assumption)
apply (rule bij_is_fun [THEN apply_type], assumption)
apply (erule Least_le [THEN lt_trans2, THEN ltD])
apply (erule lt_Ord)
apply (erule succ_leI)
apply (erule LeastI)
apply (erule lt_Ord)
done
lemma lemma_simp_induct:
"⟦∀b. b<a ⟶ F(b) ⊆ S ∧ (∀x<a. (x<b | (∃Y ∈ F(b). f`x ⊆ Y))
⟶ (∃! Y. Y ∈ F(b) ∧ f`x ⊆ Y));
f ∈ a->f``(a); Limit(a);
∀i j. i≤j ⟶ F(i) ⊆ F(j)⟧
⟹ (⋃j<a. F(j)) ⊆ S ∧
(∀x ∈ f``a. ∃! Y. Y ∈ (⋃j<a. F(j)) ∧ x ⊆ Y)"
apply (rule conjI)
apply (rule subsetI)
apply (erule OUN_E, blast)
apply (rule ballI)
apply (erule imageE)
apply (drule ltI, erule Limit_is_Ord)
apply (drule Limit_has_succ, assumption)
apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption)
apply (erule conjE)
apply (drule ospec)
apply (erule leI [THEN succ_leE])
apply (erule impE)
apply (fast elim!: leI [THEN succ_leE, THEN lt_Ord, THEN le_refl])
apply (drule apply_equality, assumption)
apply (elim conjE ex1E)
apply (rule ex1I, blast)
apply (elim conjE OUN_E)
apply (erule_tac i="succ(xa)" and j=aa
in Ord_linear_le [OF lt_Ord lt_Ord], assumption)
prefer 2
apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast)
apply (drule_tac x1=aa in spec [THEN mp], assumption)
apply (frule succ_leE)
apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast)
done
theorem WO2_AC16: "⟦WO2; 0<m; k ∈ nat; m ∈ nat⟧ ⟹ AC16(k #+ m,k)"
unfolding AC16_def
apply (rule allI)
apply (rule impI)
apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp, simp)
apply (frule WO2_imp_ex_Card)
apply (elim exE conjE)
apply (drule eqpoll_trans [THEN eqpoll_sym,
THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
assumption)
apply (drule eqpoll_trans [THEN eqpoll_sym,
THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
assumption+)
apply (elim exE)
apply (rename_tac h)
apply (rule_tac x = "⋃j<a. recfunAC16 (h,f,j,a) " in exI)
apply (rule_tac P="λz. Y ∧ (∀x ∈ z. Z(x))" for Y Z
in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
apply (rule lemma_simp_induct)
apply (blast del: conjI notI
intro!: main_induct eqpoll_imp_lepoll [THEN lepoll_infinite] )
apply (blast intro: bij_is_fun [THEN surj_image, THEN surj_is_fun])
apply (erule eqpoll_imp_lepoll [THEN lepoll_infinite,
THEN infinite_Card_is_InfCard,
THEN InfCard_is_Limit],
assumption+)
apply (blast dest!: recfunAC16_mono)
done
end