Quelle  Normal.thy   Sprache: Isabelle

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

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 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 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, 🍋‹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, 🍋‹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, 🍋‹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 🍋 ‹the next ordinal satisfying class 🍋‹A››
  fixes sup_greater  🍋 ‹sup of those ordinals over all 🍋‹A››
  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‹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‹🍋‹next_greater› works as expected: it returns a larger value
and one that belongs to class 🍋‹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 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‹Immediate properties of the definitions›

lemma NormalI:
  "\\i j. i F(i) < F(j); \l. Limit(l) \ F(l) = (\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 \ 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 using limit
    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‹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 🍋‹∪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, 🍋‹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) 
    🍋 ‹this lemma is @{thm increasing_LimitI [no_vars]}›
   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‹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 -
  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 ‹The Alephs›
text ‹This is the well-known transfinite enumeration of the cardinal 
numbers.›

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