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.*}
```