src/ZF/Constructible/L_axioms.thy
changeset 13323 2c287f50c9f3
parent 13316 d16629fd0f95
child 13339 0f89104dd377
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Jul 09 13:41:38 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Jul 09 15:39:44 2002 +0200
     1.3 @@ -292,7 +292,7 @@
     1.4  apply (intro Imp_reflection All_reflection, assumption)
     1.5  done
     1.6  
     1.7 -lemmas FOL_reflection = 
     1.8 +lemmas FOL_reflections = 
     1.9          Triv_reflection Not_reflection And_reflection Or_reflection
    1.10          Imp_reflection Iff_reflection Ex_reflection All_reflection
    1.11          Rex_reflection Rall_reflection
    1.12 @@ -340,6 +340,39 @@
    1.13     "8"  == "succ(7)"
    1.14     "9"  == "succ(8)"
    1.15  
    1.16 +
    1.17 +subsubsection{*The Empty Set*}
    1.18 +
    1.19 +constdefs empty_fm :: "i=>i"
    1.20 +    "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
    1.21 +
    1.22 +lemma empty_type [TC]:
    1.23 +     "x \<in> nat ==> empty_fm(x) \<in> formula"
    1.24 +by (simp add: empty_fm_def) 
    1.25 +
    1.26 +lemma arity_empty_fm [simp]:
    1.27 +     "x \<in> nat ==> arity(empty_fm(x)) = succ(x)"
    1.28 +by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac) 
    1.29 +
    1.30 +lemma sats_empty_fm [simp]:
    1.31 +   "[| x \<in> nat; env \<in> list(A)|]
    1.32 +    ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))"
    1.33 +by (simp add: empty_fm_def empty_def)
    1.34 +
    1.35 +lemma empty_iff_sats:
    1.36 +      "[| nth(i,env) = x; nth(j,env) = y; 
    1.37 +          i \<in> nat; env \<in> list(A)|]
    1.38 +       ==> empty(**A, x) <-> sats(A, empty_fm(i), env)"
    1.39 +by simp
    1.40 +
    1.41 +theorem empty_reflection:
    1.42 +     "REFLECTS[\<lambda>x. empty(L,f(x)), 
    1.43 +               \<lambda>i x. empty(**Lset(i),f(x))]"
    1.44 +apply (simp only: empty_def setclass_simps)
    1.45 +apply (intro FOL_reflections)  
    1.46 +done
    1.47 +
    1.48 +
    1.49  subsubsection{*Unordered pairs*}
    1.50  
    1.51  constdefs upair_fm :: "[i,i,i]=>i"
    1.52 @@ -384,7 +417,7 @@
    1.53       "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)), 
    1.54                 \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]" 
    1.55  apply (simp add: upair_def)
    1.56 -apply (intro FOL_reflection)  
    1.57 +apply (intro FOL_reflections)  
    1.58  done
    1.59  
    1.60  subsubsection{*Ordered pairs*}
    1.61 @@ -420,7 +453,7 @@
    1.62       "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)), 
    1.63                 \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
    1.64  apply (simp only: pair_def setclass_simps)
    1.65 -apply (intro FOL_reflection upair_reflection)  
    1.66 +apply (intro FOL_reflections upair_reflection)  
    1.67  done
    1.68  
    1.69  
    1.70 @@ -456,7 +489,7 @@
    1.71       "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)), 
    1.72                 \<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
    1.73  apply (simp only: union_def setclass_simps)
    1.74 -apply (intro FOL_reflection)  
    1.75 +apply (intro FOL_reflections)  
    1.76  done
    1.77  
    1.78  
    1.79 @@ -493,7 +526,41 @@
    1.80       "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)), 
    1.81                 \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
    1.82  apply (simp only: is_cons_def setclass_simps)
    1.83 -apply (intro FOL_reflection upair_reflection union_reflection)  
    1.84 +apply (intro FOL_reflections upair_reflection union_reflection)  
    1.85 +done
    1.86 +
    1.87 +
    1.88 +subsubsection{*Successor Function*}
    1.89 +
    1.90 +constdefs succ_fm :: "[i,i]=>i"
    1.91 +    "succ_fm(x,y) == cons_fm(x,x,y)"
    1.92 +
    1.93 +lemma succ_type [TC]:
    1.94 +     "[| x \<in> nat; y \<in> nat |] ==> succ_fm(x,y) \<in> formula"
    1.95 +by (simp add: succ_fm_def) 
    1.96 +
    1.97 +lemma arity_succ_fm [simp]:
    1.98 +     "[| x \<in> nat; y \<in> nat |] 
    1.99 +      ==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)"
   1.100 +by (simp add: succ_fm_def)
   1.101 +
   1.102 +lemma sats_succ_fm [simp]:
   1.103 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.104 +    ==> sats(A, succ_fm(x,y), env) <-> 
   1.105 +        successor(**A, nth(x,env), nth(y,env))"
   1.106 +by (simp add: succ_fm_def successor_def)
   1.107 +
   1.108 +lemma successor_iff_sats:
   1.109 +      "[| nth(i,env) = x; nth(j,env) = y; 
   1.110 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.111 +       ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)"
   1.112 +by simp
   1.113 +
   1.114 +theorem successor_reflection:
   1.115 +     "REFLECTS[\<lambda>x. successor(L,f(x),g(x)), 
   1.116 +               \<lambda>i x. successor(**Lset(i),f(x),g(x))]"
   1.117 +apply (simp only: successor_def setclass_simps)
   1.118 +apply (intro cons_reflection)  
   1.119  done
   1.120  
   1.121  
   1.122 @@ -530,7 +597,7 @@
   1.123       "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), 
   1.124                 \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" 
   1.125  apply (simp only: fun_apply_def setclass_simps)
   1.126 -apply (intro FOL_reflection pair_reflection)  
   1.127 +apply (intro FOL_reflections pair_reflection)  
   1.128  done
   1.129  
   1.130  
   1.131 @@ -542,13 +609,13 @@
   1.132  lemma sats_subset_fm':
   1.133     "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.134      ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))" 
   1.135 -by (simp add: subset_fm_def subset_def) 
   1.136 +by (simp add: subset_fm_def Relative.subset_def) 
   1.137  
   1.138  theorem subset_reflection:
   1.139       "REFLECTS[\<lambda>x. subset(L,f(x),g(x)), 
   1.140                 \<lambda>i x. subset(**Lset(i),f(x),g(x))]" 
   1.141 -apply (simp only: subset_def setclass_simps)
   1.142 -apply (intro FOL_reflection)  
   1.143 +apply (simp only: Relative.subset_def setclass_simps)
   1.144 +apply (intro FOL_reflections)  
   1.145  done
   1.146  
   1.147  lemma sats_transset_fm':
   1.148 @@ -560,7 +627,7 @@
   1.149       "REFLECTS[\<lambda>x. transitive_set(L,f(x)),
   1.150                 \<lambda>i x. transitive_set(**Lset(i),f(x))]"
   1.151  apply (simp only: transitive_set_def setclass_simps)
   1.152 -apply (intro FOL_reflection subset_reflection)  
   1.153 +apply (intro FOL_reflections subset_reflection)  
   1.154  done
   1.155  
   1.156  lemma sats_ordinal_fm':
   1.157 @@ -576,7 +643,7 @@
   1.158  theorem ordinal_reflection:
   1.159       "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
   1.160  apply (simp only: ordinal_def setclass_simps)
   1.161 -apply (intro FOL_reflection transitive_set_reflection)  
   1.162 +apply (intro FOL_reflections transitive_set_reflection)  
   1.163  done
   1.164  
   1.165  
   1.166 @@ -615,7 +682,7 @@
   1.167       "REFLECTS[\<lambda>x. membership(L,f(x),g(x)), 
   1.168                 \<lambda>i x. membership(**Lset(i),f(x),g(x))]"
   1.169  apply (simp only: membership_def setclass_simps)
   1.170 -apply (intro FOL_reflection pair_reflection)  
   1.171 +apply (intro FOL_reflections pair_reflection)  
   1.172  done
   1.173  
   1.174  subsubsection{*Predecessor Set*}
   1.175 @@ -654,7 +721,7 @@
   1.176       "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)), 
   1.177                 \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" 
   1.178  apply (simp only: pred_set_def setclass_simps)
   1.179 -apply (intro FOL_reflection pair_reflection)  
   1.180 +apply (intro FOL_reflections pair_reflection)  
   1.181  done
   1.182  
   1.183  
   1.184 @@ -694,7 +761,7 @@
   1.185       "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)), 
   1.186                 \<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
   1.187  apply (simp only: is_domain_def setclass_simps)
   1.188 -apply (intro FOL_reflection pair_reflection)  
   1.189 +apply (intro FOL_reflections pair_reflection)  
   1.190  done
   1.191  
   1.192  
   1.193 @@ -733,10 +800,51 @@
   1.194       "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)), 
   1.195                 \<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
   1.196  apply (simp only: is_range_def setclass_simps)
   1.197 -apply (intro FOL_reflection pair_reflection)  
   1.198 +apply (intro FOL_reflections pair_reflection)  
   1.199  done
   1.200  
   1.201   
   1.202 +subsubsection{*Field*}
   1.203 +
   1.204 +(* "is_field(M,r,z) == 
   1.205 +	\<exists>dr[M]. is_domain(M,r,dr) & 
   1.206 +            (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
   1.207 +constdefs field_fm :: "[i,i]=>i"
   1.208 +    "field_fm(r,z) == 
   1.209 +       Exists(And(domain_fm(succ(r),0), 
   1.210 +              Exists(And(range_fm(succ(succ(r)),0), 
   1.211 +                         union_fm(1,0,succ(succ(z)))))))"
   1.212 +
   1.213 +lemma field_type [TC]:
   1.214 +     "[| x \<in> nat; y \<in> nat |] ==> field_fm(x,y) \<in> formula"
   1.215 +by (simp add: field_fm_def) 
   1.216 +
   1.217 +lemma arity_field_fm [simp]:
   1.218 +     "[| x \<in> nat; y \<in> nat |] 
   1.219 +      ==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)"
   1.220 +by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.221 +
   1.222 +lemma sats_field_fm [simp]:
   1.223 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.224 +    ==> sats(A, field_fm(x,y), env) <-> 
   1.225 +        is_field(**A, nth(x,env), nth(y,env))"
   1.226 +by (simp add: field_fm_def is_field_def)
   1.227 +
   1.228 +lemma field_iff_sats:
   1.229 +      "[| nth(i,env) = x; nth(j,env) = y; 
   1.230 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.231 +       ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)"
   1.232 +by simp
   1.233 +
   1.234 +theorem field_reflection:
   1.235 +     "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)), 
   1.236 +               \<lambda>i x. is_field(**Lset(i),f(x),g(x))]"
   1.237 +apply (simp only: is_field_def setclass_simps)
   1.238 +apply (intro FOL_reflections domain_reflection range_reflection
   1.239 +             union_reflection)
   1.240 +done
   1.241 +
   1.242 +
   1.243  subsubsection{*Image*}
   1.244  
   1.245  (* "image(M,r,A,z) == 
   1.246 @@ -761,7 +869,7 @@
   1.247     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.248      ==> sats(A, image_fm(x,y,z), env) <-> 
   1.249          image(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.250 -by (simp add: image_fm_def image_def)
   1.251 +by (simp add: image_fm_def Relative.image_def)
   1.252  
   1.253  lemma image_iff_sats:
   1.254        "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.255 @@ -772,8 +880,8 @@
   1.256  theorem image_reflection:
   1.257       "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)), 
   1.258                 \<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
   1.259 -apply (simp only: image_def setclass_simps)
   1.260 -apply (intro FOL_reflection pair_reflection)  
   1.261 +apply (simp only: Relative.image_def setclass_simps)
   1.262 +apply (intro FOL_reflections pair_reflection)  
   1.263  done
   1.264  
   1.265  
   1.266 @@ -808,7 +916,7 @@
   1.267       "REFLECTS[\<lambda>x. is_relation(L,f(x)), 
   1.268                 \<lambda>i x. is_relation(**Lset(i),f(x))]"
   1.269  apply (simp only: is_relation_def setclass_simps)
   1.270 -apply (intro FOL_reflection pair_reflection)  
   1.271 +apply (intro FOL_reflections pair_reflection)  
   1.272  done
   1.273  
   1.274  
   1.275 @@ -848,7 +956,7 @@
   1.276       "REFLECTS[\<lambda>x. is_function(L,f(x)), 
   1.277                 \<lambda>i x. is_function(**Lset(i),f(x))]"
   1.278  apply (simp only: is_function_def setclass_simps)
   1.279 -apply (intro FOL_reflection pair_reflection)  
   1.280 +apply (intro FOL_reflections pair_reflection)  
   1.281  done
   1.282  
   1.283  
   1.284 @@ -887,19 +995,74 @@
   1.285     ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
   1.286  by simp
   1.287  
   1.288 -lemmas function_reflection = 
   1.289 -        upair_reflection pair_reflection union_reflection
   1.290 -	cons_reflection fun_apply_reflection subset_reflection
   1.291 -	transitive_set_reflection ordinal_reflection membership_reflection
   1.292 -	pred_set_reflection domain_reflection range_reflection image_reflection
   1.293 +lemmas function_reflections = 
   1.294 +        empty_reflection upair_reflection pair_reflection union_reflection
   1.295 +	cons_reflection successor_reflection 
   1.296 +        fun_apply_reflection subset_reflection
   1.297 +	transitive_set_reflection membership_reflection
   1.298 +	pred_set_reflection domain_reflection range_reflection field_reflection
   1.299 +        image_reflection
   1.300  	is_relation_reflection is_function_reflection
   1.301  
   1.302 +lemmas function_iff_sats = 
   1.303 +        empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats
   1.304 +	cons_iff_sats successor_iff_sats
   1.305 +        fun_apply_iff_sats  Memrel_iff_sats
   1.306 +	pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
   1.307 +        image_iff_sats
   1.308 +	relation_iff_sats function_iff_sats
   1.309 +
   1.310  
   1.311  theorem typed_function_reflection:
   1.312       "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)), 
   1.313                 \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
   1.314  apply (simp only: typed_function_def setclass_simps)
   1.315 -apply (intro FOL_reflection function_reflection)  
   1.316 +apply (intro FOL_reflections function_reflections)  
   1.317 +done
   1.318 +
   1.319 +
   1.320 +subsubsection{*Composition of Relations*}
   1.321 +
   1.322 +(* "composition(M,r,s,t) == 
   1.323 +        \<forall>p[M]. p \<in> t <-> 
   1.324 +               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   1.325 +                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   1.326 +                xy \<in> s & yz \<in> r)" *)
   1.327 +constdefs composition_fm :: "[i,i,i]=>i"
   1.328 +  "composition_fm(r,s,t) == 
   1.329 +     Forall(Iff(Member(0,succ(t)),
   1.330 +             Exists(Exists(Exists(Exists(Exists( 
   1.331 +              And(pair_fm(4,2,5),
   1.332 +               And(pair_fm(4,3,1),
   1.333 +                And(pair_fm(3,2,0),
   1.334 +                 And(Member(1,s#+6), Member(0,r#+6))))))))))))"
   1.335 +
   1.336 +lemma composition_type [TC]:
   1.337 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> composition_fm(x,y,z) \<in> formula"
   1.338 +by (simp add: composition_fm_def) 
   1.339 +
   1.340 +lemma arity_composition_fm [simp]:
   1.341 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.342 +      ==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   1.343 +by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.344 +
   1.345 +lemma sats_composition_fm [simp]:
   1.346 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.347 +    ==> sats(A, composition_fm(x,y,z), env) <-> 
   1.348 +        composition(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.349 +by (simp add: composition_fm_def composition_def)
   1.350 +
   1.351 +lemma composition_iff_sats:
   1.352 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.353 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.354 +       ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
   1.355 +by simp
   1.356 +
   1.357 +theorem composition_reflection:
   1.358 +     "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)), 
   1.359 +               \<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]"
   1.360 +apply (simp only: composition_def setclass_simps)
   1.361 +apply (intro FOL_reflections pair_reflection)  
   1.362  done
   1.363  
   1.364  
   1.365 @@ -944,7 +1107,7 @@
   1.366       "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)), 
   1.367                 \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
   1.368  apply (simp only: injection_def setclass_simps)
   1.369 -apply (intro FOL_reflection function_reflection typed_function_reflection)  
   1.370 +apply (intro FOL_reflections function_reflections typed_function_reflection)  
   1.371  done
   1.372  
   1.373  
   1.374 @@ -986,7 +1149,7 @@
   1.375       "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)), 
   1.376                 \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
   1.377  apply (simp only: surjection_def setclass_simps)
   1.378 -apply (intro FOL_reflection function_reflection typed_function_reflection)  
   1.379 +apply (intro FOL_reflections function_reflections typed_function_reflection)  
   1.380  done
   1.381  
   1.382  
   1.383 @@ -1080,18 +1243,98 @@
   1.384       "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)), 
   1.385                 \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
   1.386  apply (simp only: order_isomorphism_def setclass_simps)
   1.387 -apply (intro FOL_reflection function_reflection bijection_reflection)  
   1.388 +apply (intro FOL_reflections function_reflections bijection_reflection)  
   1.389 +done
   1.390 +
   1.391 +subsubsection{*Limit Ordinals*}
   1.392 +
   1.393 +text{*A limit ordinal is a non-empty, successor-closed ordinal*}
   1.394 +
   1.395 +(* "limit_ordinal(M,a) == 
   1.396 +	ordinal(M,a) & ~ empty(M,a) & 
   1.397 +        (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" *)
   1.398 +
   1.399 +constdefs limit_ordinal_fm :: "i=>i"
   1.400 +    "limit_ordinal_fm(x) == 
   1.401 +        And(ordinal_fm(x),
   1.402 +            And(Neg(empty_fm(x)),
   1.403 +	        Forall(Implies(Member(0,succ(x)),
   1.404 +                               Exists(And(Member(0,succ(succ(x))),
   1.405 +                                          succ_fm(1,0)))))))"
   1.406 +
   1.407 +lemma limit_ordinal_type [TC]:
   1.408 +     "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula"
   1.409 +by (simp add: limit_ordinal_fm_def) 
   1.410 +
   1.411 +lemma arity_limit_ordinal_fm [simp]:
   1.412 +     "x \<in> nat ==> arity(limit_ordinal_fm(x)) = succ(x)"
   1.413 +by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.414 +
   1.415 +lemma sats_limit_ordinal_fm [simp]:
   1.416 +   "[| x \<in> nat; env \<in> list(A)|]
   1.417 +    ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))"
   1.418 +by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm')
   1.419 +
   1.420 +lemma limit_ordinal_iff_sats:
   1.421 +      "[| nth(i,env) = x; nth(j,env) = y; 
   1.422 +          i \<in> nat; env \<in> list(A)|]
   1.423 +       ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)"
   1.424 +by simp
   1.425 +
   1.426 +theorem limit_ordinal_reflection:
   1.427 +     "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)), 
   1.428 +               \<lambda>i x. limit_ordinal(**Lset(i),f(x))]"
   1.429 +apply (simp only: limit_ordinal_def setclass_simps)
   1.430 +apply (intro FOL_reflections ordinal_reflection 
   1.431 +             empty_reflection successor_reflection)  
   1.432  done
   1.433  
   1.434 -lemmas fun_plus_reflection =
   1.435 -        typed_function_reflection injection_reflection surjection_reflection
   1.436 -        bijection_reflection order_isomorphism_reflection
   1.437 +subsubsection{*Omega: The Set of Natural Numbers*}
   1.438 +
   1.439 +(* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
   1.440 +constdefs omega_fm :: "i=>i"
   1.441 +    "omega_fm(x) == 
   1.442 +       And(limit_ordinal_fm(x),
   1.443 +           Forall(Implies(Member(0,succ(x)),
   1.444 +                          Neg(limit_ordinal_fm(0)))))"
   1.445 +
   1.446 +lemma omega_type [TC]:
   1.447 +     "x \<in> nat ==> omega_fm(x) \<in> formula"
   1.448 +by (simp add: omega_fm_def) 
   1.449 +
   1.450 +lemma arity_omega_fm [simp]:
   1.451 +     "x \<in> nat ==> arity(omega_fm(x)) = succ(x)"
   1.452 +by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.453 +
   1.454 +lemma sats_omega_fm [simp]:
   1.455 +   "[| x \<in> nat; env \<in> list(A)|]
   1.456 +    ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))"
   1.457 +by (simp add: omega_fm_def omega_def)
   1.458  
   1.459 -lemmas fun_plus_iff_sats = upair_iff_sats pair_iff_sats union_iff_sats
   1.460 -	cons_iff_sats fun_apply_iff_sats ordinal_iff_sats Memrel_iff_sats
   1.461 -	pred_set_iff_sats domain_iff_sats range_iff_sats image_iff_sats
   1.462 -	relation_iff_sats function_iff_sats typed_function_iff_sats 
   1.463 +lemma omega_iff_sats:
   1.464 +      "[| nth(i,env) = x; nth(j,env) = y; 
   1.465 +          i \<in> nat; env \<in> list(A)|]
   1.466 +       ==> omega(**A, x) <-> sats(A, omega_fm(i), env)"
   1.467 +by simp
   1.468 +
   1.469 +theorem omega_reflection:
   1.470 +     "REFLECTS[\<lambda>x. omega(L,f(x)), 
   1.471 +               \<lambda>i x. omega(**Lset(i),f(x))]"
   1.472 +apply (simp only: omega_def setclass_simps)
   1.473 +apply (intro FOL_reflections limit_ordinal_reflection)  
   1.474 +done
   1.475 +
   1.476 +
   1.477 +lemmas fun_plus_reflections =
   1.478 +        typed_function_reflection composition_reflection
   1.479 +        injection_reflection surjection_reflection
   1.480 +        bijection_reflection order_isomorphism_reflection
   1.481 +        ordinal_reflection limit_ordinal_reflection omega_reflection
   1.482 +
   1.483 +lemmas fun_plus_iff_sats = 
   1.484 +	typed_function_iff_sats composition_iff_sats
   1.485          injection_iff_sats surjection_iff_sats bijection_iff_sats 
   1.486          order_isomorphism_iff_sats
   1.487 +        ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats
   1.488  
   1.489  end