Theory Normal
section ‹Closed Unbounded Classes and Normal Functions›
theory Normal imports ZF begin
text‹
One source is the book
Frank R. Drake.
\emph{Set Theory: An Introduction to Large Cardinals}.
North-Holland, 1974.
›
subsection ‹Closed and Unbounded (c.u.) Classes of Ordinals›
definition
Closed :: "(i⇒o) ⇒ o" where
"Closed(P) ≡ ∀I. I ≠ 0 ⟶ (∀i∈I. Ord(i) ∧ P(i)) ⟶ P(⋃(I))"
definition
Unbounded :: "(i⇒o) ⇒ o" where
"Unbounded(P) ≡ ∀i. Ord(i) ⟶ (∃j. i<j ∧ P(j))"
definition
Closed_Unbounded :: "(i⇒o) ⇒ o" where
"Closed_Unbounded(P) ≡ Closed(P) ∧ Unbounded(P)"
subsubsection‹Simple facts about c.u. classes›
lemma ClosedI:
"⟦⋀I. ⟦I ≠ 0; ∀i∈I. Ord(i) ∧ P(i)⟧ ⟹ P(⋃(I))⟧
⟹ Closed(P)"
by (simp add: Closed_def)
lemma ClosedD:
"⟦Closed(P); I ≠ 0; ⋀i. i∈I ⟹ Ord(i); ⋀i. i∈I ⟹ P(i)⟧
⟹ P(⋃(I))"
by (simp add: Closed_def)
lemma UnboundedD:
"⟦Unbounded(P); Ord(i)⟧ ⟹ ∃j. i<j ∧ P(j)"
by (simp add: Unbounded_def)
lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ⟹ Unbounded(C)"
by (simp add: Closed_Unbounded_def)
text‹The universal class, V, is closed and unbounded.
A bit odd, since C. U. concerns only ordinals, but it's used below!›
theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(λx. True)"
by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
text‹The class of ordinals, \<^term>‹Ord›, is closed and unbounded.›
theorem Closed_Unbounded_Ord [simp]: "Closed_Unbounded(Ord)"
by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
text‹The class of limit ordinals, \<^term>‹Limit›, is closed and unbounded.›
theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"
proof -
have "∃j. i < j ∧ Limit(j)" if "Ord(i)" for i
apply (rule_tac x="i++nat" in exI)
apply (blast intro: oadd_lt_self oadd_LimitI Limit_has_0 that)
done
then show ?thesis
by (auto simp: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union)
qed
text‹The class of cardinals, \<^term>‹Card›, is closed and unbounded.›
theorem Closed_Unbounded_Card [simp]: "Closed_Unbounded(Card)"
proof -
have "∀i. Ord(i) ⟶ (∃j. i < j ∧ Card(j))"
by (blast intro: lt_csucc Card_csucc)
then show ?thesis
by (simp add: Closed_Unbounded_def Closed_def Unbounded_def)
qed
subsubsection‹The intersection of any set-indexed family of c.u. classes is
c.u.›
text‹The constructions below come from Kunen, \emph{Set Theory}, page 78.›
locale cub_family =
fixes P and A
fixes next_greater
fixes sup_greater
assumes closed: "a∈A ⟹ Closed(P(a))"
and unbounded: "a∈A ⟹ Unbounded(P(a))"
and A_non0: "A≠0"
defines "next_greater(a,x) ≡ μ y. x<y ∧ P(a,y)"
and "sup_greater(x) ≡ ⋃a∈A. next_greater(a,x)"
begin
text‹Trivial that the intersection is closed.›
lemma Closed_INT: "Closed(λx. ∀i∈A. P(i,x))"
by (blast intro: ClosedI ClosedD [OF closed])
text‹All remaining effort goes to show that the intersection is unbounded.›
lemma Ord_sup_greater:
"Ord(sup_greater(x))"
by (simp add: sup_greater_def next_greater_def)
lemma Ord_next_greater:
"Ord(next_greater(a,x))"
by (simp add: next_greater_def)
text‹\<^term>‹next_greater› works as expected: it returns a larger value
and one that belongs to class \<^term>‹P(a)›.›
lemma
assumes "Ord(x)" "a∈A"
shows next_greater_in_P: "P(a, next_greater(a,x))"
and next_greater_gt: "x < next_greater(a,x)"
proof -
obtain y where "x < y" "P(a,y)"
using assms UnboundedD [OF unbounded] by blast
then have "P(a, next_greater(a,x)) ∧ x < next_greater(a,x)"
unfolding next_greater_def
by (blast intro: LeastI2 lt_Ord2)
then show "P(a, next_greater(a,x))" "x < next_greater(a,x)"
by auto
qed
lemma sup_greater_gt:
"Ord(x) ⟹ x < sup_greater(x)"
using A_non0 unfolding sup_greater_def
by (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)
lemma next_greater_le_sup_greater:
"a∈A ⟹ next_greater(a,x) ≤ sup_greater(x)"
unfolding sup_greater_def
by (force intro: UN_upper_le Ord_next_greater)
lemma omega_sup_greater_eq_UN:
assumes "Ord(x)" "a∈A"
shows "sup_greater^ω (x) =
(⋃n∈nat. next_greater(a, sup_greater^n (x)))"
proof (rule le_anti_sym)
show "sup_greater^ω (x) ≤ (⋃n∈nat. next_greater(a, sup_greater^n (x)))"
using assms
unfolding iterates_omega_def
by (blast intro: leI le_implies_UN_le_UN next_greater_gt Ord_iterates Ord_sup_greater)
next
have "Ord(⋃n∈nat. sup_greater^n (x))"
by (blast intro: Ord_iterates Ord_sup_greater assms)
moreover have "next_greater(a, sup_greater^n (x)) ≤
(⋃n∈nat. sup_greater^n (x))" if "n ∈ nat" for n
proof (rule UN_upper_le)
show "next_greater(a, sup_greater^n (x)) ≤ sup_greater^succ(n) (x)"
using assms by (simp add: next_greater_le_sup_greater)
show "Ord(⋃xa∈nat. sup_greater^xa (x))"
using assms by (blast intro: Ord_iterates Ord_sup_greater)
qed (use that in auto)
ultimately
show "(⋃n∈nat. next_greater(a, sup_greater^n (x))) ≤ sup_greater^ω (x)"
using assms unfolding iterates_omega_def by (blast intro: UN_least_le)
qed
lemma P_omega_sup_greater:
"⟦Ord(x); a∈A⟧ ⟹ P(a, sup_greater^ω (x))"
apply (simp add: omega_sup_greater_eq_UN)
apply (rule ClosedD [OF closed])
apply (blast intro: ltD, auto)
apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)
apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)
done
lemma omega_sup_greater_gt:
"Ord(x) ⟹ x < sup_greater^ω (x)"
apply (simp add: iterates_omega_def)
apply (rule UN_upper_lt [of 1], simp_all)
apply (blast intro: sup_greater_gt)
apply (blast intro: Ord_iterates Ord_sup_greater)
done
lemma Unbounded_INT: "Unbounded(λx. ∀a∈A. P(a,x))"
unfolding Unbounded_def
by (blast intro!: omega_sup_greater_gt P_omega_sup_greater)
lemma Closed_Unbounded_INT:
"Closed_Unbounded(λx. ∀a∈A. P(a,x))"
by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)
end
theorem Closed_Unbounded_INT:
assumes "⋀a. a∈A ⟹ Closed_Unbounded(P(a))"
shows "Closed_Unbounded(λx. ∀a∈A. P(a, x))"
proof (cases "A=0")
case False
with assms [unfolded Closed_Unbounded_def] show ?thesis
by (intro cub_family.Closed_Unbounded_INT [OF cub_family.intro]) auto
qed auto
lemma Int_iff_INT2:
"P(x) ∧ Q(x) ⟷ (∀i∈2. (i=0 ⟶ P(x)) ∧ (i=1 ⟶ Q(x)))"
by auto
theorem Closed_Unbounded_Int:
"⟦Closed_Unbounded(P); Closed_Unbounded(Q)⟧
⟹ Closed_Unbounded(λx. P(x) ∧ Q(x))"
unfolding Int_iff_INT2
by (rule Closed_Unbounded_INT, auto)
subsection ‹Normal Functions›
definition
mono_le_subset :: "(i⇒i) ⇒ o" where
"mono_le_subset(M) ≡ ∀i j. i≤j ⟶ M(i) ⊆ M(j)"
definition
mono_Ord :: "(i⇒i) ⇒ o" where
"mono_Ord(F) ≡ ∀i j. i<j ⟶ F(i) < F(j)"
definition
cont_Ord :: "(i⇒i) ⇒ o" where
"cont_Ord(F) ≡ ∀l. Limit(l) ⟶ F(l) = (⋃i<l. F(i))"
definition
Normal :: "(i⇒i) ⇒ o" where
"Normal(F) ≡ mono_Ord(F) ∧ cont_Ord(F)"
subsubsection‹Immediate properties of the definitions›
lemma NormalI:
"⟦⋀i j. i<j ⟹ F(i) < F(j); ⋀l. Limit(l) ⟹ F(l) = (⋃i<l. F(i))⟧
⟹ Normal(F)"
by (simp add: Normal_def mono_Ord_def cont_Ord_def)
lemma mono_Ord_imp_Ord: "⟦Ord(i); mono_Ord(F)⟧ ⟹ Ord(F(i))"
apply (auto simp add: mono_Ord_def)
apply (blast intro: lt_Ord)
done
lemma mono_Ord_imp_mono: "⟦i<j; mono_Ord(F)⟧ ⟹ F(i) < F(j)"
by (simp add: mono_Ord_def)
lemma Normal_imp_Ord [simp]: "⟦Normal(F); Ord(i)⟧ ⟹ Ord(F(i))"
by (simp add: Normal_def mono_Ord_imp_Ord)
lemma Normal_imp_cont: "⟦Normal(F); Limit(l)⟧ ⟹ F(l) = (⋃i<l. F(i))"
by (simp add: Normal_def cont_Ord_def)
lemma Normal_imp_mono: "⟦i<j; Normal(F)⟧ ⟹ F(i) < F(j)"
by (simp add: Normal_def mono_Ord_def)
lemma Normal_increasing:
assumes i: "Ord(i)" and F: "Normal(F)" shows"i ≤ F(i)"
using i
proof (induct i rule: trans_induct3)
case 0 thus ?case by (simp add: subset_imp_le F)
next
case (succ i)
hence "F(i) < F(succ(i))" using F
by (simp add: Normal_def mono_Ord_def)
thus ?case using succ.hyps
by (blast intro: lt_trans1)
next
case (limit l)
hence "l = (⋃y<l. y)"
by (simp add: Limit_OUN_eq)
also have "... ≤ (⋃y<l. F(y))" using limit
by (blast intro: ltD le_implies_OUN_le_OUN)
finally have "l ≤ (⋃y<l. F(y))" .
moreover have "(⋃y<l. F(y)) ≤ F(l)" using limit F
by (simp add: Normal_imp_cont lt_Ord)
ultimately show ?case
by (blast intro: le_trans)
qed
subsubsection‹The class of fixedpoints is closed and unbounded›
text‹The proof is from Drake, pages 113--114.›
lemma mono_Ord_imp_le_subset: "mono_Ord(F) ⟹ mono_le_subset(F)"
apply (simp add: mono_le_subset_def, clarify)
apply (subgoal_tac "F(i)≤F(j)", blast dest: le_imp_subset)
apply (simp add: le_iff)
apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono)
done
text‹The following equation is taken for granted in any set theory text.›
lemma cont_Ord_Union:
"⟦cont_Ord(F); mono_le_subset(F); X=0 ⟶ F(0)=0; ∀x∈X. Ord(x)⟧
⟹ F(⋃(X)) = (⋃y∈X. F(y))"
apply (frule Ord_set_cases)
apply (erule disjE, force)
apply (thin_tac "X=0 ⟶ Q" for Q, auto)
txt‹The trival case of \<^term>‹⋃X ∈ X››
apply (rule equalityI, blast intro: Ord_Union_eq_succD)
apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff)
apply (blast elim: equalityE)
txt‹The limit case, \<^term>‹Limit(⋃X)›:
@{subgoals[display,indent=0,margin=65]}
›
apply (simp add: OUN_Union_eq cont_Ord_def)
apply (rule equalityI)
txt‹First inclusion:›
apply (rule UN_least [OF OUN_least])
apply (simp add: mono_le_subset_def, blast intro: leI)
txt‹Second inclusion:›
apply (rule UN_least)
apply (frule Union_upper_le, blast, blast)
apply (erule leE, drule ltD, elim UnionE)
apply (simp add: OUnion_def)
apply blast+
done
lemma Normal_Union:
"⟦X≠0; ∀x∈X. Ord(x); Normal(F)⟧ ⟹ F(⋃(X)) = (⋃y∈X. F(y))"
unfolding Normal_def
by (blast intro: mono_Ord_imp_le_subset cont_Ord_Union)
lemma Normal_imp_fp_Closed: "Normal(F) ⟹ Closed(λi. F(i) = i)"
apply (simp add: Closed_def ball_conj_distrib, clarify)
apply (frule Ord_set_cases)
apply (auto simp add: Normal_Union)
done
lemma iterates_Normal_increasing:
"⟦n∈nat; x < F(x); Normal(F)⟧
⟹ F^n (x) < F^(succ(n)) (x)"
by (induct n rule: nat_induct) (simp_all add: Normal_imp_mono)
lemma Ord_iterates_Normal:
"⟦n∈nat; Normal(F); Ord(x)⟧ ⟹ Ord(F^n (x))"
by (simp)
text‹THIS RESULT IS UNUSED›
lemma iterates_omega_Limit:
"⟦Normal(F); x < F(x)⟧ ⟹ Limit(F^ω (x))"
apply (frule lt_Ord)
apply (simp add: iterates_omega_def)
apply (rule increasing_LimitI)
apply (blast intro: UN_upper_lt [of "1"] Normal_imp_Ord
Ord_iterates lt_imp_0_lt
iterates_Normal_increasing, clarify)
apply (rule bexI)
apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal])
apply (rule UN_I, erule nat_succI)
apply (blast intro: iterates_Normal_increasing Ord_iterates_Normal
ltD [OF lt_trans1, OF succ_leI, OF ltI])
done
lemma iterates_omega_fixedpoint:
"⟦Normal(F); Ord(a)⟧ ⟹ F(F^ω (a)) = F^ω (a)"
apply (frule Normal_increasing, assumption)
apply (erule leE)
apply (simp_all add: iterates_omega_triv [OF sym])
apply (simp add: iterates_omega_def Normal_Union)
apply (rule equalityI, force simp add: nat_succI)
txt‹Opposite inclusion:
@{subgoals[display,indent=0,margin=65]}
›
apply clarify
apply (rule UN_I, assumption)
apply (frule iterates_Normal_increasing, assumption, assumption, simp)
apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F])
done
lemma iterates_omega_increasing:
"⟦Normal(F); Ord(a)⟧ ⟹ a ≤ F^ω (a)"
by (simp add: iterates_omega_def UN_upper_le [of 0])
lemma Normal_imp_fp_Unbounded: "Normal(F) ⟹ Unbounded(λi. F(i) = i)"
apply (unfold Unbounded_def, clarify)
apply (rule_tac x="F^ω (succ(i))" in exI)
apply (simp add: iterates_omega_fixedpoint)
apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])
done
theorem Normal_imp_fp_Closed_Unbounded:
"Normal(F) ⟹ Closed_Unbounded(λi. F(i) = i)"
by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed Normal_imp_fp_Unbounded)
subsubsection‹Function ‹normalize››
text‹Function ‹normalize› maps a function ‹F› to a
normal function that bounds it above. The result is normal if and
only if ‹F› is continuous: succ is not bounded above by any
normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
›
definition
normalize :: "[i⇒i, i] ⇒ i" where
"normalize(F,a) ≡ transrec2(a, F(0), λx r. F(succ(x)) ∪ succ(r))"
lemma Ord_normalize [simp, intro]:
"⟦Ord(a); ⋀x. Ord(x) ⟹ Ord(F(x))⟧ ⟹ Ord(normalize(F, a))"
proof (induct a rule: trans_induct3)
qed (simp_all add: ltD def_transrec2 [OF normalize_def])
lemma normalize_increasing:
assumes ab: "a < b" and F: "⋀x. Ord(x) ⟹ Ord(F(x))"
shows "normalize(F,a) < normalize(F,b)"
proof -
{ fix x
have "Ord(b)" using ab by (blast intro: lt_Ord2)
hence "x < b ⟹ normalize(F,x) < normalize(F,b)"
proof (induct b arbitrary: x rule: trans_induct3)
case 0 thus ?case by simp
next
case (succ b)
thus ?case
by (auto simp add: le_iff def_transrec2 [OF normalize_def] intro: Un_upper2_lt F)
next
case (limit l)
hence sc: "succ(x) < l"
by (blast intro: Limit_has_succ)
hence "normalize(F,x) < normalize(F,succ(x))"
by (blast intro: limit elim: ltE)
hence "normalize(F,x) < (⋃j<l. normalize(F,j))"
by (blast intro: OUN_upper_lt lt_Ord F sc)
thus ?case using limit
by (simp add: def_transrec2 [OF normalize_def])
qed
} thus ?thesis using ab .
qed
theorem Normal_normalize:
assumes "⋀x. Ord(x) ⟹ Ord(F(x))" shows "Normal(normalize(F))"
proof (rule NormalI)
show "⋀i j. i < j ⟹ normalize(F,i) < normalize(F,j)"
using assms by (blast intro!: normalize_increasing)
show "⋀l. Limit(l) ⟹ normalize(F, l) = (⋃i<l. normalize(F,i))"
by (simp add: def_transrec2 [OF normalize_def])
qed
theorem le_normalize:
assumes a: "Ord(a)" and coF: "cont_Ord(F)" and F: "⋀x. Ord(x) ⟹ Ord(F(x))"
shows "F(a) ≤ normalize(F,a)"
using a
proof (induct a rule: trans_induct3)
case 0 thus ?case by (simp add: F def_transrec2 [OF normalize_def])
next
case (succ a)
thus ?case
by (simp add: def_transrec2 [OF normalize_def] Un_upper1_le F )
next
case (limit l)
thus ?case using F coF [unfolded cont_Ord_def]
by (simp add: def_transrec2 [OF normalize_def] le_implies_OUN_le_OUN ltD)
qed
subsection ‹The Alephs›
text ‹This is the well-known transfinite enumeration of the cardinal
numbers.›
definition
Aleph :: "i ⇒ i" (‹ℵ_› [90] 90) where
"Aleph(a) ≡ transrec2(a, nat, λx r. csucc(r))"
lemma Card_Aleph [simp, intro]:
"Ord(a) ⟹ Card(Aleph(a))"
apply (erule trans_induct3)
apply (simp_all add: Card_csucc Card_nat Card_is_Ord
def_transrec2 [OF Aleph_def])
done
lemma Aleph_increasing:
assumes ab: "a < b" shows "Aleph(a) < Aleph(b)"
proof -
{ fix x
have "Ord(b)" using ab by (blast intro: lt_Ord2)
hence "x < b ⟹ Aleph(x) < Aleph(b)"
proof (induct b arbitrary: x rule: trans_induct3)
case 0 thus ?case by simp
next
case (succ b)
thus ?case
by (force simp add: le_iff def_transrec2 [OF Aleph_def]
intro: lt_trans lt_csucc Card_is_Ord)
next
case (limit l)
hence sc: "succ(x) < l"
by (blast intro: Limit_has_succ)
hence "ℵ x < (⋃j<l. ℵj)" using limit
by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord)
thus ?case using limit
by (simp add: def_transrec2 [OF Aleph_def])
qed
} thus ?thesis using ab .
qed
theorem Normal_Aleph: "Normal(Aleph)"
proof (rule NormalI)
show "⋀i j. i < j ⟹ ℵi < ℵj"
by (blast intro!: Aleph_increasing)
show "⋀l. Limit(l) ⟹ ℵl = (⋃i<l. ℵi)"
by (simp add: def_transrec2 [OF Aleph_def])
qed
end