author paulson Tue, 09 Jul 2002 15:39:44 +0200 changeset 13323 2c287f50c9f3 parent 13322 3323ecc0b97c child 13324 39d1b3a4c6f4
More relativization, reflection and proofs of separation
 src/ZF/Constructible/L_axioms.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/ROOT.ML file | annotate | diff | comparison | revisions src/ZF/Constructible/Relative.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/Separation.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/WF_absolute.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/document/root.tex file | annotate | diff | comparison | revisions
--- a/src/ZF/Constructible/L_axioms.thy	Tue Jul 09 13:41:38 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Tue Jul 09 15:39:44 2002 +0200
@@ -292,7 +292,7 @@
apply (intro Imp_reflection All_reflection, assumption)
done

-lemmas FOL_reflection =
+lemmas FOL_reflections =
Triv_reflection Not_reflection And_reflection Or_reflection
Imp_reflection Iff_reflection Ex_reflection All_reflection
Rex_reflection Rall_reflection
@@ -340,6 +340,39 @@
"8"  == "succ(7)"
"9"  == "succ(8)"

+
+subsubsection{*The Empty Set*}
+
+constdefs empty_fm :: "i=>i"
+    "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
+
+lemma empty_type [TC]:
+     "x \<in> nat ==> empty_fm(x) \<in> formula"
+
+lemma arity_empty_fm [simp]:
+     "x \<in> nat ==> arity(empty_fm(x)) = succ(x)"
+by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_empty_fm [simp]:
+   "[| x \<in> nat; env \<in> list(A)|]
+    ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))"
+
+lemma empty_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y;
+          i \<in> nat; env \<in> list(A)|]
+       ==> empty(**A, x) <-> sats(A, empty_fm(i), env)"
+by simp
+
+theorem empty_reflection:
+     "REFLECTS[\<lambda>x. empty(L,f(x)),
+               \<lambda>i x. empty(**Lset(i),f(x))]"
+apply (simp only: empty_def setclass_simps)
+apply (intro FOL_reflections)
+done
+
+
subsubsection{*Unordered pairs*}

constdefs upair_fm :: "[i,i,i]=>i"
@@ -384,7 +417,7 @@
"REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),
\<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"
-apply (intro FOL_reflection)
+apply (intro FOL_reflections)
done

subsubsection{*Ordered pairs*}
@@ -420,7 +453,7 @@
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
\<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
apply (simp only: pair_def setclass_simps)
-apply (intro FOL_reflection upair_reflection)
+apply (intro FOL_reflections upair_reflection)
done

@@ -456,7 +489,7 @@
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
\<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
apply (simp only: union_def setclass_simps)
-apply (intro FOL_reflection)
+apply (intro FOL_reflections)
done

@@ -493,7 +526,41 @@
"REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
\<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_cons_def setclass_simps)
-apply (intro FOL_reflection upair_reflection union_reflection)
+apply (intro FOL_reflections upair_reflection union_reflection)
+done
+
+
+subsubsection{*Successor Function*}
+
+constdefs succ_fm :: "[i,i]=>i"
+    "succ_fm(x,y) == cons_fm(x,x,y)"
+
+lemma succ_type [TC]:
+     "[| x \<in> nat; y \<in> nat |] ==> succ_fm(x,y) \<in> formula"
+
+lemma arity_succ_fm [simp]:
+     "[| x \<in> nat; y \<in> nat |]
+      ==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)"
+
+lemma sats_succ_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
+    ==> sats(A, succ_fm(x,y), env) <->
+        successor(**A, nth(x,env), nth(y,env))"
+
+lemma successor_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y;
+          i \<in> nat; j \<in> nat; env \<in> list(A)|]
+       ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)"
+by simp
+
+theorem successor_reflection:
+     "REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
+               \<lambda>i x. successor(**Lset(i),f(x),g(x))]"
+apply (simp only: successor_def setclass_simps)
+apply (intro cons_reflection)
done

@@ -530,7 +597,7 @@
"REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
\<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
apply (simp only: fun_apply_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (intro FOL_reflections pair_reflection)
done

@@ -542,13 +609,13 @@
lemma sats_subset_fm':
"[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"

theorem subset_reflection:
"REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
\<lambda>i x. subset(**Lset(i),f(x),g(x))]"
-apply (simp only: subset_def setclass_simps)
-apply (intro FOL_reflection)
+apply (simp only: Relative.subset_def setclass_simps)
+apply (intro FOL_reflections)
done

lemma sats_transset_fm':
@@ -560,7 +627,7 @@
"REFLECTS[\<lambda>x. transitive_set(L,f(x)),
\<lambda>i x. transitive_set(**Lset(i),f(x))]"
apply (simp only: transitive_set_def setclass_simps)
-apply (intro FOL_reflection subset_reflection)
+apply (intro FOL_reflections subset_reflection)
done

lemma sats_ordinal_fm':
@@ -576,7 +643,7 @@
theorem ordinal_reflection:
"REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
apply (simp only: ordinal_def setclass_simps)
-apply (intro FOL_reflection transitive_set_reflection)
+apply (intro FOL_reflections transitive_set_reflection)
done

@@ -615,7 +682,7 @@
"REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
\<lambda>i x. membership(**Lset(i),f(x),g(x))]"
apply (simp only: membership_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (intro FOL_reflections pair_reflection)
done

subsubsection{*Predecessor Set*}
@@ -654,7 +721,7 @@
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
\<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
apply (simp only: pred_set_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (intro FOL_reflections pair_reflection)
done

@@ -694,7 +761,7 @@
"REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
\<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
apply (simp only: is_domain_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (intro FOL_reflections pair_reflection)
done

@@ -733,10 +800,51 @@
"REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
\<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
apply (simp only: is_range_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (intro FOL_reflections pair_reflection)
done

+subsubsection{*Field*}
+
+(* "is_field(M,r,z) ==
+	\<exists>dr[M]. is_domain(M,r,dr) &
+            (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
+constdefs field_fm :: "[i,i]=>i"
+    "field_fm(r,z) ==
+       Exists(And(domain_fm(succ(r),0),
+              Exists(And(range_fm(succ(succ(r)),0),
+                         union_fm(1,0,succ(succ(z)))))))"
+
+lemma field_type [TC]:
+     "[| x \<in> nat; y \<in> nat |] ==> field_fm(x,y) \<in> formula"
+
+lemma arity_field_fm [simp]:
+     "[| x \<in> nat; y \<in> nat |]
+      ==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)"
+by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_field_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
+    ==> sats(A, field_fm(x,y), env) <->
+        is_field(**A, nth(x,env), nth(y,env))"
+
+lemma field_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y;
+          i \<in> nat; j \<in> nat; env \<in> list(A)|]
+       ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)"
+by simp
+
+theorem field_reflection:
+     "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
+               \<lambda>i x. is_field(**Lset(i),f(x),g(x))]"
+apply (simp only: is_field_def setclass_simps)
+apply (intro FOL_reflections domain_reflection range_reflection
+             union_reflection)
+done
+
+
subsubsection{*Image*}

(* "image(M,r,A,z) ==
@@ -761,7 +869,7 @@
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, image_fm(x,y,z), env) <->
image(**A, nth(x,env), nth(y,env), nth(z,env))"

lemma image_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
@@ -772,8 +880,8 @@
theorem image_reflection:
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
\<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: image_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (simp only: Relative.image_def setclass_simps)
+apply (intro FOL_reflections pair_reflection)
done

@@ -808,7 +916,7 @@
"REFLECTS[\<lambda>x. is_relation(L,f(x)),
\<lambda>i x. is_relation(**Lset(i),f(x))]"
apply (simp only: is_relation_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (intro FOL_reflections pair_reflection)
done

@@ -848,7 +956,7 @@
"REFLECTS[\<lambda>x. is_function(L,f(x)),
\<lambda>i x. is_function(**Lset(i),f(x))]"
apply (simp only: is_function_def setclass_simps)
-apply (intro FOL_reflection pair_reflection)
+apply (intro FOL_reflections pair_reflection)
done

@@ -887,19 +995,74 @@
==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
by simp

-lemmas function_reflection =
-        upair_reflection pair_reflection union_reflection
-	cons_reflection fun_apply_reflection subset_reflection
-	transitive_set_reflection ordinal_reflection membership_reflection
-	pred_set_reflection domain_reflection range_reflection image_reflection
+lemmas function_reflections =
+        empty_reflection upair_reflection pair_reflection union_reflection
+	cons_reflection successor_reflection
+        fun_apply_reflection subset_reflection
+	transitive_set_reflection membership_reflection
+	pred_set_reflection domain_reflection range_reflection field_reflection
+        image_reflection
is_relation_reflection is_function_reflection

+lemmas function_iff_sats =
+        empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats
+	cons_iff_sats successor_iff_sats
+        fun_apply_iff_sats  Memrel_iff_sats
+	pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
+        image_iff_sats
+	relation_iff_sats function_iff_sats
+

theorem typed_function_reflection:
"REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
\<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
apply (simp only: typed_function_def setclass_simps)
-apply (intro FOL_reflection function_reflection)
+apply (intro FOL_reflections function_reflections)
+done
+
+
+subsubsection{*Composition of Relations*}
+
+(* "composition(M,r,s,t) ==
+        \<forall>p[M]. p \<in> t <->
+               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
+                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
+                xy \<in> s & yz \<in> r)" *)
+constdefs composition_fm :: "[i,i,i]=>i"
+  "composition_fm(r,s,t) ==
+     Forall(Iff(Member(0,succ(t)),
+             Exists(Exists(Exists(Exists(Exists(
+              And(pair_fm(4,2,5),
+               And(pair_fm(4,3,1),
+                And(pair_fm(3,2,0),
+                 And(Member(1,s#+6), Member(0,r#+6))))))))))))"
+
+lemma composition_type [TC]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> composition_fm(x,y,z) \<in> formula"
+
+lemma arity_composition_fm [simp]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
+      ==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_composition_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, composition_fm(x,y,z), env) <->
+        composition(**A, nth(x,env), nth(y,env), nth(z,env))"
+
+lemma composition_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
+          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+       ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
+by simp
+
+theorem composition_reflection:
+     "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
+               \<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: composition_def setclass_simps)
+apply (intro FOL_reflections pair_reflection)
done

@@ -944,7 +1107,7 @@
"REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
\<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
apply (simp only: injection_def setclass_simps)
-apply (intro FOL_reflection function_reflection typed_function_reflection)
+apply (intro FOL_reflections function_reflections typed_function_reflection)
done

@@ -986,7 +1149,7 @@
"REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
\<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
apply (simp only: surjection_def setclass_simps)
-apply (intro FOL_reflection function_reflection typed_function_reflection)
+apply (intro FOL_reflections function_reflections typed_function_reflection)
done

@@ -1080,18 +1243,98 @@
"REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
\<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
apply (simp only: order_isomorphism_def setclass_simps)
-apply (intro FOL_reflection function_reflection bijection_reflection)
+apply (intro FOL_reflections function_reflections bijection_reflection)
+done
+
+subsubsection{*Limit Ordinals*}
+
+text{*A limit ordinal is a non-empty, successor-closed ordinal*}
+
+(* "limit_ordinal(M,a) ==
+	ordinal(M,a) & ~ empty(M,a) &
+        (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" *)
+
+constdefs limit_ordinal_fm :: "i=>i"
+    "limit_ordinal_fm(x) ==
+        And(ordinal_fm(x),
+            And(Neg(empty_fm(x)),
+	        Forall(Implies(Member(0,succ(x)),
+                               Exists(And(Member(0,succ(succ(x))),
+                                          succ_fm(1,0)))))))"
+
+lemma limit_ordinal_type [TC]:
+     "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula"
+
+lemma arity_limit_ordinal_fm [simp]:
+     "x \<in> nat ==> arity(limit_ordinal_fm(x)) = succ(x)"
+by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_limit_ordinal_fm [simp]:
+   "[| x \<in> nat; env \<in> list(A)|]
+    ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))"
+by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm')
+
+lemma limit_ordinal_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y;
+          i \<in> nat; env \<in> list(A)|]
+       ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)"
+by simp
+
+theorem limit_ordinal_reflection:
+     "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
+               \<lambda>i x. limit_ordinal(**Lset(i),f(x))]"
+apply (simp only: limit_ordinal_def setclass_simps)
+apply (intro FOL_reflections ordinal_reflection
+             empty_reflection successor_reflection)
done

-lemmas fun_plus_reflection =
-        typed_function_reflection injection_reflection surjection_reflection
-        bijection_reflection order_isomorphism_reflection
+subsubsection{*Omega: The Set of Natural Numbers*}
+
+(* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
+constdefs omega_fm :: "i=>i"
+    "omega_fm(x) ==
+       And(limit_ordinal_fm(x),
+           Forall(Implies(Member(0,succ(x)),
+                          Neg(limit_ordinal_fm(0)))))"
+
+lemma omega_type [TC]:
+     "x \<in> nat ==> omega_fm(x) \<in> formula"
+
+lemma arity_omega_fm [simp]:
+     "x \<in> nat ==> arity(omega_fm(x)) = succ(x)"
+by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_omega_fm [simp]:
+   "[| x \<in> nat; env \<in> list(A)|]
+    ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))"

-lemmas fun_plus_iff_sats = upair_iff_sats pair_iff_sats union_iff_sats
-	cons_iff_sats fun_apply_iff_sats ordinal_iff_sats Memrel_iff_sats
-	pred_set_iff_sats domain_iff_sats range_iff_sats image_iff_sats
-	relation_iff_sats function_iff_sats typed_function_iff_sats
+lemma omega_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y;
+          i \<in> nat; env \<in> list(A)|]
+       ==> omega(**A, x) <-> sats(A, omega_fm(i), env)"
+by simp
+
+theorem omega_reflection:
+     "REFLECTS[\<lambda>x. omega(L,f(x)),
+               \<lambda>i x. omega(**Lset(i),f(x))]"
+apply (simp only: omega_def setclass_simps)
+apply (intro FOL_reflections limit_ordinal_reflection)
+done
+
+
+lemmas fun_plus_reflections =
+        typed_function_reflection composition_reflection
+        injection_reflection surjection_reflection
+        bijection_reflection order_isomorphism_reflection
+        ordinal_reflection limit_ordinal_reflection omega_reflection
+
+lemmas fun_plus_iff_sats =
+	typed_function_iff_sats composition_iff_sats
injection_iff_sats surjection_iff_sats bijection_iff_sats
order_isomorphism_iff_sats
+        ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats

end
--- a/src/ZF/Constructible/ROOT.ML	Tue Jul 09 13:41:38 2002 +0200
+++ b/src/ZF/Constructible/ROOT.ML	Tue Jul 09 15:39:44 2002 +0200
@@ -4,6 +4,8 @@

Inner Models and Absoluteness
+
+Build using	isatool usedir  -d pdf ZF Constructible
*)

use_thy "Reflection";
--- a/src/ZF/Constructible/Relative.thy	Tue Jul 09 13:41:38 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Tue Jul 09 15:39:44 2002 +0200
@@ -104,8 +104,9 @@
composition :: "[i=>o,i,i,i] => o"
"composition(M,r,s,t) ==
\<forall>p[M]. p \<in> t <->
-               (\<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)"
-
+               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
+                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
+                xy \<in> s & yz \<in> r)"

injection :: "[i=>o,i,i,i] => o"
"injection(M,A,B,f) == 
--- a/src/ZF/Constructible/Separation.thy	Tue Jul 09 13:41:38 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Tue Jul 09 15:39:44 2002 +0200
@@ -1,13 +1,16 @@
-header{*Proving instances of Separation using Reflection!*}
+header{*Some Instances of Separation and Strong Replacement*}

-theory Separation = L_axioms:
+(*This theory proves all instances needed for locale M_axioms*)
+
+theory Separation = L_axioms + WFrec:

text{*Helps us solve for de Bruijn indices!*}
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
by simp

lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
-lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats fun_plus_iff_sats
+lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
+                   fun_plus_iff_sats

lemma Collect_conj_in_DPow:
"[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |]
@@ -48,7 +51,7 @@
lemma Inter_Reflects:
"REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
\<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]"
-by (intro FOL_reflection)
+by (intro FOL_reflections)

lemma Inter_separation:
"L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
@@ -68,11 +71,11 @@

subsection{*Separation for Cartesian Product*}

-lemma cartprod_Reflects [simplified]:
+lemma cartprod_Reflects:
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
pair(**Lset(i),x,y,z))]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma cartprod_separation:
"[| L(A); L(B) |]
@@ -94,13 +97,10 @@

subsection{*Separation for Image*}

-text{*No @{text simplified} here: it simplifies the occurrence of
-      the predicate @{term pair}!*}
lemma image_Reflects:
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
\<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))]"
-by (intro FOL_reflection function_reflection)
-
+by (intro FOL_reflections function_reflections)

lemma image_separation:
"[| L(A); L(r) |]
@@ -126,7 +126,7 @@
"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)),
\<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma converse_separation:
"L(r) ==> separation(L,
@@ -152,7 +152,7 @@
lemma restrict_Reflects:
"REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
\<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma restrict_separation:
"L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
@@ -181,7 +181,7 @@
\<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).
pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma comp_separation:
"[| L(r); L(s) |]
@@ -209,7 +209,7 @@
lemma pred_Reflects:
"REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
\<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma pred_separation:
"[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
@@ -234,7 +234,7 @@
lemma Memrel_Reflects:
"REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
\<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma Memrel_separation:
"separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
@@ -263,7 +263,7 @@
\<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) &
is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma funspace_succ_replacement:
"L(n) ==>
@@ -295,7 +295,7 @@
(\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
\<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
-by (intro FOL_reflection function_reflection)
+by (intro FOL_reflections function_reflections)

lemma well_ord_iso_separation:
"[| L(A); L(f); L(r) |]
@@ -325,7 +325,7 @@
\<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
order_isomorphism(**Lset(i),par,r,x,mx,g)]"
-by (intro FOL_reflection function_reflection fun_plus_reflection)
+by (intro FOL_reflections function_reflections fun_plus_reflections)

lemma obase_separation:
--{*part of the order type formalization*}
@@ -360,7 +360,7 @@
ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
-by (intro FOL_reflection function_reflection fun_plus_reflection)
+by (intro FOL_reflections function_reflections fun_plus_reflections)

lemma obase_equals_separation:
@@ -395,7 +395,7 @@
ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
order_isomorphism(**Lset(i),par,r,x,mx,g))]"
-by (intro FOL_reflection function_reflection fun_plus_reflection)
+by (intro FOL_reflections function_reflections fun_plus_reflections)

lemma omap_replacement:
"[| L(A); L(r) |]
@@ -420,4 +420,272 @@
done

+
+subsection{*Separation for a Theorem about @{term "obase"}*}
+
+lemma is_recfun_reflects:
+  "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L].
+                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
+                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
+                                   fx \<noteq> gx),
+   \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i).
+          pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r &
+                (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) &
+                  fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]"
+by (intro FOL_reflections function_reflections fun_plus_reflections)
+
+lemma is_recfun_separation:
+     --{*for well-founded recursion*}
+     "[| L(r); L(f); L(g); L(a); L(b) |]
+     ==> separation(L,
+            \<lambda>x. \<exists>xa[L]. \<exists>xb[L].
+                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
+                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
+                                   fx \<noteq> gx))"
+apply (rule separation_CollectI)
+apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast )
+apply (rule ReflectsE [OF is_recfun_reflects], assumption)
+apply (drule subset_Lset_ltD, assumption)
+apply (erule reflection_imp_L_separation)
+apply (rule DPowI2)
+apply (rename_tac u)
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[x,u,r,f,g,a,b]" in pair_iff_sats)
+apply (rule sep_rules | simp)+
+done
+
+
+ML
+{*
+val Inter_separation = thm "Inter_separation";
+val cartprod_separation = thm "cartprod_separation";
+val image_separation = thm "image_separation";
+val converse_separation = thm "converse_separation";
+val restrict_separation = thm "restrict_separation";
+val comp_separation = thm "comp_separation";
+val pred_separation = thm "pred_separation";
+val Memrel_separation = thm "Memrel_separation";
+val funspace_succ_replacement = thm "funspace_succ_replacement";
+val well_ord_iso_separation = thm "well_ord_iso_separation";
+val obase_separation = thm "obase_separation";
+val obase_equals_separation = thm "obase_equals_separation";
+val omap_replacement = thm "omap_replacement";
+val is_recfun_separation = thm "is_recfun_separation";
+
+val m_axioms =
+    [Inter_separation, cartprod_separation, image_separation,
+     converse_separation, restrict_separation, comp_separation,
+     pred_separation, Memrel_separation, funspace_succ_replacement,
+     well_ord_iso_separation, obase_separation,
+     obase_equals_separation, omap_replacement, is_recfun_separation]
+
+fun axiomsL th =
+    kill_flex_triv_prems (m_axioms MRS (trivaxL th));
+
+bind_thm ("cartprod_iff", axiomsL (thm "M_axioms.cartprod_iff"));
+bind_thm ("cartprod_closed", axiomsL (thm "M_axioms.cartprod_closed"));
+bind_thm ("sum_closed", axiomsL (thm "M_axioms.sum_closed"));
+bind_thm ("M_converse_iff", axiomsL (thm "M_axioms.M_converse_iff"));
+bind_thm ("converse_closed", axiomsL (thm "M_axioms.converse_closed"));
+bind_thm ("converse_abs", axiomsL (thm "M_axioms.converse_abs"));
+bind_thm ("image_closed", axiomsL (thm "M_axioms.image_closed"));
+bind_thm ("vimage_abs", axiomsL (thm "M_axioms.vimage_abs"));
+bind_thm ("vimage_closed", axiomsL (thm "M_axioms.vimage_closed"));
+bind_thm ("domain_abs", axiomsL (thm "M_axioms.domain_abs"));
+bind_thm ("domain_closed", axiomsL (thm "M_axioms.domain_closed"));
+bind_thm ("range_abs", axiomsL (thm "M_axioms.range_abs"));
+bind_thm ("range_closed", axiomsL (thm "M_axioms.range_closed"));
+bind_thm ("field_abs", axiomsL (thm "M_axioms.field_abs"));
+bind_thm ("field_closed", axiomsL (thm "M_axioms.field_closed"));
+bind_thm ("relation_abs", axiomsL (thm "M_axioms.relation_abs"));
+bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs"));
+bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed"));
+bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs"));
+bind_thm ("typed_apply_abs", axiomsL (thm "M_axioms.typed_apply_abs"));
+bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs"));
+bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs"));
+bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs"));
+bind_thm ("bijection_abs", axiomsL (thm "M_axioms.bijection_abs"));
+bind_thm ("M_comp_iff", axiomsL (thm "M_axioms.M_comp_iff"));
+bind_thm ("comp_closed", axiomsL (thm "M_axioms.comp_closed"));
+bind_thm ("composition_abs", axiomsL (thm "M_axioms.composition_abs"));
+bind_thm ("restriction_is_function", axiomsL (thm "M_axioms.restriction_is_function"));
+bind_thm ("restriction_abs", axiomsL (thm "M_axioms.restriction_abs"));
+bind_thm ("M_restrict_iff", axiomsL (thm "M_axioms.M_restrict_iff"));
+bind_thm ("restrict_closed", axiomsL (thm "M_axioms.restrict_closed"));
+bind_thm ("Inter_abs", axiomsL (thm "M_axioms.Inter_abs"));
+bind_thm ("Inter_closed", axiomsL (thm "M_axioms.Inter_closed"));
+bind_thm ("Int_closed", axiomsL (thm "M_axioms.Int_closed"));
+bind_thm ("finite_fun_closed", axiomsL (thm "M_axioms.finite_fun_closed"));
+bind_thm ("is_funspace_abs", axiomsL (thm "M_axioms.is_funspace_abs"));
+bind_thm ("succ_fun_eq2", axiomsL (thm "M_axioms.succ_fun_eq2"));
+bind_thm ("funspace_succ", axiomsL (thm "M_axioms.funspace_succ"));
+bind_thm ("finite_funspace_closed", axiomsL (thm "M_axioms.finite_funspace_closed"));
+*}
+
+ML
+{*
+bind_thm ("is_recfun_equal", axiomsL (thm "M_axioms.is_recfun_equal"));
+bind_thm ("is_recfun_cut", axiomsL (thm "M_axioms.is_recfun_cut"));
+bind_thm ("is_recfun_functional", axiomsL (thm "M_axioms.is_recfun_functional"));
+bind_thm ("is_recfun_relativize", axiomsL (thm "M_axioms.is_recfun_relativize"));
+bind_thm ("is_recfun_restrict", axiomsL (thm "M_axioms.is_recfun_restrict"));
+bind_thm ("univalent_is_recfun", axiomsL (thm "M_axioms.univalent_is_recfun"));
+bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep"));
+bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun"));
+bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun"));
+bind_thm ("is_recfun_iff_M", axiomsL (thm "M_axioms.is_recfun_iff_M"));
+bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs"));
+bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs"));
+bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs"));
+bind_thm ("wellordered_is_trans_on", axiomsL (thm "M_axioms.wellordered_is_trans_on"));
+bind_thm ("wellordered_is_linear", axiomsL (thm "M_axioms.wellordered_is_linear"));
+bind_thm ("wellordered_is_wellfounded_on", axiomsL (thm "M_axioms.wellordered_is_wellfounded_on"));
+bind_thm ("wellfounded_imp_wellfounded_on", axiomsL (thm "M_axioms.wellfounded_imp_wellfounded_on"));
+bind_thm ("wellfounded_on_subset_A", axiomsL (thm "M_axioms.wellfounded_on_subset_A"));
+bind_thm ("wellfounded_on_iff_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_iff_wellfounded"));
+bind_thm ("wellfounded_on_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_imp_wellfounded"));
+bind_thm ("wellfounded_on_field_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_field_imp_wellfounded"));
+bind_thm ("wellfounded_iff_wellfounded_on_field", axiomsL (thm "M_axioms.wellfounded_iff_wellfounded_on_field"));
+bind_thm ("wellfounded_induct", axiomsL (thm "M_axioms.wellfounded_induct"));
+bind_thm ("wellfounded_on_induct", axiomsL (thm "M_axioms.wellfounded_on_induct"));
+bind_thm ("wellfounded_on_induct2", axiomsL (thm "M_axioms.wellfounded_on_induct2"));
+bind_thm ("linear_imp_relativized", axiomsL (thm "M_axioms.linear_imp_relativized"));
+bind_thm ("trans_on_imp_relativized", axiomsL (thm "M_axioms.trans_on_imp_relativized"));
+bind_thm ("wf_on_imp_relativized", axiomsL (thm "M_axioms.wf_on_imp_relativized"));
+bind_thm ("wf_imp_relativized", axiomsL (thm "M_axioms.wf_imp_relativized"));
+bind_thm ("well_ord_imp_relativized", axiomsL (thm "M_axioms.well_ord_imp_relativized"));
+bind_thm ("order_isomorphism_abs", axiomsL (thm "M_axioms.order_isomorphism_abs"));
+bind_thm ("pred_set_abs", axiomsL (thm "M_axioms.pred_set_abs"));
+*}
+
+ML
+{*
+bind_thm ("pred_closed", axiomsL (thm "M_axioms.pred_closed"));
+bind_thm ("membership_abs", axiomsL (thm "M_axioms.membership_abs"));
+bind_thm ("M_Memrel_iff", axiomsL (thm "M_axioms.M_Memrel_iff"));
+bind_thm ("Memrel_closed", axiomsL (thm "M_axioms.Memrel_closed"));
+bind_thm ("wellordered_iso_predD", axiomsL (thm "M_axioms.wellordered_iso_predD"));
+bind_thm ("wellordered_iso_pred_eq", axiomsL (thm "M_axioms.wellordered_iso_pred_eq"));
+bind_thm ("wellfounded_on_asym", axiomsL (thm "M_axioms.wellfounded_on_asym"));
+bind_thm ("wellordered_asym", axiomsL (thm "M_axioms.wellordered_asym"));
+bind_thm ("ord_iso_pred_imp_lt", axiomsL (thm "M_axioms.ord_iso_pred_imp_lt"));
+bind_thm ("obase_iff", axiomsL (thm "M_axioms.obase_iff"));
+bind_thm ("omap_iff", axiomsL (thm "M_axioms.omap_iff"));
+bind_thm ("omap_unique", axiomsL (thm "M_axioms.omap_unique"));
+bind_thm ("omap_yields_Ord", axiomsL (thm "M_axioms.omap_yields_Ord"));
+bind_thm ("otype_iff", axiomsL (thm "M_axioms.otype_iff"));
+bind_thm ("otype_eq_range", axiomsL (thm "M_axioms.otype_eq_range"));
+bind_thm ("Ord_otype", axiomsL (thm "M_axioms.Ord_otype"));
+bind_thm ("domain_omap", axiomsL (thm "M_axioms.domain_omap"));
+bind_thm ("omap_subset", axiomsL (thm "M_axioms.omap_subset"));
+bind_thm ("omap_funtype", axiomsL (thm "M_axioms.omap_funtype"));
+bind_thm ("wellordered_omap_bij", axiomsL (thm "M_axioms.wellordered_omap_bij"));
+bind_thm ("omap_ord_iso", axiomsL (thm "M_axioms.omap_ord_iso"));
+bind_thm ("Ord_omap_image_pred", axiomsL (thm "M_axioms.Ord_omap_image_pred"));
+bind_thm ("restrict_omap_ord_iso", axiomsL (thm "M_axioms.restrict_omap_ord_iso"));
+bind_thm ("obase_equals", axiomsL (thm "M_axioms.obase_equals"));
+bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
+bind_thm ("obase_exists", axiomsL (thm "M_axioms.obase_exists"));
+bind_thm ("omap_exists", axiomsL (thm "M_axioms.omap_exists"));
+bind_thm ("otype_exists", axiomsL (thm "M_axioms.otype_exists"));
+bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
+bind_thm ("ordertype_exists", axiomsL (thm "M_axioms.ordertype_exists"));
+bind_thm ("relativized_imp_well_ord", axiomsL (thm "M_axioms.relativized_imp_well_ord"));
+bind_thm ("well_ord_abs", axiomsL (thm "M_axioms.well_ord_abs"));
+*}
+
+declare cartprod_closed [intro,simp]
+declare sum_closed [intro,simp]
+declare converse_closed [intro,simp]
+declare converse_abs [simp]
+declare image_closed [intro,simp]
+declare vimage_abs [simp]
+declare vimage_closed [intro,simp]
+declare domain_abs [simp]
+declare domain_closed [intro,simp]
+declare range_abs [simp]
+declare range_closed [intro,simp]
+declare field_abs [simp]
+declare field_closed [intro,simp]
+declare relation_abs [simp]
+declare function_abs [simp]
+declare apply_closed [intro,simp]
+declare typed_function_abs [simp]
+declare injection_abs [simp]
+declare surjection_abs [simp]
+declare bijection_abs [simp]
+declare comp_closed [intro,simp]
+declare composition_abs [simp]
+declare restriction_abs [simp]
+declare restrict_closed [intro,simp]
+declare Inter_abs [simp]
+declare Inter_closed [intro,simp]
+declare Int_closed [intro,simp]
+declare finite_fun_closed [rule_format]
+declare is_funspace_abs [simp]
+declare finite_funspace_closed [intro,simp]
+
+
+(***NOW FOR THE LOCALE M_TRANCL***)
+
+subsection{*Separation for Reflexive/Transitive Closure*}
+
+lemma rtrancl_reflects:
+  "REFLECTS[\<lambda>p.
+    \<exists>nnat[L]. \<exists>n[L]. \<exists>n'[L]. omega(L,nnat) & n\<in>nnat & successor(L,n,n') &
+     (\<exists>f[L].
+      typed_function(L,n',A,f) &
+      (\<exists>x[L]. \<exists>y[L]. \<exists>zero[L]. pair(L,x,y,p) & empty(L,zero) &
+	fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) &
+	(\<forall>j[L]. j\<in>n -->
+	  (\<exists>fj[L]. \<exists>sj[L]. \<exists>fsj[L]. \<exists>ffp[L].
+	    fun_apply(L,f,j,fj) & successor(L,j,sj) &
+	    fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \<in> r))),
+\<lambda>i p.
+    \<exists>nnat \<in> Lset(i). \<exists>n \<in> Lset(i). \<exists>n' \<in> Lset(i).
+     omega(**Lset(i),nnat) & n\<in>nnat & successor(**Lset(i),n,n') &
+     (\<exists>f \<in> Lset(i).
+      typed_function(**Lset(i),n',A,f) &
+      (\<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) &
+	fun_apply(**Lset(i),f,zero,x) & fun_apply(**Lset(i),f,n,y)) &
+	(\<forall>j \<in> Lset(i). j\<in>n -->
+	  (\<exists>fj \<in> Lset(i). \<exists>sj \<in> Lset(i). \<exists>fsj \<in> Lset(i). \<exists>ffp \<in> Lset(i).
+	    fun_apply(**Lset(i),f,j,fj) & successor(**Lset(i),j,sj) &
+	    fun_apply(**Lset(i),f,sj,fsj) & pair(**Lset(i),fj,fsj,ffp) & ffp \<in> r)))]"
+by (intro FOL_reflections function_reflections fun_plus_reflections)
+
+
+text{*This formula describes @{term "rtrancl(r)"}.*}
+lemma rtrancl_separation:
+     "[| L(r); L(A) |] ==>
+      separation (L, \<lambda>p.
+	  \<exists>nnat[L]. \<exists>n[L]. \<exists>n'[L].
+           omega(L,nnat) & n\<in>nnat & successor(L,n,n') &
+	   (\<exists>f[L].
+	    typed_function(L,n',A,f) &
+	    (\<exists>x[L]. \<exists>y[L]. \<exists>zero[L]. pair(L,x,y,p) & empty(L,zero) &
+	      fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) &
+	      (\<forall>j[L]. j\<in>n -->
+		(\<exists>fj[L]. \<exists>sj[L]. \<exists>fsj[L]. \<exists>ffp[L].
+		  fun_apply(L,f,j,fj) & successor(L,j,sj) &
+		  fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \<in> r))))"
+apply (rule separation_CollectI)
+apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
+apply (rule ReflectsE [OF rtrancl_reflects], assumption)
+apply (drule subset_Lset_ltD, assumption)
+apply (erule reflection_imp_L_separation)
+apply (rule DPowI2)
+apply (rename_tac u)
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[x,u,r,A]" in omega_iff_sats)
+txt{*SLOW, maybe just due to the formula's size*}
+apply (rule sep_rules | simp)+
+done
+
+
end
--- a/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 13:41:38 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 15:39:44 2002 +0200
@@ -133,18 +133,24 @@

locale M_trancl = M_axioms +
-(*THEY NEED RELATIVIZATION*)
assumes rtrancl_separation:
-     "[| M(r); M(A) |] ==>
-	separation
-	   (M, \<lambda>p. \<exists>n[M]. n\<in>nat &
-                    (\<exists>f[M].
-                     f \<in> succ(n) -> A &
-                     (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) &
-                           f0 = x & fn = y) &
-                           (\<forall>i\<in>n. <fi, fsucc(i)> \<in> r)))"
+	 "[| M(r); M(A) |] ==>
+	  separation (M, \<lambda>p.
+	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
+               omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
+	       (\<exists>f[M].
+		typed_function(M,n',A,f) &
+		(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
+		  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
+		  (\<forall>j[M]. j\<in>n -->
+		    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
+		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
+		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r))))"
and wellfounded_trancl_separation:
-     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+)"
+	 "[| M(r); M(Z) |] ==>
+	  separation (M, \<lambda>x.
+	      \<exists>w[M]. \<exists>wx[M]. \<exists>rp[M].
+	       w \<in> Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \<in> rp)"

lemma (in M_trancl) rtran_closure_rtrancl:
@@ -203,6 +209,9 @@
"[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)"

+lemma (in M_trancl) wellfounded_trancl_separation':
+     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & <w,x> \<in> r^+)"
+by (insert wellfounded_trancl_separation [of r Z], simp)

text{*Alternative proof of @{text wf_on_trancl}; inspiration for the
relativized version.  Original version is on theory WF.*}
@@ -213,7 +222,6 @@
apply (blast elim: tranclE)
done

-
lemma (in M_trancl) wellfounded_on_trancl:
"[| wellfounded_on(M,A,r);  r-A <= A; M(r); M(A) |]
==> wellfounded_on(M,A,r^+)"
@@ -222,7 +230,7 @@
apply (rename_tac Z x)
apply (subgoal_tac "M({x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+})")
prefer 2
- apply (blast intro: wellfounded_trancl_separation)
+ apply (blast intro: wellfounded_trancl_separation')
apply (drule_tac x = "{x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+}" in rspec, safe)
apply (blast dest: transM, simp)
apply (rename_tac y w)
--- a/src/ZF/Constructible/document/root.tex	Tue Jul 09 13:41:38 2002 +0200
+++ b/src/ZF/Constructible/document/root.tex	Tue Jul 09 15:39:44 2002 +0200
@@ -16,9 +16,8 @@
% this should be the last package used
\usepackage{pdfsetup}

-% proper setup for best-style documents
\urlstyle{rm}
-\isabellestyle{it}
+\isabellestyle{tt} %and not {it}!

\begin{document}