more use of relativized quantifiers
authorpaulson
Mon Jul 01 18:16:18 2002 +0200 (2002-07-01)
changeset 13268240509babf00
parent 13267 502f69ea6627
child 13269 3ba9be497c33
more use of relativized quantifiers
list_closed
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
     1.3 @@ -0,0 +1,173 @@
     1.4 +theory Datatype_absolute = WF_absolute:
     1.5 +
     1.6 +(*Epsilon.thy*)
     1.7 +lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
     1.8 +apply (insert arg_subset_eclose [of "{i}"], simp) 
     1.9 +apply (frule eclose_subset, blast) 
    1.10 +done
    1.11 +
    1.12 +lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
    1.13 +apply (rule equalityI)
    1.14 +apply (erule eclose_sing_Ord)  
    1.15 +apply (rule succ_subset_eclose_sing) 
    1.16 +done
    1.17 +
    1.18 +(*Ordinal.thy*)
    1.19 +lemma relation_Memrel: "relation(Memrel(A))"
    1.20 +by (simp add: relation_def Memrel_def, blast)
    1.21 +
    1.22 +lemma (in M_axioms) nat_case_closed:
    1.23 +  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
    1.24 +apply (case_tac "k=0", simp) 
    1.25 +apply (case_tac "\<exists>m. k = succ(m)")
    1.26 +apply force 
    1.27 +apply (simp add: nat_case_def) 
    1.28 +done
    1.29 +
    1.30 +
    1.31 +subsection{*The lfp of a continuous function can be expressed as a union*}
    1.32 +
    1.33 +constdefs
    1.34 +  contin :: "[i=>i]=>o"
    1.35 +   "contin(h) == (\<forall>A. A\<noteq>0 --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"
    1.36 +
    1.37 +lemma bnd_mono_iterates_subset: "[|bnd_mono(D, h); n \<in> nat|] ==> h^n (0) <= D"
    1.38 +apply (induct_tac n) 
    1.39 + apply (simp_all add: bnd_mono_def, blast) 
    1.40 +done
    1.41 +
    1.42 +
    1.43 +lemma contin_iterates_eq: 
    1.44 +    "contin(h) \<Longrightarrow> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
    1.45 +apply (simp add: contin_def) 
    1.46 +apply (rule trans) 
    1.47 +apply (rule equalityI) 
    1.48 + apply (simp_all add: UN_subset_iff) 
    1.49 + apply safe
    1.50 + apply (erule_tac [2] natE) 
    1.51 +  apply (rule_tac a="succ(x)" in UN_I) 
    1.52 +   apply simp_all 
    1.53 +apply blast 
    1.54 +done
    1.55 +
    1.56 +lemma lfp_subset_Union:
    1.57 +     "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) <= (\<Union>n\<in>nat. h^n(0))"
    1.58 +apply (rule lfp_lowerbound) 
    1.59 + apply (simp add: contin_iterates_eq) 
    1.60 +apply (simp add: contin_def bnd_mono_iterates_subset UN_subset_iff) 
    1.61 +done
    1.62 +
    1.63 +lemma Union_subset_lfp:
    1.64 +     "bnd_mono(D,h) ==> (\<Union>n\<in>nat. h^n(0)) <= lfp(D,h)"
    1.65 +apply (simp add: UN_subset_iff)
    1.66 +apply (rule ballI)  
    1.67 +apply (induct_tac x, simp_all) 
    1.68 +apply (rule subset_trans [of _ "h(lfp(D,h))"])
    1.69 + apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] )  
    1.70 +apply (erule lfp_lemma2) 
    1.71 +done
    1.72 +
    1.73 +lemma lfp_eq_Union:
    1.74 +     "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) = (\<Union>n\<in>nat. h^n(0))"
    1.75 +by (blast del: subsetI 
    1.76 +          intro: lfp_subset_Union Union_subset_lfp)
    1.77 +
    1.78 +
    1.79 +subsection {*lists without univ*}
    1.80 +
    1.81 +lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ 
    1.82 +                        Pair_in_univ zero_in_univ
    1.83 +
    1.84 +lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
    1.85 +apply (rule bnd_monoI)
    1.86 + apply (intro subset_refl zero_subset_univ A_subset_univ 
    1.87 +	      sum_subset_univ Sigma_subset_univ) 
    1.88 + apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI)
    1.89 +done
    1.90 +
    1.91 +lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
    1.92 +by (simp add: contin_def, blast)
    1.93 +
    1.94 +text{*Re-expresses lists using sum and product*}
    1.95 +lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
    1.96 +apply (simp add: list_def) 
    1.97 +apply (rule equalityI) 
    1.98 + apply (rule lfp_lowerbound) 
    1.99 +  prefer 2 apply (rule lfp_subset)
   1.100 + apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
   1.101 + apply (simp add: Nil_def Cons_def)
   1.102 + apply blast 
   1.103 +txt{*Opposite inclusion*}
   1.104 +apply (rule lfp_lowerbound) 
   1.105 + prefer 2 apply (rule lfp_subset) 
   1.106 +apply (clarify, subst lfp_unfold [OF list.bnd_mono]) 
   1.107 +apply (simp add: Nil_def Cons_def)
   1.108 +apply (blast intro: datatype_univs
   1.109 +             dest: lfp_subset [THEN subsetD])
   1.110 +done
   1.111 +
   1.112 +text{*Re-expresses lists using "iterates", no univ.*}
   1.113 +lemma list_eq_Union:
   1.114 +     "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
   1.115 +by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
   1.116 +
   1.117 +
   1.118 +subsection {*Absoluteness for "Iterates"*}
   1.119 +
   1.120 +lemma (in M_trancl) iterates_relativize:
   1.121 +  "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
   1.122 +     strong_replacement(M, 
   1.123 +       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
   1.124 +              is_recfun (Memrel(succ(n)), x,
   1.125 +                         \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
   1.126 +              y = nat_case(v, \<lambda>m. F(g`m), x))|] 
   1.127 +   ==> iterates(F,n,v) = z <-> 
   1.128 +       (\<exists>g[M]. is_recfun(Memrel(succ(n)), n, 
   1.129 +                             \<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n), g) &
   1.130 +            z = nat_case(v, \<lambda>m. F(g`m), n))"
   1.131 +by (simp add: iterates_nat_def recursor_def transrec_def 
   1.132 +              eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M
   1.133 +              wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
   1.134 +
   1.135 +
   1.136 +lemma (in M_wfrank) iterates_closed [intro,simp]:
   1.137 +  "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
   1.138 +     strong_replacement(M, 
   1.139 +       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
   1.140 +              is_recfun (Memrel(succ(n)), x,
   1.141 +                         \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
   1.142 +              y = nat_case(v, \<lambda>m. F(g`m), x))|] 
   1.143 +   ==> M(iterates(F,n,v))"
   1.144 +by (simp add: iterates_nat_def recursor_def transrec_def 
   1.145 +              eclose_sing_Ord_eq trans_wfrec_closed nat_into_M
   1.146 +              wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
   1.147 +
   1.148 +
   1.149 +locale M_datatypes = M_wfrank +
   1.150 +(*THEY NEED RELATIVIZATION*)
   1.151 +  assumes list_replacement1: 
   1.152 +	   "[|M(A); n \<in> nat|] ==> 
   1.153 +	    strong_replacement(M, 
   1.154 +	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
   1.155 +		     is_recfun (Memrel(succ(n)), x,
   1.156 +				\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
   1.157 +		     y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
   1.158 +      and list_replacement2': 
   1.159 +           "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
   1.160 +
   1.161 +
   1.162 +lemma (in M_datatypes) list_replacement1':
   1.163 +  "[|M(A); n \<in> nat|]
   1.164 +   ==> strong_replacement
   1.165 +	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> &
   1.166 +               is_recfun (Memrel(succ(n)), x,
   1.167 +		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) &
   1.168 + 	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
   1.169 +by (insert list_replacement1, simp) 
   1.170 +
   1.171 +
   1.172 +lemma (in M_datatypes) list_closed [intro,simp]:
   1.173 +     "M(A) ==> M(list(A))"
   1.174 +by (simp add: list_eq_Union list_replacement1' list_replacement2')
   1.175 +
   1.176 +end
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:10:53 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:16:18 2002 +0200
     2.3 @@ -62,8 +62,7 @@
     2.4  
     2.5  lemma replacement: "replacement(L,P)"
     2.6  apply (simp add: replacement_def, clarify)
     2.7 -apply (frule LReplace_in_L, assumption+)
     2.8 -apply clarify 
     2.9 +apply (frule LReplace_in_L, assumption+, clarify) 
    2.10  apply (rule_tac x=Y in exI)   
    2.11  apply (simp add: Replace_iff univalent_def, blast) 
    2.12  done
     3.1 --- a/src/ZF/Constructible/Normal.thy	Mon Jul 01 18:10:53 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Normal.thy	Mon Jul 01 18:16:18 2002 +0200
     3.3 @@ -316,8 +316,7 @@
     3.4     --"this lemma is @{thm increasing_LimitI [no_vars]}"
     3.5   apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
     3.6                       Ord_UN Ord_iterates lt_imp_0_lt
     3.7 -                     iterates_Normal_increasing)
     3.8 -apply clarify
     3.9 +                     iterates_Normal_increasing, clarify)
    3.10  apply (rule bexI) 
    3.11   apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
    3.12  apply (rule UN_I, erule nat_succI) 
     4.1 --- a/src/ZF/Constructible/ROOT.ML	Mon Jul 01 18:10:53 2002 +0200
     4.2 +++ b/src/ZF/Constructible/ROOT.ML	Mon Jul 01 18:16:18 2002 +0200
     4.3 @@ -9,3 +9,4 @@
     4.4  use_thy "Reflection";
     4.5  use_thy "WF_absolute";
     4.6  use_thy "L_axioms";
     4.7 +use_thy "Datatype_absolute";
     5.1 --- a/src/ZF/Constructible/Reflection.thy	Mon Jul 01 18:10:53 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Reflection.thy	Mon Jul 01 18:16:18 2002 +0200
     5.3 @@ -55,7 +55,7 @@
     5.4  
     5.5  theorem (in reflection) Not_reflection [intro]:
     5.6       "Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
     5.7 -by (simp add: Reflects_def); 
     5.8 +by (simp add: Reflects_def) 
     5.9  
    5.10  theorem (in reflection) And_reflection [intro]:
    5.11       "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
     6.1 --- a/src/ZF/Constructible/Relative.thy	Mon Jul 01 18:10:53 2002 +0200
     6.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Jul 01 18:16:18 2002 +0200
     6.3 @@ -2,6 +2,11 @@
     6.4  
     6.5  theory Relative = Main:
     6.6  
     6.7 +(*func.thy*)
     6.8 +lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
     6.9 +by (simp add: succ_def mem_not_refl cons_fun_eq)
    6.10 +
    6.11 +
    6.12  subsection{* Relativized versions of standard set-theoretic concepts *}
    6.13  
    6.14  constdefs
    6.15 @@ -96,6 +101,10 @@
    6.16          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
    6.17          (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
    6.18  
    6.19 +  is_funspace :: "[i=>o,i,i,i] => o"
    6.20 +    "is_funspace(M,A,B,F) == 
    6.21 +        \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
    6.22 +
    6.23    composition :: "[i=>o,i,i,i] => o"
    6.24      "composition(M,r,s,t) == 
    6.25          \<forall>p. M(p) --> (p \<in> t <-> 
    6.26 @@ -385,29 +394,28 @@
    6.27        and Union_ax:	    "Union_ax(M)"
    6.28        and power_ax:         "power_ax(M)"
    6.29        and replacement:      "replacement(M,P)"
    6.30 -      and M_nat:            "M(nat)"   (*i.e. the axiom of infinity*)
    6.31 +      and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
    6.32    and Inter_separation:
    6.33 -     "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
    6.34 +     "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
    6.35    and cartprod_separation:
    6.36       "[| M(A); M(B) |] 
    6.37        ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"
    6.38    and image_separation:
    6.39       "[| M(A); M(r) |] 
    6.40 -      ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & (\<exists>x\<in>A. M(x) & pair(M,x,y,p)))"
    6.41 +      ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
    6.42    and vimage_separation:
    6.43       "[| M(A); M(r) |] 
    6.44 -      ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
    6.45 +      ==> separation(M, \<lambda>x. \<exists>p[M]. p\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,p)))"
    6.46    and converse_separation:
    6.47       "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. 
    6.48                      M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
    6.49    and restrict_separation:
    6.50 -     "M(A) 
    6.51 -      ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
    6.52 +     "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
    6.53    and comp_separation:
    6.54       "[| M(r); M(s) |]
    6.55 -      ==> separation(M, \<lambda>xz. \<exists>x y z. M(x) & M(y) & M(z) &
    6.56 -			   (\<exists>xy\<in>s. \<exists>yz\<in>r. M(xy) & M(yz) & 
    6.57 -		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
    6.58 +      ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
    6.59 +		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
    6.60 +                  xy\<in>s & yz\<in>r)"
    6.61    and pred_separation:
    6.62       "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
    6.63    and Memrel_separation:
    6.64 @@ -418,6 +426,10 @@
    6.65        ==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & 
    6.66  	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    6.67  	     order_isomorphism(M,par,r,x,mx,g))"
    6.68 +  and funspace_succ_replacement:
    6.69 +     "M(n) ==> 
    6.70 +      strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. 
    6.71 +                pair(M,f,b,p) & pair(M,n,b,nb) & z = {cons(nb,f)})"
    6.72    and well_ord_iso_separation:
    6.73       "[| M(A); M(f); M(r) |] 
    6.74        ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) & (\<exists>p. M(p) & 
    6.75 @@ -440,15 +452,23 @@
    6.76  	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
    6.77  	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
    6.78  
    6.79 -lemma (in M_axioms) Ball_abs [simp]: 
    6.80 +lemma (in M_axioms) ball_abs [simp]: 
    6.81       "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
    6.82  by (blast intro: transM) 
    6.83  
    6.84 -lemma (in M_axioms) Bex_abs [simp]: 
    6.85 +lemma (in M_axioms) rall_abs [simp]: 
    6.86 +     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
    6.87 +by (blast intro: transM) 
    6.88 +
    6.89 +lemma (in M_axioms) bex_abs [simp]: 
    6.90       "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
    6.91  by (blast intro: transM) 
    6.92  
    6.93 -lemma (in M_axioms) Ball_iff_equiv: 
    6.94 +lemma (in M_axioms) rex_abs [simp]: 
    6.95 +     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
    6.96 +by (blast intro: transM) 
    6.97 +
    6.98 +lemma (in M_axioms) ball_iff_equiv: 
    6.99       "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <-> 
   6.100                 (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   6.101  by (blast intro: transM)
   6.102 @@ -570,11 +590,9 @@
   6.103      "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
   6.104       ==> strong_replacement(M,P)"
   6.105  apply (simp add: strong_replacement_def, clarify) 
   6.106 -apply (frule replacementD [OF replacement], assumption)
   6.107 -apply clarify 
   6.108 +apply (frule replacementD [OF replacement], assumption, clarify) 
   6.109  apply (drule_tac x=A in spec, clarify)  
   6.110 -apply (drule_tac z=Y in separationD, assumption)
   6.111 -apply clarify 
   6.112 +apply (drule_tac z=Y in separationD, assumption, clarify) 
   6.113  apply (blast dest: transM) 
   6.114  done
   6.115  
   6.116 @@ -692,6 +710,10 @@
   6.117       "[| M(A); M(B) |] ==> M(A*B)"
   6.118  by (frule cartprod_closed_lemma, assumption, force)
   6.119  
   6.120 +lemma (in M_axioms) sum_closed [intro,simp]: 
   6.121 +     "[| M(A); M(B) |] ==> M(A+B)"
   6.122 +by (simp add: sum_def)
   6.123 +
   6.124  lemma (in M_axioms) image_closed [intro,simp]: 
   6.125       "[| M(A); M(r) |] ==> M(r``A)"
   6.126  apply (simp add: image_iff_Collect)
   6.127 @@ -758,9 +780,9 @@
   6.128       "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   6.129  apply (simp add: is_converse_def)
   6.130  apply (rule iffI)
   6.131 - prefer 2 apply (blast intro: elim:); 
   6.132 + prefer 2 apply blast 
   6.133  apply (rule M_equalityI)
   6.134 -  apply (simp add: )
   6.135 +  apply simp
   6.136    apply (blast dest: transM)+
   6.137  done
   6.138  
   6.139 @@ -819,20 +841,20 @@
   6.140       "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
   6.141        ==> function(z)"
   6.142  apply (rotate_tac 1)
   6.143 -apply (simp add: restriction_def Ball_iff_equiv) 
   6.144 +apply (simp add: restriction_def ball_iff_equiv) 
   6.145  apply (unfold function_def, blast) 
   6.146  done
   6.147  
   6.148  lemma (in M_axioms) restriction_abs [simp]: 
   6.149       "[| M(f); M(A); M(z) |] 
   6.150        ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
   6.151 -apply (simp add: Ball_iff_equiv restriction_def restrict_def)
   6.152 +apply (simp add: ball_iff_equiv restriction_def restrict_def)
   6.153  apply (blast intro!: equalityI dest: transM) 
   6.154  done
   6.155  
   6.156  
   6.157  lemma (in M_axioms) M_restrict_iff:
   6.158 -     "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
   6.159 +     "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
   6.160  by (simp add: restrict_def, blast dest: transM)
   6.161  
   6.162  lemma (in M_axioms) restrict_closed [intro,simp]: 
   6.163 @@ -845,8 +867,7 @@
   6.164       "[| M(r); M(s) |] 
   6.165        ==> r O s = 
   6.166            {xz \<in> domain(s) * range(r).  
   6.167 -            \<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) & 
   6.168 -                xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))}"
   6.169 +            \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r}"
   6.170  apply (simp add: comp_def)
   6.171  apply (rule equalityI) 
   6.172   apply clarify 
   6.173 @@ -902,6 +923,8 @@
   6.174  apply (frule Inter_closed, force+) 
   6.175  done
   6.176  
   6.177 +subsection{*Functions and function space*}
   6.178 +
   6.179  text{*M contains all finite functions*}
   6.180  lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
   6.181       "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
   6.182 @@ -919,6 +942,39 @@
   6.183       "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
   6.184  by (blast intro: finite_fun_closed_lemma) 
   6.185  
   6.186 +text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
   6.187 +all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
   6.188 +lemma (in M_axioms) is_funspace_abs [simp]:
   6.189 +     "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
   6.190 +apply (simp add: is_funspace_def)
   6.191 +apply (rule iffI)
   6.192 + prefer 2 apply blast 
   6.193 +apply (rule M_equalityI)
   6.194 +  apply simp_all
   6.195 +done
   6.196 +
   6.197 +lemma (in M_axioms) succ_fun_eq2:
   6.198 +     "[|M(B); M(n->B)|] ==>
   6.199 +      succ(n) -> B = 
   6.200 +      \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
   6.201 +apply (simp add: succ_fun_eq)
   6.202 +apply (blast dest: transM)  
   6.203 +done
   6.204 +
   6.205 +lemma (in M_axioms) funspace_succ:
   6.206 +     "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
   6.207 +apply (insert funspace_succ_replacement [of n]) 
   6.208 +apply (force simp add: succ_fun_eq2 univalent_def) 
   6.209 +done
   6.210 +
   6.211 +text{*@{term M} contains all finite function spaces.  Needed to prove the
   6.212 +absoluteness of transitive closure.*}
   6.213 +lemma (in M_axioms) finite_funspace_closed [intro,simp]:
   6.214 +     "[|n\<in>nat; M(B)|] ==> M(n->B)"
   6.215 +apply (induct_tac n, simp)
   6.216 +apply (simp add: funspace_succ nat_into_M) 
   6.217 +done
   6.218 +
   6.219  
   6.220  subsection{*Absoluteness for ordinals*}
   6.221  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
     7.1 --- a/src/ZF/Constructible/WF_absolute.thy	Mon Jul 01 18:10:53 2002 +0200
     7.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
     7.3 @@ -1,5 +1,20 @@
     7.4  theory WF_absolute = WFrec:
     7.5  
     7.6 +(*????move to Wellorderings.thy*)
     7.7 +lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
     7.8 +     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
     7.9 +by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
    7.10 +
    7.11 +lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
    7.12 +     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
    7.13 +by (blast intro: wellfounded_imp_wellfounded_on
    7.14 +                 wellfounded_on_field_imp_wellfounded)
    7.15 +
    7.16 +lemma (in M_axioms) wellfounded_on_subset_A:
    7.17 +     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
    7.18 +by (simp add: wellfounded_on_def, blast)
    7.19 +
    7.20 +
    7.21  subsection{*Every well-founded relation is a subset of some inverse image of
    7.22        an ordinal*}
    7.23  
    7.24 @@ -127,7 +142,7 @@
    7.25  
    7.26    tran_closure :: "[i=>o,i,i] => o"
    7.27      "tran_closure(M,r,t) ==
    7.28 -         \<exists>s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)"
    7.29 +         \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
    7.30  
    7.31  
    7.32  locale M_trancl = M_axioms +
    7.33 @@ -135,11 +150,14 @@
    7.34    assumes rtrancl_separation:
    7.35       "[| M(r); M(A) |] ==>
    7.36  	separation
    7.37 -	   (M, \<lambda>p. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    7.38 -                    (\<exists>x y. p = <x,y> &  f`0 = x & f`n = y) &
    7.39 -                          (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r))"
    7.40 +	   (M, \<lambda>p. \<exists>n[M]. n\<in>nat & 
    7.41 +                    (\<exists>f[M]. 
    7.42 +                     f \<in> succ(n) -> A &
    7.43 +                     (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) &  
    7.44 +                           f`0 = x & f`n = y) &
    7.45 +                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
    7.46        and wellfounded_trancl_separation:
    7.47 -     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z)"
    7.48 +     "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+)"
    7.49  
    7.50  
    7.51  lemma (in M_trancl) rtran_closure_rtrancl:
    7.52 @@ -165,7 +183,7 @@
    7.53  apply (insert rtrancl_separation [of r "field(r)"])
    7.54  apply (simp add: rtrancl_alt_eq_rtrancl [symmetric]
    7.55                   rtrancl_alt_def field_closed typed_apply_abs apply_closed
    7.56 -                 Ord_succ_mem_iff M_nat
    7.57 +                 Ord_succ_mem_iff M_nat nat_into_M
    7.58                   nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
    7.59  done
    7.60  
    7.61 @@ -215,11 +233,10 @@
    7.62  apply (simp add: wellfounded_on_def)
    7.63  apply (safe intro!: equalityI)
    7.64  apply (rename_tac Z x)
    7.65 -apply (subgoal_tac "M({x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z})")
    7.66 +apply (subgoal_tac "M({x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+})")
    7.67   prefer 2
    7.68 - apply (simp add: wellfounded_trancl_separation)
    7.69 -apply (drule_tac x = "{x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
    7.70 -apply safe
    7.71 + apply (blast intro: wellfounded_trancl_separation) 
    7.72 +apply (drule_tac x = "{x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+}" in spec, safe)
    7.73  apply (blast dest: transM, simp)
    7.74  apply (rename_tac y w)
    7.75  apply (drule_tac x=w in bspec, assumption, clarify)
    7.76 @@ -228,22 +245,6 @@
    7.77   apply blast
    7.78  done
    7.79  
    7.80 -(*????move to Wellorderings.thy*)
    7.81 -lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
    7.82 -     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
    7.83 -by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
    7.84 -
    7.85 -lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
    7.86 -     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
    7.87 -by (blast intro: wellfounded_imp_wellfounded_on
    7.88 -                 wellfounded_on_field_imp_wellfounded)
    7.89 -
    7.90 -lemma (in M_axioms) wellfounded_on_subset_A:
    7.91 -     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
    7.92 -by (simp add: wellfounded_on_def, blast)
    7.93 -
    7.94 -
    7.95 -
    7.96  lemma (in M_trancl) wellfounded_trancl:
    7.97       "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)"
    7.98  apply (rotate_tac -1)
    7.99 @@ -259,14 +260,14 @@
   7.100  
   7.101  
   7.102  (*NEEDS RELATIVIZATION*)
   7.103 -locale M_recursion = M_trancl +
   7.104 +locale M_wfrank = M_trancl +
   7.105    assumes wfrank_separation':
   7.106       "M(r) ==>
   7.107  	separation
   7.108 -	   (M, \<lambda>x. ~ (\<exists>f. M(f) & is_recfun(r^+, x, %x f. range(f), f)))"
   7.109 +	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
   7.110   and wfrank_strong_replacement':
   7.111       "M(r) ==>
   7.112 -      strong_replacement(M, \<lambda>x z. \<exists>y f. M(y) & M(f) &
   7.113 +      strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
   7.114  		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
   7.115  		  y = range(f))"
   7.116   and Ord_wfrank_separation:
   7.117 @@ -279,13 +280,13 @@
   7.118  constdefs
   7.119   wellfoundedrank :: "[i=>o,i,i] => i"
   7.120      "wellfoundedrank(M,r,A) ==
   7.121 -        {p. x\<in>A, \<exists>y f. M(y) & M(f) &
   7.122 +        {p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 
   7.123                         p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
   7.124                         y = range(f)}"
   7.125  
   7.126 -lemma (in M_recursion) exists_wfrank:
   7.127 +lemma (in M_wfrank) exists_wfrank:
   7.128      "[| wellfounded(M,r); M(a); M(r) |]
   7.129 -     ==> \<exists>f. M(f) & is_recfun(r^+, a, %x f. range(f), f)"
   7.130 +     ==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)"
   7.131  apply (rule wellfounded_exists_is_recfun)
   7.132        apply (blast intro: wellfounded_trancl)
   7.133       apply (rule trans_trancl)
   7.134 @@ -294,7 +295,7 @@
   7.135  apply (simp_all add: trancl_subset_times)
   7.136  done
   7.137  
   7.138 -lemma (in M_recursion) M_wellfoundedrank:
   7.139 +lemma (in M_wfrank) M_wellfoundedrank:
   7.140      "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
   7.141  apply (insert wfrank_strong_replacement' [of r])
   7.142  apply (simp add: wellfoundedrank_def)
   7.143 @@ -306,7 +307,7 @@
   7.144   apply (simp add: trancl_subset_times, blast)
   7.145  done
   7.146  
   7.147 -lemma (in M_recursion) Ord_wfrank_range [rule_format]:
   7.148 +lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
   7.149      "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
   7.150       ==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
   7.151  apply (drule wellfounded_trancl, assumption)
   7.152 @@ -337,7 +338,7 @@
   7.153  apply (blast dest: pair_components_in_M)
   7.154  done
   7.155  
   7.156 -lemma (in M_recursion) Ord_range_wellfoundedrank:
   7.157 +lemma (in M_wfrank) Ord_range_wellfoundedrank:
   7.158      "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |]
   7.159       ==> Ord (range(wellfoundedrank(M,r,A)))"
   7.160  apply (frule wellfounded_trancl, assumption)
   7.161 @@ -349,23 +350,23 @@
   7.162   apply (blast intro: Ord_wfrank_range)
   7.163  txt{*We still must show that the range is a transitive set.*}
   7.164  apply (simp add: Transset_def, clarify, simp)
   7.165 -apply (rename_tac x i f u)
   7.166 +apply (rename_tac x f i u)
   7.167  apply (frule is_recfun_imp_in_r, assumption)
   7.168  apply (subgoal_tac "M(u) & M(i) & M(x)")
   7.169   prefer 2 apply (blast dest: transM, clarify)
   7.170  apply (rule_tac a=u in rangeI)
   7.171  apply (rule ReplaceI)
   7.172 -  apply (rule_tac x=i in exI, simp)
   7.173 -  apply (rule_tac x="restrict(f, r^+ -`` {u})" in exI)
   7.174 -  apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
   7.175 - apply blast
   7.176 +  apply (rule_tac x=i in rexI, simp)
   7.177 +   apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
   7.178 +    apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
   7.179 +   apply (simp, simp, blast) 
   7.180  txt{*Unicity requirement of Replacement*}
   7.181  apply clarify
   7.182  apply (frule apply_recfun2, assumption)
   7.183  apply (simp add: trans_trancl is_recfun_cut)+
   7.184  done
   7.185  
   7.186 -lemma (in M_recursion) function_wellfoundedrank:
   7.187 +lemma (in M_wfrank) function_wellfoundedrank:
   7.188      "[| wellfounded(M,r); M(r); M(A)|]
   7.189       ==> function(wellfoundedrank(M,r,A))"
   7.190  apply (simp add: wellfoundedrank_def function_def, clarify)
   7.191 @@ -375,7 +376,7 @@
   7.192      apply (simp_all add: trancl_subset_times trans_trancl)
   7.193  done
   7.194  
   7.195 -lemma (in M_recursion) domain_wellfoundedrank:
   7.196 +lemma (in M_wfrank) domain_wellfoundedrank:
   7.197      "[| wellfounded(M,r); M(r); M(A)|]
   7.198       ==> domain(wellfoundedrank(M,r,A)) = A"
   7.199  apply (simp add: wellfoundedrank_def function_def)
   7.200 @@ -384,9 +385,9 @@
   7.201  apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
   7.202  apply (rule domainI)
   7.203  apply (rule ReplaceI)
   7.204 -  apply (rule_tac x="range(f)" in exI)
   7.205 +  apply (rule_tac x="range(f)" in rexI)
   7.206    apply simp
   7.207 -  apply (rule_tac x=f in exI, blast, assumption)
   7.208 +  apply (rule_tac x=f in rexI, blast, simp_all)
   7.209  txt{*Uniqueness (for Replacement): repeated above!*}
   7.210  apply clarify
   7.211  apply (drule is_recfun_functional, assumption)
   7.212 @@ -394,7 +395,7 @@
   7.213      apply (simp_all add: trancl_subset_times trans_trancl)
   7.214  done
   7.215  
   7.216 -lemma (in M_recursion) wellfoundedrank_type:
   7.217 +lemma (in M_wfrank) wellfoundedrank_type:
   7.218      "[| wellfounded(M,r);  M(r); M(A)|]
   7.219       ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
   7.220  apply (frule function_wellfoundedrank [of r A], assumption+)
   7.221 @@ -404,13 +405,13 @@
   7.222  apply (simp add: domain_wellfoundedrank)
   7.223  done
   7.224  
   7.225 -lemma (in M_recursion) Ord_wellfoundedrank:
   7.226 +lemma (in M_wfrank) Ord_wellfoundedrank:
   7.227      "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |]
   7.228       ==> Ord(wellfoundedrank(M,r,A) ` a)"
   7.229  by (blast intro: apply_funtype [OF wellfoundedrank_type]
   7.230                   Ord_in_Ord [OF Ord_range_wellfoundedrank])
   7.231  
   7.232 -lemma (in M_recursion) wellfoundedrank_eq:
   7.233 +lemma (in M_wfrank) wellfoundedrank_eq:
   7.234       "[| is_recfun(r^+, a, %x. range, f);
   7.235           wellfounded(M,r);  a \<in> A; M(f); M(r); M(A)|]
   7.236        ==> wellfoundedrank(M,r,A) ` a = range(f)"
   7.237 @@ -418,9 +419,9 @@
   7.238   prefer 2 apply (blast intro: wellfoundedrank_type)
   7.239  apply (simp add: wellfoundedrank_def)
   7.240  apply (rule ReplaceI)
   7.241 -  apply (rule_tac x="range(f)" in exI)
   7.242 +  apply (rule_tac x="range(f)" in rexI) 
   7.243    apply blast
   7.244 - apply assumption
   7.245 + apply simp_all
   7.246  txt{*Unicity requirement of Replacement*}
   7.247  apply clarify
   7.248  apply (drule is_recfun_functional, assumption)
   7.249 @@ -429,7 +430,7 @@
   7.250  done
   7.251  
   7.252  
   7.253 -lemma (in M_recursion) wellfoundedrank_lt:
   7.254 +lemma (in M_wfrank) wellfoundedrank_lt:
   7.255       "[| <a,b> \<in> r;
   7.256           wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   7.257        ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
   7.258 @@ -454,7 +455,7 @@
   7.259  done
   7.260  
   7.261  
   7.262 -lemma (in M_recursion) wellfounded_imp_subset_rvimage:
   7.263 +lemma (in M_wfrank) wellfounded_imp_subset_rvimage:
   7.264       "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
   7.265        ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   7.266  apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
   7.267 @@ -465,12 +466,12 @@
   7.268  apply (blast intro: apply_rangeI wellfoundedrank_type)
   7.269  done
   7.270  
   7.271 -lemma (in M_recursion) wellfounded_imp_wf:
   7.272 +lemma (in M_wfrank) wellfounded_imp_wf:
   7.273       "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
   7.274  by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
   7.275            intro: wf_rvimage_Ord [THEN wf_subset])
   7.276  
   7.277 -lemma (in M_recursion) wellfounded_on_imp_wf_on:
   7.278 +lemma (in M_wfrank) wellfounded_on_imp_wf_on:
   7.279       "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
   7.280  apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
   7.281  apply (rule wellfounded_imp_wf)
   7.282 @@ -478,11 +479,11 @@
   7.283  done
   7.284  
   7.285  
   7.286 -theorem (in M_recursion) wf_abs [simp]:
   7.287 +theorem (in M_wfrank) wf_abs [simp]:
   7.288       "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
   7.289  by (blast intro: wellfounded_imp_wf wf_imp_relativized)
   7.290  
   7.291 -theorem (in M_recursion) wf_on_abs [simp]:
   7.292 +theorem (in M_wfrank) wf_on_abs [simp]:
   7.293       "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
   7.294  by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
   7.295  
   7.296 @@ -493,20 +494,20 @@
   7.297  
   7.298  lemma (in M_trancl) wfrec_relativize:
   7.299    "[|wf(r); M(a); M(r);  
   7.300 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   7.301 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   7.302            pair(M,x,y,z) & 
   7.303            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   7.304            y = H(x, restrict(g, r -`` {x}))); 
   7.305       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   7.306     ==> wfrec(r,a,H) = z <-> 
   7.307 -       (\<exists>f. M(f) & is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   7.308 +       (\<exists>f[M]. is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   7.309              z = H(a,restrict(f,r-``{a})))"
   7.310  apply (frule wf_trancl) 
   7.311  apply (simp add: wftrec_def wfrec_def, safe)
   7.312   apply (frule wf_exists_is_recfun 
   7.313                [of concl: "r^+" a "\<lambda>x f. H(x, restrict(f, r -`` {x}))"]) 
   7.314        apply (simp_all add: trans_trancl function_restrictI trancl_subset_times)
   7.315 - apply (clarify, rule_tac x=f in exI) 
   7.316 + apply (clarify, rule_tac x=x in rexI) 
   7.317   apply (simp_all add: the_recfun_eq trans_trancl trancl_subset_times)
   7.318  done
   7.319  
   7.320 @@ -516,10 +517,10 @@
   7.321        before we can replace @{term "r^+"} by @{term r}. *}
   7.322  theorem (in M_trancl) trans_wfrec_relativize:
   7.323    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
   7.324 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   7.325 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   7.326                  pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   7.327       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   7.328 -   ==> wfrec(r,a,H) = z <-> (\<exists>f. M(f) & is_recfun(r,a,H,f) & z = H(a,f))" 
   7.329 +   ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
   7.330  by (simp cong: is_recfun_cong
   7.331           add: wfrec_relativize trancl_eq_r
   7.332                 is_recfun_restrict_idem domain_restrict_idem)
   7.333 @@ -527,11 +528,11 @@
   7.334  
   7.335  lemma (in M_trancl) trans_eq_pair_wfrec_iff:
   7.336    "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
   7.337 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   7.338 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   7.339                  pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   7.340       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   7.341     ==> y = <x, wfrec(r, x, H)> <-> 
   7.342 -       (\<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   7.343 +       (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   7.344  apply safe  
   7.345   apply (simp add: trans_wfrec_relativize [THEN iff_sym]) 
   7.346  txt{*converse direction*}
   7.347 @@ -543,7 +544,7 @@
   7.348  subsection{*M is closed under well-founded recursion*}
   7.349  
   7.350  text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
   7.351 -lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
   7.352 +lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
   7.353       "[|wf(r); M(r); 
   7.354          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   7.355          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   7.356 @@ -557,20 +558,20 @@
   7.357  done
   7.358  
   7.359  text{*Eliminates one instance of replacement.*}
   7.360 -lemma (in M_recursion) wfrec_replacement_iff:
   7.361 -     "strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   7.362 +lemma (in M_wfrank) wfrec_replacement_iff:
   7.363 +     "strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. 
   7.364                  pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <->
   7.365        strong_replacement(M, 
   7.366 -           \<lambda>x y. \<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   7.367 +           \<lambda>x y. \<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   7.368  apply simp 
   7.369  apply (rule strong_replacement_cong, blast) 
   7.370  done
   7.371  
   7.372  text{*Useful version for transitive relations*}
   7.373 -theorem (in M_recursion) trans_wfrec_closed:
   7.374 +theorem (in M_wfrank) trans_wfrec_closed:
   7.375       "[|wf(r); trans(r); relation(r); M(r); M(a);
   7.376          strong_replacement(M, 
   7.377 -             \<lambda>x z. \<exists>y g. M(y) & M(g) &
   7.378 +             \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   7.379                      pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   7.380          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   7.381        ==> M(wfrec(r,a,H))"
   7.382 @@ -582,13 +583,13 @@
   7.383  section{*Absoluteness without assuming transitivity*}
   7.384  lemma (in M_trancl) eq_pair_wfrec_iff:
   7.385    "[|wf(r);  M(r);  M(y); 
   7.386 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   7.387 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   7.388            pair(M,x,y,z) & 
   7.389            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   7.390            y = H(x, restrict(g, r -`` {x}))); 
   7.391       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   7.392     ==> y = <x, wfrec(r, x, H)> <-> 
   7.393 -       (\<exists>f. M(f) & is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   7.394 +       (\<exists>f[M]. is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   7.395              y = <x, H(x,restrict(f,r-``{x}))>)"
   7.396  apply safe  
   7.397   apply (simp add: wfrec_relativize [THEN iff_sym]) 
   7.398 @@ -597,7 +598,7 @@
   7.399  apply (simp add: wfrec_relativize, blast) 
   7.400  done
   7.401  
   7.402 -lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
   7.403 +lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
   7.404       "[|wf(r); M(r); 
   7.405          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   7.406          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   7.407 @@ -611,9 +612,9 @@
   7.408  done
   7.409  
   7.410  text{*Full version not assuming transitivity, but maybe not very useful.*}
   7.411 -theorem (in M_recursion) wfrec_closed:
   7.412 +theorem (in M_wfrank) wfrec_closed:
   7.413       "[|wf(r); M(r); M(a);
   7.414 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   7.415 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   7.416            pair(M,x,y,z) & 
   7.417            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   7.418            y = H(x, restrict(g, r -`` {x}))); 
     8.1 --- a/src/ZF/Constructible/WFrec.thy	Mon Jul 01 18:10:53 2002 +0200
     8.2 +++ b/src/ZF/Constructible/WFrec.thy	Mon Jul 01 18:16:18 2002 +0200
     8.3 @@ -117,9 +117,7 @@
     8.4  
     8.5  lemma (in M_axioms) is_recfun_functional:
     8.6       "[|is_recfun(r,a,H,f);  is_recfun(r,a,H,g);  
     8.7 -       wellfounded(M,r); trans(r); 
     8.8 -       M(f); M(g); M(r) |]   
     8.9 -      ==> f=g"
    8.10 +       wellfounded(M,r); trans(r); M(f); M(g); M(r) |] ==> f=g"
    8.11  apply (rule fun_extension)
    8.12  apply (erule is_recfun_type)+
    8.13  apply (blast intro!: is_recfun_equal dest: transM) 
    8.14 @@ -183,9 +181,8 @@
    8.15         \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(Y);
    8.16         \<forall>b. M(b) -->
    8.17  	   b \<in> Y <->
    8.18 -	   (\<exists>x\<in>r -`` {a1}.
    8.19 -	       \<exists>y. M(y) \<and>
    8.20 -		   (\<exists>g. M(g) \<and> b = \<langle>x,y\<rangle> \<and> is_recfun(r,x,H,g) \<and> y = H(x,g)));
    8.21 +	   (\<exists>x\<in>r -`` {a1}. \<exists>y[M]. \<exists>g[M]. 
    8.22 +              b = \<langle>x,y\<rangle> & is_recfun(r,x,H,g) \<and> y = H(x,g));
    8.23            \<langle>x,a1\<rangle> \<in> r; M(f); is_recfun(r,x,H,f) |]
    8.24         ==> restrict(Y, r -`` {x}) = f"
    8.25  apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y <-> <y,z>:f") 
    8.26 @@ -203,17 +200,17 @@
    8.27  apply (frule_tac y="<y,z>" in transM, assumption, simp) 
    8.28  apply (rule_tac x=y in bexI)
    8.29  prefer 2 apply (blast dest: transD)
    8.30 -apply (rule_tac x=z in exI, simp) 
    8.31 -apply (rule_tac x="restrict(f, r -`` {y})" in exI) 
    8.32 -apply (simp add: vimage_closed restrict_closed is_recfun_restrict
    8.33 -                 apply_recfun is_recfun_type [THEN apply_iff]) 
    8.34 +apply (rule_tac x=z in rexI) 
    8.35 +apply (rule_tac x="restrict(f, r -`` {y})" in rexI) 
    8.36 +apply (simp_all add: is_recfun_restrict
    8.37 +                     apply_recfun is_recfun_type [THEN apply_iff]) 
    8.38  done
    8.39  
    8.40  text{*For typical applications of Replacement for recursive definitions*}
    8.41  lemma (in M_axioms) univalent_is_recfun:
    8.42       "[|wellfounded(M,r); trans(r); M(r)|]
    8.43 -      ==> univalent (M, A, \<lambda>x p. \<exists>y. M(y) &
    8.44 -                    (\<exists>f. M(f) & p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f)))"
    8.45 +      ==> univalent (M, A, \<lambda>x p. 
    8.46 +              \<exists>y[M]. \<exists>f[M]. p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f))"
    8.47  apply (simp add: univalent_def) 
    8.48  apply (blast dest: is_recfun_functional) 
    8.49  done
    8.50 @@ -221,60 +218,60 @@
    8.51  text{*Proof of the inductive step for @{text exists_is_recfun}, since
    8.52        we must prove two versions.*}
    8.53  lemma (in M_axioms) exists_is_recfun_indstep:
    8.54 -    "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f)); 
    8.55 +    "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f[M]. is_recfun(r, y, H, f)); 
    8.56         wellfounded(M,r); trans(r); M(r); M(a1);
    8.57 -       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    8.58 -                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    8.59 +       strong_replacement(M, \<lambda>x z. 
    8.60 +              \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    8.61         \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]   
    8.62 -      ==> \<exists>f. M(f) & is_recfun(r,a1,H,f)"
    8.63 +      ==> \<exists>f[M]. is_recfun(r,a1,H,f)"
    8.64  apply (drule_tac A="r-``{a1}" in strong_replacementD)
    8.65    apply blast 
    8.66   txt{*Discharge the "univalent" obligation of Replacement*}
    8.67   apply (simp add: univalent_is_recfun) 
    8.68  txt{*Show that the constructed object satisfies @{text is_recfun}*} 
    8.69  apply clarify 
    8.70 -apply (rule_tac x=Y in exI)  
    8.71 +apply (rule_tac x=Y in rexI)  
    8.72  txt{*Unfold only the top-level occurrence of @{term is_recfun}*}
    8.73  apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1])
    8.74 -txt{*The big iff-formula defininng @{term Y} is now redundant*}
    8.75 +txt{*The big iff-formula defining @{term Y} is now redundant*}
    8.76  apply safe 
    8.77   apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H]) 
    8.78  txt{*one more case*}
    8.79  apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff)
    8.80  apply (rename_tac x) 
    8.81  apply (rule_tac x=x in exI, simp) 
    8.82 -apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI) 
    8.83 +apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in rexI) 
    8.84  apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 
    8.85 -apply (rule_tac x=f in exI) 
    8.86 -apply (simp add: restrict_Y_lemma [of r H]) 
    8.87 +apply (rename_tac f) 
    8.88 +apply (rule_tac x=f in rexI) 
    8.89 +apply (simp add: restrict_Y_lemma [of r H], simp_all)
    8.90  done
    8.91  
    8.92  text{*Relativized version, when we have the (currently weaker) premise
    8.93        @{term "wellfounded(M,r)"}*}
    8.94  lemma (in M_axioms) wellfounded_exists_is_recfun:
    8.95      "[|wellfounded(M,r);  trans(r);  
    8.96 -       separation(M, \<lambda>x. ~ (\<exists>f. M(f) \<and> is_recfun(r, x, H, f)));
    8.97 -       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    8.98 -                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    8.99 +       separation(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r, x, H, f)));
   8.100 +       strong_replacement(M, \<lambda>x z. 
   8.101 +          \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   8.102         M(r);  M(a);  
   8.103         \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]   
   8.104 -      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
   8.105 +      ==> \<exists>f[M]. is_recfun(r,a,H,f)"
   8.106  apply (rule wellfounded_induct, assumption+, clarify)
   8.107  apply (rule exists_is_recfun_indstep, assumption+)
   8.108  done
   8.109  
   8.110  lemma (in M_axioms) wf_exists_is_recfun [rule_format]:
   8.111 -    "[|wf(r);  trans(r);  
   8.112 -       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.113 -                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   8.114 -        M(r);  
   8.115 +    "[|wf(r);  trans(r);  M(r);  
   8.116 +       strong_replacement(M, \<lambda>x z. 
   8.117 +         \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   8.118         \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]   
   8.119 -      ==> M(a) --> (\<exists>f. M(f) & is_recfun(r,a,H,f))"
   8.120 +      ==> M(a) --> (\<exists>f[M]. is_recfun(r,a,H,f))"
   8.121  apply (rule wf_induct, assumption+)
   8.122  apply (frule wf_imp_relativized)
   8.123  apply (intro impI)
   8.124 -apply (rule exists_is_recfun_indstep)
   8.125 -      apply (blast dest: pair_components_in_M)+
   8.126 +apply (rule exists_is_recfun_indstep) 
   8.127 +      apply (blast dest: transM del: rev_rallE, assumption+)
   8.128  done
   8.129  
   8.130  constdefs
   8.131 @@ -346,24 +343,23 @@
   8.132                    fun_apply(M,f,j,fj) & fj = k"
   8.133  
   8.134  
   8.135 -locale M_recursion = M_axioms +
   8.136 +locale M_ord_arith = M_axioms +
   8.137    assumes oadd_strong_replacement:
   8.138     "[| M(i); M(j) |] ==>
   8.139      strong_replacement(M, 
   8.140 -         \<lambda>x z. \<exists>y f fx. M(y) & M(f) & M(fx) & 
   8.141 -		         pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) & 
   8.142 -		         image(M,f,x,fx) & y = i Un fx)" 
   8.143 +         \<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) & 
   8.144 +		                      image(M,f,x,fx) & y = i Un fx)" 
   8.145   and omult_strong_replacement':
   8.146     "[| M(i); M(j) |] ==>
   8.147 -    strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.148 -	     pair(M,x,y,z) & 
   8.149 +    strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. 
   8.150 +	     z = <x,y> &
   8.151  	     is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
   8.152  	     y = (THE z. omult_eqns(i, x, g, z)))" 
   8.153  
   8.154  
   8.155  
   8.156  text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*}
   8.157 -lemma (in M_recursion) is_oadd_fun_iff:
   8.158 +lemma (in M_ord_arith) is_oadd_fun_iff:
   8.159     "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
   8.160      ==> is_oadd_fun(M,i,j,a,f) <->
   8.161  	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
   8.162 @@ -377,10 +373,10 @@
   8.163  done
   8.164  
   8.165  
   8.166 -lemma (in M_recursion) oadd_strong_replacement':
   8.167 +lemma (in M_ord_arith) oadd_strong_replacement':
   8.168      "[| M(i); M(j) |] ==>
   8.169 -     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.170 -		  pair(M,x,y,z) & 
   8.171 +     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   8.172 +		  z = <x,y> &
   8.173  		  is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
   8.174  		  y = i Un g``x)" 
   8.175  apply (insert oadd_strong_replacement [of i j]) 
   8.176 @@ -389,28 +385,25 @@
   8.177  done
   8.178  
   8.179  
   8.180 -lemma (in M_recursion) exists_oadd:
   8.181 +lemma (in M_ord_arith) exists_oadd:
   8.182      "[| Ord(j);  M(i);  M(j) |]
   8.183 -     ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
   8.184 +     ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
   8.185  apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
   8.186 -    apply simp 
   8.187 -   apply (blast intro: oadd_strong_replacement') 
   8.188 -  apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
   8.189 +    apply (simp_all add: Memrel_type oadd_strong_replacement') 
   8.190 +done 
   8.191 +
   8.192 +lemma (in M_ord_arith) exists_oadd_fun:
   8.193 +    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)"
   8.194 +apply (rule exists_oadd [THEN rexE])
   8.195 +apply (erule Ord_succ, assumption, simp) 
   8.196 +apply (rename_tac f) 
   8.197 +apply (frule is_recfun_type)
   8.198 +apply (rule_tac x=f in rexI) 
   8.199 + apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   8.200 +                  is_oadd_fun_iff Ord_trans [OF _ succI1], assumption)
   8.201  done
   8.202  
   8.203 -lemma (in M_recursion) exists_oadd_fun:
   8.204 -    "[| Ord(j);  M(i);  M(j) |] 
   8.205 -     ==> \<exists>f. M(f) & is_oadd_fun(M,i,succ(j),succ(j),f)"
   8.206 -apply (rule exists_oadd [THEN exE])
   8.207 -apply (erule Ord_succ, assumption, simp) 
   8.208 -apply (rename_tac f, clarify) 
   8.209 -apply (frule is_recfun_type)
   8.210 -apply (rule_tac x=f in exI) 
   8.211 -apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   8.212 -                 is_oadd_fun_iff Ord_trans [OF _ succI1])
   8.213 -done
   8.214 -
   8.215 -lemma (in M_recursion) is_oadd_fun_apply:
   8.216 +lemma (in M_ord_arith) is_oadd_fun_apply:
   8.217      "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] 
   8.218       ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
   8.219  apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) 
   8.220 @@ -419,7 +412,7 @@
   8.221  apply (simp add: image_fun, blast) 
   8.222  done
   8.223  
   8.224 -lemma (in M_recursion) is_oadd_fun_iff_oadd [rule_format]:
   8.225 +lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]:
   8.226      "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
   8.227       ==> j<J --> f`j = i++j"
   8.228  apply (erule_tac i=j in trans_induct, clarify) 
   8.229 @@ -428,25 +421,25 @@
   8.230  apply (blast intro: lt_trans ltI lt_Ord) 
   8.231  done
   8.232  
   8.233 -lemma (in M_recursion) oadd_abs_fun_apply_iff:
   8.234 +lemma (in M_ord_arith) oadd_abs_fun_apply_iff:
   8.235      "[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |] 
   8.236       ==> fun_apply(M,f,j,k) <-> f`j = k"
   8.237  by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs) 
   8.238  
   8.239 -lemma (in M_recursion) Ord_oadd_abs:
   8.240 +lemma (in M_ord_arith) Ord_oadd_abs:
   8.241      "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
   8.242  apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd)
   8.243  apply (frule exists_oadd_fun [of j i], blast+)
   8.244  done
   8.245  
   8.246 -lemma (in M_recursion) oadd_abs:
   8.247 +lemma (in M_ord_arith) oadd_abs:
   8.248      "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
   8.249  apply (case_tac "Ord(i) & Ord(j)")
   8.250   apply (simp add: Ord_oadd_abs)
   8.251  apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
   8.252  done
   8.253  
   8.254 -lemma (in M_recursion) oadd_closed [intro,simp]:
   8.255 +lemma (in M_ord_arith) oadd_closed [intro,simp]:
   8.256      "[| M(i); M(j) |] ==> M(i++j)"
   8.257  apply (simp add: oadd_eq_if_raw_oadd, clarify) 
   8.258  apply (simp add: raw_oadd_eq_oadd) 
   8.259 @@ -490,7 +483,7 @@
   8.260  by (simp add: omult_eqns_def)
   8.261  
   8.262  
   8.263 -lemma (in M_recursion) the_omult_eqns_closed:
   8.264 +lemma (in M_ord_arith) the_omult_eqns_closed:
   8.265      "[| M(i); M(x); M(g); function(g) |] 
   8.266       ==> M(THE z. omult_eqns(i, x, g, z))"
   8.267  apply (case_tac "Ord(x)")
   8.268 @@ -501,39 +494,37 @@
   8.269  apply (simp add: omult_eqns_Limit) 
   8.270  done
   8.271  
   8.272 -lemma (in M_recursion) exists_omult:
   8.273 +lemma (in M_ord_arith) exists_omult:
   8.274      "[| Ord(j);  M(i);  M(j) |]
   8.275 -     ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
   8.276 +     ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
   8.277  apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
   8.278 -    apply simp
   8.279 -   apply (blast intro: omult_strong_replacement') 
   8.280 -  apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
   8.281 +    apply (simp_all add: Memrel_type omult_strong_replacement') 
   8.282  apply (blast intro: the_omult_eqns_closed) 
   8.283  done
   8.284  
   8.285 -lemma (in M_recursion) exists_omult_fun:
   8.286 -    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f. M(f) & is_omult_fun(M,i,succ(j),f)"
   8.287 -apply (rule exists_omult [THEN exE])
   8.288 +lemma (in M_ord_arith) exists_omult_fun:
   8.289 +    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_omult_fun(M,i,succ(j),f)"
   8.290 +apply (rule exists_omult [THEN rexE])
   8.291  apply (erule Ord_succ, assumption, simp) 
   8.292 -apply (rename_tac f, clarify) 
   8.293 +apply (rename_tac f) 
   8.294  apply (frule is_recfun_type)
   8.295 -apply (rule_tac x=f in exI) 
   8.296 +apply (rule_tac x=f in rexI) 
   8.297  apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   8.298                   is_omult_fun_def Ord_trans [OF _ succI1])
   8.299 -apply (force dest: Ord_in_Ord' 
   8.300 -             simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
   8.301 -                       the_omult_eqns_Limit) 
   8.302 + apply (force dest: Ord_in_Ord' 
   8.303 +              simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
   8.304 +                        the_omult_eqns_Limit, assumption)
   8.305  done
   8.306  
   8.307 -lemma (in M_recursion) is_omult_fun_apply_0:
   8.308 +lemma (in M_ord_arith) is_omult_fun_apply_0:
   8.309      "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
   8.310  by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
   8.311  
   8.312 -lemma (in M_recursion) is_omult_fun_apply_succ:
   8.313 +lemma (in M_ord_arith) is_omult_fun_apply_succ:
   8.314      "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
   8.315  by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) 
   8.316  
   8.317 -lemma (in M_recursion) is_omult_fun_apply_Limit:
   8.318 +lemma (in M_ord_arith) is_omult_fun_apply_Limit:
   8.319      "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] 
   8.320       ==> f ` x = (\<Union>y\<in>x. f`y)"
   8.321  apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
   8.322 @@ -541,7 +532,7 @@
   8.323  apply (simp add: ball_conj_distrib omult_Limit image_function)
   8.324  done
   8.325  
   8.326 -lemma (in M_recursion) is_omult_fun_eq_omult:
   8.327 +lemma (in M_ord_arith) is_omult_fun_eq_omult:
   8.328      "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] 
   8.329       ==> j<J --> f`j = i**j"
   8.330  apply (erule_tac i=j in trans_induct3)
   8.331 @@ -555,12 +546,12 @@
   8.332  apply (blast intro: lt_trans ltI lt_Ord) 
   8.333  done
   8.334  
   8.335 -lemma (in M_recursion) omult_abs_fun_apply_iff:
   8.336 +lemma (in M_ord_arith) omult_abs_fun_apply_iff:
   8.337      "[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |] 
   8.338       ==> fun_apply(M,f,j,k) <-> f`j = k"
   8.339  by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs) 
   8.340  
   8.341 -lemma (in M_recursion) omult_abs:
   8.342 +lemma (in M_ord_arith) omult_abs:
   8.343      "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
   8.344  apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult)
   8.345  apply (frule exists_omult_fun [of j i], blast+)