src/ZF/Constructible/Normal.thy
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 32960 69916a850301
child 46823 57bf0cecb366
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
paulson@13505
     1
(*  Title:      ZF/Constructible/Normal.thy
paulson@13505
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13505
     3
*)
paulson@13505
     4
paulson@13223
     5
header {*Closed Unbounded Classes and Normal Functions*}
paulson@13223
     6
haftmann@16417
     7
theory Normal imports Main begin
paulson@13223
     8
paulson@13223
     9
text{*
paulson@13223
    10
One source is the book
paulson@13223
    11
paulson@13223
    12
Frank R. Drake.
paulson@13223
    13
\emph{Set Theory: An Introduction to Large Cardinals}.
paulson@13223
    14
North-Holland, 1974.
paulson@13223
    15
*}
paulson@13223
    16
paulson@13223
    17
paulson@13223
    18
subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
paulson@13223
    19
wenzelm@21233
    20
definition
wenzelm@21404
    21
  Closed :: "(i=>o) => o" where
paulson@13223
    22
    "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
paulson@13223
    23
wenzelm@21404
    24
definition
wenzelm@21404
    25
  Unbounded :: "(i=>o) => o" where
paulson@13223
    26
    "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"
paulson@13223
    27
wenzelm@21404
    28
definition
wenzelm@21404
    29
  Closed_Unbounded :: "(i=>o) => o" where
paulson@13223
    30
    "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"
paulson@13223
    31
paulson@13223
    32
paulson@13223
    33
subsubsection{*Simple facts about c.u. classes*}
paulson@13223
    34
paulson@13223
    35
lemma ClosedI:
paulson@13223
    36
     "[| !!I. [| I \<noteq> 0; \<forall>i\<in>I. Ord(i) \<and> P(i) |] ==> P(\<Union>(I)) |] 
paulson@13223
    37
      ==> Closed(P)"
paulson@13223
    38
by (simp add: Closed_def)
paulson@13223
    39
paulson@13223
    40
lemma ClosedD:
paulson@13223
    41
     "[| Closed(P); I \<noteq> 0; !!i. i\<in>I ==> Ord(i); !!i. i\<in>I ==> P(i) |] 
paulson@13223
    42
      ==> P(\<Union>(I))"
paulson@13223
    43
by (simp add: Closed_def)
paulson@13223
    44
paulson@13223
    45
lemma UnboundedD:
paulson@13223
    46
     "[| Unbounded(P);  Ord(i) |] ==> \<exists>j. i<j \<and> P(j)"
paulson@13223
    47
by (simp add: Unbounded_def)
paulson@13223
    48
paulson@13223
    49
lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ==> Unbounded(C)"
paulson@13223
    50
by (simp add: Closed_Unbounded_def) 
paulson@13223
    51
paulson@13223
    52
paulson@13223
    53
text{*The universal class, V, is closed and unbounded.
paulson@13223
    54
      A bit odd, since C. U. concerns only ordinals, but it's used below!*}
paulson@13223
    55
theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(\<lambda>x. True)"
paulson@13223
    56
by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
paulson@13223
    57
paulson@13223
    58
text{*The class of ordinals, @{term Ord}, is closed and unbounded.*}
paulson@13223
    59
theorem Closed_Unbounded_Ord   [simp]: "Closed_Unbounded(Ord)"
paulson@13223
    60
by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
paulson@13223
    61
paulson@13223
    62
text{*The class of limit ordinals, @{term Limit}, is closed and unbounded.*}
paulson@13223
    63
theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"
paulson@13223
    64
apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union, 
paulson@13223
    65
       clarify)
paulson@13223
    66
apply (rule_tac x="i++nat" in exI)  
paulson@13223
    67
apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0) 
paulson@13223
    68
done
paulson@13223
    69
paulson@13223
    70
text{*The class of cardinals, @{term Card}, is closed and unbounded.*}
paulson@13223
    71
theorem Closed_Unbounded_Card  [simp]: "Closed_Unbounded(Card)"
paulson@13223
    72
apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
paulson@13223
    73
apply (blast intro: lt_csucc Card_csucc)
paulson@13223
    74
done
paulson@13223
    75
paulson@13223
    76
paulson@13223
    77
subsubsection{*The intersection of any set-indexed family of c.u. classes is
paulson@13223
    78
      c.u.*}
paulson@13223
    79
paulson@13223
    80
text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
wenzelm@13428
    81
locale cub_family =
paulson@13223
    82
  fixes P and A
paulson@13223
    83
  fixes next_greater -- "the next ordinal satisfying class @{term A}"
paulson@13223
    84
  fixes sup_greater  -- "sup of those ordinals over all @{term A}"
paulson@13223
    85
  assumes closed:    "a\<in>A ==> Closed(P(a))"
paulson@13223
    86
      and unbounded: "a\<in>A ==> Unbounded(P(a))"
paulson@13223
    87
      and A_non0: "A\<noteq>0"
skalberg@14171
    88
  defines "next_greater(a,x) == \<mu> y. x<y \<and> P(a,y)"
paulson@13223
    89
      and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
paulson@13223
    90
 
paulson@13223
    91
paulson@13223
    92
text{*Trivial that the intersection is closed.*}
paulson@13223
    93
lemma (in cub_family) Closed_INT: "Closed(\<lambda>x. \<forall>i\<in>A. P(i,x))"
paulson@13223
    94
by (blast intro: ClosedI ClosedD [OF closed])
paulson@13223
    95
paulson@13223
    96
text{*All remaining effort goes to show that the intersection is unbounded.*}
paulson@13223
    97
paulson@13223
    98
lemma (in cub_family) Ord_sup_greater:
paulson@13223
    99
     "Ord(sup_greater(x))"
paulson@13223
   100
by (simp add: sup_greater_def next_greater_def)
paulson@13223
   101
paulson@13223
   102
lemma (in cub_family) Ord_next_greater:
paulson@13223
   103
     "Ord(next_greater(a,x))"
paulson@13223
   104
by (simp add: next_greater_def Ord_Least)
paulson@13223
   105
paulson@13223
   106
text{*@{term next_greater} works as expected: it returns a larger value
paulson@13223
   107
and one that belongs to class @{term "P(a)"}. *}
paulson@13223
   108
lemma (in cub_family) next_greater_lemma:
paulson@13223
   109
     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x)) \<and> x < next_greater(a,x)"
paulson@13223
   110
apply (simp add: next_greater_def)
paulson@13223
   111
apply (rule exE [OF UnboundedD [OF unbounded]])
paulson@13223
   112
  apply assumption+
paulson@13223
   113
apply (blast intro: LeastI2 lt_Ord2) 
paulson@13223
   114
done
paulson@13223
   115
paulson@13223
   116
lemma (in cub_family) next_greater_in_P:
paulson@13223
   117
     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x))"
paulson@13223
   118
by (blast dest: next_greater_lemma)
paulson@13223
   119
paulson@13223
   120
lemma (in cub_family) next_greater_gt:
paulson@13223
   121
     "[| Ord(x); a\<in>A |] ==> x < next_greater(a,x)"
paulson@13223
   122
by (blast dest: next_greater_lemma)
paulson@13223
   123
paulson@13223
   124
lemma (in cub_family) sup_greater_gt:
paulson@13223
   125
     "Ord(x) ==> x < sup_greater(x)"
paulson@13223
   126
apply (simp add: sup_greater_def)
paulson@13223
   127
apply (insert A_non0)
paulson@13223
   128
apply (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)
paulson@13223
   129
done
paulson@13223
   130
paulson@13223
   131
lemma (in cub_family) next_greater_le_sup_greater:
paulson@13223
   132
     "a\<in>A ==> next_greater(a,x) \<le> sup_greater(x)"
paulson@13223
   133
apply (simp add: sup_greater_def) 
paulson@13223
   134
apply (blast intro: UN_upper_le Ord_next_greater)
paulson@13223
   135
done
paulson@13223
   136
paulson@13223
   137
lemma (in cub_family) omega_sup_greater_eq_UN:
paulson@13223
   138
     "[| Ord(x); a\<in>A |] 
paulson@13223
   139
      ==> sup_greater^\<omega> (x) = 
paulson@13223
   140
          (\<Union>n\<in>nat. next_greater(a, sup_greater^n (x)))"
paulson@13223
   141
apply (simp add: iterates_omega_def)
paulson@13223
   142
apply (rule le_anti_sym)
paulson@13223
   143
apply (rule le_implies_UN_le_UN) 
paulson@13223
   144
apply (blast intro: leI next_greater_gt Ord_iterates Ord_sup_greater)  
paulson@13223
   145
txt{*Opposite bound:
paulson@13223
   146
@{subgoals[display,indent=0,margin=65]}
paulson@13223
   147
*}
paulson@13223
   148
apply (rule UN_least_le) 
paulson@13223
   149
apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
paulson@13223
   150
apply (rule_tac a="succ(n)" in UN_upper_le)
paulson@13223
   151
apply (simp_all add: next_greater_le_sup_greater) 
paulson@13223
   152
apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
paulson@13223
   153
done
paulson@13223
   154
paulson@13223
   155
lemma (in cub_family) P_omega_sup_greater:
paulson@13223
   156
     "[| Ord(x); a\<in>A |] ==> P(a, sup_greater^\<omega> (x))"
paulson@13223
   157
apply (simp add: omega_sup_greater_eq_UN)
paulson@13223
   158
apply (rule ClosedD [OF closed]) 
paulson@13223
   159
apply (blast intro: ltD, auto)
paulson@13223
   160
apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)
paulson@13223
   161
apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)
paulson@13223
   162
done
paulson@13223
   163
paulson@13223
   164
lemma (in cub_family) omega_sup_greater_gt:
paulson@13223
   165
     "Ord(x) ==> x < sup_greater^\<omega> (x)"
paulson@13223
   166
apply (simp add: iterates_omega_def)
paulson@13223
   167
apply (rule UN_upper_lt [of 1], simp_all) 
paulson@13223
   168
 apply (blast intro: sup_greater_gt) 
paulson@13223
   169
apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
paulson@13223
   170
done
paulson@13223
   171
paulson@13223
   172
lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
paulson@13223
   173
apply (unfold Unbounded_def)  
paulson@13223
   174
apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater) 
paulson@13223
   175
done
paulson@13223
   176
paulson@13223
   177
lemma (in cub_family) Closed_Unbounded_INT: 
paulson@13223
   178
     "Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
paulson@13223
   179
by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)
paulson@13223
   180
paulson@13223
   181
paulson@13223
   182
theorem Closed_Unbounded_INT:
paulson@13223
   183
    "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))
paulson@13223
   184
     ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"
paulson@13223
   185
apply (case_tac "A=0", simp)
wenzelm@13428
   186
apply (rule cub_family.Closed_Unbounded_INT [OF cub_family.intro])
paulson@13223
   187
apply (simp_all add: Closed_Unbounded_def)
paulson@13223
   188
done
paulson@13223
   189
paulson@13223
   190
lemma Int_iff_INT2:
paulson@13223
   191
     "P(x) \<and> Q(x)  <->  (\<forall>i\<in>2. (i=0 --> P(x)) \<and> (i=1 --> Q(x)))"
paulson@13223
   192
by auto
paulson@13223
   193
paulson@13223
   194
theorem Closed_Unbounded_Int:
paulson@13223
   195
     "[| Closed_Unbounded(P); Closed_Unbounded(Q) |] 
paulson@13223
   196
      ==> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"
paulson@13223
   197
apply (simp only: Int_iff_INT2)
paulson@13223
   198
apply (rule Closed_Unbounded_INT, auto) 
paulson@13223
   199
done
paulson@13223
   200
paulson@13223
   201
paulson@13223
   202
subsection {*Normal Functions*} 
paulson@13223
   203
wenzelm@21233
   204
definition
wenzelm@21404
   205
  mono_le_subset :: "(i=>i) => o" where
paulson@13223
   206
    "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
paulson@13223
   207
wenzelm@21404
   208
definition
wenzelm@21404
   209
  mono_Ord :: "(i=>i) => o" where
paulson@13223
   210
    "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"
paulson@13223
   211
wenzelm@21404
   212
definition
wenzelm@21404
   213
  cont_Ord :: "(i=>i) => o" where
paulson@13223
   214
    "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"
paulson@13223
   215
wenzelm@21404
   216
definition
wenzelm@21404
   217
  Normal :: "(i=>i) => o" where
paulson@13223
   218
    "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"
paulson@13223
   219
paulson@13223
   220
paulson@13223
   221
subsubsection{*Immediate properties of the definitions*}
paulson@13223
   222
paulson@13223
   223
lemma NormalI:
paulson@13223
   224
     "[|!!i j. i<j ==> F(i) < F(j);  !!l. Limit(l) ==> F(l) = (\<Union>i<l. F(i))|]
paulson@13223
   225
      ==> Normal(F)"
paulson@13223
   226
by (simp add: Normal_def mono_Ord_def cont_Ord_def)
paulson@13223
   227
paulson@13223
   228
lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
paulson@13223
   229
apply (simp add: mono_Ord_def) 
paulson@13223
   230
apply (blast intro: lt_Ord) 
paulson@13223
   231
done
paulson@13223
   232
paulson@13223
   233
lemma mono_Ord_imp_mono: "[| i<j; mono_Ord(F) |] ==> F(i) < F(j)"
paulson@13223
   234
by (simp add: mono_Ord_def)
paulson@13223
   235
paulson@13223
   236
lemma Normal_imp_Ord [simp]: "[| Normal(F); Ord(i) |] ==> Ord(F(i))"
paulson@13223
   237
by (simp add: Normal_def mono_Ord_imp_Ord) 
paulson@13223
   238
paulson@13223
   239
lemma Normal_imp_cont: "[| Normal(F); Limit(l) |] ==> F(l) = (\<Union>i<l. F(i))"
paulson@13223
   240
by (simp add: Normal_def cont_Ord_def)
paulson@13223
   241
paulson@13223
   242
lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
paulson@13223
   243
by (simp add: Normal_def mono_Ord_def)
paulson@13223
   244
paulson@13223
   245
lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
paulson@13223
   246
apply (induct i rule: trans_induct3_rule)
paulson@13223
   247
  apply (simp add: subset_imp_le)
paulson@13223
   248
 apply (subgoal_tac "F(x) < F(succ(x))")
paulson@13223
   249
  apply (force intro: lt_trans1)
paulson@13223
   250
 apply (simp add: Normal_def mono_Ord_def)
paulson@13223
   251
apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
paulson@13223
   252
 apply (simp add: Normal_imp_cont Limit_OUN_eq) 
paulson@13223
   253
apply (blast intro: ltD le_implies_OUN_le_OUN)
paulson@13223
   254
done
paulson@13223
   255
paulson@13223
   256
paulson@13223
   257
subsubsection{*The class of fixedpoints is closed and unbounded*}
paulson@13223
   258
paulson@13223
   259
text{*The proof is from Drake, pages 113--114.*}
paulson@13223
   260
paulson@13223
   261
lemma mono_Ord_imp_le_subset: "mono_Ord(F) ==> mono_le_subset(F)"
paulson@13223
   262
apply (simp add: mono_le_subset_def, clarify)
paulson@13223
   263
apply (subgoal_tac "F(i)\<le>F(j)", blast dest: le_imp_subset) 
paulson@13223
   264
apply (simp add: le_iff) 
paulson@13223
   265
apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono) 
paulson@13223
   266
done
paulson@13223
   267
paulson@13223
   268
text{*The following equation is taken for granted in any set theory text.*}
paulson@13223
   269
lemma cont_Ord_Union:
paulson@13223
   270
     "[| cont_Ord(F); mono_le_subset(F); X=0 --> F(0)=0; \<forall>x\<in>X. Ord(x) |] 
paulson@13223
   271
      ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
paulson@13223
   272
apply (frule Ord_set_cases)
paulson@13223
   273
apply (erule disjE, force) 
paulson@13223
   274
apply (thin_tac "X=0 --> ?Q", auto)
paulson@13223
   275
 txt{*The trival case of @{term "\<Union>X \<in> X"}*}
paulson@13223
   276
 apply (rule equalityI, blast intro: Ord_Union_eq_succD) 
paulson@13223
   277
 apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff) 
paulson@13223
   278
 apply (blast elim: equalityE)
paulson@13223
   279
txt{*The limit case, @{term "Limit(\<Union>X)"}:
paulson@13223
   280
@{subgoals[display,indent=0,margin=65]}
paulson@13223
   281
*}
paulson@13223
   282
apply (simp add: OUN_Union_eq cont_Ord_def)
paulson@13223
   283
apply (rule equalityI) 
paulson@13223
   284
txt{*First inclusion:*}
paulson@13223
   285
 apply (rule UN_least [OF OUN_least])
paulson@13223
   286
 apply (simp add: mono_le_subset_def, blast intro: leI) 
paulson@13223
   287
txt{*Second inclusion:*}
paulson@13223
   288
apply (rule UN_least) 
paulson@13223
   289
apply (frule Union_upper_le, blast, blast intro: Ord_Union)
paulson@13223
   290
apply (erule leE, drule ltD, elim UnionE)
paulson@13223
   291
 apply (simp add: OUnion_def)
paulson@13223
   292
 apply blast+
paulson@13223
   293
done
paulson@13223
   294
paulson@13223
   295
lemma Normal_Union:
paulson@13223
   296
     "[| X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
paulson@13223
   297
apply (simp add: Normal_def) 
paulson@13223
   298
apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union) 
paulson@13223
   299
done
paulson@13223
   300
paulson@13223
   301
lemma Normal_imp_fp_Closed: "Normal(F) ==> Closed(\<lambda>i. F(i) = i)"
paulson@13223
   302
apply (simp add: Closed_def ball_conj_distrib, clarify)
paulson@13223
   303
apply (frule Ord_set_cases)
paulson@13223
   304
apply (auto simp add: Normal_Union)
paulson@13223
   305
done
paulson@13223
   306
paulson@13223
   307
paulson@13223
   308
lemma iterates_Normal_increasing:
paulson@13223
   309
     "[| n\<in>nat;  x < F(x);  Normal(F) |] 
paulson@13223
   310
      ==> F^n (x) < F^(succ(n)) (x)"  
paulson@13223
   311
apply (induct n rule: nat_induct)
paulson@13223
   312
apply (simp_all add: Normal_imp_mono)
paulson@13223
   313
done
paulson@13223
   314
paulson@13223
   315
lemma Ord_iterates_Normal:
paulson@13223
   316
     "[| n\<in>nat;  Normal(F);  Ord(x) |] ==> Ord(F^n (x))"  
paulson@13223
   317
by (simp add: Ord_iterates) 
paulson@13223
   318
paulson@13223
   319
text{*THIS RESULT IS UNUSED*}
paulson@13223
   320
lemma iterates_omega_Limit:
paulson@13223
   321
     "[| Normal(F);  x < F(x) |] ==> Limit(F^\<omega> (x))"  
paulson@13223
   322
apply (frule lt_Ord) 
paulson@13223
   323
apply (simp add: iterates_omega_def)
paulson@13223
   324
apply (rule increasing_LimitI) 
paulson@13223
   325
   --"this lemma is @{thm increasing_LimitI [no_vars]}"
paulson@13223
   326
 apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
paulson@13223
   327
                     Ord_UN Ord_iterates lt_imp_0_lt
paulson@13268
   328
                     iterates_Normal_increasing, clarify)
paulson@13223
   329
apply (rule bexI) 
paulson@13223
   330
 apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
paulson@13223
   331
apply (rule UN_I, erule nat_succI) 
paulson@13223
   332
apply (blast intro:  iterates_Normal_increasing Ord_iterates_Normal
paulson@13223
   333
                     ltD [OF lt_trans1, OF succ_leI, OF ltI]) 
paulson@13223
   334
done
paulson@13223
   335
paulson@13223
   336
lemma iterates_omega_fixedpoint:
paulson@13223
   337
     "[| Normal(F); Ord(a) |] ==> F(F^\<omega> (a)) = F^\<omega> (a)" 
paulson@13223
   338
apply (frule Normal_increasing, assumption)
paulson@13223
   339
apply (erule leE) 
paulson@13223
   340
 apply (simp_all add: iterates_omega_triv [OF sym])  (*for subgoal 2*)
paulson@13223
   341
apply (simp add:  iterates_omega_def Normal_Union) 
paulson@13223
   342
apply (rule equalityI, force simp add: nat_succI) 
paulson@13223
   343
txt{*Opposite inclusion:
paulson@13223
   344
@{subgoals[display,indent=0,margin=65]}
paulson@13223
   345
*}
paulson@13223
   346
apply clarify
paulson@13223
   347
apply (rule UN_I, assumption) 
paulson@13223
   348
apply (frule iterates_Normal_increasing, assumption, assumption, simp)
paulson@13223
   349
apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F]) 
paulson@13223
   350
done
paulson@13223
   351
paulson@13223
   352
lemma iterates_omega_increasing:
paulson@13223
   353
     "[| Normal(F); Ord(a) |] ==> a \<le> F^\<omega> (a)"   
paulson@13223
   354
apply (unfold iterates_omega_def)
paulson@13223
   355
apply (rule UN_upper_le [of 0], simp_all)
paulson@13223
   356
done
paulson@13223
   357
paulson@13223
   358
lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\<lambda>i. F(i) = i)"
paulson@13223
   359
apply (unfold Unbounded_def, clarify)
paulson@13223
   360
apply (rule_tac x="F^\<omega> (succ(i))" in exI)
paulson@13223
   361
apply (simp add: iterates_omega_fixedpoint) 
paulson@13223
   362
apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])
paulson@13223
   363
done
paulson@13223
   364
paulson@13223
   365
paulson@13223
   366
theorem Normal_imp_fp_Closed_Unbounded: 
paulson@13223
   367
     "Normal(F) ==> Closed_Unbounded(\<lambda>i. F(i) = i)"
paulson@13223
   368
by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed
paulson@13223
   369
              Normal_imp_fp_Unbounded)
paulson@13223
   370
paulson@13223
   371
paulson@13223
   372
subsubsection{*Function @{text normalize}*}
paulson@13223
   373
paulson@13223
   374
text{*Function @{text normalize} maps a function @{text F} to a 
paulson@13223
   375
      normal function that bounds it above.  The result is normal if and
paulson@13223
   376
      only if @{text F} is continuous: succ is not bounded above by any 
paulson@13223
   377
      normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
paulson@13223
   378
*}
wenzelm@21233
   379
definition
wenzelm@21404
   380
  normalize :: "[i=>i, i] => i" where
paulson@13223
   381
    "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
paulson@13223
   382
paulson@13223
   383
paulson@13223
   384
lemma Ord_normalize [simp, intro]:
paulson@13223
   385
     "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
paulson@13223
   386
apply (induct a rule: trans_induct3_rule)
paulson@13223
   387
apply (simp_all add: ltD def_transrec2 [OF normalize_def])
paulson@13223
   388
done
paulson@13223
   389
paulson@13223
   390
lemma normalize_lemma [rule_format]:
paulson@13223
   391
     "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |] 
paulson@13223
   392
      ==> \<forall>a. a < b --> normalize(F, a) < normalize(F, b)"
paulson@13223
   393
apply (erule trans_induct3)
paulson@13223
   394
  apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
paulson@13223
   395
 apply clarify
paulson@13223
   396
apply (rule Un_upper2_lt) 
paulson@13223
   397
  apply auto
paulson@13223
   398
 apply (drule spec, drule mp, assumption) 
paulson@13223
   399
 apply (erule leI) 
paulson@13223
   400
apply (drule Limit_has_succ, assumption)
paulson@13223
   401
apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
paulson@13223
   402
done  
paulson@13223
   403
paulson@13223
   404
lemma normalize_increasing:
paulson@13223
   405
     "[| a < b;  !!x. Ord(x) ==> Ord(F(x)) |] 
paulson@13223
   406
      ==> normalize(F, a) < normalize(F, b)"
paulson@13223
   407
by (blast intro!: normalize_lemma intro: lt_Ord2) 
paulson@13223
   408
paulson@13223
   409
theorem Normal_normalize:
paulson@13223
   410
     "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
paulson@13223
   411
apply (rule NormalI) 
paulson@13223
   412
apply (blast intro!: normalize_increasing)
paulson@13223
   413
apply (simp add: def_transrec2 [OF normalize_def])
paulson@13223
   414
done
paulson@13223
   415
paulson@13223
   416
theorem le_normalize:
paulson@13223
   417
     "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |] 
paulson@13223
   418
      ==> F(a) \<le> normalize(F,a)"
paulson@13223
   419
apply (erule trans_induct3) 
paulson@13223
   420
apply (simp_all add: def_transrec2 [OF normalize_def])
paulson@13223
   421
apply (simp add: Un_upper1_le) 
paulson@13223
   422
apply (simp add: cont_Ord_def) 
paulson@13223
   423
apply (blast intro: ltD le_implies_OUN_le_OUN)
paulson@13223
   424
done
paulson@13223
   425
paulson@13223
   426
paulson@13223
   427
subsection {*The Alephs*}
paulson@13223
   428
text {*This is the well-known transfinite enumeration of the cardinal 
paulson@13223
   429
numbers.*}
paulson@13223
   430
wenzelm@21233
   431
definition
wenzelm@21404
   432
  Aleph :: "i => i" where
paulson@13223
   433
    "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
paulson@13223
   434
wenzelm@21233
   435
notation (xsymbols)
wenzelm@21233
   436
  Aleph  ("\<aleph>_" [90] 90)
paulson@13223
   437
paulson@13223
   438
lemma Card_Aleph [simp, intro]:
paulson@13223
   439
     "Ord(a) ==> Card(Aleph(a))"
paulson@13223
   440
apply (erule trans_induct3) 
paulson@13223
   441
apply (simp_all add: Card_csucc Card_nat Card_is_Ord
paulson@13223
   442
                     def_transrec2 [OF Aleph_def])
paulson@13223
   443
done
paulson@13223
   444
paulson@13223
   445
lemma Aleph_lemma [rule_format]:
paulson@13223
   446
     "Ord(b) ==> \<forall>a. a < b --> Aleph(a) < Aleph(b)"
paulson@13223
   447
apply (erule trans_induct3) 
paulson@13223
   448
apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])  
paulson@13223
   449
apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
paulson@13223
   450
apply (drule Limit_has_succ, assumption)
paulson@13223
   451
apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
paulson@13223
   452
done  
paulson@13223
   453
paulson@13223
   454
lemma Aleph_increasing:
paulson@13223
   455
     "a < b ==> Aleph(a) < Aleph(b)"
paulson@13223
   456
by (blast intro!: Aleph_lemma intro: lt_Ord2) 
paulson@13223
   457
paulson@13223
   458
theorem Normal_Aleph: "Normal(Aleph)"
paulson@13223
   459
apply (rule NormalI) 
paulson@13223
   460
apply (blast intro!: Aleph_increasing)
paulson@13223
   461
apply (simp add: def_transrec2 [OF Aleph_def])
paulson@13223
   462
done
paulson@13223
   463
paulson@13223
   464
end