src/ZF/Constructible/WF_absolute.thy
changeset 13251 74cb2af8811e
parent 13247 e3c289f0724b
child 13254 5146ccaedf42
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Wed Jun 26 12:17:21 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jun 26 18:31:20 2002 +0200
     1.3 @@ -1,10 +1,10 @@
     1.4  theory WF_absolute = WFrec:
     1.5  
     1.6 -subsection{*Every well-founded relation is a subset of some inverse image of 
     1.7 +subsection{*Every well-founded relation is a subset of some inverse image of
     1.8        an ordinal*}
     1.9  
    1.10  lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
    1.11 -by (blast intro: wf_rvimage wf_Memrel )
    1.12 +by (blast intro: wf_rvimage wf_Memrel)
    1.13  
    1.14  
    1.15  constdefs
    1.16 @@ -21,7 +21,7 @@
    1.17  lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
    1.18  apply (rule_tac a="a" in wf_induct, assumption)
    1.19  apply (subst wfrank, assumption)
    1.20 -apply (rule Ord_succ [THEN Ord_UN], blast) 
    1.21 +apply (rule Ord_succ [THEN Ord_UN], blast)
    1.22  done
    1.23  
    1.24  lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
    1.25 @@ -34,19 +34,19 @@
    1.26  by (simp add: wftype_def Ord_wfrank)
    1.27  
    1.28  lemma wftypeI: "\<lbrakk>wf(r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
    1.29 -apply (simp add: wftype_def) 
    1.30 -apply (blast intro: wfrank_lt [THEN ltD]) 
    1.31 +apply (simp add: wftype_def)
    1.32 +apply (blast intro: wfrank_lt [THEN ltD])
    1.33  done
    1.34  
    1.35  
    1.36  lemma wf_imp_subset_rvimage:
    1.37       "[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
    1.38 -apply (rule_tac x="wftype(r)" in exI) 
    1.39 -apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI) 
    1.40 -apply (simp add: Ord_wftype, clarify) 
    1.41 -apply (frule subsetD, assumption, clarify) 
    1.42 +apply (rule_tac x="wftype(r)" in exI)
    1.43 +apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
    1.44 +apply (simp add: Ord_wftype, clarify)
    1.45 +apply (frule subsetD, assumption, clarify)
    1.46  apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
    1.47 -apply (blast intro: wftypeI  ) 
    1.48 +apply (blast intro: wftypeI)
    1.49  done
    1.50  
    1.51  theorem wf_iff_subset_rvimage:
    1.52 @@ -59,65 +59,65 @@
    1.53  
    1.54  constdefs
    1.55    rtrancl_alt :: "[i,i]=>i"
    1.56 -    "rtrancl_alt(A,r) == 
    1.57 +    "rtrancl_alt(A,r) ==
    1.58         {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    1.59                   (\<exists>x y. p = <x,y> &  f`0 = x & f`n = y) &
    1.60                         (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
    1.61  
    1.62 -lemma alt_rtrancl_lemma1 [rule_format]: 
    1.63 +lemma alt_rtrancl_lemma1 [rule_format]:
    1.64      "n \<in> nat
    1.65 -     ==> \<forall>f \<in> succ(n) -> field(r). 
    1.66 +     ==> \<forall>f \<in> succ(n) -> field(r).
    1.67           (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
    1.68 -apply (induct_tac n) 
    1.69 -apply (simp_all add: apply_funtype rtrancl_refl, clarify) 
    1.70 -apply (rename_tac n f) 
    1.71 -apply (rule rtrancl_into_rtrancl) 
    1.72 +apply (induct_tac n)
    1.73 +apply (simp_all add: apply_funtype rtrancl_refl, clarify)
    1.74 +apply (rename_tac n f)
    1.75 +apply (rule rtrancl_into_rtrancl)
    1.76   prefer 2 apply assumption
    1.77  apply (drule_tac x="restrict(f,succ(n))" in bspec)
    1.78 - apply (blast intro: restrict_type2) 
    1.79 -apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    1.80 + apply (blast intro: restrict_type2)
    1.81 +apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
    1.82  done
    1.83  
    1.84  lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
    1.85  apply (simp add: rtrancl_alt_def)
    1.86 -apply (blast intro: alt_rtrancl_lemma1 )  
    1.87 +apply (blast intro: alt_rtrancl_lemma1)
    1.88  done
    1.89  
    1.90  lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
    1.91 -apply (simp add: rtrancl_alt_def, clarify) 
    1.92 -apply (frule rtrancl_type [THEN subsetD], clarify, simp) 
    1.93 -apply (erule rtrancl_induct) 
    1.94 +apply (simp add: rtrancl_alt_def, clarify)
    1.95 +apply (frule rtrancl_type [THEN subsetD], clarify, simp)
    1.96 +apply (erule rtrancl_induct)
    1.97   txt{*Base case, trivial*}
    1.98 - apply (rule_tac x=0 in bexI) 
    1.99 -  apply (rule_tac x="lam x:1. xa" in bexI) 
   1.100 -   apply simp_all 
   1.101 + apply (rule_tac x=0 in bexI)
   1.102 +  apply (rule_tac x="lam x:1. xa" in bexI)
   1.103 +   apply simp_all
   1.104  txt{*Inductive step*}
   1.105 -apply clarify 
   1.106 -apply (rename_tac n f) 
   1.107 -apply (rule_tac x="succ(n)" in bexI) 
   1.108 +apply clarify
   1.109 +apply (rename_tac n f)
   1.110 +apply (rule_tac x="succ(n)" in bexI)
   1.111   apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
   1.112 -  apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
   1.113 -  apply (blast intro: mem_asym)  
   1.114 - apply typecheck 
   1.115 - apply auto 
   1.116 +  apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
   1.117 +  apply (blast intro: mem_asym)
   1.118 + apply typecheck
   1.119 + apply auto
   1.120  done
   1.121  
   1.122  lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
   1.123  by (blast del: subsetI
   1.124 -	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) 
   1.125 +	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
   1.126  
   1.127  
   1.128  constdefs
   1.129  
   1.130    rtran_closure :: "[i=>o,i,i] => o"
   1.131 -    "rtran_closure(M,r,s) == 
   1.132 +    "rtran_closure(M,r,s) ==
   1.133          \<forall>A. M(A) --> is_field(M,r,A) -->
   1.134 - 	 (\<forall>p. M(p) --> 
   1.135 -          (p \<in> s <-> 
   1.136 -           (\<exists>n\<in>nat. M(n) & 
   1.137 + 	 (\<forall>p. M(p) -->
   1.138 +          (p \<in> s <->
   1.139 +           (\<exists>n\<in>nat. M(n) &
   1.140              (\<exists>n'. M(n') & successor(M,n,n') &
   1.141               (\<exists>f. M(f) & typed_function(M,n',A,f) &
   1.142 -              (\<exists>x\<in>A. M(x) & (\<exists>y\<in>A. M(y) & pair(M,x,y,p) &  
   1.143 +              (\<exists>x\<in>A. M(x) & (\<exists>y\<in>A. M(y) & pair(M,x,y,p) &
   1.144                     fun_apply(M,f,0,x) & fun_apply(M,f,n,y))) &
   1.145                (\<forall>i\<in>n. M(i) -->
   1.146                  (\<forall>i'. M(i') --> successor(M,i,i') -->
   1.147 @@ -126,7 +126,7 @@
   1.148                     (\<forall>q. M(q) --> pair(M,fi,fi',q) --> q \<in> r))))))))))"
   1.149  
   1.150    tran_closure :: "[i=>o,i,i] => o"
   1.151 -    "tran_closure(M,r,t) == 
   1.152 +    "tran_closure(M,r,t) ==
   1.153           \<exists>s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)"
   1.154  
   1.155  
   1.156 @@ -142,335 +142,350 @@
   1.157       "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z)"
   1.158  
   1.159  
   1.160 -lemma (in M_trancl) rtran_closure_rtrancl: 
   1.161 +lemma (in M_trancl) rtran_closure_rtrancl:
   1.162       "M(r) ==> rtran_closure(M,r,rtrancl(r))"
   1.163 -apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] 
   1.164 +apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
   1.165                   rtrancl_alt_def field_closed typed_apply_abs apply_closed
   1.166 -                 Ord_succ_mem_iff M_nat  nat_0_le [THEN ltD], clarify) 
   1.167 -apply (rule iffI) 
   1.168 - apply clarify 
   1.169 - apply simp 
   1.170 - apply (rename_tac n f) 
   1.171 - apply (rule_tac x=n in bexI) 
   1.172 -  apply (rule_tac x=f in exI) 
   1.173 +                 Ord_succ_mem_iff M_nat  nat_0_le [THEN ltD], clarify)
   1.174 +apply (rule iffI)
   1.175 + apply clarify
   1.176 + apply simp
   1.177 + apply (rename_tac n f)
   1.178 + apply (rule_tac x=n in bexI)
   1.179 +  apply (rule_tac x=f in exI)
   1.180    apply simp
   1.181    apply (blast dest: finite_fun_closed dest: transM)
   1.182   apply assumption
   1.183  apply clarify
   1.184 -apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast)  
   1.185 +apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast)
   1.186  done
   1.187  
   1.188 -lemma (in M_trancl) rtrancl_closed [intro,simp]: 
   1.189 +lemma (in M_trancl) rtrancl_closed [intro,simp]:
   1.190       "M(r) ==> M(rtrancl(r))"
   1.191 -apply (insert rtrancl_separation [of r "field(r)"]) 
   1.192 -apply (simp add: rtrancl_alt_eq_rtrancl [symmetric] 
   1.193 +apply (insert rtrancl_separation [of r "field(r)"])
   1.194 +apply (simp add: rtrancl_alt_eq_rtrancl [symmetric]
   1.195                   rtrancl_alt_def field_closed typed_apply_abs apply_closed
   1.196                   Ord_succ_mem_iff M_nat
   1.197                   nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
   1.198  done
   1.199  
   1.200 -lemma (in M_trancl) rtrancl_abs [simp]: 
   1.201 +lemma (in M_trancl) rtrancl_abs [simp]:
   1.202       "[| M(r); M(z) |] ==> rtran_closure(M,r,z) <-> z = rtrancl(r)"
   1.203  apply (rule iffI)
   1.204   txt{*Proving the right-to-left implication*}
   1.205 - prefer 2 apply (blast intro: rtran_closure_rtrancl) 
   1.206 + prefer 2 apply (blast intro: rtran_closure_rtrancl)
   1.207  apply (rule M_equalityI)
   1.208 -apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] 
   1.209 +apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
   1.210                   rtrancl_alt_def field_closed typed_apply_abs apply_closed
   1.211                   Ord_succ_mem_iff M_nat
   1.212 -                 nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) 
   1.213 +                 nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
   1.214   prefer 2 apply assumption
   1.215   prefer 2 apply blast
   1.216 -apply (rule iffI, clarify) 
   1.217 -apply (simp add: nat_0_le [THEN ltD]  apply_funtype, blast, clarify, simp) 
   1.218 - apply (rename_tac n f) 
   1.219 - apply (rule_tac x=n in bexI) 
   1.220 +apply (rule iffI, clarify)
   1.221 +apply (simp add: nat_0_le [THEN ltD]  apply_funtype, blast, clarify, simp)
   1.222 + apply (rename_tac n f)
   1.223 + apply (rule_tac x=n in bexI)
   1.224    apply (rule_tac x=f in exI)
   1.225    apply (blast dest!: finite_fun_closed, assumption)
   1.226  done
   1.227  
   1.228  
   1.229 -lemma (in M_trancl) trancl_closed [intro,simp]: 
   1.230 +lemma (in M_trancl) trancl_closed [intro,simp]:
   1.231       "M(r) ==> M(trancl(r))"
   1.232 -by (simp add: trancl_def comp_closed rtrancl_closed) 
   1.233 +by (simp add: trancl_def comp_closed rtrancl_closed)
   1.234  
   1.235 -lemma (in M_trancl) trancl_abs [simp]: 
   1.236 +lemma (in M_trancl) trancl_abs [simp]:
   1.237       "[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)"
   1.238 -by (simp add: tran_closure_def trancl_def) 
   1.239 +by (simp add: tran_closure_def trancl_def)
   1.240  
   1.241  
   1.242 -text{*Alternative proof of @{text wf_on_trancl}; inspiration for the 
   1.243 +text{*Alternative proof of @{text wf_on_trancl}; inspiration for the
   1.244        relativized version.  Original version is on theory WF.*}
   1.245  lemma "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
   1.246 -apply (simp add: wf_on_def wf_def) 
   1.247 +apply (simp add: wf_on_def wf_def)
   1.248  apply (safe intro!: equalityI)
   1.249 -apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec) 
   1.250 -apply (blast elim: tranclE) 
   1.251 +apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
   1.252 +apply (blast elim: tranclE)
   1.253  done
   1.254  
   1.255  
   1.256  lemma (in M_trancl) wellfounded_on_trancl:
   1.257       "[| wellfounded_on(M,A,r);  r-``A <= A; M(r); M(A) |]
   1.258 -      ==> wellfounded_on(M,A,r^+)" 
   1.259 -apply (simp add: wellfounded_on_def) 
   1.260 +      ==> wellfounded_on(M,A,r^+)"
   1.261 +apply (simp add: wellfounded_on_def)
   1.262  apply (safe intro!: equalityI)
   1.263  apply (rename_tac Z x)
   1.264 -apply (subgoal_tac "M({x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z})") 
   1.265 - prefer 2 
   1.266 - apply (simp add: wellfounded_trancl_separation) 
   1.267 -apply (drule_tac x = "{x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec) 
   1.268 +apply (subgoal_tac "M({x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z})")
   1.269 + prefer 2
   1.270 + apply (simp add: wellfounded_trancl_separation)
   1.271 +apply (drule_tac x = "{x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
   1.272  apply safe
   1.273 -apply (blast dest: transM, simp) 
   1.274 -apply (rename_tac y w) 
   1.275 +apply (blast dest: transM, simp)
   1.276 +apply (rename_tac y w)
   1.277  apply (drule_tac x=w in bspec, assumption, clarify)
   1.278  apply (erule tranclE)
   1.279    apply (blast dest: transM)   (*transM is needed to prove M(xa)*)
   1.280 - apply blast 
   1.281 + apply blast
   1.282  done
   1.283  
   1.284 +(*????move to Wellorderings.thy*)
   1.285 +lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
   1.286 +     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
   1.287 +by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
   1.288 +
   1.289 +lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
   1.290 +     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
   1.291 +by (blast intro: wellfounded_imp_wellfounded_on
   1.292 +                 wellfounded_on_field_imp_wellfounded)
   1.293 +
   1.294 +lemma (in M_axioms) wellfounded_on_subset_A:
   1.295 +     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
   1.296 +by (simp add: wellfounded_on_def, blast)
   1.297 +
   1.298 +
   1.299 +
   1.300 +lemma (in M_trancl) wellfounded_trancl:
   1.301 +     "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)"
   1.302 +apply (rotate_tac -1)
   1.303 +apply (simp add: wellfounded_iff_wellfounded_on_field)
   1.304 +apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl)
   1.305 +   apply blast
   1.306 +  apply (simp_all add: trancl_type [THEN field_rel_subset])
   1.307 +done
   1.308  
   1.309  text{*Relativized to M: Every well-founded relation is a subset of some
   1.310 -inverse image of an ordinal.  Key step is the construction (in M) of a 
   1.311 +inverse image of an ordinal.  Key step is the construction (in M) of a
   1.312  rank function.*}
   1.313  
   1.314  
   1.315  (*NEEDS RELATIVIZATION*)
   1.316  locale M_recursion = M_trancl +
   1.317    assumes wfrank_separation':
   1.318 -     "[| M(r); M(A) |] ==>
   1.319 +     "M(r) ==>
   1.320  	separation
   1.321 -	   (M, \<lambda>x. x \<in> A --> 
   1.322 -		~(\<exists>f. M(f) \<and> is_recfun(r^+, x, %x f. range(f), f)))"
   1.323 +	   (M, \<lambda>x. ~ (\<exists>f. M(f) & is_recfun(r^+, x, %x f. range(f), f)))"
   1.324   and wfrank_strong_replacement':
   1.325       "M(r) ==>
   1.326        strong_replacement(M, \<lambda>x z. \<exists>y f. M(y) & M(f) &
   1.327 -		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & 
   1.328 +		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
   1.329  		  y = range(f))"
   1.330   and Ord_wfrank_separation:
   1.331 -     "[| M(r); M(A) |] ==>
   1.332 -      separation (M, \<lambda>x. x \<in> A \<longrightarrow>
   1.333 -                \<not> (\<forall>f. M(f) \<longrightarrow>
   1.334 +     "M(r) ==>
   1.335 +      separation (M, \<lambda>x. ~ (\<forall>f. M(f) \<longrightarrow>
   1.336                         is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))"
   1.337  
   1.338 -constdefs 
   1.339 +text{*This function, defined using replacement, is a rank function for
   1.340 +well-founded relations within the class M.*}
   1.341 +constdefs
   1.342   wellfoundedrank :: "[i=>o,i,i] => i"
   1.343 -    "wellfoundedrank(M,r,A) == 
   1.344 -        {p. x\<in>A, \<exists>y f. M(y) & M(f) & 
   1.345 -                       p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) & 
   1.346 +    "wellfoundedrank(M,r,A) ==
   1.347 +        {p. x\<in>A, \<exists>y f. M(y) & M(f) &
   1.348 +                       p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
   1.349                         y = range(f)}"
   1.350  
   1.351  lemma (in M_recursion) exists_wfrank:
   1.352 -    "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
   1.353 +    "[| wellfounded(M,r); M(a); M(r) |]
   1.354       ==> \<exists>f. M(f) & is_recfun(r^+, a, %x f. range(f), f)"
   1.355 -apply (rule wellfounded_exists_is_recfun [of A]) 
   1.356 -apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.357 -apply (rule trans_trancl [THEN trans_imp_trans_on], assumption+)
   1.358 -apply (simp_all add: trancl_subset_times) 
   1.359 +apply (rule wellfounded_exists_is_recfun)
   1.360 +      apply (blast intro: wellfounded_trancl)
   1.361 +     apply (rule trans_trancl)
   1.362 +    apply (erule wfrank_separation')
   1.363 +   apply (erule wfrank_strong_replacement')
   1.364 +apply (simp_all add: trancl_subset_times)
   1.365  done
   1.366  
   1.367  lemma (in M_recursion) M_wellfoundedrank:
   1.368 -    "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |] 
   1.369 -     ==> M(wellfoundedrank(M,r,A))"
   1.370 -apply (insert wfrank_strong_replacement' [of r]) 
   1.371 -apply (simp add: wellfoundedrank_def) 
   1.372 -apply (rule strong_replacement_closed) 
   1.373 +    "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
   1.374 +apply (insert wfrank_strong_replacement' [of r])
   1.375 +apply (simp add: wellfoundedrank_def)
   1.376 +apply (rule strong_replacement_closed)
   1.377     apply assumption+
   1.378 - apply (rule univalent_is_recfun) 
   1.379 -     apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.380 -    apply (rule trans_on_trancl) 
   1.381 -   apply (simp add: trancl_subset_times) 
   1.382 -  apply blast+
   1.383 + apply (rule univalent_is_recfun)
   1.384 +   apply (blast intro: wellfounded_trancl)
   1.385 +  apply (rule trans_trancl)
   1.386 + apply (simp add: trancl_subset_times)
   1.387 +apply blast
   1.388  done
   1.389  
   1.390  lemma (in M_recursion) Ord_wfrank_range [rule_format]:
   1.391 -    "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
   1.392 +    "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
   1.393       ==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
   1.394 -apply (subgoal_tac "wellfounded_on(M, A, r^+)") 
   1.395 - prefer 2
   1.396 - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.397 -apply (erule wellfounded_on_induct2, assumption+)
   1.398 -apply (simp add: trancl_subset_times) 
   1.399 -apply (blast intro: Ord_wfrank_separation, clarify)
   1.400 +apply (drule wellfounded_trancl, assumption)
   1.401 +apply (rule wellfounded_induct, assumption+)
   1.402 +  apply (simp add:);
   1.403 + apply (blast intro: Ord_wfrank_separation);
   1.404 +apply (clarify)
   1.405  txt{*The reasoning in both cases is that we get @{term y} such that
   1.406 -   @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that 
   1.407 +   @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
   1.408     @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
   1.409  apply (rule OrdI [OF _ Ord_is_Transset])
   1.410   txt{*An ordinal is a transitive set...*}
   1.411 - apply (simp add: Transset_def) 
   1.412 + apply (simp add: Transset_def)
   1.413   apply clarify
   1.414 - apply (frule apply_recfun2, assumption) 
   1.415 + apply (frule apply_recfun2, assumption)
   1.416   apply (force simp add: restrict_iff)
   1.417 -txt{*...of ordinals.  This second case requires the induction hyp.*} 
   1.418 -apply clarify 
   1.419 +txt{*...of ordinals.  This second case requires the induction hyp.*}
   1.420 +apply clarify
   1.421  apply (rename_tac i y)
   1.422 -apply (frule apply_recfun2, assumption) 
   1.423 -apply (frule is_recfun_imp_in_r, assumption) 
   1.424 -apply (frule is_recfun_restrict) 
   1.425 +apply (frule apply_recfun2, assumption)
   1.426 +apply (frule is_recfun_imp_in_r, assumption)
   1.427 +apply (frule is_recfun_restrict)
   1.428      (*simp_all won't work*)
   1.429 -    apply (simp add: trans_on_trancl trancl_subset_times)+  
   1.430 +    apply (simp add: trans_trancl trancl_subset_times)+
   1.431  apply (drule spec [THEN mp], assumption)
   1.432  apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
   1.433 - apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec) 
   1.434 + apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec)
   1.435   apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
   1.436  apply (blast dest: pair_components_in_M)
   1.437  done
   1.438  
   1.439  lemma (in M_recursion) Ord_range_wellfoundedrank:
   1.440 -    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |] 
   1.441 +    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |]
   1.442       ==> Ord (range(wellfoundedrank(M,r,A)))"
   1.443 -apply (subgoal_tac "wellfounded_on(M, A, r^+)") 
   1.444 - prefer 2
   1.445 - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.446 -apply (frule trancl_subset_times) 
   1.447 +apply (frule wellfounded_trancl, assumption)
   1.448 +apply (frule trancl_subset_times)
   1.449  apply (simp add: wellfoundedrank_def)
   1.450  apply (rule OrdI [OF _ Ord_is_Transset])
   1.451   prefer 2
   1.452 - txt{*by our previous result the range consists of ordinals.*} 
   1.453 - apply (blast intro: Ord_wfrank_range) 
   1.454 + txt{*by our previous result the range consists of ordinals.*}
   1.455 + apply (blast intro: Ord_wfrank_range)
   1.456  txt{*We still must show that the range is a transitive set.*}
   1.457  apply (simp add: Transset_def, clarify, simp)
   1.458 -apply (rename_tac x i f u)   
   1.459 -apply (frule is_recfun_imp_in_r, assumption) 
   1.460 -apply (subgoal_tac "M(u) & M(i) & M(x)") 
   1.461 - prefer 2 apply (blast dest: transM, clarify) 
   1.462 -apply (rule_tac a=u in rangeI) 
   1.463 -apply (rule ReplaceI) 
   1.464 -  apply (rule_tac x=i in exI, simp) 
   1.465 +apply (rename_tac x i f u)
   1.466 +apply (frule is_recfun_imp_in_r, assumption)
   1.467 +apply (subgoal_tac "M(u) & M(i) & M(x)")
   1.468 + prefer 2 apply (blast dest: transM, clarify)
   1.469 +apply (rule_tac a=u in rangeI)
   1.470 +apply (rule ReplaceI)
   1.471 +  apply (rule_tac x=i in exI, simp)
   1.472    apply (rule_tac x="restrict(f, r^+ -`` {u})" in exI)
   1.473 -  apply (blast intro: is_recfun_restrict trans_on_trancl dest: apply_recfun2)
   1.474 +  apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
   1.475   apply blast
   1.476 -txt{*Unicity requirement of Replacement*} 
   1.477 +txt{*Unicity requirement of Replacement*}
   1.478  apply clarify
   1.479 -apply (frule apply_recfun2, assumption) 
   1.480 -apply (simp add: trans_on_trancl is_recfun_cut)+
   1.481 +apply (frule apply_recfun2, assumption)
   1.482 +apply (simp add: trans_trancl is_recfun_cut)+
   1.483  done
   1.484  
   1.485  lemma (in M_recursion) function_wellfoundedrank:
   1.486 -    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   1.487 +    "[| wellfounded(M,r); M(r); M(A)|]
   1.488       ==> function(wellfoundedrank(M,r,A))"
   1.489 -apply (simp add: wellfoundedrank_def function_def, clarify) 
   1.490 +apply (simp add: wellfoundedrank_def function_def, clarify)
   1.491  txt{*Uniqueness: repeated below!*}
   1.492  apply (drule is_recfun_functional, assumption)
   1.493 -    apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.494 -    apply (simp_all add: trancl_subset_times 
   1.495 -                         trans_trancl [THEN trans_imp_trans_on]) 
   1.496 -apply (blast dest: transM) 
   1.497 +     apply (blast intro: wellfounded_trancl)
   1.498 +    apply (simp_all add: trancl_subset_times trans_trancl)
   1.499  done
   1.500  
   1.501  lemma (in M_recursion) domain_wellfoundedrank:
   1.502 -    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   1.503 +    "[| wellfounded(M,r); M(r); M(A)|]
   1.504       ==> domain(wellfoundedrank(M,r,A)) = A"
   1.505 -apply (simp add: wellfoundedrank_def function_def) 
   1.506 +apply (simp add: wellfoundedrank_def function_def)
   1.507  apply (rule equalityI, auto)
   1.508 -apply (frule transM, assumption)  
   1.509 -apply (frule exists_wfrank, assumption+, clarify) 
   1.510 -apply (rule domainI) 
   1.511 +apply (frule transM, assumption)
   1.512 +apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
   1.513 +apply (rule domainI)
   1.514  apply (rule ReplaceI)
   1.515 -apply (rule_tac x="range(f)" in exI)
   1.516 -apply simp  
   1.517 -apply (rule_tac x=f in exI, blast, assumption)
   1.518 +  apply (rule_tac x="range(f)" in exI)
   1.519 +  apply simp
   1.520 +  apply (rule_tac x=f in exI, blast, assumption)
   1.521  txt{*Uniqueness (for Replacement): repeated above!*}
   1.522  apply clarify
   1.523  apply (drule is_recfun_functional, assumption)
   1.524 -    apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.525 -    apply (simp_all add: trancl_subset_times 
   1.526 -                         trans_trancl [THEN trans_imp_trans_on]) 
   1.527 +    apply (blast intro: wellfounded_trancl)
   1.528 +    apply (simp_all add: trancl_subset_times trans_trancl)
   1.529  done
   1.530  
   1.531  lemma (in M_recursion) wellfoundedrank_type:
   1.532 -    "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   1.533 +    "[| wellfounded(M,r);  M(r); M(A)|]
   1.534       ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
   1.535 -apply (frule function_wellfoundedrank, assumption+) 
   1.536 -apply (frule function_imp_Pi) 
   1.537 - apply (simp add: wellfoundedrank_def relation_def) 
   1.538 - apply blast  
   1.539 +apply (frule function_wellfoundedrank [of r A], assumption+)
   1.540 +apply (frule function_imp_Pi)
   1.541 + apply (simp add: wellfoundedrank_def relation_def)
   1.542 + apply blast
   1.543  apply (simp add: domain_wellfoundedrank)
   1.544  done
   1.545  
   1.546  lemma (in M_recursion) Ord_wellfoundedrank:
   1.547 -    "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |] 
   1.548 +    "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |]
   1.549       ==> Ord(wellfoundedrank(M,r,A) ` a)"
   1.550  by (blast intro: apply_funtype [OF wellfoundedrank_type]
   1.551                   Ord_in_Ord [OF Ord_range_wellfoundedrank])
   1.552  
   1.553  lemma (in M_recursion) wellfoundedrank_eq:
   1.554       "[| is_recfun(r^+, a, %x. range, f);
   1.555 -         wellfounded(M,r);  a \<in> A; r \<subseteq> A*A;  M(f); M(r); M(A)|] 
   1.556 +         wellfounded(M,r);  a \<in> A; M(f); M(r); M(A)|]
   1.557        ==> wellfoundedrank(M,r,A) ` a = range(f)"
   1.558 -apply (rule apply_equality) 
   1.559 - prefer 2 apply (blast intro: wellfoundedrank_type ) 
   1.560 +apply (rule apply_equality)
   1.561 + prefer 2 apply (blast intro: wellfoundedrank_type)
   1.562  apply (simp add: wellfoundedrank_def)
   1.563  apply (rule ReplaceI)
   1.564 -  apply (rule_tac x="range(f)" in exI) 
   1.565 -  apply blast 
   1.566 +  apply (rule_tac x="range(f)" in exI)
   1.567 +  apply blast
   1.568   apply assumption
   1.569 -txt{*Unicity requirement of Replacement*} 
   1.570 +txt{*Unicity requirement of Replacement*}
   1.571  apply clarify
   1.572  apply (drule is_recfun_functional, assumption)
   1.573 -    apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.574 -    apply (simp_all add: trancl_subset_times 
   1.575 -                         trans_trancl [THEN trans_imp_trans_on])
   1.576 -apply (blast dest: transM) 
   1.577 +    apply (blast intro: wellfounded_trancl)
   1.578 +    apply (simp_all add: trancl_subset_times trans_trancl)
   1.579  done
   1.580  
   1.581  
   1.582  lemma (in M_recursion) wellfoundedrank_lt:
   1.583       "[| <a,b> \<in> r;
   1.584 -         wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|] 
   1.585 +         wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   1.586        ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
   1.587 -apply (subgoal_tac "wellfounded_on(M, A, r^+)") 
   1.588 - prefer 2
   1.589 - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.590 +apply (frule wellfounded_trancl, assumption)
   1.591  apply (subgoal_tac "a\<in>A & b\<in>A")
   1.592   prefer 2 apply blast
   1.593 -apply (simp add: lt_def Ord_wellfoundedrank, clarify)   
   1.594 -apply (frule exists_wfrank [of concl: _ b], assumption+, clarify) 
   1.595 +apply (simp add: lt_def Ord_wellfoundedrank, clarify)
   1.596 +apply (frule exists_wfrank [of concl: _ b], assumption+, clarify)
   1.597  apply (rename_tac fb)
   1.598 -apply (frule is_recfun_restrict [of concl: _ a])
   1.599 -    apply (rule trans_on_trancl, assumption)
   1.600 -   apply (simp_all add: r_into_trancl trancl_subset_times) 
   1.601 +apply (frule is_recfun_restrict [of concl: "r^+" a])
   1.602 +    apply (rule trans_trancl, assumption)
   1.603 +   apply (simp_all add: r_into_trancl trancl_subset_times)
   1.604  txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
   1.605 -apply (simp add: wellfoundedrank_eq) 
   1.606 +apply (simp add: wellfoundedrank_eq)
   1.607  apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
   1.608     apply (simp_all add: transM [of a])
   1.609  txt{*We have used equations for wellfoundedrank and now must use some
   1.610      for  @{text is_recfun}. *}
   1.611 -apply (rule_tac a=a in rangeI) 
   1.612 -apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff 
   1.613 -                 r_into_trancl apply_recfun r_into_trancl)  
   1.614 +apply (rule_tac a=a in rangeI)
   1.615 +apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
   1.616 +                 r_into_trancl apply_recfun r_into_trancl)
   1.617  done
   1.618  
   1.619  
   1.620  lemma (in M_recursion) wellfounded_imp_subset_rvimage:
   1.621 -     "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|] 
   1.622 +     "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
   1.623        ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   1.624  apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
   1.625  apply (rule_tac x="wellfoundedrank(M,r,A)" in exI)
   1.626 -apply (simp add: Ord_range_wellfoundedrank, clarify) 
   1.627 -apply (frule subsetD, assumption, clarify) 
   1.628 +apply (simp add: Ord_range_wellfoundedrank, clarify)
   1.629 +apply (frule subsetD, assumption, clarify)
   1.630  apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD])
   1.631 -apply (blast intro: apply_rangeI wellfoundedrank_type) 
   1.632 +apply (blast intro: apply_rangeI wellfoundedrank_type)
   1.633  done
   1.634  
   1.635 -lemma (in M_recursion) wellfounded_imp_wf: 
   1.636 -     "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)" 
   1.637 +lemma (in M_recursion) wellfounded_imp_wf:
   1.638 +     "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
   1.639  by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
   1.640            intro: wf_rvimage_Ord [THEN wf_subset])
   1.641  
   1.642 -lemma (in M_recursion) wellfounded_on_imp_wf_on: 
   1.643 -     "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)" 
   1.644 -apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) 
   1.645 +lemma (in M_recursion) wellfounded_on_imp_wf_on:
   1.646 +     "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
   1.647 +apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
   1.648  apply (rule wellfounded_imp_wf)
   1.649 -apply (simp_all add: relation_def)  
   1.650 +apply (simp_all add: relation_def)
   1.651  done
   1.652  
   1.653  
   1.654 -theorem (in M_recursion) wf_abs [simp]: 
   1.655 +theorem (in M_recursion) wf_abs [simp]:
   1.656       "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
   1.657 -by (blast intro: wellfounded_imp_wf wf_imp_relativized) 
   1.658 +by (blast intro: wellfounded_imp_wf wf_imp_relativized)
   1.659  
   1.660 -theorem (in M_recursion) wf_on_abs [simp]: 
   1.661 +theorem (in M_recursion) wf_on_abs [simp]:
   1.662       "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
   1.663 -by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) 
   1.664 +by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
   1.665  
   1.666  end