Quelle Normal.thy Sprache: Isabelle

(*  Title:      ZF/Constructible/Normal.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section \<open>Closed Unbounded Classes and Normal Functions\<close>

theory Normal imports ZF begin

text\<open>
One source is the book

Frank R. Drake.
\emph{Set Theory: An Introduction to Large Cardinals}.
North-Holland, 1974.
\<close>

subsection \<open>Closed and Unbounded (c.u.) Classes of Ordinals\<close>

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 P(j))"

definition
  Closed_Unbounded :: "(i\o) \ o" where
    "Closed_Unbounded(P) \ Closed(P) \ Unbounded(P)"

subsubsection\<open>Simple facts about c.u. classes\<close>

lemma ClosedI:
  "\\I. \I \ 0; \i\I. Ord(i) \ P(i)\ \ P(\(I))\
      \<Longrightarrow> Closed(P)"
  by (simp add: Closed_def)

lemma ClosedD:
  "\Closed(P); I \ 0; \i. i\I \ Ord(i); \i. i\I \ P(i)\
      \<Longrightarrow> P(\<Union>(I))"
  by (simp add: Closed_def)

lemma UnboundedD:
  "\Unbounded(P); Ord(i)\ \ \j. i P(j)"
  by (simp add: Unbounded_def)

lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) \ Unbounded(C)"
  by (simp add: Closed_Unbounded_def)

text\<open>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\<open>The class of ordinals, \<^term>\<open>Ord\<close>, is closed and unbounded.\<close>
theorem Closed_Unbounded_Ord   [simp]: "Closed_Unbounded(Ord)"
  by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)

text\<open>The class of limit ordinals, \<^term>\<open>Limit\<close>, is closed and unbounded.\<close>
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\<open>The class of cardinals, \<^term>\<open>Card\<close>, is closed and unbounded.\<close>
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\<open>The intersection of any set-indexed family of c.u. classes is
      c.u.\<close>

text\<open>The constructions below come from Kunen, \emph{Set Theory}, page 78.\<close>
locale cub_family =
  fixes P and A
  fixes next_greater \<comment> \<open>the next ordinal satisfying class \<^term>\<open>A\<close>\<close>
  fixes sup_greater  \<comment> \<open>sup of those ordinals over all \<^term>\<open>A\<close>\<close>
  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 P(a,y)"
      and "sup_greater(x) \ \a\A. next_greater(a,x)"

begin

text\<open>Trivial that the intersection is closed.\<close>
lemma Closed_INT: "Closed(\x. \i\A. P(i,x))"
  by (blast intro: ClosedI ClosedD [OF closed])

text\<open>All remaining effort goes to show that the intersection is unbounded.\<close>

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\<open>\<^term>\<open>next_greater\<close> works as expected: it returns a larger value
and one that belongs to class \<^term>\<open>P(a)\<close>.\<close>
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) =
          (\<Union>n\<in>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)) \
             (\<Union>n\<in>nat. sup_greater^n (x))" if "n \<in> 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)\
      \<Longrightarrow> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"
  unfolding Int_iff_INT2
  by (rule Closed_Unbounded_INT, auto)

subsection \<open>Normal Functions\<close>

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 F(i) < F(j)"

definition
  cont_Ord :: "(i\i) \ o" where
    "cont_Ord(F) \ \l. Limit(l) \ F(l) = (\i

definition
  Normal :: "(i\i) \ o" where
    "Normal(F) \ mono_Ord(F) \ cont_Ord(F)"

subsubsection\<open>Immediate properties of the definitions\<close>

lemma NormalI:
  "\\i j. i F(i) < F(j); \l. Limit(l) \ F(l) = (\i
      \<Longrightarrow> 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 \ 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
  by (simp add: Normal_def cont_Ord_def)

lemma Normal_imp_mono: "\i \ 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
    by (simp add: Limit_OUN_eq)
  also have "... \ (\y
    by (blast intro: ltD le_implies_OUN_le_OUN)
  finally have "l \ (\y
  moreover have "(\y F(l)" using limit F
    by (simp add: Normal_imp_cont lt_Ord)
  ultimately show ?case
    by (blast intro: le_trans)
qed

subsubsection\<open>The class of fixedpoints is closed and unbounded\<close>

text\<open>The proof is from Drake, pages 113--114.\<close>

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\<open>The following equation is taken for granted in any set theory text.\<close>
lemma cont_Ord_Union:
  "\cont_Ord(F); mono_le_subset(F); X=0 \ F(0)=0; \x\X. Ord(x)\
      \<Longrightarrow> F(\<Union>(X)) = (\<Union>y\<in>X. F(y))"
  apply (frule Ord_set_cases)
  apply (erule disjE, force)
  apply (thin_tac "X=0 \ Q" for Q, auto)
  txt\<open>The trival case of \<^term>\<open>\<Union>X \<in> X\<close>\<close>
   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\<open>The limit case, \<^term>\<open>Limit(\<Union>X)\<close>:
@{subgoals[display,indent=0,margin=65]}
\<close>
  apply (simp add: OUN_Union_eq cont_Ord_def)
  apply (rule equalityI)
  txt\<open>First inclusion:\<close>
   apply (rule UN_least [OF OUN_least])
   apply (simp add: mono_le_subset_def, blast intro: leI)
  txt\<open>Second inclusion:\<close>
  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)\
      \<Longrightarrow> 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\<open>THIS RESULT IS UNUSED\<close>
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)
    \<comment> \<open>this lemma is @{thm increasing_LimitI [no_vars]}\<close>
   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])  (*for subgoal 2*)
apply (simp add:  iterates_omega_def Normal_Union)
apply (rule equalityI, force simp add: nat_succI)
txt\<open>Opposite inclusion:
@{subgoals[display,indent=0,margin=65]}
\<close>
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\<open>Function \<open>normalize\<close>\<close>

text\<open>Function \<open>normalize\<close> maps a function \<open>F\<close> to a
      normal function that bounds it above.  The result is normal if and
      only if \<open>F\<close> is continuous: succ is not bounded above by any
      normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
\<close>
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 -
  have "Ord(b)" using ab by (blast intro: lt_Ord2)
  hence "x < b \ normalize(F,x) < normalize(F,b)" for x
  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
      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
    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 \<open>The Alephs\<close>
text \<open>This is the well-known transfinite enumeration of the cardinal
numbers.\<close>

definition
  Aleph :: "i \ i" (\(\open_block notation=\prefix \\\\_)\ [90] 90) where
    "\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 -
  have "Ord(b)" using ab by (blast intro: lt_Ord2)
  hence "x < b \ Aleph(x) < Aleph(b)" for x
  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 < (\jj)" 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" for i j
    by (blast intro!: Aleph_increasing)
  show "Limit(l) \ \l = (\ii)" for l
    by (simp add: def_transrec2 [OF Aleph_def])
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.