development and tweaks

--- a/src/ZF/AC/AC15_WO6.thy	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/AC/AC15_WO6.thy	Mon Jun 24 11:59:21 2002 +0200
@@ -40,10 +40,9 @@
 lemma cons_times_nat_not_Finite:
      "0\<notin>A ==> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. ~Finite(B)"
 apply clarify 
-apply (drule subset_consI [THEN subset_imp_lepoll, THEN lepoll_Finite])
 apply (rule nat_not_Finite [THEN notE] )
 apply (subgoal_tac "x ~= 0")
-apply (blast intro: lepoll_Sigma [THEN lepoll_Finite], blast) 
+ apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
 done
 
 lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"

--- a/src/ZF/Constructible/Formula.thy	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Mon Jun 24 11:59:21 2002 +0200
@@ -22,54 +22,7 @@
 lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
 by (simp add: bool_of_o_def) 
 
-(*????????????????Cardinal.ML*)
-lemma Finite_cons_iff [iff]:  "Finite(cons(y,x)) <-> Finite(x)"
-by (blast intro: Finite_cons subset_Finite)
-
-lemma Finite_succ_iff [iff]:  "Finite(succ(x)) <-> Finite(x)"
-by (simp add: succ_def)
-
-declare Finite_0 [simp]
-
-lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
-by (erule Finite_induct, simp_all)
-
-lemma Finite_RepFun_lemma [rule_format]:
-     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] 
-      ==> \<forall>A. x = RepFun(A,f) --> Finite(A)" 
-apply (erule Finite_induct)
- apply clarify 
- apply (case_tac "A=0", simp)
- apply (blast del: allE, clarify) 
-apply (subgoal_tac "\<exists>z\<in>A. x = f(z)") 
- prefer 2 apply (blast del: allE elim: equalityE, clarify) 
-apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
- apply (blast intro: Diff_sing_Finite) 
-apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)") 
-apply (rule equalityI) 
- apply (blast intro: elim: equalityE) 
-apply (blast intro: elim: equalityCE) 
-done
-
-text{*I don't know why, but if the premise is expressed using meta-connectives
-then  the simplifier cannot prove it automatically in conditional rewriting.*}
-lemma Finite_RepFun_iff:
-     "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
-by (blast intro: Finite_RepFun Finite_RepFun_lemma [of _ f]) 
-
-lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
-apply (erule Finite_induct) 
-apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) 
-done
-
-lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
-apply (subgoal_tac "Finite({{x} . x \<in> A})")
- apply (simp add: Finite_RepFun_iff ) 
-apply (blast intro: subset_Finite) 
-done
-
-lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
-by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
+(*????????????????CardinalArith *)
 
 lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
 apply (erule nat_induct)
@@ -922,6 +875,10 @@
 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
 done
 
+
+lemma Ord_in_L: "Ord(i) ==> L(i)"
+by (blast intro: Ord_in_Lset L_I)
+
 text{*This is lrank(lrank(a)) = lrank(a) *}
 declare Ord_lrank [THEN lrank_of_Ord, simp]
 
@@ -963,13 +920,13 @@
 
 subsection{*For L to satisfy the ZF axioms*}
 
-lemma Union_in_L: "L(X) ==> L(Union(X))"
+theorem Union_in_L: "L(X) ==> L(Union(X))"
 apply (simp add: L_def, clarify) 
 apply (drule Ord_imp_greater_Limit) 
 apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
 done
 
-lemma doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
+theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
 apply (simp add: L_def, clarify) 
 apply (drule Ord2_imp_greater_Limit, assumption) 
 apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 
@@ -1000,7 +957,7 @@
 apply (auto intro: L_I iff: Lset_succ_lrank_iff) 
 done
 
-lemma LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
+theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
 by (blast intro: L_I dest: L_D LPow_in_Lset)
 
 end

--- a/src/ZF/Constructible/ROOT.ML	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/Constructible/ROOT.ML	Mon Jun 24 11:59:21 2002 +0200
@@ -1,4 +1,11 @@
+(*  Title:      ZF/Constructible/ROOT.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+Inner Models and Absoluteness
+*)
+
 use_thy "Reflection";
 use_thy "WFrec";
-use_thy "WF_extras";
 use_thy "L_axioms";

--- a/src/ZF/Constructible/Relative.thy	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Mon Jun 24 11:59:21 2002 +0200
@@ -18,15 +18,15 @@
     "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))"
 
+  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)"
+
   successor :: "[i=>o,i,i] => o"
     "successor(M,a,z) == \<exists>x. M(x) & 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))"
 
-  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)"
-
   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)"
 
@@ -72,6 +72,11 @@
     "is_range(M,r,z) == 
 	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"
 
+  is_field :: "[i=>o,i,i] => o"
+    "is_field(M,r,z) == 
+	\<exists>dr. M(dr) & is_domain(M,r,dr) & 
+            (\<exists>rr. M(rr) & is_range(M,r,rr) & union(M,dr,rr,z))"
+
   is_relation :: "[i=>o,i] => o"
     "is_relation(M,r) == 
         (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"
@@ -91,6 +96,13 @@
         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
         (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
 
+  composition :: "[i=>o,i,i,i] => o"
+    "composition(M,r,s,t) == 
+        \<forall>p. M(p) --> (p \<in> t <-> 
+                      (\<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) & 
+                           p = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))))"
+
+
   injection :: "[i=>o,i,i,i] => o"
     "injection(M,A,B,f) == 
 	typed_function(M,A,B,f) &
@@ -373,6 +385,7 @@
       and Union_ax:	    "Union_ax(M)"
       and power_ax:         "power_ax(M)"
       and replacement:      "replacement(M,P)"
+      and M_nat:            "M(nat)"   (*i.e. the axiom of infinity*)
   and Inter_separation:
      "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
   and cartprod_separation:
@@ -398,7 +411,7 @@
   and pred_separation:
      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
   and Memrel_separation:
-     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) \<and> x \<in> y)"
+     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) & x \<in> y)"
   and obase_separation:
      --{*part of the order type formalization*}
      "[| M(A); M(r) |] 
@@ -407,8 +420,8 @@
 	     order_isomorphism(M,par,r,x,mx,g))"
   and well_ord_iso_separation:
      "[| M(A); M(f); M(r) |] 
-      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) \<and> (\<exists>p. M(p) \<and> 
-		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
+      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) & (\<exists>p. M(p) & 
+		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   and obase_equals_separation:
      "[| M(A); M(r) |] 
       ==> separation
@@ -419,7 +432,7 @@
   and is_recfun_separation:
      --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
      "[| M(A); M(f); M(g); M(a); M(b) |] 
-     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
+     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & f`x \<noteq> g`x)"
   and omap_replacement:
      "[| M(A); M(r) |] 
       ==> strong_replacement(M,
@@ -440,6 +453,12 @@
                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
 by (blast intro: transM)
 
+text{*Simplifies proofs of equalities when there's an iff-equality
+      available for rewriting, universally quantified over M. *}
+lemma (in M_axioms) M_equalityI: 
+     "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
+by (blast intro!: equalityI dest: transM) 
+
 lemma (in M_axioms) empty_abs [simp]: 
      "M(z) ==> empty(M,z) <-> z=0"
 apply (simp add: empty_def)
@@ -516,15 +535,15 @@
 apply (blast intro!: equalityI dest: transM) 
 done
 
-lemma (in M_axioms) Union_closed [intro]:
+lemma (in M_axioms) Union_closed [intro,simp]:
      "M(A) ==> M(Union(A))"
 by (insert Union_ax, simp add: Union_ax_def) 
 
-lemma (in M_axioms) Un_closed [intro]:
+lemma (in M_axioms) Un_closed [intro,simp]:
      "[| M(A); M(B) |] ==> M(A Un B)"
 by (simp only: Un_eq_Union, blast) 
 
-lemma (in M_axioms) cons_closed [intro]:
+lemma (in M_axioms) cons_closed [intro,simp]:
      "[| M(a); M(A) |] ==> M(cons(a,A))"
 by (subst cons_eq [symmetric], blast) 
 
@@ -538,7 +557,7 @@
 apply (blast intro: transM) 
 done
 
-lemma (in M_axioms) separation_closed [intro]:
+lemma (in M_axioms) separation_closed [intro,simp]:
      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
 apply (insert separation, simp add: separation_def) 
 apply (drule spec [THEN mp], assumption, clarify) 
@@ -565,7 +584,7 @@
 
 
 (*The last premise expresses that P takes M to M*)
-lemma (in M_axioms) strong_replacement_closed [intro]:
+lemma (in M_axioms) strong_replacement_closed [intro,simp]:
      "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
        !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
 apply (simp add: strong_replacement_def) 
@@ -589,7 +608,7 @@
   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   even for f : M -> M.
 *)
-lemma (in M_axioms) RepFun_closed [intro]:
+lemma (in M_axioms) RepFun_closed [intro,simp]:
      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
       ==> M(RepFun(A,f))"
 apply (simp add: RepFun_def) 
@@ -669,20 +688,20 @@
 prefer 6 apply (rule refl) 
 prefer 4 apply assumption
 prefer 4 apply assumption
-apply (insert cartprod_separation [of A B], simp, blast+)
+apply (insert cartprod_separation [of A B], auto)
 done
 
 
 text{*All the lemmas above are necessary because Powerset is not absolute.
       I should have used Replacement instead!*}
-lemma (in M_axioms) cartprod_closed [intro]: 
+lemma (in M_axioms) cartprod_closed [intro,simp]: 
      "[| M(A); M(B) |] ==> M(A*B)"
 by (frule cartprod_closed_lemma, assumption, force)
 
-lemma (in M_axioms) image_closed [intro]: 
+lemma (in M_axioms) image_closed [intro,simp]: 
      "[| M(A); M(r) |] ==> M(r``A)"
 apply (simp add: image_iff_Collect)
-apply (insert image_separation [of A r], simp, blast) 
+apply (insert image_separation [of A r], simp) 
 done
 
 lemma (in M_axioms) vimage_abs [simp]: 
@@ -692,10 +711,10 @@
  apply (blast intro!: equalityI dest: transM, blast) 
 done
 
-lemma (in M_axioms) vimage_closed [intro]: 
+lemma (in M_axioms) vimage_closed [intro,simp]: 
      "[| M(A); M(r) |] ==> M(r-``A)"
 apply (simp add: vimage_iff_Collect)
-apply (insert vimage_separation [of A r], simp, blast) 
+apply (insert vimage_separation [of A r], simp) 
 done
 
 lemma (in M_axioms) domain_abs [simp]: 
@@ -704,10 +723,9 @@
 apply (blast intro!: equalityI dest: transM) 
 done
 
-lemma (in M_axioms) domain_closed [intro]: 
+lemma (in M_axioms) domain_closed [intro,simp]: 
      "M(r) ==> M(domain(r))"
 apply (simp add: domain_eq_vimage)
-apply (blast intro: vimage_closed) 
 done
 
 lemma (in M_axioms) range_abs [simp]: 
@@ -716,24 +734,31 @@
 apply (blast intro!: equalityI dest: transM)
 done
 
-lemma (in M_axioms) range_closed [intro]: 
+lemma (in M_axioms) range_closed [intro,simp]: 
      "M(r) ==> M(range(r))"
 apply (simp add: range_eq_image)
-apply (blast intro: image_closed) 
 done
 
+lemma (in M_axioms) field_abs [simp]: 
+     "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
+by (simp add: domain_closed range_closed is_field_def field_def)
+
+lemma (in M_axioms) field_closed [intro,simp]: 
+     "M(r) ==> M(field(r))"
+by (simp add: domain_closed range_closed Un_closed field_def) 
+
+
 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) \<and> (\<exists>y. M(y) \<and> p = \<langle>x,y\<rangle> \<and> z = \<langle>y,x\<rangle>)}"
+        \<exists>p\<in>r. \<exists>x. M(x) & (\<exists>y. M(y) & p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>)}"
 by (blast dest: transM)
 
-lemma (in M_axioms) converse_closed [intro]: 
+lemma (in M_axioms) converse_closed [intro,simp]: 
      "M(r) ==> M(converse(r))"
 apply (simp add: M_converse_iff)
-apply (insert converse_separation [of r], simp) 
-apply (blast intro: image_closed) 
+apply (insert converse_separation [of r], simp)
 done
 
 lemma (in M_axioms) relation_abs [simp]: 
@@ -749,10 +774,9 @@
   apply (blast dest: pair_components_in_M)+
 done
 
-lemma (in M_axioms) apply_closed [intro]: 
+lemma (in M_axioms) apply_closed [intro,simp]: 
      "[|M(f); M(a)|] ==> M(f`a)"
-apply (simp add: apply_def) 
-apply (blast intro: elim:); 
+apply (simp add: apply_def)
 done
 
 lemma (in M_axioms) apply_abs: 
@@ -808,19 +832,18 @@
      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
 by (simp add: restrict_def, blast dest: transM)
 
-lemma (in M_axioms) restrict_closed [intro]: 
+lemma (in M_axioms) restrict_closed [intro,simp]: 
      "[| M(A); M(r) |] ==> M(restrict(r,A))"
 apply (simp add: M_restrict_iff)
-apply (insert restrict_separation [of A], simp, blast) 
+apply (insert restrict_separation [of A], simp) 
 done
 
-
 lemma (in M_axioms) M_comp_iff:
      "[| M(r); M(s) |] 
       ==> r O s = 
           {xz \<in> domain(s) * range(r).  
-            \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> (\<exists>z. M(z) \<and> 
-                xz = \<langle>x,z\<rangle> \<and> \<langle>x,y\<rangle> \<in> s \<and> \<langle>y,z\<rangle> \<in> r))}"
+            \<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) & 
+                xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))}"
 apply (simp add: comp_def)
 apply (rule equalityI) 
  apply (clarify ); 
@@ -828,10 +851,24 @@
  apply  (blast dest:  transM)+
 done
 
-lemma (in M_axioms) comp_closed [intro]: 
+lemma (in M_axioms) comp_closed [intro,simp]: 
      "[| M(r); M(s) |] ==> M(r O s)"
 apply (simp add: M_comp_iff)
-apply (insert comp_separation [of r s], simp, blast) 
+apply (insert comp_separation [of r s], simp) 
+done
+
+lemma (in M_axioms) composition_abs [simp]: 
+     "[| M(r); M(s); M(t) |] 
+      ==> composition(M,r,s,t) <-> t = r O s"
+apply safe;
+ txt{*Proving @{term "composition(M, r, s, r O s)"}*}
+ prefer 2 
+ apply (simp add: composition_def comp_def)
+ apply (blast dest: transM) 
+txt{*Opposite implication*}
+apply (rule M_equalityI)
+  apply (simp add: composition_def comp_def)
+  apply (blast del: allE dest: transM)+
 done
 
 lemma (in M_axioms) nat_into_M [intro]:
@@ -852,16 +889,34 @@
 apply (blast intro!: equalityI dest: transM) 
 done
 
-lemma (in M_axioms) Inter_closed [intro]:
+lemma (in M_axioms) Inter_closed [intro,simp]:
      "M(A) ==> M(Inter(A))"
-by (insert Inter_separation, simp add: Inter_def, blast)
+by (insert Inter_separation, simp add: Inter_def)
 
-lemma (in M_axioms) Int_closed [intro]:
+lemma (in M_axioms) Int_closed [intro,simp]:
      "[| M(A); M(B) |] ==> M(A Int B)"
 apply (subgoal_tac "M({A,B})")
 apply (frule Inter_closed, force+); 
 done
 
+text{*M contains all finite functions*}
+lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
+     "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
+apply (induct_tac n, simp)
+apply (rule ballI)  
+apply (simp add: succ_def) 
+apply (frule fun_cons_restrict_eq)
+apply (erule ssubst) 
+apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
+ apply (simp add: cons_closed nat_into_M apply_closed) 
+apply (blast intro: apply_funtype transM restrict_type2) 
+done
+
+lemma (in M_axioms) finite_fun_closed [rule_format]: 
+     "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
+by (blast intro: finite_fun_closed_lemma) 
+
+
 subsection{*Absoluteness for ordinals*}
 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
 

--- a/src/ZF/Constructible/WFrec.thy	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Mon Jun 24 11:59:21 2002 +0200
@@ -1,7 +1,7 @@
 theory WFrec = Wellorderings:
 
 
-(*WF.thy??*)
+(*FIXME: could move these to WF.thy*)
 
 lemma is_recfunI:
      "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
@@ -27,6 +27,16 @@
  apply (fast intro: lam_type, simp) 
 done
 
+lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r"
+by (blast dest:  is_recfun_type fun_is_rel)
+
+lemma apply_recfun2:
+    "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
+apply (frule apply_recfun) 
+ apply (blast dest: is_recfun_type fun_is_rel) 
+apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
+done
+
 lemma trans_on_Int_eq [simp]:
       "[| trans[A](r); <y,x> \<in> r;  r \<subseteq> A*A |] 
        ==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
@@ -38,11 +48,6 @@
 by (blast intro: trans_onD) 
 
 
-constdefs
-   M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
-     "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
-
-
 text{*Stated using @{term "trans[A](r)"} rather than
       @{term "transitive_rel(M,A,r)"} because the latter rewrites to
       the former anyway, by @{text transitive_rel_abs}.
@@ -178,6 +183,16 @@
                  apply_recfun is_recfun_type [THEN apply_iff]) 
 done
 
+(*FIXME: use this lemma just below*)
+text{*For typical applications of Replacement for recursive definitions*}
+lemma (in M_axioms) univalent_is_recfun:
+     "[|wellfounded_on(M,A,r); trans[A](r); r \<subseteq> A*A; M(r); M(A)|]
+      ==> univalent (M, A, \<lambda>x p. \<exists>y. M(y) &
+                    (\<exists>f. M(f) & p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f)))"
+apply (simp add: univalent_def) 
+apply (blast dest: is_recfun_functional) 
+done
+
 text{*Proof of the inductive step for @{text exists_is_recfun}, since
       we must prove two versions.*}
 lemma (in M_axioms) exists_is_recfun_indstep:
@@ -240,23 +255,28 @@
                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
        M(A);  M(r);  r \<subseteq> A*A;  
        \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
-      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
+      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"        
 apply (rule wf_on_induct2, assumption+)
 apply (frule wf_on_imp_relativized)  
 apply (rule exists_is_recfun_indstep, assumption+)
 done
 
-(*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
-lemma (in M_axioms) M_is_the_recfun: 
-    "[|is_recfun(r,a,H,f);  
-       wellfounded_on(M,A,r); trans[A](r); 
-       M(A); M(f); M(a); r \<subseteq> A*A |]   
-     ==> M(M_the_recfun(M,r,a,H)) & 
-         is_recfun(r, a, H, M_the_recfun(M,r,a,H))"
-apply (unfold M_the_recfun_def)
-apply (rule ex1I [THEN theI2], fast)
-apply (blast intro: is_recfun_functional, blast) 
-done
+    (*????????????????NOT USED????????????????*)
+    constdefs
+      M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
+      "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
+    
+    (*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
+    lemma (in M_axioms) M_is_the_recfun: 
+      "[|is_recfun(r,a,H,f);  
+      wellfounded_on(M,A,r); trans[A](r); 
+      M(A); M(f); M(a); r \<subseteq> A*A |]   
+      ==> M(M_the_recfun(M,r,a,H)) & 
+      is_recfun(r, a, H, M_the_recfun(M,r,a,H))"    
+    apply (unfold M_the_recfun_def)
+    apply (rule ex1I [THEN theI2], fast)
+    apply (blast intro: is_recfun_functional, blast) 
+    done
 
 constdefs
    M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
@@ -432,7 +452,7 @@
 apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
 done
 
-lemma (in M_recursion) oadd_closed [intro]:
+lemma (in M_recursion) oadd_closed [intro,simp]:
     "[| M(i); M(j) |] ==> M(i++j)"
 apply (simp add: oadd_eq_if_raw_oadd, clarify) 
 apply (simp add: raw_oadd_eq_oadd) 
@@ -485,7 +505,6 @@
   apply (simp add: omult_eqns_0)
  apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
 apply (simp add: omult_eqns_Limit) 
-apply (simp add: Union_closed image_closed) 
 done
 
 lemma (in M_recursion) exists_omult:

--- a/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:21 2002 +0200
@@ -144,10 +144,10 @@
 apply (blast dest: transM) 
 done
 
-lemma (in M_axioms) pred_closed [intro]: 
+lemma (in M_axioms) pred_closed [intro,simp]: 
      "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
 apply (simp add: Order.pred_def) 
-apply (insert pred_separation [of r x], simp, blast) 
+apply (insert pred_separation [of r x], simp) 
 done
 
 lemma (in M_axioms) membership_abs [simp]: 
@@ -170,10 +170,10 @@
 apply (blast dest: transM)
 done 
 
-lemma (in M_axioms) Memrel_closed [intro]: 
+lemma (in M_axioms) Memrel_closed [intro,simp]: 
      "M(A) ==> M(Memrel(A))"
 apply (simp add: M_Memrel_iff) 
-apply (insert Memrel_separation, simp, blast)
+apply (insert Memrel_separation, simp)
 done