src/ZF/Constructible/WF_absolute.thy
changeset 13339 0f89104dd377
parent 13324 39d1b3a4c6f4
child 13348 374d05460db4
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Wed Jul 10 16:07:52 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jul 10 16:54:07 2002 +0200
     1.3 @@ -21,13 +21,13 @@
     1.4  by (subst wfrank_def [THEN def_wfrec], simp_all)
     1.5  
     1.6  lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
     1.7 -apply (rule_tac a="a" in wf_induct, assumption)
     1.8 +apply (rule_tac a=a in wf_induct, assumption)
     1.9  apply (subst wfrank, assumption)
    1.10  apply (rule Ord_succ [THEN Ord_UN], blast)
    1.11  done
    1.12  
    1.13  lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
    1.14 -apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
    1.15 +apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption)
    1.16  apply (rule UN_I [THEN ltI])
    1.17  apply (simp add: Ord_wfrank vimage_iff)+
    1.18  done
    1.19 @@ -141,8 +141,7 @@
    1.20              (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
    1.21                             (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
    1.22  apply (simp add: rtran_closure_mem_def typed_apply_abs
    1.23 -                 Ord_succ_mem_iff nat_0_le [THEN ltD])
    1.24 -apply (blast intro: elim:); 
    1.25 +                 Ord_succ_mem_iff nat_0_le [THEN ltD], blast) 
    1.26  done
    1.27  
    1.28  locale M_trancl = M_axioms +
    1.29 @@ -159,7 +158,7 @@
    1.30       "M(r) ==> rtran_closure(M,r,rtrancl(r))"
    1.31  apply (simp add: rtran_closure_def rtran_closure_mem_iff 
    1.32                   rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def)
    1.33 -apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); 
    1.34 +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) 
    1.35  done
    1.36  
    1.37  lemma (in M_trancl) rtrancl_closed [intro,simp]:
    1.38 @@ -177,7 +176,7 @@
    1.39  apply (rule M_equalityI)
    1.40  apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
    1.41                   rtrancl_alt_def rtran_closure_mem_iff)
    1.42 -apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); 
    1.43 +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) 
    1.44  done
    1.45  
    1.46  lemma (in M_trancl) trancl_closed [intro,simp]:
    1.47 @@ -235,10 +234,10 @@
    1.48  
    1.49  (*NEEDS RELATIVIZATION*)
    1.50  locale M_wfrank = M_trancl +
    1.51 -  assumes wfrank_separation':
    1.52 +  assumes wfrank_separation:
    1.53       "M(r) ==>
    1.54 -	separation
    1.55 -	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
    1.56 +      separation (M, \<lambda>x. 
    1.57 +         ~ (\<exists>f[M]. M_is_recfun(M, r^+, x, %mm x f y. y = range(f), f)))"
    1.58   and wfrank_strong_replacement':
    1.59       "M(r) ==>
    1.60        strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
    1.61 @@ -247,7 +246,15 @@
    1.62   and Ord_wfrank_separation:
    1.63       "M(r) ==>
    1.64        separation (M, \<lambda>x. ~ (\<forall>f. M(f) \<longrightarrow>
    1.65 -                       is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))"
    1.66 +                       is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))" 
    1.67 +
    1.68 +lemma (in M_wfrank) wfrank_separation':
    1.69 +     "M(r) ==>
    1.70 +      separation
    1.71 +	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
    1.72 +apply (insert wfrank_separation [of r])
    1.73 +apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
    1.74 +done
    1.75  
    1.76  text{*This function, defined using replacement, is a rank function for
    1.77  well-founded relations within the class M.*}