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