More relativization, reflection and proofs of separation
authorpaulson
Tue Jul 09 15:39:44 2002 +0200 (2002-07-09)
changeset 133232c287f50c9f3
parent 13322 3323ecc0b97c
child 13324 39d1b3a4c6f4
More relativization, reflection and proofs of separation
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/document/root.tex
     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
     2.1 --- a/src/ZF/Constructible/ROOT.ML	Tue Jul 09 13:41:38 2002 +0200
     2.2 +++ b/src/ZF/Constructible/ROOT.ML	Tue Jul 09 15:39:44 2002 +0200
     2.3 @@ -4,6 +4,8 @@
     2.4      Copyright   2002  University of Cambridge
     2.5  
     2.6  Inner Models and Absoluteness
     2.7 +
     2.8 +Build using	isatool usedir  -d pdf ZF Constructible
     2.9  *)
    2.10  
    2.11  use_thy "Reflection";
     3.1 --- a/src/ZF/Constructible/Relative.thy	Tue Jul 09 13:41:38 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 09 15:39:44 2002 +0200
     3.3 @@ -104,8 +104,9 @@
     3.4    composition :: "[i=>o,i,i,i] => o"
     3.5      "composition(M,r,s,t) == 
     3.6          \<forall>p[M]. p \<in> t <-> 
     3.7 -               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. pair(M,x,z,p) & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r)"
     3.8 -
     3.9 +               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
    3.10 +                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
    3.11 +                xy \<in> s & yz \<in> r)"
    3.12  
    3.13    injection :: "[i=>o,i,i,i] => o"
    3.14      "injection(M,A,B,f) == 
     4.1 --- a/src/ZF/Constructible/Separation.thy	Tue Jul 09 13:41:38 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Separation.thy	Tue Jul 09 15:39:44 2002 +0200
     4.3 @@ -1,13 +1,16 @@
     4.4 -header{*Proving instances of Separation using Reflection!*}
     4.5 +header{*Some Instances of Separation and Strong Replacement*}
     4.6  
     4.7 -theory Separation = L_axioms:
     4.8 +(*This theory proves all instances needed for locale M_axioms*)
     4.9 +
    4.10 +theory Separation = L_axioms + WFrec:
    4.11  
    4.12  text{*Helps us solve for de Bruijn indices!*}
    4.13  lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
    4.14  by simp
    4.15  
    4.16  lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
    4.17 -lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats fun_plus_iff_sats
    4.18 +lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats 
    4.19 +                   fun_plus_iff_sats
    4.20  
    4.21  lemma Collect_conj_in_DPow:
    4.22       "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |] 
    4.23 @@ -48,7 +51,7 @@
    4.24  lemma Inter_Reflects:
    4.25       "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y, 
    4.26                 \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]"
    4.27 -by (intro FOL_reflection)  
    4.28 +by (intro FOL_reflections)  
    4.29  
    4.30  lemma Inter_separation:
    4.31       "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
    4.32 @@ -68,11 +71,11 @@
    4.33  
    4.34  subsection{*Separation for Cartesian Product*}
    4.35  
    4.36 -lemma cartprod_Reflects [simplified]:
    4.37 +lemma cartprod_Reflects:
    4.38       "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
    4.39                  \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B & 
    4.40                                     pair(**Lset(i),x,y,z))]"
    4.41 -by (intro FOL_reflection function_reflection)  
    4.42 +by (intro FOL_reflections function_reflections)
    4.43  
    4.44  lemma cartprod_separation:
    4.45       "[| L(A); L(B) |] 
    4.46 @@ -94,13 +97,10 @@
    4.47  
    4.48  subsection{*Separation for Image*}
    4.49  
    4.50 -text{*No @{text simplified} here: it simplifies the occurrence of 
    4.51 -      the predicate @{term pair}!*}
    4.52  lemma image_Reflects:
    4.53       "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
    4.54             \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p))]"
    4.55 -by (intro FOL_reflection function_reflection)
    4.56 -
    4.57 +by (intro FOL_reflections function_reflections)
    4.58  
    4.59  lemma image_separation:
    4.60       "[| L(A); L(r) |] 
    4.61 @@ -126,7 +126,7 @@
    4.62    "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
    4.63       \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). 
    4.64                       pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
    4.65 -by (intro FOL_reflection function_reflection)
    4.66 +by (intro FOL_reflections function_reflections)
    4.67  
    4.68  lemma converse_separation:
    4.69       "L(r) ==> separation(L, 
    4.70 @@ -152,7 +152,7 @@
    4.71  lemma restrict_Reflects:
    4.72       "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
    4.73          \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
    4.74 -by (intro FOL_reflection function_reflection)
    4.75 +by (intro FOL_reflections function_reflections)
    4.76  
    4.77  lemma restrict_separation:
    4.78     "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
    4.79 @@ -181,7 +181,7 @@
    4.80          \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i). 
    4.81  		  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) & 
    4.82                    pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
    4.83 -by (intro FOL_reflection function_reflection)
    4.84 +by (intro FOL_reflections function_reflections)
    4.85  
    4.86  lemma comp_separation:
    4.87       "[| L(r); L(s) |]
    4.88 @@ -209,7 +209,7 @@
    4.89  lemma pred_Reflects:
    4.90       "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
    4.91                      \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
    4.92 -by (intro FOL_reflection function_reflection)
    4.93 +by (intro FOL_reflections function_reflections)
    4.94  
    4.95  lemma pred_separation:
    4.96       "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
    4.97 @@ -234,7 +234,7 @@
    4.98  lemma Memrel_Reflects:
    4.99       "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
   4.100              \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]"
   4.101 -by (intro FOL_reflection function_reflection)
   4.102 +by (intro FOL_reflections function_reflections)
   4.103  
   4.104  lemma Memrel_separation:
   4.105       "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
   4.106 @@ -263,7 +263,7 @@
   4.107  	      \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i). 
   4.108  		pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) & 
   4.109  		is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
   4.110 -by (intro FOL_reflection function_reflection)
   4.111 +by (intro FOL_reflections function_reflections)
   4.112  
   4.113  lemma funspace_succ_replacement:
   4.114       "L(n) ==> 
   4.115 @@ -295,7 +295,7 @@
   4.116                  (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
   4.117          \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i). 
   4.118                  fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
   4.119 -by (intro FOL_reflection function_reflection)
   4.120 +by (intro FOL_reflections function_reflections)
   4.121  
   4.122  lemma well_ord_iso_separation:
   4.123       "[| L(A); L(f); L(r) |] 
   4.124 @@ -325,7 +325,7 @@
   4.125          \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i). 
   4.126  	     ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
   4.127  	     order_isomorphism(**Lset(i),par,r,x,mx,g)]"
   4.128 -by (intro FOL_reflection function_reflection fun_plus_reflection)
   4.129 +by (intro FOL_reflections function_reflections fun_plus_reflections)
   4.130  
   4.131  lemma obase_separation:
   4.132       --{*part of the order type formalization*}
   4.133 @@ -360,7 +360,7 @@
   4.134  		ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i). 
   4.135  		membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
   4.136  		order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
   4.137 -by (intro FOL_reflection function_reflection fun_plus_reflection)
   4.138 +by (intro FOL_reflections function_reflections fun_plus_reflections)
   4.139  
   4.140  
   4.141  lemma obase_equals_separation:
   4.142 @@ -395,7 +395,7 @@
   4.143  	 ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & 
   4.144           membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & 
   4.145           order_isomorphism(**Lset(i),par,r,x,mx,g))]"
   4.146 -by (intro FOL_reflection function_reflection fun_plus_reflection)
   4.147 +by (intro FOL_reflections function_reflections fun_plus_reflections)
   4.148  
   4.149  lemma omap_replacement:
   4.150       "[| L(A); L(r) |] 
   4.151 @@ -420,4 +420,272 @@
   4.152  apply (simp_all add: succ_Un_distrib [symmetric])
   4.153  done
   4.154  
   4.155 +
   4.156 +subsection{*Separation for a Theorem about @{term "obase"}*}
   4.157 +
   4.158 +lemma is_recfun_reflects:
   4.159 +  "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L]. 
   4.160 +                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & 
   4.161 +                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & 
   4.162 +                                   fx \<noteq> gx),
   4.163 +   \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i). 
   4.164 +          pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r &
   4.165 +                (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) & 
   4.166 +                  fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]"
   4.167 +by (intro FOL_reflections function_reflections fun_plus_reflections)
   4.168 +
   4.169 +lemma is_recfun_separation:
   4.170 +     --{*for well-founded recursion*}
   4.171 +     "[| L(r); L(f); L(g); L(a); L(b) |] 
   4.172 +     ==> separation(L, 
   4.173 +            \<lambda>x. \<exists>xa[L]. \<exists>xb[L]. 
   4.174 +                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r & 
   4.175 +                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & 
   4.176 +                                   fx \<noteq> gx))"
   4.177 +apply (rule separation_CollectI) 
   4.178 +apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast ) 
   4.179 +apply (rule ReflectsE [OF is_recfun_reflects], assumption)
   4.180 +apply (drule subset_Lset_ltD, assumption) 
   4.181 +apply (erule reflection_imp_L_separation)
   4.182 +  apply (simp_all add: lt_Ord2)
   4.183 +apply (rule DPowI2)
   4.184 +apply (rename_tac u) 
   4.185 +apply (rule bex_iff_sats conj_iff_sats)+
   4.186 +apply (rule_tac env = "[x,u,r,f,g,a,b]" in pair_iff_sats) 
   4.187 +apply (rule sep_rules | simp)+
   4.188 +apply (simp_all add: succ_Un_distrib [symmetric])
   4.189 +done
   4.190 +
   4.191 +
   4.192 +ML
   4.193 +{*
   4.194 +val Inter_separation = thm "Inter_separation";
   4.195 +val cartprod_separation = thm "cartprod_separation";
   4.196 +val image_separation = thm "image_separation";
   4.197 +val converse_separation = thm "converse_separation";
   4.198 +val restrict_separation = thm "restrict_separation";
   4.199 +val comp_separation = thm "comp_separation";
   4.200 +val pred_separation = thm "pred_separation";
   4.201 +val Memrel_separation = thm "Memrel_separation";
   4.202 +val funspace_succ_replacement = thm "funspace_succ_replacement";
   4.203 +val well_ord_iso_separation = thm "well_ord_iso_separation";
   4.204 +val obase_separation = thm "obase_separation";
   4.205 +val obase_equals_separation = thm "obase_equals_separation";
   4.206 +val omap_replacement = thm "omap_replacement";
   4.207 +val is_recfun_separation = thm "is_recfun_separation";
   4.208 +
   4.209 +val m_axioms = 
   4.210 +    [Inter_separation, cartprod_separation, image_separation, 
   4.211 +     converse_separation, restrict_separation, comp_separation, 
   4.212 +     pred_separation, Memrel_separation, funspace_succ_replacement, 
   4.213 +     well_ord_iso_separation, obase_separation,
   4.214 +     obase_equals_separation, omap_replacement, is_recfun_separation]
   4.215 +
   4.216 +fun axiomsL th =
   4.217 +    kill_flex_triv_prems (m_axioms MRS (trivaxL th));
   4.218 +
   4.219 +bind_thm ("cartprod_iff", axiomsL (thm "M_axioms.cartprod_iff"));
   4.220 +bind_thm ("cartprod_closed", axiomsL (thm "M_axioms.cartprod_closed"));
   4.221 +bind_thm ("sum_closed", axiomsL (thm "M_axioms.sum_closed"));
   4.222 +bind_thm ("M_converse_iff", axiomsL (thm "M_axioms.M_converse_iff"));
   4.223 +bind_thm ("converse_closed", axiomsL (thm "M_axioms.converse_closed"));
   4.224 +bind_thm ("converse_abs", axiomsL (thm "M_axioms.converse_abs"));
   4.225 +bind_thm ("image_closed", axiomsL (thm "M_axioms.image_closed"));
   4.226 +bind_thm ("vimage_abs", axiomsL (thm "M_axioms.vimage_abs"));
   4.227 +bind_thm ("vimage_closed", axiomsL (thm "M_axioms.vimage_closed"));
   4.228 +bind_thm ("domain_abs", axiomsL (thm "M_axioms.domain_abs"));
   4.229 +bind_thm ("domain_closed", axiomsL (thm "M_axioms.domain_closed"));
   4.230 +bind_thm ("range_abs", axiomsL (thm "M_axioms.range_abs"));
   4.231 +bind_thm ("range_closed", axiomsL (thm "M_axioms.range_closed"));
   4.232 +bind_thm ("field_abs", axiomsL (thm "M_axioms.field_abs"));
   4.233 +bind_thm ("field_closed", axiomsL (thm "M_axioms.field_closed"));
   4.234 +bind_thm ("relation_abs", axiomsL (thm "M_axioms.relation_abs"));
   4.235 +bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs"));
   4.236 +bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed"));
   4.237 +bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs"));
   4.238 +bind_thm ("typed_apply_abs", axiomsL (thm "M_axioms.typed_apply_abs"));
   4.239 +bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs"));
   4.240 +bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs"));
   4.241 +bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs"));
   4.242 +bind_thm ("bijection_abs", axiomsL (thm "M_axioms.bijection_abs"));
   4.243 +bind_thm ("M_comp_iff", axiomsL (thm "M_axioms.M_comp_iff"));
   4.244 +bind_thm ("comp_closed", axiomsL (thm "M_axioms.comp_closed"));
   4.245 +bind_thm ("composition_abs", axiomsL (thm "M_axioms.composition_abs"));
   4.246 +bind_thm ("restriction_is_function", axiomsL (thm "M_axioms.restriction_is_function"));
   4.247 +bind_thm ("restriction_abs", axiomsL (thm "M_axioms.restriction_abs"));
   4.248 +bind_thm ("M_restrict_iff", axiomsL (thm "M_axioms.M_restrict_iff"));
   4.249 +bind_thm ("restrict_closed", axiomsL (thm "M_axioms.restrict_closed"));
   4.250 +bind_thm ("Inter_abs", axiomsL (thm "M_axioms.Inter_abs"));
   4.251 +bind_thm ("Inter_closed", axiomsL (thm "M_axioms.Inter_closed"));
   4.252 +bind_thm ("Int_closed", axiomsL (thm "M_axioms.Int_closed"));
   4.253 +bind_thm ("finite_fun_closed", axiomsL (thm "M_axioms.finite_fun_closed"));
   4.254 +bind_thm ("is_funspace_abs", axiomsL (thm "M_axioms.is_funspace_abs"));
   4.255 +bind_thm ("succ_fun_eq2", axiomsL (thm "M_axioms.succ_fun_eq2"));
   4.256 +bind_thm ("funspace_succ", axiomsL (thm "M_axioms.funspace_succ"));
   4.257 +bind_thm ("finite_funspace_closed", axiomsL (thm "M_axioms.finite_funspace_closed"));
   4.258 +*}
   4.259 +
   4.260 +ML
   4.261 +{*
   4.262 +bind_thm ("is_recfun_equal", axiomsL (thm "M_axioms.is_recfun_equal"));  
   4.263 +bind_thm ("is_recfun_cut", axiomsL (thm "M_axioms.is_recfun_cut")); 
   4.264 +bind_thm ("is_recfun_functional", axiomsL (thm "M_axioms.is_recfun_functional"));
   4.265 +bind_thm ("is_recfun_relativize", axiomsL (thm "M_axioms.is_recfun_relativize"));
   4.266 +bind_thm ("is_recfun_restrict", axiomsL (thm "M_axioms.is_recfun_restrict"));
   4.267 +bind_thm ("univalent_is_recfun", axiomsL (thm "M_axioms.univalent_is_recfun"));
   4.268 +bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep"));
   4.269 +bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun"));
   4.270 +bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun")); 
   4.271 +bind_thm ("is_recfun_iff_M", axiomsL (thm "M_axioms.is_recfun_iff_M"));
   4.272 +bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs"));  
   4.273 +bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs"));  
   4.274 +bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs"));  
   4.275 +bind_thm ("wellordered_is_trans_on", axiomsL (thm "M_axioms.wellordered_is_trans_on")); 
   4.276 +bind_thm ("wellordered_is_linear", axiomsL (thm "M_axioms.wellordered_is_linear")); 
   4.277 +bind_thm ("wellordered_is_wellfounded_on", axiomsL (thm "M_axioms.wellordered_is_wellfounded_on")); 
   4.278 +bind_thm ("wellfounded_imp_wellfounded_on", axiomsL (thm "M_axioms.wellfounded_imp_wellfounded_on")); 
   4.279 +bind_thm ("wellfounded_on_subset_A", axiomsL (thm "M_axioms.wellfounded_on_subset_A"));
   4.280 +bind_thm ("wellfounded_on_iff_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_iff_wellfounded"));
   4.281 +bind_thm ("wellfounded_on_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_imp_wellfounded"));
   4.282 +bind_thm ("wellfounded_on_field_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_field_imp_wellfounded"));
   4.283 +bind_thm ("wellfounded_iff_wellfounded_on_field", axiomsL (thm "M_axioms.wellfounded_iff_wellfounded_on_field"));
   4.284 +bind_thm ("wellfounded_induct", axiomsL (thm "M_axioms.wellfounded_induct")); 
   4.285 +bind_thm ("wellfounded_on_induct", axiomsL (thm "M_axioms.wellfounded_on_induct")); 
   4.286 +bind_thm ("wellfounded_on_induct2", axiomsL (thm "M_axioms.wellfounded_on_induct2")); 
   4.287 +bind_thm ("linear_imp_relativized", axiomsL (thm "M_axioms.linear_imp_relativized")); 
   4.288 +bind_thm ("trans_on_imp_relativized", axiomsL (thm "M_axioms.trans_on_imp_relativized")); 
   4.289 +bind_thm ("wf_on_imp_relativized", axiomsL (thm "M_axioms.wf_on_imp_relativized")); 
   4.290 +bind_thm ("wf_imp_relativized", axiomsL (thm "M_axioms.wf_imp_relativized")); 
   4.291 +bind_thm ("well_ord_imp_relativized", axiomsL (thm "M_axioms.well_ord_imp_relativized")); 
   4.292 +bind_thm ("order_isomorphism_abs", axiomsL (thm "M_axioms.order_isomorphism_abs"));  
   4.293 +bind_thm ("pred_set_abs", axiomsL (thm "M_axioms.pred_set_abs"));  
   4.294 +*}
   4.295 +
   4.296 +ML
   4.297 +{*
   4.298 +bind_thm ("pred_closed", axiomsL (thm "M_axioms.pred_closed"));  
   4.299 +bind_thm ("membership_abs", axiomsL (thm "M_axioms.membership_abs"));  
   4.300 +bind_thm ("M_Memrel_iff", axiomsL (thm "M_axioms.M_Memrel_iff"));
   4.301 +bind_thm ("Memrel_closed", axiomsL (thm "M_axioms.Memrel_closed"));  
   4.302 +bind_thm ("wellordered_iso_predD", axiomsL (thm "M_axioms.wellordered_iso_predD"));
   4.303 +bind_thm ("wellordered_iso_pred_eq", axiomsL (thm "M_axioms.wellordered_iso_pred_eq"));
   4.304 +bind_thm ("wellfounded_on_asym", axiomsL (thm "M_axioms.wellfounded_on_asym"));
   4.305 +bind_thm ("wellordered_asym", axiomsL (thm "M_axioms.wellordered_asym"));
   4.306 +bind_thm ("ord_iso_pred_imp_lt", axiomsL (thm "M_axioms.ord_iso_pred_imp_lt"));
   4.307 +bind_thm ("obase_iff", axiomsL (thm "M_axioms.obase_iff"));
   4.308 +bind_thm ("omap_iff", axiomsL (thm "M_axioms.omap_iff"));
   4.309 +bind_thm ("omap_unique", axiomsL (thm "M_axioms.omap_unique"));
   4.310 +bind_thm ("omap_yields_Ord", axiomsL (thm "M_axioms.omap_yields_Ord"));
   4.311 +bind_thm ("otype_iff", axiomsL (thm "M_axioms.otype_iff"));
   4.312 +bind_thm ("otype_eq_range", axiomsL (thm "M_axioms.otype_eq_range"));
   4.313 +bind_thm ("Ord_otype", axiomsL (thm "M_axioms.Ord_otype"));
   4.314 +bind_thm ("domain_omap", axiomsL (thm "M_axioms.domain_omap"));
   4.315 +bind_thm ("omap_subset", axiomsL (thm "M_axioms.omap_subset")); 
   4.316 +bind_thm ("omap_funtype", axiomsL (thm "M_axioms.omap_funtype")); 
   4.317 +bind_thm ("wellordered_omap_bij", axiomsL (thm "M_axioms.wellordered_omap_bij"));
   4.318 +bind_thm ("omap_ord_iso", axiomsL (thm "M_axioms.omap_ord_iso"));
   4.319 +bind_thm ("Ord_omap_image_pred", axiomsL (thm "M_axioms.Ord_omap_image_pred"));
   4.320 +bind_thm ("restrict_omap_ord_iso", axiomsL (thm "M_axioms.restrict_omap_ord_iso"));
   4.321 +bind_thm ("obase_equals", axiomsL (thm "M_axioms.obase_equals")); 
   4.322 +bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
   4.323 +bind_thm ("obase_exists", axiomsL (thm "M_axioms.obase_exists"));
   4.324 +bind_thm ("omap_exists", axiomsL (thm "M_axioms.omap_exists"));
   4.325 +bind_thm ("otype_exists", axiomsL (thm "M_axioms.otype_exists"));
   4.326 +bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
   4.327 +bind_thm ("ordertype_exists", axiomsL (thm "M_axioms.ordertype_exists"));
   4.328 +bind_thm ("relativized_imp_well_ord", axiomsL (thm "M_axioms.relativized_imp_well_ord")); 
   4.329 +bind_thm ("well_ord_abs", axiomsL (thm "M_axioms.well_ord_abs"));  
   4.330 +*}
   4.331 +
   4.332 +declare cartprod_closed [intro,simp]
   4.333 +declare sum_closed [intro,simp]
   4.334 +declare converse_closed [intro,simp]
   4.335 +declare converse_abs [simp]
   4.336 +declare image_closed [intro,simp]
   4.337 +declare vimage_abs [simp]
   4.338 +declare vimage_closed [intro,simp]
   4.339 +declare domain_abs [simp]
   4.340 +declare domain_closed [intro,simp]
   4.341 +declare range_abs [simp]
   4.342 +declare range_closed [intro,simp]
   4.343 +declare field_abs [simp]
   4.344 +declare field_closed [intro,simp]
   4.345 +declare relation_abs [simp]
   4.346 +declare function_abs [simp]
   4.347 +declare apply_closed [intro,simp]
   4.348 +declare typed_function_abs [simp]
   4.349 +declare injection_abs [simp]
   4.350 +declare surjection_abs [simp]
   4.351 +declare bijection_abs [simp]
   4.352 +declare comp_closed [intro,simp]
   4.353 +declare composition_abs [simp]
   4.354 +declare restriction_abs [simp]
   4.355 +declare restrict_closed [intro,simp]
   4.356 +declare Inter_abs [simp]
   4.357 +declare Inter_closed [intro,simp]
   4.358 +declare Int_closed [intro,simp]
   4.359 +declare finite_fun_closed [rule_format]
   4.360 +declare is_funspace_abs [simp]
   4.361 +declare finite_funspace_closed [intro,simp]
   4.362 +
   4.363 +
   4.364 +(***NOW FOR THE LOCALE M_TRANCL***)
   4.365 +
   4.366 +subsection{*Separation for Reflexive/Transitive Closure*}
   4.367 +
   4.368 +lemma rtrancl_reflects:
   4.369 +  "REFLECTS[\<lambda>p. 
   4.370 +    \<exists>nnat[L]. \<exists>n[L]. \<exists>n'[L]. omega(L,nnat) & n\<in>nnat & successor(L,n,n') &
   4.371 +     (\<exists>f[L]. 
   4.372 +      typed_function(L,n',A,f) &
   4.373 +      (\<exists>x[L]. \<exists>y[L]. \<exists>zero[L]. pair(L,x,y,p) & empty(L,zero) &
   4.374 +	fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) &
   4.375 +	(\<forall>j[L]. j\<in>n --> 
   4.376 +	  (\<exists>fj[L]. \<exists>sj[L]. \<exists>fsj[L]. \<exists>ffp[L]. 
   4.377 +	    fun_apply(L,f,j,fj) & successor(L,j,sj) &
   4.378 +	    fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \<in> r))),
   4.379 +\<lambda>i p. 
   4.380 +    \<exists>nnat \<in> Lset(i). \<exists>n \<in> Lset(i). \<exists>n' \<in> Lset(i). 
   4.381 +     omega(**Lset(i),nnat) & n\<in>nnat & successor(**Lset(i),n,n') &
   4.382 +     (\<exists>f \<in> Lset(i). 
   4.383 +      typed_function(**Lset(i),n',A,f) &
   4.384 +      (\<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). \<exists>zero \<in> Lset(i). pair(**Lset(i),x,y,p) & empty(**Lset(i),zero) &
   4.385 +	fun_apply(**Lset(i),f,zero,x) & fun_apply(**Lset(i),f,n,y)) &
   4.386 +	(\<forall>j \<in> Lset(i). j\<in>n --> 
   4.387 +	  (\<exists>fj \<in> Lset(i). \<exists>sj \<in> Lset(i). \<exists>fsj \<in> Lset(i). \<exists>ffp \<in> Lset(i). 
   4.388 +	    fun_apply(**Lset(i),f,j,fj) & successor(**Lset(i),j,sj) &
   4.389 +	    fun_apply(**Lset(i),f,sj,fsj) & pair(**Lset(i),fj,fsj,ffp) & ffp \<in> r)))]"
   4.390 +by (intro FOL_reflections function_reflections fun_plus_reflections)
   4.391 +
   4.392 +
   4.393 +text{*This formula describes @{term "rtrancl(r)"}.*}
   4.394 +lemma rtrancl_separation:
   4.395 +     "[| L(r); L(A) |] ==>
   4.396 +      separation (L, \<lambda>p. 
   4.397 +	  \<exists>nnat[L]. \<exists>n[L]. \<exists>n'[L]. 
   4.398 +           omega(L,nnat) & n\<in>nnat & successor(L,n,n') &
   4.399 +	   (\<exists>f[L]. 
   4.400 +	    typed_function(L,n',A,f) &
   4.401 +	    (\<exists>x[L]. \<exists>y[L]. \<exists>zero[L]. pair(L,x,y,p) & empty(L,zero) &
   4.402 +	      fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) &
   4.403 +	      (\<forall>j[L]. j\<in>n --> 
   4.404 +		(\<exists>fj[L]. \<exists>sj[L]. \<exists>fsj[L]. \<exists>ffp[L]. 
   4.405 +		  fun_apply(L,f,j,fj) & successor(L,j,sj) &
   4.406 +		  fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \<in> r))))"
   4.407 +apply (rule separation_CollectI) 
   4.408 +apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) 
   4.409 +apply (rule ReflectsE [OF rtrancl_reflects], assumption)
   4.410 +apply (drule subset_Lset_ltD, assumption) 
   4.411 +apply (erule reflection_imp_L_separation)
   4.412 +  apply (simp_all add: lt_Ord2)
   4.413 +apply (rule DPowI2)
   4.414 +apply (rename_tac u) 
   4.415 +apply (rule bex_iff_sats conj_iff_sats)+
   4.416 +apply (rule_tac env = "[x,u,r,A]" in omega_iff_sats)
   4.417 +txt{*SLOW, maybe just due to the formula's size*}
   4.418 +apply (rule sep_rules | simp)+
   4.419 +apply (simp_all add: succ_Un_distrib [symmetric])
   4.420 +done
   4.421 +
   4.422 +
   4.423  end
     5.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 13:41:38 2002 +0200
     5.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 15:39:44 2002 +0200
     5.3 @@ -133,18 +133,24 @@
     5.4  
     5.5  
     5.6  locale M_trancl = M_axioms +
     5.7 -(*THEY NEED RELATIVIZATION*)
     5.8    assumes rtrancl_separation:
     5.9 -     "[| M(r); M(A) |] ==>
    5.10 -	separation
    5.11 -	   (M, \<lambda>p. \<exists>n[M]. n\<in>nat & 
    5.12 -                    (\<exists>f[M]. 
    5.13 -                     f \<in> succ(n) -> A &
    5.14 -                     (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) &  
    5.15 -                           f`0 = x & f`n = y) &
    5.16 -                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
    5.17 +	 "[| M(r); M(A) |] ==>
    5.18 +	  separation (M, \<lambda>p. 
    5.19 +	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    5.20 +               omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
    5.21 +	       (\<exists>f[M]. 
    5.22 +		typed_function(M,n',A,f) &
    5.23 +		(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    5.24 +		  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    5.25 +		  (\<forall>j[M]. j\<in>n --> 
    5.26 +		    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    5.27 +		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
    5.28 +		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r))))"
    5.29        and wellfounded_trancl_separation:
    5.30 -     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+)"
    5.31 +	 "[| M(r); M(Z) |] ==> 
    5.32 +	  separation (M, \<lambda>x. 
    5.33 +	      \<exists>w[M]. \<exists>wx[M]. \<exists>rp[M]. 
    5.34 +	       w \<in> Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \<in> rp)"
    5.35  
    5.36  
    5.37  lemma (in M_trancl) rtran_closure_rtrancl:
    5.38 @@ -203,6 +209,9 @@
    5.39       "[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)"
    5.40  by (simp add: tran_closure_def trancl_def)
    5.41  
    5.42 +lemma (in M_trancl) wellfounded_trancl_separation':
    5.43 +     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & <w,x> \<in> r^+)"
    5.44 +by (insert wellfounded_trancl_separation [of r Z], simp) 
    5.45  
    5.46  text{*Alternative proof of @{text wf_on_trancl}; inspiration for the
    5.47        relativized version.  Original version is on theory WF.*}
    5.48 @@ -213,7 +222,6 @@
    5.49  apply (blast elim: tranclE)
    5.50  done
    5.51  
    5.52 -
    5.53  lemma (in M_trancl) wellfounded_on_trancl:
    5.54       "[| wellfounded_on(M,A,r);  r-``A <= A; M(r); M(A) |]
    5.55        ==> wellfounded_on(M,A,r^+)"
    5.56 @@ -222,7 +230,7 @@
    5.57  apply (rename_tac Z x)
    5.58  apply (subgoal_tac "M({x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+})")
    5.59   prefer 2
    5.60 - apply (blast intro: wellfounded_trancl_separation) 
    5.61 + apply (blast intro: wellfounded_trancl_separation') 
    5.62  apply (drule_tac x = "{x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+}" in rspec, safe)
    5.63  apply (blast dest: transM, simp)
    5.64  apply (rename_tac y w)
     6.1 --- a/src/ZF/Constructible/document/root.tex	Tue Jul 09 13:41:38 2002 +0200
     6.2 +++ b/src/ZF/Constructible/document/root.tex	Tue Jul 09 15:39:44 2002 +0200
     6.3 @@ -16,9 +16,8 @@
     6.4  % this should be the last package used
     6.5  \usepackage{pdfsetup}
     6.6  
     6.7 -% proper setup for best-style documents
     6.8  \urlstyle{rm}
     6.9 -\isabellestyle{it}
    6.10 +\isabellestyle{tt} %and not {it}!
    6.11  
    6.12  
    6.13  \begin{document}