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.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.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.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.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.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.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.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.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
```