# HG changeset patch
# User paulson
# Date 1025772844 -7200
# Node ID 09276ee04361514901e1885ece0be87d45125552
# Parent  f504f5d284d304e10358396233f6860a11253437
tweaks

diff -r f504f5d284d3 -r 09276ee04361 src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 04 10:53:52 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 04 10:54:04 2002 +0200
@@ -138,10 +138,10 @@
 lemma (in M_datatypes) list_replacement1':
   "[|M(A); n \<in> nat|]
    ==> strong_replacement
-	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x,z\<rangle> &
-               is_recfun (Memrel(succ(n)), x,
+	  (M, \<lambda>x y. \<exists>z[M]. y = \<langle>x,z\<rangle> &
+               (\<exists>g[M]. is_recfun (Memrel(succ(n)), x,
 		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
- 	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
+ 	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x)))"
 by (insert list_replacement1, simp add: nat_into_M) 
 
 
@@ -149,4 +149,5 @@
      "M(A) ==> M(list(A))"
 by (simp add: list_eq_Union list_replacement1' list_replacement2')
 
+
 end
diff -r f504f5d284d3 -r 09276ee04361 src/ZF/Constructible/WF_absolute.thy
--- a/src/ZF/Constructible/WF_absolute.thy	Thu Jul 04 10:53:52 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Thu Jul 04 10:54:04 2002 +0200
@@ -335,20 +335,21 @@
  apply (blast intro: Ord_wfrank_range)
 txt{*We still must show that the range is a transitive set.*}
 apply (simp add: Transset_def, clarify, simp)
-apply (rename_tac x f i u)
+apply (rename_tac x i f u)
 apply (frule is_recfun_imp_in_r, assumption)
 apply (subgoal_tac "M(u) & M(i) & M(x)")
  prefer 2 apply (blast dest: transM, clarify)
 apply (rule_tac a=u in rangeI)
-apply (rule ReplaceI)
-  apply (rule_tac x=i in rexI, simp)
-   apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
-    apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
-   apply (simp, simp, blast) 
+apply (rule_tac x=u in ReplaceI)
+  apply simp 
+  apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
+   apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
+  apply simp 
+apply blast 
 txt{*Unicity requirement of Replacement*}
 apply clarify
 apply (frule apply_recfun2, assumption)
-apply (simp add: trans_trancl is_recfun_cut)+
+apply (simp add: trans_trancl is_recfun_cut)
 done
 
 lemma (in M_wfrank) function_wellfoundedrank:
@@ -368,10 +369,9 @@
 apply (rule equalityI, auto)
 apply (frule transM, assumption)
 apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
-apply (rule domainI)
-apply (rule ReplaceI)
-  apply (rule_tac x="range(f)" in rexI)
-  apply simp
+apply (rule_tac b="range(f)" in domainI)
+apply (rule_tac x=x in ReplaceI)
+  apply simp 
   apply (rule_tac x=f in rexI, blast, simp_all)
 txt{*Uniqueness (for Replacement): repeated above!*}
 apply clarify
@@ -502,8 +502,8 @@
       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[M]. \<exists>g[M].
-                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+     strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
+                pair(M,x,y,z) & (\<exists>g[M]. 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]. is_recfun(r,a,H,f) & z = H(a,f))" 
 by (simp cong: is_recfun_cong
@@ -513,13 +513,13 @@
 
 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[M]. \<exists>g[M].
-                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+     strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
+                pair(M,x,y,z) & (\<exists>g[M]. 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]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
-apply safe  
- apply (simp add: trans_wfrec_relativize [THEN iff_sym]) 
+apply safe 
+ apply (simp add: trans_wfrec_relativize [THEN iff_sym, of concl: _ x]) 
 txt{*converse direction*}
 apply (rule sym)
 apply (simp add: trans_wfrec_relativize, blast) 
@@ -577,7 +577,7 @@
        (\<exists>f[M]. 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]) 
+ apply (simp add: wfrec_relativize [THEN iff_sym, of concl: _ x]) 
 txt{*converse direction*}
 apply (rule sym)
 apply (simp add: wfrec_relativize, blast) 
diff -r f504f5d284d3 -r 09276ee04361 src/ZF/Constructible/WFrec.thy
--- a/src/ZF/Constructible/WFrec.thy	Thu Jul 04 10:53:52 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Thu Jul 04 10:54:04 2002 +0200
@@ -187,10 +187,10 @@
  apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
 			   apply_recfun is_recfun_cut) 
 txt{*Opposite inclusion: something in f, show in Y*}
-apply (frule_tac y="<y,z>" in transM, assumption, simp) 
-apply (rule_tac x=y in bexI)
-prefer 2 apply (blast dest: transD)
-apply (rule_tac x=z in rexI) 
+apply (frule_tac y="<y,z>" in transM, assumption)  
+apply (simp add: vimage_singleton_iff) 
+apply (rule conjI) 
+ apply (blast dest: transD) 
 apply (rule_tac x="restrict(f, r -`` {y})" in rexI) 
 apply (simp_all add: is_recfun_restrict
                      apply_recfun is_recfun_type [THEN apply_iff]) 
@@ -200,7 +200,7 @@
 lemma (in M_axioms) univalent_is_recfun:
      "[|wellfounded(M,r); trans(r); M(r)|]
       ==> univalent (M, A, \<lambda>x p. 
-              \<exists>y[M]. \<exists>f[M]. p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f))"
+              \<exists>y[M]. p = \<langle>x,y\<rangle> & (\<exists>f[M]. is_recfun(r,x,H,f) & y = H(x,f)))"
 apply (simp add: univalent_def) 
 apply (blast dest: is_recfun_functional) 
 done
@@ -228,13 +228,10 @@
  apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H]) 
 txt{*one more case*}
 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 rexI) 
 apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 
 apply (rename_tac f) 
 apply (rule_tac x=f in rexI) 
-apply (simp add: restrict_Y_lemma [of r H], simp_all)
+apply (simp_all add: restrict_Y_lemma [of r H])
 done
 
 text{*Relativized version, when we have the (currently weaker) premise
@@ -337,14 +334,16 @@
   assumes oadd_strong_replacement:
    "[| M(i); M(j) |] ==>
     strong_replacement(M, 
-         \<lambda>x z. \<exists>y[M]. \<exists>f[M]. \<exists>fx[M]. pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) & 
-		                      image(M,f,x,fx) & y = i Un fx)" 
+         \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & 
+                  (\<exists>f[M]. \<exists>fx[M]. is_oadd_fun(M,i,j,x,f) & 
+		           image(M,f,x,fx) & y = i Un fx))"
+
  and omult_strong_replacement':
    "[| M(i); M(j) |] ==>
-    strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. 
-	     z = <x,y> &
-	     is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
-	     y = (THE z. omult_eqns(i, x, g, z)))" 
+    strong_replacement(M, 
+         \<lambda>x z. \<exists>y[M]. z = <x,y> &
+	     (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
+	     y = (THE z. omult_eqns(i, x, g, z))))" 
 
 
 
@@ -365,10 +364,10 @@
 
 lemma (in M_ord_arith) oadd_strong_replacement':
     "[| M(i); M(j) |] ==>
-     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
-		  z = <x,y> &
-		  is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
-		  y = i Un g``x)" 
+     strong_replacement(M, 
+            \<lambda>x z. \<exists>y[M]. z = <x,y> &
+		  (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
+		  y = i Un g``x))" 
 apply (insert oadd_strong_replacement [of i j]) 
 apply (simp add: Memrel_closed Un_closed image_closed is_oadd_fun_def
                  is_recfun_iff_M)  
diff -r f504f5d284d3 -r 09276ee04361 src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 10:53:52 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 10:54:04 2002 +0200
@@ -346,23 +346,23 @@
   obase :: "[i=>o,i,i,i] => o"
        --{*the domain of @{text om}, eventually shown to equal @{text A}*}
    "obase(M,A,r,z) == 
-	\<forall>a. M(a) --> 
-         (a \<in> z <-> 
+	\<forall>a[M]. 
+         a \<in> z <-> 
           (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
                                membership(M,x,mx) & pred_set(M,A,a,r,par) &  
-                               order_isomorphism(M,par,r,x,mx,g))))"
+                               order_isomorphism(M,par,r,x,mx,g)))"
 
 
   omap :: "[i=>o,i,i,i] => o"  
     --{*the function that maps wosets to order types*}
    "omap(M,A,r,f) == 
-	\<forall>z. M(z) --> 
-         (z \<in> f <-> 
+	\<forall>z[M].
+         z \<in> f <-> 
           (\<exists>a\<in>A. M(a) & 
            (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
                          pair(M,a,x,z) & membership(M,x,mx) & 
                          pred_set(M,A,a,r,par) &  
-                         order_isomorphism(M,par,r,x,mx,g))))"
+                         order_isomorphism(M,par,r,x,mx,g)))"
 
 
   otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
@@ -392,8 +392,10 @@
                    g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
 apply (rotate_tac 1) 
 apply (simp add: omap_def Memrel_closed pred_closed) 
-apply (rule iffI) 
-apply (drule_tac x=z in spec, blast dest: transM)+ 
+apply (rule iffI)
+ apply (drule_tac [2] x=z in rspec)
+ apply (drule_tac x=z in rspec)
+ apply (blast dest: transM)+
 done
 
 lemma (in M_axioms) omap_unique:
@@ -576,35 +578,37 @@
        M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
 apply (frule omap_ord_iso, assumption+) 
 apply (frule obase_equals, assumption+, blast) 
-done
+done 
 
 lemma (in M_axioms) obase_exists:
-     "[| M(A); M(r) |] ==> \<exists>z. M(z) & obase(M,A,r,z)"
+     "[| M(A); M(r) |] ==> \<exists>z[M]. obase(M,A,r,z)"
 apply (simp add: obase_def) 
 apply (insert obase_separation [of A r])
 apply (simp add: separation_def)  
 done
 
 lemma (in M_axioms) omap_exists:
-     "[| M(A); M(r) |] ==> \<exists>z. M(z) & omap(M,A,r,z)"
+     "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)"
 apply (insert obase_exists [of A r]) 
 apply (simp add: omap_def) 
 apply (insert omap_replacement [of A r])
 apply (simp add: strong_replacement_def, clarify) 
-apply (drule_tac x=z in spec, clarify) 
+apply (drule_tac x=x in spec, clarify) 
 apply (simp add: Memrel_closed pred_closed obase_iff)
 apply (erule impE) 
  apply (clarsimp simp add: univalent_def)
  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  
-apply (rule_tac x=Y in exI) 
-apply (simp add: Memrel_closed pred_closed obase_iff, blast)   
+apply (rule_tac x=Y in rexI) 
+apply (simp add: Memrel_closed pred_closed obase_iff, blast, assumption)
 done
 
+declare rall_simps [simp] rex_simps [simp]
+
 lemma (in M_axioms) otype_exists:
      "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"
-apply (insert omap_exists [of A r]) 
-apply (simp add: otype_def, clarify) 
-apply (rule_tac x="range(z)" in exI) 
+apply (insert omap_exists [of A r])  
+apply (simp add: otype_def, safe)
+apply (rule_tac x="range(x)" in exI) 
 apply blast 
 done