Theory WO6_WO1
theory WO6_WO1
imports Cardinal_aux
begin
definition
NN :: "i ⇒ i" where
"NN(y) ≡ {m ∈ nat. ∃a. ∃f. Ord(a) ∧ domain(f)=a ∧
(⋃b<a. f`b) = y ∧ (∀b<a. f`b ≲ m)}"
definition
uu :: "[i, i, i, i] ⇒ i" where
"uu(f, beta, gamma, delta) ≡ (f`beta * f`gamma) ∩ f`delta"
definition
vv1 :: "[i, i, i] ⇒ i" where
"vv1(f,m,b) ≡
let g = μ g. (∃d. Ord(d) ∧ (domain(uu(f,b,g,d)) ≠ 0 ∧
domain(uu(f,b,g,d)) ≲ m));
d = μ d. domain(uu(f,b,g,d)) ≠ 0 ∧
domain(uu(f,b,g,d)) ≲ m
in if f`b ≠ 0 then domain(uu(f,b,g,d)) else 0"
definition
ww1 :: "[i, i, i] ⇒ i" where
"ww1(f,m,b) ≡ f`b - vv1(f,m,b)"
definition
gg1 :: "[i, i, i] ⇒ i" where
"gg1(f,a,m) ≡ λb ∈ a++a. if b<a then vv1(f,m,b) else ww1(f,m,b--a)"
definition
vv2 :: "[i, i, i, i] ⇒ i" where
"vv2(f,b,g,s) ≡
if f`g ≠ 0 then {uu(f, b, g, μ d. uu(f,b,g,d) ≠ 0)`s} else 0"
definition
ww2 :: "[i, i, i, i] ⇒ i" where
"ww2(f,b,g,s) ≡ f`g - vv2(f,b,g,s)"
definition
gg2 :: "[i, i, i, i] ⇒ i" where
"gg2(f,a,b,s) ≡
λg ∈ a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
lemma WO2_WO3: "WO2 ⟹ WO3"
by (unfold WO2_def WO3_def, fast)
lemma WO3_WO1: "WO3 ⟹ WO1"
unfolding eqpoll_def WO1_def WO3_def
apply (intro allI)
apply (drule_tac x=A in spec)
apply (blast intro: bij_is_inj well_ord_rvimage
well_ord_Memrel [THEN well_ord_subset])
done
lemma WO1_WO2: "WO1 ⟹ WO2"
unfolding eqpoll_def WO1_def WO2_def
apply (blast intro!: Ord_ordertype ordermap_bij)
done
lemma lam_sets: "f ∈ A->B ⟹ (λx ∈ A. {f`x}): A -> {{b}. b ∈ B}"
by (fast intro!: lam_type apply_type)
lemma surj_imp_eq': "f ∈ surj(A,B) ⟹ (⋃a ∈ A. {f`a}) = B"
unfolding surj_def
apply (fast elim!: apply_type)
done
lemma surj_imp_eq: "⟦f ∈ surj(A,B); Ord(A)⟧ ⟹ (⋃a<A. {f`a}) = B"
by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)
lemma WO1_WO4: "WO1 ⟹ WO4(1)"
unfolding WO1_def WO4_def
apply (rule allI)
apply (erule_tac x = A in allE)
apply (erule exE)
apply (intro exI conjI)
apply (erule Ord_ordertype)
apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN lam_sets, THEN domain_of_fun])
apply (simp_all add: singleton_eqpoll_1 eqpoll_imp_lepoll Ord_ordertype
ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq]
ltD)
done
lemma WO4_mono: "⟦m≤n; WO4(m)⟧ ⟹ WO4(n)"
unfolding WO4_def
apply (blast dest!: spec intro: lepoll_trans [OF _ le_imp_lepoll])
done
lemma WO4_WO5: "⟦m ∈ nat; 1≤m; WO4(m)⟧ ⟹ WO5"
by (unfold WO4_def WO5_def, blast)
lemma WO5_WO6: "WO5 ⟹ WO6"
by (unfold WO4_def WO5_def WO6_def, blast)
lemma lt_oadd_odiff_disj:
"⟦k < i++j; Ord(i); Ord(j)⟧
⟹ k < i | (¬ k<i ∧ k = i ++ (k--i) ∧ (k--i)<j)"
apply (rule_tac i = k and j = i in Ord_linear2)
prefer 4
apply (drule odiff_lt_mono2, assumption)
apply (simp add: oadd_odiff_inverse odiff_oadd_inverse)
apply (auto elim!: lt_Ord)
done
lemma domain_uu_subset: "domain(uu(f,b,g,d)) ⊆ f`b"
by (unfold uu_def, blast)
lemma quant_domain_uu_lepoll_m:
"∀b<a. f`b ≲ m ⟹ ∀b<a. ∀g<a. ∀d<a. domain(uu(f,b,g,d)) ≲ m"
by (blast intro: domain_uu_subset [THEN subset_imp_lepoll] lepoll_trans)
lemma uu_subset1: "uu(f,b,g,d) ⊆ f`b * f`g"
by (unfold uu_def, blast)
lemma uu_subset2: "uu(f,b,g,d) ⊆ f`d"
by (unfold uu_def, blast)
lemma uu_lepoll_m: "⟦∀b<a. f`b ≲ m; d<a⟧ ⟹ uu(f,b,g,d) ≲ m"
by (blast intro: uu_subset2 [THEN subset_imp_lepoll] lepoll_trans)
lemma cases:
"∀b<a. ∀g<a. ∀d<a. u(f,b,g,d) ≲ m
⟹ (∀b<a. f`b ≠ 0 ⟶
(∃g<a. ∃d<a. u(f,b,g,d) ≠ 0 ∧ u(f,b,g,d) ≺ m))
| (∃b<a. f`b ≠ 0 ∧ (∀g<a. ∀d<a. u(f,b,g,d) ≠ 0 ⟶
u(f,b,g,d) ≈ m))"
unfolding lesspoll_def
apply (blast del: equalityI)
done
lemma UN_oadd: "Ord(a) ⟹ (⋃b<a++a. C(b)) = (⋃b<a. C(b) ∪ C(a++b))"
by (blast intro: ltI lt_oadd1 oadd_lt_mono2 dest!: lt_oadd_disj)
lemma vv1_subset: "vv1(f,m,b) ⊆ f`b"
by (simp add: vv1_def Let_def domain_uu_subset)
lemma UN_gg1_eq:
"⟦Ord(a); m ∈ nat⟧ ⟹ (⋃b<a++a. gg1(f,a,m)`b) = (⋃b<a. f`b)"
by (simp add: gg1_def UN_oadd lt_oadd1 oadd_le_self [THEN le_imp_not_lt]
lt_Ord odiff_oadd_inverse ltD vv1_subset [THEN Diff_partition]
ww1_def)
lemma domain_gg1: "domain(gg1(f,a,m)) = a++a"
by (simp add: lam_funtype [THEN domain_of_fun] gg1_def)
lemma nested_LeastI:
"⟦P(a, b); Ord(a); Ord(b);
Least_a = (μ a. ∃x. Ord(x) ∧ P(a, x))⟧
⟹ P(Least_a, μ b. P(Least_a, b))"
apply (erule ssubst)
apply (rule_tac Q = "λz. P (z, μ b. P (z, b))" in LeastI2)
apply (fast elim!: LeastI)+
done
lemmas nested_Least_instance =
nested_LeastI [of "λg d. domain(uu(f,b,g,d)) ≠ 0 ∧
domain(uu(f,b,g,d)) ≲ m"] for f b m
lemma gg1_lepoll_m:
"⟦Ord(a); m ∈ nat;
∀b<a. f`b ≠0 ⟶
(∃g<a. ∃d<a. domain(uu(f,b,g,d)) ≠ 0 ∧
domain(uu(f,b,g,d)) ≲ m);
∀b<a. f`b ≲ succ(m); b<a++a⟧
⟹ gg1(f,a,m)`b ≲ m"
apply (simp add: gg1_def empty_lepollI)
apply (safe dest!: lt_oadd_odiff_disj)
apply (simp add: vv1_def Let_def empty_lepollI)
apply (fast intro: nested_Least_instance [THEN conjunct2]
elim!: lt_Ord)
apply (simp add: ww1_def empty_lepollI)
apply (case_tac "f` (b--a) = 0", simp add: empty_lepollI)
apply (rule Diff_lepoll, blast)
apply (rule vv1_subset)
apply (drule ospec [THEN mp], assumption+)
apply (elim oexE conjE)
apply (simp add: vv1_def Let_def lt_Ord nested_Least_instance [THEN conjunct1])
done
lemma ex_d_uu_not_empty:
"⟦b<a; g<a; f`b≠0; f`g≠0;
y*y ⊆ y; (⋃b<a. f`b)=y⟧
⟹ ∃d<a. uu(f,b,g,d) ≠ 0"
by (unfold uu_def, blast)
lemma uu_not_empty:
"⟦b<a; g<a; f`b≠0; f`g≠0; y*y ⊆ y; (⋃b<a. f`b)=y⟧
⟹ uu(f,b,g,μ d. (uu(f,b,g,d) ≠ 0)) ≠ 0"
apply (drule ex_d_uu_not_empty, assumption+)
apply (fast elim!: LeastI lt_Ord)
done
lemma not_empty_rel_imp_domain: "⟦r ⊆ A*B; r≠0⟧ ⟹ domain(r)≠0"
by blast
lemma Least_uu_not_empty_lt_a:
"⟦b<a; g<a; f`b≠0; f`g≠0; y*y ⊆ y; (⋃b<a. f`b)=y⟧
⟹ (μ d. uu(f,b,g,d) ≠ 0) < a"
apply (erule ex_d_uu_not_empty [THEN oexE], assumption+)
apply (blast intro: Least_le [THEN lt_trans1] lt_Ord)
done
lemma subset_Diff_sing: "⟦B ⊆ A; a∉B⟧ ⟹ B ⊆ A-{a}"
by blast
lemma supset_lepoll_imp_eq:
"⟦A ≲ m; m ≲ B; B ⊆ A; m ∈ nat⟧ ⟹ A=B"
apply (erule natE)
apply (fast dest!: lepoll_0_is_0 intro!: equalityI)
apply (safe intro!: equalityI)
apply (rule ccontr)
apply (rule succ_lepoll_natE)
apply (erule lepoll_trans)
apply (rule lepoll_trans)
apply (erule subset_Diff_sing [THEN subset_imp_lepoll], assumption)
apply (rule Diff_sing_lepoll, assumption+)
done
lemma uu_Least_is_fun:
"⟦∀g<a. ∀d<a. domain(uu(f, b, g, d))≠0 ⟶
domain(uu(f, b, g, d)) ≈ succ(m);
∀b<a. f`b ≲ succ(m); y*y ⊆ y;
(⋃b<a. f`b)=y; b<a; g<a; d<a;
f`b≠0; f`g≠0; m ∈ nat; s ∈ f`b⟧
⟹ uu(f, b, g, μ d. uu(f,b,g,d)≠0) ∈ f`b -> f`g"
apply (drule_tac x2=g in ospec [THEN ospec, THEN mp])
apply (rule_tac [3] not_empty_rel_imp_domain [OF uu_subset1 uu_not_empty])
apply (rule_tac [2] Least_uu_not_empty_lt_a, assumption+)
apply (rule rel_is_fun)
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
apply (erule uu_lepoll_m)
apply (rule Least_uu_not_empty_lt_a, assumption+)
apply (rule uu_subset1)
apply (rule supset_lepoll_imp_eq [OF _ eqpoll_sym [THEN eqpoll_imp_lepoll]])
apply (fast intro!: domain_uu_subset)+
done
lemma vv2_subset:
"⟦∀g<a. ∀d<a. domain(uu(f, b, g, d))≠0 ⟶
domain(uu(f, b, g, d)) ≈ succ(m);
∀b<a. f`b ≲ succ(m); y*y ⊆ y;
(⋃b<a. f`b)=y; b<a; g<a; m ∈ nat; s ∈ f`b⟧
⟹ vv2(f,b,g,s) ⊆ f`g"
apply (simp add: vv2_def)
apply (blast intro: uu_Least_is_fun [THEN apply_type])
done
lemma UN_gg2_eq:
"⟦∀g<a. ∀d<a. domain(uu(f,b,g,d)) ≠ 0 ⟶
domain(uu(f,b,g,d)) ≈ succ(m);
∀b<a. f`b ≲ succ(m); y*y ⊆ y;
(⋃b<a. f`b)=y; Ord(a); m ∈ nat; s ∈ f`b; b<a⟧
⟹ (⋃g<a++a. gg2(f,a,b,s) ` g) = y"
unfolding gg2_def
apply (drule sym)
apply (simp add: ltD UN_oadd oadd_le_self [THEN le_imp_not_lt]
lt_Ord odiff_oadd_inverse ww2_def
vv2_subset [THEN Diff_partition])
done
lemma domain_gg2: "domain(gg2(f,a,b,s)) = a++a"
by (simp add: lam_funtype [THEN domain_of_fun] gg2_def)
lemma vv2_lepoll: "⟦m ∈ nat; m≠0⟧ ⟹ vv2(f,b,g,s) ≲ m"
unfolding vv2_def
apply (simp add: empty_lepollI)
apply (fast dest!: le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_0_is_0]
intro!: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
not_lt_imp_le [THEN le_imp_subset, THEN subset_imp_lepoll]
nat_into_Ord nat_1I)
done
lemma ww2_lepoll:
"⟦∀b<a. f`b ≲ succ(m); g<a; m ∈ nat; vv2(f,b,g,d) ⊆ f`g⟧
⟹ ww2(f,b,g,d) ≲ m"
unfolding ww2_def
apply (case_tac "f`g = 0")
apply (simp add: empty_lepollI)
apply (drule ospec, assumption)
apply (rule Diff_lepoll, assumption+)
apply (simp add: vv2_def not_emptyI)
done
lemma gg2_lepoll_m:
"⟦∀g<a. ∀d<a. domain(uu(f,b,g,d)) ≠ 0 ⟶
domain(uu(f,b,g,d)) ≈ succ(m);
∀b<a. f`b ≲ succ(m); y*y ⊆ y;
(⋃b<a. f`b)=y; b<a; s ∈ f`b; m ∈ nat; m≠ 0; g<a++a⟧
⟹ gg2(f,a,b,s) ` g ≲ m"
apply (simp add: gg2_def empty_lepollI)
apply (safe elim!: lt_Ord2 dest!: lt_oadd_odiff_disj)
apply (simp add: vv2_lepoll)
apply (simp add: ww2_lepoll vv2_subset)
done
lemma lemma_ii: "⟦succ(m) ∈ NN(y); y*y ⊆ y; m ∈ nat; m≠0⟧ ⟹ m ∈ NN(y)"
unfolding NN_def
apply (elim CollectE exE conjE)
apply (rule quant_domain_uu_lepoll_m [THEN cases, THEN disjE], assumption)
apply (simp add: lesspoll_succ_iff)
apply (rule_tac x = "a++a" in exI)
apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m)
apply (elim oexE conjE)
apply (rule_tac A = "f`B" for B in not_emptyE, assumption)
apply (rule CollectI)
apply (erule succ_natD)
apply (rule_tac x = "a++a" in exI)
apply (rule_tac x = "gg2 (f,a,b,x) " in exI)
apply (simp add: Ord_oadd domain_gg2 UN_gg2_eq gg2_lepoll_m)
done
lemma z_n_subset_z_succ_n:
"∀n ∈ nat. rec(n, x, λk r. r ∪ r*r) ⊆ rec(succ(n), x, λk r. r ∪ r*r)"
by (fast intro: rec_succ [THEN ssubst])
lemma le_subsets:
"⟦∀n ∈ nat. f(n)<=f(succ(n)); n≤m; n ∈ nat; m ∈ nat⟧
⟹ f(n)<=f(m)"
apply (erule_tac P = "n≤m" in rev_mp)
apply (rule_tac P = "λz. n≤z ⟶ f (n) ⊆ f (z) " in nat_induct)
apply (auto simp add: le_iff)
done
lemma le_imp_rec_subset:
"⟦n≤m; m ∈ nat⟧
⟹ rec(n, x, λk r. r ∪ r*r) ⊆ rec(m, x, λk r. r ∪ r*r)"
apply (rule z_n_subset_z_succ_n [THEN le_subsets])
apply (blast intro: lt_nat_in_nat)+
done
lemma lemma_iv: "∃y. x ∪ y*y ⊆ y"
apply (rule_tac x = "⋃n ∈ nat. rec (n, x, λk r. r ∪ r*r) " in exI)
apply safe
apply (rule nat_0I [THEN UN_I], simp)
apply (rule_tac a = "succ (n ∪ na) " in UN_I)
apply (erule Un_nat_type [THEN nat_succI], assumption)
apply (auto intro: le_imp_rec_subset [THEN subsetD]
intro!: Un_upper1_le Un_upper2_le Un_nat_type
elim!: nat_into_Ord)
done
lemma WO6_imp_NN_not_empty: "WO6 ⟹ NN(y) ≠ 0"
by (unfold WO6_def NN_def, clarify, blast)
lemma lemma1:
"⟦(⋃b<a. f`b)=y; x ∈ y; ∀b<a. f`b ≲ 1; Ord(a)⟧ ⟹ ∃c<a. f`c = {x}"
by (fast elim!: lepoll_1_is_sing)
lemma lemma2:
"⟦(⋃b<a. f`b)=y; x ∈ y; ∀b<a. f`b ≲ 1; Ord(a)⟧
⟹ f` (μ i. f`i = {x}) = {x}"
apply (drule lemma1, assumption+)
apply (fast elim!: lt_Ord intro: LeastI)
done
lemma NN_imp_ex_inj: "1 ∈ NN(y) ⟹ ∃a f. Ord(a) ∧ f ∈ inj(y, a)"
unfolding NN_def
apply (elim CollectE exE conjE)
apply (rule_tac x = a in exI)
apply (rule_tac x = "λx ∈ y. μ i. f`i = {x}" in exI)
apply (rule conjI, assumption)
apply (rule_tac d = "λi. THE x. x ∈ f`i" in lam_injective)
apply (drule lemma1, assumption+)
apply (fast elim!: Least_le [THEN lt_trans1, THEN ltD] lt_Ord)
apply (rule lemma2 [THEN ssubst], assumption+, blast)
done
lemma y_well_ord: "⟦y*y ⊆ y; 1 ∈ NN(y)⟧ ⟹ ∃r. well_ord(y, r)"
apply (drule NN_imp_ex_inj)
apply (fast elim!: well_ord_rvimage [OF _ well_ord_Memrel])
done
lemma rev_induct_lemma [rule_format]:
"⟦n ∈ nat; ⋀m. ⟦m ∈ nat; m≠0; P(succ(m))⟧ ⟹ P(m)⟧
⟹ n≠0 ⟶ P(n) ⟶ P(1)"
by (erule nat_induct, blast+)
lemma rev_induct:
"⟦n ∈ nat; P(n); n≠0;
⋀m. ⟦m ∈ nat; m≠0; P(succ(m))⟧ ⟹ P(m)⟧
⟹ P(1)"
by (rule rev_induct_lemma, blast+)
lemma NN_into_nat: "n ∈ NN(y) ⟹ n ∈ nat"
by (simp add: NN_def)
lemma lemma3: "⟦n ∈ NN(y); y*y ⊆ y; n≠0⟧ ⟹ 1 ∈ NN(y)"
apply (rule rev_induct [OF NN_into_nat], assumption+)
apply (rule lemma_ii, assumption+)
done
lemma NN_y_0: "0 ∈ NN(y) ⟹ y=0"
unfolding NN_def
apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst)
done
lemma WO6_imp_WO1: "WO6 ⟹ WO1"
unfolding WO1_def
apply (rule allI)
apply (case_tac "A=0")
apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
apply (rule_tac x = A in lemma_iv [elim_format])
apply (erule exE)
apply (drule WO6_imp_NN_not_empty)
apply (erule Un_subset_iff [THEN iffD1, THEN conjE])
apply (erule_tac A = "NN (y) " in not_emptyE)
apply (frule y_well_ord)
apply (fast intro!: lemma3 dest!: NN_y_0 elim!: not_emptyE)
apply (fast elim: well_ord_subset)
done
end