# HG changeset patch
# User paulson
# Date 1029508908 -7200
# Node ID 52a16cb7fefbece677278d965fdf032290c859bb
# Parent  59066e97b551c9e8c0511bfe0c6ca2aff3832b8a
Relativized right up to L satisfies V=L!

diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -246,7 +246,7 @@
 apply (subgoal_tac "L(env) & L(p)") 
  prefer 2 apply (blast intro: transL) 
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF DPow_body_reflection], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -316,4 +316,351 @@
 lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L]
   and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L]
 
+
+subsubsection{*The Operator @{term is_Collect}*}
+
+text{*The formula @{term is_P} has one free variable, 0, and it is
+enclosed within a single quantifier.*}
+
+(* is_Collect :: "[i=>o,i,i=>o,i] => o"
+    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)" *)
+
+constdefs Collect_fm :: "[i, i, i]=>i"
+ "Collect_fm(A,is_P,z) == 
+        Forall(Iff(Member(0,succ(z)),
+                   And(Member(0,succ(A)), is_P)))"
+
+lemma is_Collect_type [TC]:
+     "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
+      ==> Collect_fm(x,is_P,y) \<in> formula"
+by (simp add: Collect_fm_def)
+
+lemma sats_Collect_fm:
+  assumes is_P_iff_sats: 
+      "!!a. a \<in> A ==> is_P(a) <-> sats(A, p, Cons(a, env))"
+  shows 
+      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
+       ==> sats(A, Collect_fm(x,p,y), env) <->
+           is_Collect(**A, nth(x,env), is_P, nth(y,env))"
+by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym])
+
+lemma Collect_iff_sats:
+  assumes is_P_iff_sats: 
+      "!!a. a \<in> A ==> is_P(a) <-> sats(A, p, Cons(a, env))"
+  shows 
+  "[| nth(i,env) = x; nth(j,env) = y;
+      i \<in> nat; j \<in> nat; env \<in> list(A)|]
+   ==> is_Collect(**A, x, is_P, y) <-> sats(A, Collect_fm(i,p,j), env)"
+by (simp add: sats_Collect_fm [OF is_P_iff_sats])
+
+
+text{*The second argument of @{term is_P} gives it direct access to @{term x},
+  which is essential for handling free variable references.*}
+theorem Collect_reflection:
+  assumes is_P_reflection:
+    "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
+                     \<lambda>i x. is_P(**Lset(i), f(x), g(x))]"
+  shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
+               \<lambda>i x. is_Collect(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
+apply (simp (no_asm_use) only: is_Collect_def setclass_simps)
+apply (intro FOL_reflections is_P_reflection)
+done
+
+
+subsubsection{*The Operator @{term is_Replace}*}
+
+text{*BEWARE!  The formula @{term is_P} has free variables 0, 1
+ and not the usual 1, 0!  It is enclosed within two quantifiers.*}
+
+(*  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
+    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))" *)
+
+constdefs Replace_fm :: "[i, i, i]=>i"
+ "Replace_fm(A,is_P,z) == 
+        Forall(Iff(Member(0,succ(z)),
+                   Exists(And(Member(0,A#+2), is_P))))"
+
+lemma is_Replace_type [TC]:
+     "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
+      ==> Replace_fm(x,is_P,y) \<in> formula"
+by (simp add: Replace_fm_def)
+
+lemma sats_Replace_fm:
+  assumes is_P_iff_sats: 
+      "!!a b. [|a \<in> A; b \<in> A|] 
+              ==> is_P(a,b) <-> sats(A, p, Cons(a,Cons(b,env)))"
+  shows 
+      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
+       ==> sats(A, Replace_fm(x,p,y), env) <->
+           is_Replace(**A, nth(x,env), is_P, nth(y,env))"
+by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym])
+
+lemma Replace_iff_sats:
+  assumes is_P_iff_sats: 
+      "!!a b. [|a \<in> A; b \<in> A|] 
+              ==> is_P(a,b) <-> sats(A, p, Cons(a,Cons(b,env)))"
+  shows 
+  "[| nth(i,env) = x; nth(j,env) = y;
+      i \<in> nat; j \<in> nat; env \<in> list(A)|]
+   ==> is_Replace(**A, x, is_P, y) <-> sats(A, Replace_fm(i,p,j), env)"
+by (simp add: sats_Replace_fm [OF is_P_iff_sats])
+
+
+text{*The second argument of @{term is_P} gives it direct access to @{term x},
+  which is essential for handling free variable references.*}
+theorem Replace_reflection:
+  assumes is_P_reflection:
+    "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
+                     \<lambda>i x. is_P(**Lset(i), f(x), g(x), h(x))]"
+  shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
+               \<lambda>i x. is_Replace(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
+apply (simp (no_asm_use) only: is_Replace_def setclass_simps)
+apply (intro FOL_reflections is_P_reflection)
+done
+
+
+
+subsubsection{*The Operator @{term is_DPow'}, Internalized*}
+
+(*  "is_DPow'(M,A,Z) == 
+       \<forall>X[M]. X \<in> Z <-> 
+         subset(M,X,A) & 
+           (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
+                    is_Collect(M, A, is_DPow_body(M,A,env,p), X))" *)
+
+constdefs DPow'_fm :: "[i,i]=>i"
+    "DPow'_fm(A,Z) == 
+      Forall(
+       Iff(Member(0,succ(Z)),
+        And(subset_fm(0,succ(A)),
+         Exists(Exists(
+          And(mem_formula_fm(0),
+           And(mem_list_fm(A#+3,1),
+            Collect_fm(A#+3, 
+                       DPow_body_fm(A#+4, 2, 1, 0), 2))))))))"
+
+lemma is_DPow'_type [TC]:
+     "[| x \<in> nat; y \<in> nat |] ==> DPow'_fm(x,y) \<in> formula"
+by (simp add: DPow'_fm_def)
+
+lemma sats_DPow'_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
+    ==> sats(A, DPow'_fm(x,y), env) <->
+        is_DPow'(**A, nth(x,env), nth(y,env))"
+by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm)
+
+lemma DPow'_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y; 
+          i \<in> nat; j \<in> nat; env \<in> list(A)|]
+       ==> is_DPow'(**A, x, y) <-> sats(A, DPow'_fm(i,j), env)"
+by (simp add: sats_DPow'_fm)
+
+theorem DPow'_reflection:
+     "REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
+               \<lambda>i x. is_DPow'(**Lset(i),f(x),g(x))]"
+apply (simp only: is_DPow'_def setclass_simps)
+apply (intro FOL_reflections function_reflections mem_formula_reflection
+             mem_list_reflection Collect_reflection DPow_body_reflection)
+done
+
+(*????????????????move up*)
+
+
+
+
+
+subsection{*Additional Constraints on the Class Model @{term M}*}
+
+constdefs
+  transrec_body :: "[i=>o,i,i,i,i] => o"
+    "transrec_body(M,g,x) ==
+      \<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
+
+lemma (in M_DPow) transrec_body_abs:
+     "[|M(x); M(g); M(z)|]
+    ==> transrec_body(M,g,x,y,z) <-> y \<in> x & z = DPow'(g`y)"
+by (simp add: transrec_body_def DPow'_abs transM [of _ x])
+
+locale M_Lset = M_DPow +
+ assumes strong_rep:
+   "[|M(x); M(g)|] ==> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))"
+ and transrec_rep: 
+    "M(i) ==> transrec_replacement(M, \<lambda>x f u. 
+              \<exists>r[M]. is_Replace(M, x, transrec_body(M,f,x), r) & 
+                     big_union(M, r, u), i)"
+
+
+lemma (in M_Lset) strong_rep':
+   "[|M(x); M(g)|]
+    ==> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))"
+by (insert strong_rep [of x g], simp add: transrec_body_abs)
+
+lemma (in M_Lset) DPow_apply_closed:
+   "[|M(f); M(x); y\<in>x|] ==> M(DPow'(f`y))"
+by (blast intro: DPow'_closed dest: transM) 
+
+lemma (in M_Lset) RepFun_DPow_apply_closed:
+   "[|M(f); M(x)|] ==> M({DPow'(f`y). y\<in>x})"
+by (blast intro: DPow_apply_closed RepFun_closed2 strong_rep') 
+
+lemma (in M_Lset) RepFun_DPow_abs:
+     "[|M(x); M(f); M(r) |]
+      ==> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) <->
+          r =  {DPow'(f`y). y\<in>x}"
+apply (simp add: transrec_body_abs RepFun_def) 
+apply (rule iff_trans) 
+apply (rule Replace_abs) 
+apply (simp_all add: DPow_apply_closed strong_rep') 
+done
+
+lemma (in M_Lset) transrec_rep':
+   "M(i) ==> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)"
+apply (insert transrec_rep [of i]) 
+apply (simp add: RepFun_DPow_apply_closed RepFun_DPow_abs 
+       transrec_replacement_def) 
+done
+
+
+
+constdefs
+
+  is_Lset :: "[i=>o, i, i] => o"
+   "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
+
+lemma (in M_Lset) Lset_abs:
+  "[|Ord(i);  M(i);  M(z)|] 
+   ==> is_Lset(M,i,z) <-> z = Lset(i)"
+apply (simp add: is_Lset_def Lset_eq_transrec_DPow') 
+apply (rule transrec_abs)  
+apply (simp_all add: transrec_rep' relativize2_def RepFun_DPow_apply_closed)
+done
+
+lemma (in M_Lset) Lset_closed:
+  "[|Ord(i);  M(i)|] ==> M(Lset(i))"
+apply (simp add: Lset_eq_transrec_DPow') 
+apply (rule transrec_closed [OF transrec_rep']) 
+apply (simp_all add: relativize2_def RepFun_DPow_apply_closed)
+done
+
+
+subsection{*Instantiating the Locale @{text M_Lset}*}
+
+
+subsubsection{*The First Instance of Replacement*}
+
+lemma strong_rep_Reflects:
+ "REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L].
+                          v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)),
+   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i).
+            v \<in> x & fun_apply(**Lset(i),g,v,gy) & is_DPow'(**Lset(i),gy,u))]"
+by (intro FOL_reflections function_reflections DPow'_reflection)
+
+lemma strong_rep:
+   "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
+apply (unfold transrec_body_def)  
+apply (rule strong_replacementI) 
+apply (rule rallI)
+apply (rename_tac B)  
+apply (rule separation_CollectI) 
+apply (rule_tac A="{x,g,B,z}" in subset_LsetE, blast) 
+apply (rule ReflectsE [OF strong_rep_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2)
+apply (rule DPow_LsetI)
+apply (rename_tac u) 
+apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[v,u,x,g,B,z]" in mem_iff_sats) 
+apply (rule sep_rules DPow'_iff_sats | simp)+
+done
+
+
+subsubsection{*The Second Instance of Replacement*}
+
+lemma transrec_rep_Reflects:
+ "REFLECTS [\<lambda>x. \<exists>v[L]. v \<in> B &
+              (\<exists>y[L]. pair(L,v,y,x) &
+             is_wfrec (L, \<lambda>x f u. \<exists>r[L].
+                is_Replace (L, x, \<lambda>y z. 
+                     \<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) & 
+                      is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)),
+    \<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B &
+              (\<exists>y \<in> Lset(i). pair(**Lset(i),v,y,x) &
+             is_wfrec (**Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
+                is_Replace (**Lset(i), x, \<lambda>y z. 
+                     \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(**Lset(i),f,y,gy) & 
+                      is_DPow'(**Lset(i),gy,z), r) & 
+                      big_union(**Lset(i),r,u), mr, v, y))]" 
+apply (simp only: setclass_simps [symmetric])
+  --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[**Lset(i)]"} within the body
+       of the @{term is_wfrec} application. *}
+apply (intro FOL_reflections function_reflections 
+          is_wfrec_reflection Replace_reflection DPow'_reflection) 
+done
+
+
+
+lemma transrec_rep: 
+    "[|L(j)|]
+    ==> transrec_replacement(L, \<lambda>x f u. 
+              \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
+                     big_union(L, r, u), j)"
+apply (subgoal_tac "L(Memrel(eclose({j})))")
+ prefer 2 apply simp
+apply (rule transrec_replacementI, assumption)
+apply (rule strong_replacementI)
+apply (unfold transrec_body_def)  
+apply (rule rallI)
+apply (rename_tac B)
+apply (rule separation_CollectI)
+apply (rule_tac A="{j,B,z,Memrel(eclose({j}))}" in subset_LsetE, blast)
+apply (rule ReflectsE [OF transrec_rep_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption)
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2 Memrel_closed)
+apply (elim conjE)
+apply (rule DPow_LsetI)
+apply (rename_tac w)
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[v,w,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
+apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
+       simp)+
+done
+
+
+subsubsection{*Actually Instantiating @{text M_Lset}*}
+
+lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
+  apply (rule M_Lset_axioms.intro)
+       apply (assumption | rule strong_rep transrec_rep)+
+  done
+
+theorem M_Lset_L: "PROP M_Lset(L)"
+apply (rule M_Lset.intro) 
+     apply (rule M_DPow.axioms [OF M_DPow_L])+
+apply (rule M_Lset_axioms_L) 
+done
+
+text{*Finally: the point of the whole theory!*}
+lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
+   and Lset_abs = M_Lset.Lset_abs [OF M_Lset_L]
+
+
+subsection{*The Notion of Constructible Set*}
+
+
+constdefs
+  constructible :: "[i=>o,i] => o"
+    "constructible(M,x) ==
+       \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
+
+
+theorem V_equals_L_in_L:
+  "L(x) ==> constructible(L,x)"
+apply (simp add: constructible_def Lset_abs Lset_closed) 
+apply (simp add: L_def)
+apply (blast intro: Ord_in_L) 
+done
+
+
 end
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Datatype_absolute.thy
+    ID: $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {*Absoluteness Properties for Recursive Datatypes*}
 
 theory Datatype_absolute = Formula + WF_absolute:
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Formula.thy
+    ID: $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {* First-Order Formulas and the Definition of the Class L *}
 
 theory Formula = Main:
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Internalize.thy
--- a/src/ZF/Constructible/Internalize.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Internalize.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Internalize.thy
+    ID: $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 theory Internalize = L_axioms + Datatype_absolute:
 
 subsection{*Internalized Forms of Data Structuring Operators*}
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,8 @@
+(*  Title:      ZF/Constructible/L_axioms.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
 
 header {* The ZF Axioms (Except Separation) in L *}
 
@@ -1079,7 +1084,7 @@
     ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
 by (simp add: function_fm_def is_function_def)
 
-lemma function_iff_sats:
+lemma is_function_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
        ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
@@ -1141,11 +1146,11 @@
 lemmas function_iff_sats =
         empty_iff_sats number1_iff_sats
         upair_iff_sats pair_iff_sats union_iff_sats
-        cons_iff_sats successor_iff_sats
+        big_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 pre_image_iff_sats
-        relation_iff_sats function_iff_sats
+        relation_iff_sats is_function_iff_sats
 
 
 theorem typed_function_reflection:
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/MetaExists.thy
--- a/src/ZF/Constructible/MetaExists.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/MetaExists.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/MetaExists.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header{*The meta-existential quantifier*}
 
 theory MetaExists = Main:
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Normal.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Normal.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {*Closed Unbounded Classes and Normal Functions*}
 
 theory Normal = Main:
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -82,7 +82,7 @@
 lemma rtrancl_separation:
      "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
+apply (rule_tac A="{r,A,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -190,7 +190,7 @@
               \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
                w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
 apply (rule separation_CollectI)
-apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast )
+apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -252,7 +252,7 @@
       separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
          ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF wfrank_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -294,7 +294,7 @@
 apply (rule rallI)
 apply (rename_tac B)
 apply (rule separation_CollectI)
-apply (rule_tac A="{B,r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{B,r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -333,7 +333,7 @@
              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
              ordinal(L,rangef)))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -411,7 +411,7 @@
 apply (rule separation_CollectI)
 apply (insert nonempty)
 apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
+apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -492,7 +492,7 @@
 apply (rule separation_CollectI)
 apply (insert nonempty)
 apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
+apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -612,7 +612,7 @@
 apply (rule rallI)
 apply (rule separation_CollectI)
 apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast )
+apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -680,7 +680,7 @@
 apply (rename_tac B)
 apply (rule separation_CollectI)
 apply (subgoal_tac "L(Memrel(succ(n)))")
-apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast )
+apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Reflection.thy
--- a/src/ZF/Constructible/Reflection.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Reflection.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Reflection.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {* The Reflection Theorem*}
 
 theory Reflection = Normal:
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Relative.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {*Relativization and Absoluteness*}
 
 theory Relative = Main:
@@ -43,6 +49,9 @@
   is_Collect :: "[i=>o,i,i=>o,i] => o"
     "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
 
+  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
+    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))"
+
   inter :: "[i=>o,i,i,i] => o"
     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
 
@@ -294,12 +303,20 @@
       ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
 by (simp add: separation_def) 
 
-text{*Congruence rules for replacement*}
 lemma univalent_cong [cong]:
      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
       ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
 by (simp add: univalent_def) 
 
+lemma univalent_triv [intro,simp]:
+     "univalent(M, A, \<lambda>x y. y = f(x))"
+by (simp add: univalent_def) 
+
+lemma univalent_conjI2 [intro,simp]:
+     "univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))"
+by (simp add: univalent_def, blast) 
+
+text{*Congruence rule for replacement*}
 lemma strong_replacement_cong [cong]:
      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
       ==> strong_replacement(M, %x y. P(x,y)) <-> 
@@ -616,21 +633,46 @@
 done
 
 
+subsubsection{*The Operator @{term is_Replace}*}
+
+
+lemma is_Replace_cong [cong]:
+     "[| A=A'; 
+         !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y);
+         z=z' |] 
+      ==> is_Replace(M, A, %x y. P(x,y), z) <-> 
+          is_Replace(M, A', %x y. P'(x,y), z')" 
+by (simp add: is_Replace_def) 
+
+lemma (in M_triv_axioms) univalent_Replace_iff: 
+     "[| M(A); univalent(M,A,P);
+         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] 
+      ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
+apply (simp add: Replace_iff univalent_def) 
+apply (blast dest: transM)
+done
+
 (*The last premise expresses that P takes M to M*)
 lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
      "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
-       !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
+         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
 apply (simp add: strong_replacement_def) 
-apply (drule rspec, auto) 
+apply (drule_tac x=A in rspec, safe) 
 apply (subgoal_tac "Replace(A,P) = Y")
  apply simp 
-apply (rule equality_iffI) 
-apply (simp add: Replace_iff, safe)
- apply (blast dest: transM) 
-apply (frule transM, assumption) 
- apply (simp add: univalent_def)
- apply (drule rspec [THEN iffD1], assumption, assumption)
- apply (blast dest: transM) 
+apply (rule equality_iffI)
+apply (simp add: univalent_Replace_iff)
+apply (blast dest: transM) 
+done
+
+lemma (in M_triv_axioms) Replace_abs: 
+     "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
+         !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |] 
+      ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
+apply (simp add: is_Replace_def)
+apply (rule iffI) 
+apply (rule M_equalityI) 
+apply (simp_all add: univalent_Replace_iff, blast, blast) 
 done
 
 (*The first premise can't simply be assumed as a schema.
@@ -1490,34 +1532,34 @@
 subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
 
 lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
-by (simp add: is_hd_def )
+by (simp add: is_hd_def)
 
 lemma (in M_triv_axioms) is_hd_Cons:
      "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
-by (force simp add: is_hd_def ) 
+by (force simp add: is_hd_def) 
 
 lemma (in M_triv_axioms) hd_abs [simp]:
      "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
 apply (simp add: hd'_def)
 apply (intro impI conjI)
  prefer 2 apply (force simp add: is_hd_def) 
-apply (simp add: quasilist_def is_hd_def )
+apply (simp add: quasilist_def is_hd_def)
 apply (elim disjE exE, auto)
 done 
 
 lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
-by (simp add: is_tl_def )
+by (simp add: is_tl_def)
 
 lemma (in M_triv_axioms) is_tl_Cons:
      "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
-by (force simp add: is_tl_def ) 
+by (force simp add: is_tl_def) 
 
 lemma (in M_triv_axioms) tl_abs [simp]:
      "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
 apply (simp add: tl'_def)
 apply (intro impI conjI)
  prefer 2 apply (force simp add: is_tl_def) 
-apply (simp add: quasilist_def is_tl_def )
+apply (simp add: quasilist_def is_tl_def)
 apply (elim disjE exE, auto)
 done 
 
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -852,7 +852,7 @@
 theorem satisfies_is_d_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_is_d(**Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_is_d_def ) 
+apply (unfold satisfies_is_d_def) 
 apply (intro FOL_reflections function_reflections is_lambda_reflection
              extra_reflections nth_reflection depth_apply_reflection 
              is_list_reflection)
@@ -944,7 +944,7 @@
 apply (rule rallI)
 apply (rename_tac B)  
 apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
+apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
 apply (rule ReflectsE [OF Member_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
@@ -986,7 +986,7 @@
 apply (rule rallI)
 apply (rename_tac B)  
 apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
+apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
 apply (rule ReflectsE [OF Equal_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
@@ -1030,7 +1030,7 @@
 apply (rule rallI)
 apply (rename_tac B)  
 apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast ) 
+apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast) 
 apply (rule ReflectsE [OF Nand_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
@@ -1079,7 +1079,7 @@
 apply (rule rallI)
 apply (rename_tac B)  
 apply (rule separation_CollectI) 
-apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast ) 
+apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast) 
 apply (rule ReflectsE [OF Forall_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
@@ -1113,7 +1113,7 @@
 apply (rule rallI)
 apply (rename_tac B)
 apply (rule separation_CollectI)
-apply (rule_tac A="{B,A,n,z,Memrel(eclose({n}))}" in subset_LsetE, blast )
+apply (rule_tac A="{B,A,n,z,Memrel(eclose({n}))}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF formula_rec_replacement_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -62,7 +62,7 @@
 lemma Inter_separation:
      "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF Inter_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -84,7 +84,7 @@
 lemma Diff_separation:
      "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
 apply (rule separation_CollectI) 
-apply (rule_tac A="{B,z}" in subset_LsetE, blast ) 
+apply (rule_tac A="{B,z}" in subset_LsetE, blast) 
 apply (rule ReflectsE [OF Diff_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
@@ -107,7 +107,7 @@
      "[| L(A); L(B) |]
       ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,B,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF cartprod_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -131,7 +131,7 @@
      "[| L(A); L(r) |]
       ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF image_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -156,7 +156,7 @@
      "L(r) ==> separation(L,
          \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF converse_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -180,7 +180,7 @@
 lemma restrict_separation:
    "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF restrict_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -211,7 +211,7 @@
                   pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
                   xy\<in>s & yz\<in>r)"
 apply (rule separation_CollectI)
-apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )
+apply (rule_tac A="{r,s,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF comp_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -235,7 +235,7 @@
 lemma pred_separation:
      "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )
+apply (rule_tac A="{r,x,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF pred_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -259,7 +259,7 @@
 lemma Memrel_separation:
      "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
 apply (rule separation_CollectI)
-apply (rule_tac A="{z}" in subset_LsetE, blast )
+apply (rule_tac A="{z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF Memrel_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -292,7 +292,7 @@
 apply (rule strong_replacementI)
 apply (rule rallI)
 apply (rule separation_CollectI)
-apply (rule_tac A="{n,A,z}" in subset_LsetE, blast )
+apply (rule_tac A="{n,A,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -320,7 +320,7 @@
       ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
                      fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -351,7 +351,7 @@
              ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
              order_isomorphism(L,par,r,x,mx,g))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF obase_reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -386,7 +386,7 @@
                               membership(L,y,my) & pred_set(L,A,x,r,pxr) &
                               order_isomorphism(L,pxr,r,y,my,g))))"
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF obase_equals_reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -422,7 +422,7 @@
 apply (rule rallI)
 apply (rename_tac B)
 apply (rule separation_CollectI)
-apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast )
+apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast)
 apply (rule ReflectsE [OF omap_reflects], assumption)
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
@@ -457,7 +457,7 @@
                 (\<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_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)
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/WF_absolute.thy
--- a/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/WF_absolute.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*}
 
 theory WF_absolute = WFrec:
@@ -310,7 +316,8 @@
  apply (rule univalent_is_recfun)
    apply (blast intro: wellfounded_trancl)
   apply (rule trans_trancl)
- apply (simp add: trancl_subset_times, blast)
+ apply (simp add: trancl_subset_times) 
+apply (blast dest: transM) 
 done
 
 lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
@@ -569,7 +576,7 @@
 apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
        in rspec [THEN rspec]) 
 apply (simp_all add: function_lam) 
-apply (blast intro: lam_closed dest: pair_components_in_M ) 
+apply (blast intro: lam_closed dest: pair_components_in_M) 
 done
 
 text{*Eliminates one instance of replacement.*}
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/WFrec.thy
--- a/src/ZF/Constructible/WFrec.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/WFrec.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header{*Relativized Well-Founded Recursion*}
 
 theory WFrec = Wellorderings:
@@ -190,7 +196,7 @@
  apply (frule is_recfun_type [THEN fun_is_rel], blast)
 apply (frule pair_components_in_M, assumption, clarify) 
 apply (rule iffI)
- apply (frule_tac y="<y,z>" in transM, assumption )
+ apply (frule_tac y="<y,z>" in transM, assumption)
  apply (rotate_tac -1)   
  apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
 			   apply_recfun is_recfun_cut) 
diff -r 59066e97b551 -r 52a16cb7fefb src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 12:48:49 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 16:41:48 2002 +0200
@@ -1,3 +1,9 @@
+(*  Title:      ZF/Constructible/Wellorderings.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
+
 header {*Relativized Wellorderings*}
 
 theory Wellorderings = Relative:
@@ -57,15 +63,15 @@
 
 lemma (in M_axioms) wellordered_is_trans_on: 
     "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
-by (auto simp add: wellordered_def )
+by (auto simp add: wellordered_def)
 
 lemma (in M_axioms) wellordered_is_linear: 
     "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
-by (auto simp add: wellordered_def )
+by (auto simp add: wellordered_def)
 
 lemma (in M_axioms) wellordered_is_wellfounded_on: 
     "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
-by (auto simp add: wellordered_def )
+by (auto simp add: wellordered_def)
 
 lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
     "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
@@ -629,7 +635,7 @@
 lemma (in M_axioms) relativized_imp_well_ord: 
      "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
 apply (insert ordertype_exists [of A r], simp)
-apply (blast intro: well_ord_ord_iso well_ord_Memrel )  
+apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
 done
 
 subsection {*Kunen's theorem 5.4, poage 127*}