# HG changeset patch
# User paulson
# Date 1025256346 -7200
# Node ID 5146ccaedf42f0fd3fc48ba7f64c1cef0b102413
# Parent  edbf32029d33ce3f126cb0cc95ce0d1a8d2bcfca
class quantifiers (some)
absoluteness and closure for WFrec-defined functions

diff -r edbf32029d33 -r 5146ccaedf42 src/ZF/Constructible/ROOT.ML
--- a/src/ZF/Constructible/ROOT.ML	Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/ROOT.ML	Fri Jun 28 11:25:46 2002 +0200
@@ -7,5 +7,5 @@
 *)
 
 use_thy "Reflection";
-use_thy "WFrec";
+use_thy "WF_absolute";
 use_thy "L_axioms";
diff -r edbf32029d33 -r 5146ccaedf42 src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Fri Jun 28 11:25:46 2002 +0200
@@ -6,7 +6,7 @@
 
 constdefs
   empty :: "[i=>o,i] => o"
-    "empty(M,z) == \<forall>x. M(x) --> x \<notin> z"
+    "empty(M,z) == \<forall>x[M]. x \<notin> z"
 
   subset :: "[i=>o,i,i] => o"
     "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
@@ -15,42 +15,42 @@
     "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
 
   pair :: "[i=>o,i,i,i] => o"
-    "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) & 
-                          (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
+    "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
+                          (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
 
   union :: "[i=>o,i,i,i] => o"
-    "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
+    "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
 
   successor :: "[i=>o,i,i] => o"
-    "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
+    "successor(M,a,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,a,z)"
 
   powerset :: "[i=>o,i,i] => o"
-    "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
+    "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
 
   inter :: "[i=>o,i,i,i] => o"
-    "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
+    "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
 
   setdiff :: "[i=>o,i,i,i] => o"
-    "setdiff(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<notin> b)"
+    "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
 
   big_union :: "[i=>o,i,i] => o"
-    "big_union(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y))"
+    "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y)"
 
   big_inter :: "[i=>o,i,i] => o"
     "big_inter(M,A,z) == 
              (A=0 --> z=0) &
-	     (A\<noteq>0 --> (\<forall>x. M(x) --> (x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y))))"
+	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y)))"
 
   cartprod :: "[i=>o,i,i,i] => o"
     "cartprod(M,A,B,z) == 
-	\<forall>u. M(u) --> (u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u))))"
+	\<forall>u[M]. u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u)))"
 
   is_converse :: "[i=>o,i,i] => o"
     "is_converse(M,r,z) == 
 	\<forall>x. M(x) --> 
             (x \<in> z <-> 
              (\<exists>w\<in>r. M(w) & 
-              (\<exists>u v. M(u) & M(v) & pair(M,u,v,w) & pair(M,v,u,x))))"
+              (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"
 
   pre_image :: "[i=>o,i,i,i] => o"
     "pre_image(M,r,A,z) == 
@@ -224,17 +224,17 @@
 by (blast intro: univ0_downwards_mem) 
 
 text{*Congruence rule for separation: can assume the variable is in @{text M}*}
-lemma [cong]:
+lemma separation_cong [cong]:
      "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
 by (simp add: separation_def) 
 
 text{*Congruence rules for replacement*}
-lemma [cong]:
+lemma univalent_cong [cong]:
      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
       ==> univalent(M,A,P) <-> univalent(M,A',P')"
 by (simp add: univalent_def) 
 
-lemma [cong]:
+lemma strong_replacement_cong [cong]:
      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
       ==> strong_replacement(M,P) <-> strong_replacement(M,P')" 
 by (simp add: strong_replacement_def) 
@@ -398,8 +398,8 @@
      "[| M(A); M(r) |] 
       ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
   and converse_separation:
-     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) & 
-				     pair(M,x,y,p) & pair(M,y,x,z)))"
+     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. 
+                    M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   and restrict_separation:
      "M(A) 
       ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
@@ -507,7 +507,7 @@
      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
 apply (simp add: cartprod_def)
 apply (rule iffI) 
-apply (blast intro!: equalityI intro: transM dest!: spec) 
+ apply (blast intro!: equalityI intro: transM dest!: rspec) 
 apply (blast dest: transM) 
 done
 
@@ -616,15 +616,6 @@
       ==> M(\<lambda>x\<in>A. b(x))"
 by (simp add: lam_def, blast dest: transM) 
 
-lemma (in M_axioms) converse_abs [simp]: 
-     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
-apply (simp add: is_converse_def)
-apply (rule iffI)
- apply (rule equalityI) 
-  apply (blast dest: transM) 
- apply (clarify, frule transM, assumption, simp, blast) 
-done
-
 lemma (in M_axioms) image_abs [simp]: 
      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
 apply (simp add: image_def)
@@ -648,11 +639,14 @@
 done
 
 lemma (in M_axioms) cartprod_iff_lemma:
-     "[| M(C); \<forall>u. M(u) --> u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
-       powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
+     "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
+         powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
 apply (simp add: powerset_def) 
-apply (rule equalityI, clarify, simp) 
+apply (rule equalityI, clarify, simp)
+
+ apply (frule transM, assumption) 
+
  apply (frule transM, assumption, simp) 
  apply blast 
 apply clarify
@@ -751,8 +745,7 @@
 lemma (in M_axioms) M_converse_iff:
      "M(r) ==> 
       converse(r) = 
-      {z \<in> range(r) * domain(r). 
-        \<exists>p\<in>r. \<exists>x. M(x) & (\<exists>y. M(y) & p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>)}"
+      {z \<in> range(r) * domain(r). \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
 by (blast dest: transM)
 
 lemma (in M_axioms) converse_closed [intro,simp]: 
@@ -761,6 +754,16 @@
 apply (insert converse_separation [of r], simp)
 done
 
+lemma (in M_axioms) converse_abs [simp]: 
+     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
+apply (simp add: is_converse_def)
+apply (rule iffI)
+ prefer 2 apply (blast intro: elim:); 
+apply (rule M_equalityI)
+  apply (simp add: )
+  apply (blast dest: transM)+
+done
+
 lemma (in M_axioms) relation_abs [simp]: 
      "M(r) ==> is_relation(M,r) <-> relation(r)"
 apply (simp add: is_relation_def relation_def) 
diff -r edbf32029d33 -r 5146ccaedf42 src/ZF/Constructible/WF_absolute.thy
--- a/src/ZF/Constructible/WF_absolute.thy	Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Fri Jun 28 11:25:46 2002 +0200
@@ -303,8 +303,7 @@
  apply (rule univalent_is_recfun)
    apply (blast intro: wellfounded_trancl)
   apply (rule trans_trancl)
- apply (simp add: trancl_subset_times)
-apply blast
+ apply (simp add: trancl_subset_times, blast)
 done
 
 lemma (in M_recursion) Ord_wfrank_range [rule_format]:
@@ -312,9 +311,8 @@
      ==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
 apply (drule wellfounded_trancl, assumption)
 apply (rule wellfounded_induct, assumption+)
-  apply (simp add:);
- apply (blast intro: Ord_wfrank_separation);
-apply (clarify)
+  apply simp
+ apply (blast intro: Ord_wfrank_separation, clarify)
 txt{*The reasoning in both cases is that we get @{term y} such that
    @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
    @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
@@ -488,4 +486,142 @@
      "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
 by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
 
+
+text{*absoluteness for wfrec-defined functions.*}
+
+(*first use is_recfun, then M_is_recfun*)
+
+lemma (in M_trancl) wfrec_relativize:
+  "[|wf(r); M(a); M(r);  
+     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+          pair(M,x,y,z) & 
+          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
+          y = H(x, restrict(g, r -`` {x}))); 
+     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
+   ==> wfrec(r,a,H) = z <-> 
+       (\<exists>f. M(f) & is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
+            z = H(a,restrict(f,r-``{a})))"
+apply (frule wf_trancl) 
+apply (simp add: wftrec_def wfrec_def, safe)
+ apply (frule wf_exists_is_recfun 
+              [of concl: "r^+" a "\<lambda>x f. H(x, restrict(f, r -`` {x}))"]) 
+      apply (simp_all add: trans_trancl function_restrictI trancl_subset_times)
+ apply (clarify, rule_tac x=f in exI) 
+ apply (simp_all add: the_recfun_eq trans_trancl trancl_subset_times)
+done
+
+
+text{*Assuming @{term r} is transitive simplifies the occurrences of @{text H}.
+      The premise @{term "relation(r)"} is necessary 
+      before we can replace @{term "r^+"} by @{term r}. *}
+theorem (in M_trancl) trans_wfrec_relativize:
+  "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
+     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
+   ==> wfrec(r,a,H) = z <-> (\<exists>f. M(f) & is_recfun(r,a,H,f) & z = H(a,f))" 
+by (simp cong: is_recfun_cong
+         add: wfrec_relativize trancl_eq_r
+               is_recfun_restrict_idem domain_restrict_idem)
+
+
+lemma (in M_trancl) trans_eq_pair_wfrec_iff:
+  "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
+     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
+   ==> y = <x, wfrec(r, x, H)> <-> 
+       (\<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
+apply safe  
+ apply (simp add: trans_wfrec_relativize [THEN iff_sym]) 
+txt{*converse direction*}
+apply (rule sym)
+apply (simp add: trans_wfrec_relativize, blast) 
+done
+
+
+subsection{*M is closed under well-founded recursion*}
+
+text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
+lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
+     "[|wf(r); M(r); 
+        strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
+        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
+      ==> M(a) --> M(wfrec(r,a,H))"
+apply (rule_tac a=a in wf_induct, assumption+)
+apply (subst wfrec, assumption, clarify)
+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: dest: pair_components_in_M ) 
+done
+
+text{*Eliminates one instance of replacement.*}
+lemma (in M_recursion) wfrec_replacement_iff:
+     "strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <->
+      strong_replacement(M, 
+           \<lambda>x y. \<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
+apply simp 
+apply (rule strong_replacement_cong, blast) 
+done
+
+text{*Useful version for transitive relations*}
+theorem (in M_recursion) trans_wfrec_closed:
+     "[|wf(r); trans(r); relation(r); M(r); M(a);
+        strong_replacement(M, 
+             \<lambda>x z. \<exists>y g. M(y) & M(g) &
+                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
+      ==> M(wfrec(r,a,H))"
+apply (frule wfrec_replacement_iff [THEN iffD1]) 
+apply (rule wfrec_closed_lemma, assumption+) 
+apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
+done
+
+section{*Absoluteness without assuming transitivity*}
+lemma (in M_trancl) eq_pair_wfrec_iff:
+  "[|wf(r);  M(r);  M(y); 
+     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+          pair(M,x,y,z) & 
+          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
+          y = H(x, restrict(g, r -`` {x}))); 
+     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
+   ==> y = <x, wfrec(r, x, H)> <-> 
+       (\<exists>f. M(f) & is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
+            y = <x, H(x,restrict(f,r-``{x}))>)"
+apply safe  
+ apply (simp add: wfrec_relativize [THEN iff_sym]) 
+txt{*converse direction*}
+apply (rule sym)
+apply (simp add: wfrec_relativize, blast) 
+done
+
+lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
+     "[|wf(r); M(r); 
+        strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
+        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
+      ==> M(a) --> M(wfrec(r,a,H))"
+apply (rule_tac a=a in wf_induct, assumption+)
+apply (subst wfrec, assumption, clarify)
+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: dest: pair_components_in_M ) 
+done
+
+text{*Full version not assuming transitivity, but maybe not very useful.*}
+theorem (in M_recursion) wfrec_closed:
+     "[|wf(r); M(r); M(a);
+     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+          pair(M,x,y,z) & 
+          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
+          y = H(x, restrict(g, r -`` {x}))); 
+        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
+      ==> M(wfrec(r,a,H))"
+apply (frule wfrec_replacement_iff [THEN iffD1]) 
+apply (rule wfrec_closed_lemma, assumption+) 
+apply (simp_all add: eq_pair_wfrec_iff) 
+done
+
 end
diff -r edbf32029d33 -r 5146ccaedf42 src/ZF/Constructible/WFrec.thy
--- a/src/ZF/Constructible/WFrec.thy	Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Fri Jun 28 11:25:46 2002 +0200
@@ -1,7 +1,7 @@
 theory WFrec = Wellorderings:
 
 
-(*FIXME: could move these to WF.thy*)
+(*Many of these might be useful in WF.thy*)
 
 lemma is_recfunI:
      "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
@@ -37,16 +37,40 @@
 apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
 done
 
-(*????GET RID OF [simp]*)
-lemma trans_Int_eq [simp]:
-      "[| trans(r); <y,x> \<in> r |] 
-       ==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
+lemma trans_Int_eq:
+      "[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
 by (blast intro: transD) 
 
-lemma trans_Int_eq2 [simp]:
-      "[| trans(r); <y,x> \<in> r |] 
-       ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
-by (blast intro: transD) 
+lemma is_recfun_restrict_idem:
+     "is_recfun(r,a,H,f) ==> restrict(f, r -`` {a}) = f"
+apply (drule is_recfun_type)
+apply (auto simp add: Pi_iff subset_Sigma_imp_relation restrict_idem)  
+done
+
+lemma is_recfun_cong_lemma:
+  "[| is_recfun(r,a,H,f); r = r'; a = a'; f = f'; 
+      !!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |] 
+             ==> H(x,g) = H'(x,g) |]
+   ==> is_recfun(r',a',H',f')"
+apply (simp add: is_recfun_def) 
+apply (erule trans) 
+apply (rule lam_cong) 
+apply (simp_all add: vimage_singleton_iff Int_lower2)  
+done
+
+text{*For @{text is_recfun} we need only pay attention to functions
+      whose domains are initial segments of @{term r}.*}
+lemma is_recfun_cong:
+  "[| r = r'; a = a'; f = f'; 
+      !!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |] 
+             ==> H(x,g) = H'(x,g) |]
+   ==> is_recfun(r,a,H,f) <-> is_recfun(r',a',H',f')"
+apply (rule iffI)
+txt{*Messy: fast and blast don't work for some reason*}
+apply (erule is_recfun_cong_lemma, auto) 
+apply (erule is_recfun_cong_lemma)
+apply (blast intro: sym)+
+done
 
 
 text{*Stated using @{term "trans(r)"} rather than
@@ -64,12 +88,11 @@
 apply (frule_tac f="f" in is_recfun_type) 
 apply (frule_tac f="g" in is_recfun_type) 
 apply (simp add: is_recfun_def)
-apply (erule_tac a=x in wellfounded_induct) 
-apply assumption+
+apply (erule_tac a=x in wellfounded_induct, assumption+)
 txt{*Separation to justify the induction*}
  apply (force intro: is_recfun_separation)
 txt{*Now the inductive argument itself*}
-apply (clarify ); 
+apply clarify 
 apply (erule ssubst)+
 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
 apply (rename_tac x1)
@@ -100,29 +123,28 @@
 apply (rule fun_extension)
 apply (erule is_recfun_type)+
 apply (blast intro!: is_recfun_equal dest: transM) 
-done
+done 
 
 text{*Tells us that is_recfun can (in principle) be relativized.*}
 lemma (in M_axioms) is_recfun_relativize:
-  "[| M(r); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] 
+  "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    ==> is_recfun(r,a,H,f) <->
-       (\<forall>z. z \<in> f <-> (\<exists>x y. M(x) & M(y) & z=<x,y> & <x,a> \<in> r & 
-                              y = H(x, restrict(f, r-``{x}))))";
-apply (simp add: is_recfun_def vimage_closed restrict_closed lam_def)
+       (\<forall>z[M]. z \<in> f <-> 
+        (\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))";
+apply (simp add: is_recfun_def lam_def)
 apply (safe intro!: equalityI) 
-  apply (drule equalityD1 [THEN subsetD], assumption) 
-  apply clarify 
-  apply (rule_tac x=x in exI) 
-  apply (blast dest: pair_components_in_M) 
- apply (blast elim!: equalityE dest: pair_components_in_M)
+   apply (drule equalityD1 [THEN subsetD], assumption) 
+   apply (blast dest: pair_components_in_M) 
+  apply (blast elim!: equalityE dest: pair_components_in_M)
+ apply (frule transM, assumption, rotate_tac -1) 
  apply simp  
  apply blast
- apply simp 
-apply (subgoal_tac "function(f)")  
- prefer 2
- apply (simp add: function_def) 
+apply (subgoal_tac "is_function(M,f)")
+ txt{*We use @{term "is_function"} rather than @{term "function"} because
+      the subgoal's easier to prove with relativized quantifiers!*}
+ prefer 2 apply (simp add: is_function_def) 
 apply (frule pair_components_in_M, assumption) 
-  apply (simp add: is_recfun_imp_function function_restrictI) 
+apply (simp add: is_recfun_imp_function function_restrictI) 
 done
 
 (* ideas for further weaking the H-closure premise:
@@ -142,10 +164,11 @@
 lemma (in M_axioms) is_recfun_restrict:
      "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; 
        M(r); M(f); 
-       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
+       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
        ==> is_recfun(r, y, H, restrict(f, r -`` {y}))"
 apply (frule pair_components_in_M, assumption, clarify) 
-apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff)
+apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff
+           trans_Int_eq)
 apply safe
   apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff]) 
   apply (frule_tac x=xa in pair_components_in_M, assumption)
@@ -157,7 +180,7 @@
  
 lemma (in M_axioms) restrict_Y_lemma:
    "[| wellfounded(M,r); trans(r); M(r);
-       \<forall>x g. M(x) \<and> M(g) & function(g) --> M(H(x,g));  M(Y);
+       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(Y);
        \<forall>b. M(b) -->
 	   b \<in> Y <->
 	   (\<exists>x\<in>r -`` {a1}.
@@ -167,6 +190,7 @@
        ==> restrict(Y, r -`` {x}) = f"
 apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y <-> <y,z>:f") 
  apply (simp (no_asm_simp) add: restrict_def) 
+ apply (thin_tac "rall(M,?P)")+  --{*essential for efficiency*}
  apply (thin_tac "All(?P)")+  --{*essential for efficiency*}
  apply (frule is_recfun_type [THEN fun_is_rel], blast)
 apply (frule pair_components_in_M, assumption, clarify) 
@@ -201,7 +225,7 @@
        wellfounded(M,r); trans(r); M(r); M(a1);
        strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
-       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g))|]   
+       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]   
       ==> \<exists>f. M(f) & is_recfun(r,a1,H,f)"
 apply (drule_tac A="r-``{a1}" in strong_replacementD)
   apply blast 
@@ -210,23 +234,16 @@
 txt{*Show that the constructed object satisfies @{text is_recfun}*} 
 apply clarify 
 apply (rule_tac x=Y in exI)  
-apply (simp (no_asm_simp) add: is_recfun_relativize) 
-(*Tried using is_recfun_iff2 here.  Much more simplification takes place
-  because an assumption can kick in.  Not sure how to relate the new 
-  proof state to the current one.*)
-apply safe
- txt{*Show that elements of @{term Y} are in the right relationship.*}
- apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec)
- apply (erule impE, blast intro: transM)
- txt{*We have an element of  @{term Y}, so we have x, y, z*} 
- apply (frule_tac y=z in transM, assumption, clarify)
- apply (simp add: restrict_Y_lemma [of r H]) 
+txt{*Unfold only the top-level occurrence of @{term is_recfun}*}
+apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1])
+txt{*The big iff-formula defininng @{term Y} is now redundant*}
+apply safe 
+ apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H]) 
 txt{*one more case*}
-apply (simp)
-apply (rule_tac x=x in bexI) 
- prefer 2 apply blast 
+apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff)
+apply (rename_tac x) 
+apply (rule_tac x=x in exI, simp) 
 apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI) 
-apply (simp)
 apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 
 apply (rule_tac x=f in exI) 
 apply (simp add: restrict_Y_lemma [of r H]) 
@@ -240,7 +257,7 @@
        strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
        M(r);  M(a);  
-       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
+       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]   
       ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
 apply (rule wellfounded_induct, assumption+, clarify)
 apply (rule exists_is_recfun_indstep, assumption+)
@@ -251,7 +268,7 @@
        strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
         M(r);  
-       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
+       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]   
       ==> M(a) --> (\<exists>f. M(f) & is_recfun(r,a,H,f))"
 apply (rule wf_induct, assumption+)
 apply (frule wf_imp_relativized)
@@ -261,24 +278,21 @@
 done
 
 constdefs
-   M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
-     "M_is_recfun(M,r,a,MH,f) == 
-      \<forall>z. M(z) -->
-          (z \<in> f <-> 
-           (\<exists>x y xa sx r_sx f_r_sx. 
-              M(x) & M(y) & M(xa) & M(sx) & M(r_sx) & M(f_r_sx) &
-	      pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
-              pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
-              xa \<in> r & MH(M, x, f_r_sx, y)))"
+ M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
+   "M_is_recfun(M,r,a,MH,f) == 
+     \<forall>z[M]. z \<in> f <-> 
+            (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
+	       pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
+               pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
+               xa \<in> r & MH(M, x, f_r_sx, y))"
 
 lemma (in M_axioms) is_recfun_iff_M:
-     "[| M(r); M(a); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g));
+     "[| M(r); M(a); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));
        \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(M,x,g,y) <-> y = H(x,g) |] ==>
        is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)"
-apply (simp add: vimage_closed restrict_closed M_is_recfun_def is_recfun_relativize)
-apply (rule all_cong, safe)
- apply (thin_tac "\<forall>x. ?P(x)")+
- apply (blast dest: transM)  (*or del: allE*)
+apply (simp add: M_is_recfun_def is_recfun_relativize)
+apply (rule rall_cong)
+apply (blast dest: transM)
 done
 
 lemma M_is_recfun_cong [cong]:
@@ -379,7 +393,7 @@
     "[| Ord(j);  M(i);  M(j) |]
      ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
 apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
-    apply (simp add: ); 
+    apply simp 
    apply (blast intro: oadd_strong_replacement') 
   apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
 done
@@ -491,7 +505,7 @@
     "[| Ord(j);  M(i);  M(j) |]
      ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
 apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
-    apply (simp add: );
+    apply simp
    apply (blast intro: omult_strong_replacement') 
   apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
 apply (blast intro: the_omult_eqns_closed)