--- a/src/ZF/Constructible/WF_absolute.thy Wed Jun 26 12:17:21 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Wed Jun 26 18:31:20 2002 +0200
@@ -1,10 +1,10 @@
theory WF_absolute = WFrec:
-subsection{*Every well-founded relation is a subset of some inverse image of
+subsection{*Every well-founded relation is a subset of some inverse image of
an ordinal*}
lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
-by (blast intro: wf_rvimage wf_Memrel )
+by (blast intro: wf_rvimage wf_Memrel)
constdefs
@@ -21,7 +21,7 @@
lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
apply (rule_tac a="a" in wf_induct, assumption)
apply (subst wfrank, assumption)
-apply (rule Ord_succ [THEN Ord_UN], blast)
+apply (rule Ord_succ [THEN Ord_UN], blast)
done
lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
@@ -34,19 +34,19 @@
by (simp add: wftype_def Ord_wfrank)
lemma wftypeI: "\<lbrakk>wf(r); x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
-apply (simp add: wftype_def)
-apply (blast intro: wfrank_lt [THEN ltD])
+apply (simp add: wftype_def)
+apply (blast intro: wfrank_lt [THEN ltD])
done
lemma wf_imp_subset_rvimage:
"[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
-apply (rule_tac x="wftype(r)" in exI)
-apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
-apply (simp add: Ord_wftype, clarify)
-apply (frule subsetD, assumption, clarify)
+apply (rule_tac x="wftype(r)" in exI)
+apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
+apply (simp add: Ord_wftype, clarify)
+apply (frule subsetD, assumption, clarify)
apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
-apply (blast intro: wftypeI )
+apply (blast intro: wftypeI)
done
theorem wf_iff_subset_rvimage:
@@ -59,65 +59,65 @@
constdefs
rtrancl_alt :: "[i,i]=>i"
- "rtrancl_alt(A,r) ==
+ "rtrancl_alt(A,r) ==
{p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
(\<exists>x y. p = <x,y> & f`0 = x & f`n = y) &
(\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
-lemma alt_rtrancl_lemma1 [rule_format]:
+lemma alt_rtrancl_lemma1 [rule_format]:
"n \<in> nat
- ==> \<forall>f \<in> succ(n) -> field(r).
+ ==> \<forall>f \<in> succ(n) -> field(r).
(\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
-apply (induct_tac n)
-apply (simp_all add: apply_funtype rtrancl_refl, clarify)
-apply (rename_tac n f)
-apply (rule rtrancl_into_rtrancl)
+apply (induct_tac n)
+apply (simp_all add: apply_funtype rtrancl_refl, clarify)
+apply (rename_tac n f)
+apply (rule rtrancl_into_rtrancl)
prefer 2 apply assumption
apply (drule_tac x="restrict(f,succ(n))" in bspec)
- apply (blast intro: restrict_type2)
-apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
+ apply (blast intro: restrict_type2)
+apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
done
lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
apply (simp add: rtrancl_alt_def)
-apply (blast intro: alt_rtrancl_lemma1 )
+apply (blast intro: alt_rtrancl_lemma1)
done
lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
-apply (simp add: rtrancl_alt_def, clarify)
-apply (frule rtrancl_type [THEN subsetD], clarify, simp)
-apply (erule rtrancl_induct)
+apply (simp add: rtrancl_alt_def, clarify)
+apply (frule rtrancl_type [THEN subsetD], clarify, simp)
+apply (erule rtrancl_induct)
txt{*Base case, trivial*}
- apply (rule_tac x=0 in bexI)
- apply (rule_tac x="lam x:1. xa" in bexI)
- apply simp_all
+ apply (rule_tac x=0 in bexI)
+ apply (rule_tac x="lam x:1. xa" in bexI)
+ apply simp_all
txt{*Inductive step*}
-apply clarify
-apply (rename_tac n f)
-apply (rule_tac x="succ(n)" in bexI)
+apply clarify
+apply (rename_tac n f)
+apply (rule_tac x="succ(n)" in bexI)
apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
- apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
- apply (blast intro: mem_asym)
- apply typecheck
- apply auto
+ apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
+ apply (blast intro: mem_asym)
+ apply typecheck
+ apply auto
done
lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
by (blast del: subsetI
- intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
+ intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
constdefs
rtran_closure :: "[i=>o,i,i] => o"
- "rtran_closure(M,r,s) ==
+ "rtran_closure(M,r,s) ==
\<forall>A. M(A) --> is_field(M,r,A) -->
- (\<forall>p. M(p) -->
- (p \<in> s <->
- (\<exists>n\<in>nat. M(n) &
+ (\<forall>p. M(p) -->
+ (p \<in> s <->
+ (\<exists>n\<in>nat. M(n) &
(\<exists>n'. M(n') & successor(M,n,n') &
(\<exists>f. M(f) & typed_function(M,n',A,f) &
- (\<exists>x\<in>A. M(x) & (\<exists>y\<in>A. M(y) & pair(M,x,y,p) &
+ (\<exists>x\<in>A. M(x) & (\<exists>y\<in>A. M(y) & pair(M,x,y,p) &
fun_apply(M,f,0,x) & fun_apply(M,f,n,y))) &
(\<forall>i\<in>n. M(i) -->
(\<forall>i'. M(i') --> successor(M,i,i') -->
@@ -126,7 +126,7 @@
(\<forall>q. M(q) --> pair(M,fi,fi',q) --> q \<in> r))))))))))"
tran_closure :: "[i=>o,i,i] => o"
- "tran_closure(M,r,t) ==
+ "tran_closure(M,r,t) ==
\<exists>s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)"
@@ -142,335 +142,350 @@
"[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z)"
-lemma (in M_trancl) rtran_closure_rtrancl:
+lemma (in M_trancl) rtran_closure_rtrancl:
"M(r) ==> rtran_closure(M,r,rtrancl(r))"
-apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
+apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
rtrancl_alt_def field_closed typed_apply_abs apply_closed
- Ord_succ_mem_iff M_nat nat_0_le [THEN ltD], clarify)
-apply (rule iffI)
- apply clarify
- apply simp
- apply (rename_tac n f)
- apply (rule_tac x=n in bexI)
- apply (rule_tac x=f in exI)
+ Ord_succ_mem_iff M_nat nat_0_le [THEN ltD], clarify)
+apply (rule iffI)
+ apply clarify
+ apply simp
+ apply (rename_tac n f)
+ apply (rule_tac x=n in bexI)
+ apply (rule_tac x=f in exI)
apply simp
apply (blast dest: finite_fun_closed dest: transM)
apply assumption
apply clarify
-apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast)
+apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast)
done
-lemma (in M_trancl) rtrancl_closed [intro,simp]:
+lemma (in M_trancl) rtrancl_closed [intro,simp]:
"M(r) ==> M(rtrancl(r))"
-apply (insert rtrancl_separation [of r "field(r)"])
-apply (simp add: rtrancl_alt_eq_rtrancl [symmetric]
+apply (insert rtrancl_separation [of r "field(r)"])
+apply (simp add: rtrancl_alt_eq_rtrancl [symmetric]
rtrancl_alt_def field_closed typed_apply_abs apply_closed
Ord_succ_mem_iff M_nat
nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
done
-lemma (in M_trancl) rtrancl_abs [simp]:
+lemma (in M_trancl) rtrancl_abs [simp]:
"[| M(r); M(z) |] ==> rtran_closure(M,r,z) <-> z = rtrancl(r)"
apply (rule iffI)
txt{*Proving the right-to-left implication*}
- prefer 2 apply (blast intro: rtran_closure_rtrancl)
+ prefer 2 apply (blast intro: rtran_closure_rtrancl)
apply (rule M_equalityI)
-apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
+apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
rtrancl_alt_def field_closed typed_apply_abs apply_closed
Ord_succ_mem_iff M_nat
- nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
+ nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
prefer 2 apply assumption
prefer 2 apply blast
-apply (rule iffI, clarify)
-apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast, clarify, simp)
- apply (rename_tac n f)
- apply (rule_tac x=n in bexI)
+apply (rule iffI, clarify)
+apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast, clarify, simp)
+ apply (rename_tac n f)
+ apply (rule_tac x=n in bexI)
apply (rule_tac x=f in exI)
apply (blast dest!: finite_fun_closed, assumption)
done
-lemma (in M_trancl) trancl_closed [intro,simp]:
+lemma (in M_trancl) trancl_closed [intro,simp]:
"M(r) ==> M(trancl(r))"
-by (simp add: trancl_def comp_closed rtrancl_closed)
+by (simp add: trancl_def comp_closed rtrancl_closed)
-lemma (in M_trancl) trancl_abs [simp]:
+lemma (in M_trancl) trancl_abs [simp]:
"[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)"
-by (simp add: tran_closure_def trancl_def)
+by (simp add: tran_closure_def trancl_def)
-text{*Alternative proof of @{text wf_on_trancl}; inspiration for the
+text{*Alternative proof of @{text wf_on_trancl}; inspiration for the
relativized version. Original version is on theory WF.*}
lemma "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)"
-apply (simp add: wf_on_def wf_def)
+apply (simp add: wf_on_def wf_def)
apply (safe intro!: equalityI)
-apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
-apply (blast elim: tranclE)
+apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
+apply (blast elim: tranclE)
done
lemma (in M_trancl) wellfounded_on_trancl:
"[| wellfounded_on(M,A,r); r-``A <= A; M(r); M(A) |]
- ==> wellfounded_on(M,A,r^+)"
-apply (simp add: wellfounded_on_def)
+ ==> wellfounded_on(M,A,r^+)"
+apply (simp add: wellfounded_on_def)
apply (safe intro!: equalityI)
apply (rename_tac Z x)
-apply (subgoal_tac "M({x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z})")
- prefer 2
- apply (simp add: wellfounded_trancl_separation)
-apply (drule_tac x = "{x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
+apply (subgoal_tac "M({x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z})")
+ prefer 2
+ apply (simp add: wellfounded_trancl_separation)
+apply (drule_tac x = "{x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
apply safe
-apply (blast dest: transM, simp)
-apply (rename_tac y w)
+apply (blast dest: transM, simp)
+apply (rename_tac y w)
apply (drule_tac x=w in bspec, assumption, clarify)
apply (erule tranclE)
apply (blast dest: transM) (*transM is needed to prove M(xa)*)
- apply blast
+ apply blast
done
+(*????move to Wellorderings.thy*)
+lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
+ "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
+by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
+
+lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
+ "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
+by (blast intro: wellfounded_imp_wellfounded_on
+ wellfounded_on_field_imp_wellfounded)
+
+lemma (in M_axioms) wellfounded_on_subset_A:
+ "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)"
+by (simp add: wellfounded_on_def, blast)
+
+
+
+lemma (in M_trancl) wellfounded_trancl:
+ "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)"
+apply (rotate_tac -1)
+apply (simp add: wellfounded_iff_wellfounded_on_field)
+apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl)
+ apply blast
+ apply (simp_all add: trancl_type [THEN field_rel_subset])
+done
text{*Relativized to M: Every well-founded relation is a subset of some
-inverse image of an ordinal. Key step is the construction (in M) of a
+inverse image of an ordinal. Key step is the construction (in M) of a
rank function.*}
(*NEEDS RELATIVIZATION*)
locale M_recursion = M_trancl +
assumes wfrank_separation':
- "[| M(r); M(A) |] ==>
+ "M(r) ==>
separation
- (M, \<lambda>x. x \<in> A -->
- ~(\<exists>f. M(f) \<and> is_recfun(r^+, x, %x f. range(f), f)))"
+ (M, \<lambda>x. ~ (\<exists>f. M(f) & is_recfun(r^+, x, %x f. range(f), f)))"
and wfrank_strong_replacement':
"M(r) ==>
strong_replacement(M, \<lambda>x z. \<exists>y f. M(y) & M(f) &
- pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
+ pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
y = range(f))"
and Ord_wfrank_separation:
- "[| M(r); M(A) |] ==>
- separation (M, \<lambda>x. x \<in> A \<longrightarrow>
- \<not> (\<forall>f. M(f) \<longrightarrow>
+ "M(r) ==>
+ separation (M, \<lambda>x. ~ (\<forall>f. M(f) \<longrightarrow>
is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))"
-constdefs
+text{*This function, defined using replacement, is a rank function for
+well-founded relations within the class M.*}
+constdefs
wellfoundedrank :: "[i=>o,i,i] => i"
- "wellfoundedrank(M,r,A) ==
- {p. x\<in>A, \<exists>y f. M(y) & M(f) &
- p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
+ "wellfoundedrank(M,r,A) ==
+ {p. x\<in>A, \<exists>y f. M(y) & M(f) &
+ p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
y = range(f)}"
lemma (in M_recursion) exists_wfrank:
- "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
+ "[| wellfounded(M,r); M(a); M(r) |]
==> \<exists>f. M(f) & is_recfun(r^+, a, %x f. range(f), f)"
-apply (rule wellfounded_exists_is_recfun [of A])
-apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
-apply (rule trans_trancl [THEN trans_imp_trans_on], assumption+)
-apply (simp_all add: trancl_subset_times)
+apply (rule wellfounded_exists_is_recfun)
+ apply (blast intro: wellfounded_trancl)
+ apply (rule trans_trancl)
+ apply (erule wfrank_separation')
+ apply (erule wfrank_strong_replacement')
+apply (simp_all add: trancl_subset_times)
done
lemma (in M_recursion) M_wellfoundedrank:
- "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |]
- ==> M(wellfoundedrank(M,r,A))"
-apply (insert wfrank_strong_replacement' [of r])
-apply (simp add: wellfoundedrank_def)
-apply (rule strong_replacement_closed)
+ "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
+apply (insert wfrank_strong_replacement' [of r])
+apply (simp add: wellfoundedrank_def)
+apply (rule strong_replacement_closed)
apply assumption+
- apply (rule univalent_is_recfun)
- apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
- apply (rule trans_on_trancl)
- apply (simp add: trancl_subset_times)
- apply blast+
+ apply (rule univalent_is_recfun)
+ apply (blast intro: wellfounded_trancl)
+ apply (rule trans_trancl)
+ apply (simp add: trancl_subset_times)
+apply blast
done
lemma (in M_recursion) Ord_wfrank_range [rule_format]:
- "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
+ "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
-apply (subgoal_tac "wellfounded_on(M, A, r^+)")
- prefer 2
- apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
-apply (erule wellfounded_on_induct2, assumption+)
-apply (simp add: trancl_subset_times)
-apply (blast intro: Ord_wfrank_separation, clarify)
+apply (drule wellfounded_trancl, assumption)
+apply (rule wellfounded_induct, assumption+)
+ apply (simp add:);
+ apply (blast intro: Ord_wfrank_separation);
+apply (clarify)
txt{*The reasoning in both cases is that we get @{term y} such that
- @{term "\<langle>y, x\<rangle> \<in> r^+"}. We find that
+ @{term "\<langle>y, x\<rangle> \<in> r^+"}. We find that
@{term "f`y = restrict(f, r^+ -`` {y})"}. *}
apply (rule OrdI [OF _ Ord_is_Transset])
txt{*An ordinal is a transitive set...*}
- apply (simp add: Transset_def)
+ apply (simp add: Transset_def)
apply clarify
- apply (frule apply_recfun2, assumption)
+ apply (frule apply_recfun2, assumption)
apply (force simp add: restrict_iff)
-txt{*...of ordinals. This second case requires the induction hyp.*}
-apply clarify
+txt{*...of ordinals. This second case requires the induction hyp.*}
+apply clarify
apply (rename_tac i y)
-apply (frule apply_recfun2, assumption)
-apply (frule is_recfun_imp_in_r, assumption)
-apply (frule is_recfun_restrict)
+apply (frule apply_recfun2, assumption)
+apply (frule is_recfun_imp_in_r, assumption)
+apply (frule is_recfun_restrict)
(*simp_all won't work*)
- apply (simp add: trans_on_trancl trancl_subset_times)+
+ apply (simp add: trans_trancl trancl_subset_times)+
apply (drule spec [THEN mp], assumption)
apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
- apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec)
+ apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec)
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
apply (blast dest: pair_components_in_M)
done
lemma (in M_recursion) Ord_range_wellfoundedrank:
- "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |]
+ "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |]
==> Ord (range(wellfoundedrank(M,r,A)))"
-apply (subgoal_tac "wellfounded_on(M, A, r^+)")
- prefer 2
- apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
-apply (frule trancl_subset_times)
+apply (frule wellfounded_trancl, assumption)
+apply (frule trancl_subset_times)
apply (simp add: wellfoundedrank_def)
apply (rule OrdI [OF _ Ord_is_Transset])
prefer 2
- txt{*by our previous result the range consists of ordinals.*}
- apply (blast intro: Ord_wfrank_range)
+ txt{*by our previous result the range consists of ordinals.*}
+ apply (blast intro: Ord_wfrank_range)
txt{*We still must show that the range is a transitive set.*}
apply (simp add: Transset_def, clarify, simp)
-apply (rename_tac x i f u)
-apply (frule is_recfun_imp_in_r, assumption)
-apply (subgoal_tac "M(u) & M(i) & M(x)")
- prefer 2 apply (blast dest: transM, clarify)
-apply (rule_tac a=u in rangeI)
-apply (rule ReplaceI)
- apply (rule_tac x=i in exI, simp)
+apply (rename_tac x i f u)
+apply (frule is_recfun_imp_in_r, assumption)
+apply (subgoal_tac "M(u) & M(i) & M(x)")
+ prefer 2 apply (blast dest: transM, clarify)
+apply (rule_tac a=u in rangeI)
+apply (rule ReplaceI)
+ apply (rule_tac x=i in exI, simp)
apply (rule_tac x="restrict(f, r^+ -`` {u})" in exI)
- apply (blast intro: is_recfun_restrict trans_on_trancl dest: apply_recfun2)
+ apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
apply blast
-txt{*Unicity requirement of Replacement*}
+txt{*Unicity requirement of Replacement*}
apply clarify
-apply (frule apply_recfun2, assumption)
-apply (simp add: trans_on_trancl is_recfun_cut)+
+apply (frule apply_recfun2, assumption)
+apply (simp add: trans_trancl is_recfun_cut)+
done
lemma (in M_recursion) function_wellfoundedrank:
- "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
+ "[| wellfounded(M,r); M(r); M(A)|]
==> function(wellfoundedrank(M,r,A))"
-apply (simp add: wellfoundedrank_def function_def, clarify)
+apply (simp add: wellfoundedrank_def function_def, clarify)
txt{*Uniqueness: repeated below!*}
apply (drule is_recfun_functional, assumption)
- apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
- apply (simp_all add: trancl_subset_times
- trans_trancl [THEN trans_imp_trans_on])
-apply (blast dest: transM)
+ apply (blast intro: wellfounded_trancl)
+ apply (simp_all add: trancl_subset_times trans_trancl)
done
lemma (in M_recursion) domain_wellfoundedrank:
- "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
+ "[| wellfounded(M,r); M(r); M(A)|]
==> domain(wellfoundedrank(M,r,A)) = A"
-apply (simp add: wellfoundedrank_def function_def)
+apply (simp add: wellfoundedrank_def function_def)
apply (rule equalityI, auto)
-apply (frule transM, assumption)
-apply (frule exists_wfrank, assumption+, clarify)
-apply (rule domainI)
+apply (frule transM, assumption)
+apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
+apply (rule domainI)
apply (rule ReplaceI)
-apply (rule_tac x="range(f)" in exI)
-apply simp
-apply (rule_tac x=f in exI, blast, assumption)
+ apply (rule_tac x="range(f)" in exI)
+ apply simp
+ apply (rule_tac x=f in exI, blast, assumption)
txt{*Uniqueness (for Replacement): repeated above!*}
apply clarify
apply (drule is_recfun_functional, assumption)
- apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
- apply (simp_all add: trancl_subset_times
- trans_trancl [THEN trans_imp_trans_on])
+ apply (blast intro: wellfounded_trancl)
+ apply (simp_all add: trancl_subset_times trans_trancl)
done
lemma (in M_recursion) wellfoundedrank_type:
- "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
+ "[| wellfounded(M,r); M(r); M(A)|]
==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
-apply (frule function_wellfoundedrank, assumption+)
-apply (frule function_imp_Pi)
- apply (simp add: wellfoundedrank_def relation_def)
- apply blast
+apply (frule function_wellfoundedrank [of r A], assumption+)
+apply (frule function_imp_Pi)
+ apply (simp add: wellfoundedrank_def relation_def)
+ apply blast
apply (simp add: domain_wellfoundedrank)
done
lemma (in M_recursion) Ord_wellfoundedrank:
- "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A; M(r); M(A) |]
+ "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A; M(r); M(A) |]
==> Ord(wellfoundedrank(M,r,A) ` a)"
by (blast intro: apply_funtype [OF wellfoundedrank_type]
Ord_in_Ord [OF Ord_range_wellfoundedrank])
lemma (in M_recursion) wellfoundedrank_eq:
"[| is_recfun(r^+, a, %x. range, f);
- wellfounded(M,r); a \<in> A; r \<subseteq> A*A; M(f); M(r); M(A)|]
+ wellfounded(M,r); a \<in> A; M(f); M(r); M(A)|]
==> wellfoundedrank(M,r,A) ` a = range(f)"
-apply (rule apply_equality)
- prefer 2 apply (blast intro: wellfoundedrank_type )
+apply (rule apply_equality)
+ prefer 2 apply (blast intro: wellfoundedrank_type)
apply (simp add: wellfoundedrank_def)
apply (rule ReplaceI)
- apply (rule_tac x="range(f)" in exI)
- apply blast
+ apply (rule_tac x="range(f)" in exI)
+ apply blast
apply assumption
-txt{*Unicity requirement of Replacement*}
+txt{*Unicity requirement of Replacement*}
apply clarify
apply (drule is_recfun_functional, assumption)
- apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
- apply (simp_all add: trancl_subset_times
- trans_trancl [THEN trans_imp_trans_on])
-apply (blast dest: transM)
+ apply (blast intro: wellfounded_trancl)
+ apply (simp_all add: trancl_subset_times trans_trancl)
done
lemma (in M_recursion) wellfoundedrank_lt:
"[| <a,b> \<in> r;
- wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
+ wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
-apply (subgoal_tac "wellfounded_on(M, A, r^+)")
- prefer 2
- apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
+apply (frule wellfounded_trancl, assumption)
apply (subgoal_tac "a\<in>A & b\<in>A")
prefer 2 apply blast
-apply (simp add: lt_def Ord_wellfoundedrank, clarify)
-apply (frule exists_wfrank [of concl: _ b], assumption+, clarify)
+apply (simp add: lt_def Ord_wellfoundedrank, clarify)
+apply (frule exists_wfrank [of concl: _ b], assumption+, clarify)
apply (rename_tac fb)
-apply (frule is_recfun_restrict [of concl: _ a])
- apply (rule trans_on_trancl, assumption)
- apply (simp_all add: r_into_trancl trancl_subset_times)
+apply (frule is_recfun_restrict [of concl: "r^+" a])
+ apply (rule trans_trancl, assumption)
+ apply (simp_all add: r_into_trancl trancl_subset_times)
txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
-apply (simp add: wellfoundedrank_eq)
+apply (simp add: wellfoundedrank_eq)
apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
apply (simp_all add: transM [of a])
txt{*We have used equations for wellfoundedrank and now must use some
for @{text is_recfun}. *}
-apply (rule_tac a=a in rangeI)
-apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
- r_into_trancl apply_recfun r_into_trancl)
+apply (rule_tac a=a in rangeI)
+apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
+ r_into_trancl apply_recfun r_into_trancl)
done
lemma (in M_recursion) wellfounded_imp_subset_rvimage:
- "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
+ "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
apply (rule_tac x="wellfoundedrank(M,r,A)" in exI)
-apply (simp add: Ord_range_wellfoundedrank, clarify)
-apply (frule subsetD, assumption, clarify)
+apply (simp add: Ord_range_wellfoundedrank, clarify)
+apply (frule subsetD, assumption, clarify)
apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD])
-apply (blast intro: apply_rangeI wellfoundedrank_type)
+apply (blast intro: apply_rangeI wellfoundedrank_type)
done
-lemma (in M_recursion) wellfounded_imp_wf:
- "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
+lemma (in M_recursion) wellfounded_imp_wf:
+ "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
intro: wf_rvimage_Ord [THEN wf_subset])
-lemma (in M_recursion) wellfounded_on_imp_wf_on:
- "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
-apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
+lemma (in M_recursion) wellfounded_on_imp_wf_on:
+ "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
+apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
apply (rule wellfounded_imp_wf)
-apply (simp_all add: relation_def)
+apply (simp_all add: relation_def)
done
-theorem (in M_recursion) wf_abs [simp]:
+theorem (in M_recursion) wf_abs [simp]:
"[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
-by (blast intro: wellfounded_imp_wf wf_imp_relativized)
+by (blast intro: wellfounded_imp_wf wf_imp_relativized)
-theorem (in M_recursion) wf_on_abs [simp]:
+theorem (in M_recursion) wf_on_abs [simp]:
"[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
-by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
+by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
end
--- a/src/ZF/Constructible/WFrec.thy Wed Jun 26 12:17:21 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Wed Jun 26 18:31:20 2002 +0200
@@ -37,71 +37,75 @@
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
done
-lemma trans_on_Int_eq [simp]:
- "[| trans[A](r); <y,x> \<in> r; r \<subseteq> A*A |]
+(*????GET RID OF [simp]*)
+lemma trans_Int_eq [simp]:
+ "[| trans(r); <y,x> \<in> r |]
==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
-by (blast intro: trans_onD)
+by (blast intro: transD)
-lemma trans_on_Int_eq2 [simp]:
- "[| trans[A](r); <y,x> \<in> r; r \<subseteq> A*A |]
+lemma trans_Int_eq2 [simp]:
+ "[| trans(r); <y,x> \<in> r |]
==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
-by (blast intro: trans_onD)
+by (blast intro: transD)
-text{*Stated using @{term "trans[A](r)"} rather than
+text{*Stated using @{term "trans(r)"} rather than
@{term "transitive_rel(M,A,r)"} because the latter rewrites to
the former anyway, by @{text transitive_rel_abs}.
- As always, theorems should be expressed in simplified form.*}
+ As always, theorems should be expressed in simplified form.
+ The last three M-premises are redundant because of @{term "M(r)"},
+ but without them we'd have to undertake
+ more work to set up the induction formula.*}
lemma (in M_axioms) is_recfun_equal [rule_format]:
"[|is_recfun(r,a,H,f); is_recfun(r,b,H,g);
- wellfounded_on(M,A,r); trans[A](r);
- M(A); M(f); M(g); M(a); M(b);
- r \<subseteq> A*A; x\<in>A |]
+ wellfounded(M,r); trans(r);
+ M(f); M(g); M(r); M(x); M(a); M(b) |]
==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x"
apply (frule_tac f="f" in is_recfun_type)
apply (frule_tac f="g" in is_recfun_type)
apply (simp add: is_recfun_def)
-apply (erule wellfounded_on_induct2, assumption+)
-apply (force intro: is_recfun_separation, clarify)
+apply (erule_tac a=x in wellfounded_induct)
+apply assumption+
+txt{*Separation to justify the induction*}
+ apply (force intro: is_recfun_separation)
+txt{*Now the inductive argument itself*}
+apply (clarify );
apply (erule ssubst)+
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
apply (rename_tac x1)
apply (rule_tac t="%z. H(x1,z)" in subst_context)
apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g")
- apply (blast intro: trans_onD)
+ apply (blast intro: transD)
apply (simp add: apply_iff)
-apply (blast intro: trans_onD sym)
+apply (blast intro: transD sym)
done
lemma (in M_axioms) is_recfun_cut:
"[|is_recfun(r,a,H,f); is_recfun(r,b,H,g);
- wellfounded_on(M,A,r); trans[A](r);
- M(A); M(f); M(g); M(a); M(b);
- r \<subseteq> A*A; <b,a>\<in>r |]
+ wellfounded(M,r); trans(r);
+ M(f); M(g); M(r); <b,a> \<in> r |]
==> restrict(f, r-``{b}) = g"
apply (frule_tac f="f" in is_recfun_type)
apply (rule fun_extension)
-apply (blast intro: trans_onD restrict_type2)
+apply (blast intro: transD restrict_type2)
apply (erule is_recfun_type, simp)
-apply (blast intro: is_recfun_equal trans_onD)
+apply (blast intro: is_recfun_equal transD dest: transM)
done
lemma (in M_axioms) is_recfun_functional:
"[|is_recfun(r,a,H,f); is_recfun(r,a,H,g);
- wellfounded_on(M,A,r); trans[A](r);
- M(A); M(f); M(g); M(a);
- r \<subseteq> A*A |]
+ wellfounded(M,r); trans(r);
+ M(f); M(g); M(r) |]
==> f=g"
apply (rule fun_extension)
apply (erule is_recfun_type)+
-apply (blast intro!: is_recfun_equal)
+apply (blast intro!: is_recfun_equal dest: transM)
done
text{*Tells us that is_recfun can (in principle) be relativized.*}
lemma (in M_axioms) is_recfun_relativize:
- "[| M(r); M(a); M(f);
- \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==>
- is_recfun(r,a,H,f) <->
+ "[| M(r); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
+ ==> is_recfun(r,a,H,f) <->
(\<forall>z. z \<in> f <-> (\<exists>x y. M(x) & M(y) & z=<x,y> & <x,a> \<in> r &
y = H(x, restrict(f, r-``{x}))))";
apply (simp add: is_recfun_def vimage_closed restrict_closed lam_def)
@@ -118,7 +122,7 @@
prefer 2
apply (simp add: function_def)
apply (frule pair_components_in_M, assumption)
- apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed)
+ apply (simp add: is_recfun_imp_function function_restrictI)
done
(* ideas for further weaking the H-closure premise:
@@ -136,23 +140,23 @@
*)
lemma (in M_axioms) is_recfun_restrict:
- "[| wellfounded_on(M,A,r); trans[A](r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r;
- M(A); M(r); M(f);
- \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)); r \<subseteq> A * A |]
+ "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r;
+ M(r); M(f);
+ \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
==> is_recfun(r, y, H, restrict(f, r -`` {y}))"
apply (frule pair_components_in_M, assumption, clarify)
apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff)
apply safe
apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff])
apply (frule_tac x=xa in pair_components_in_M, assumption)
- apply (frule_tac x=xa in apply_recfun, blast intro: trans_onD)
+ apply (frule_tac x=xa in apply_recfun, blast intro: transD)
apply (simp add: is_recfun_type [THEN apply_iff]
- is_recfun_imp_function function_restrictI)
-apply (blast intro: apply_recfun dest: trans_onD)+
+ is_recfun_imp_function function_restrictI)
+apply (blast intro: apply_recfun dest: transD)
done
lemma (in M_axioms) restrict_Y_lemma:
- "[| wellfounded_on(M,A,r); trans[A](r); M(A); M(r); r \<subseteq> A \<times> A;
+ "[| wellfounded(M,r); trans(r); M(r);
\<forall>x g. M(x) \<and> M(g) & function(g) --> M(H(x,g)); M(Y);
\<forall>b. M(b) -->
b \<in> Y <->
@@ -161,10 +165,10 @@
(\<exists>g. M(g) \<and> b = \<langle>x,y\<rangle> \<and> is_recfun(r,x,H,g) \<and> y = H(x,g)));
\<langle>x,a1\<rangle> \<in> r; M(f); is_recfun(r,x,H,f) |]
==> restrict(Y, r -`` {x}) = f"
-apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:Y <-> <y,z>:f")
-apply (simp (no_asm_simp) add: restrict_def)
-apply (thin_tac "All(?P)")+ --{*essential for efficiency*}
-apply (frule is_recfun_type [THEN fun_is_rel], blast)
+apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y <-> <y,z>:f")
+ apply (simp (no_asm_simp) add: restrict_def)
+ apply (thin_tac "All(?P)")+ --{*essential for efficiency*}
+ apply (frule is_recfun_type [THEN fun_is_rel], blast)
apply (frule pair_components_in_M, assumption, clarify)
apply (rule iffI)
apply (frule_tac y="<y,z>" in transM, assumption )
@@ -174,17 +178,16 @@
txt{*Opposite inclusion: something in f, show in Y*}
apply (frule_tac y="<y,z>" in transM, assumption, simp)
apply (rule_tac x=y in bexI)
-prefer 2 apply (blast dest: trans_onD)
+prefer 2 apply (blast dest: transD)
apply (rule_tac x=z in exI, simp)
apply (rule_tac x="restrict(f, r -`` {y})" in exI)
apply (simp add: vimage_closed restrict_closed is_recfun_restrict
apply_recfun is_recfun_type [THEN apply_iff])
done
-(*FIXME: use this lemma just below*)
text{*For typical applications of Replacement for recursive definitions*}
lemma (in M_axioms) univalent_is_recfun:
- "[|wellfounded_on(M,A,r); trans[A](r); r \<subseteq> A*A; M(r); M(A)|]
+ "[|wellfounded(M,r); trans(r); M(r)|]
==> univalent (M, A, \<lambda>x p. \<exists>y. M(y) &
(\<exists>f. M(f) & p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f)))"
apply (simp add: univalent_def)
@@ -194,69 +197,67 @@
text{*Proof of the inductive step for @{text exists_is_recfun}, since
we must prove two versions.*}
lemma (in M_axioms) exists_is_recfun_indstep:
- "[|a1 \<in> A; \<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f));
- wellfounded_on(M,A,r); trans[A](r);
+ "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f));
+ wellfounded(M,r); trans(r); M(r); M(a1);
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
- M(A); M(r); r \<subseteq> A * A;
\<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g))|]
==> \<exists>f. M(f) & is_recfun(r,a1,H,f)"
-apply (frule_tac y=a1 in transM, assumption)
apply (drule_tac A="r-``{a1}" in strong_replacementD)
- apply blast
+ apply blast
txt{*Discharge the "univalent" obligation of Replacement*}
- apply (clarsimp simp add: univalent_def)
- apply (blast dest!: is_recfun_functional)
+ apply (simp add: univalent_is_recfun)
txt{*Show that the constructed object satisfies @{text is_recfun}*}
apply clarify
apply (rule_tac x=Y in exI)
-apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed)
+apply (simp (no_asm_simp) add: is_recfun_relativize)
(*Tried using is_recfun_iff2 here. Much more simplification takes place
because an assumption can kick in. Not sure how to relate the new
proof state to the current one.*)
apply safe
-txt{*Show that elements of @{term Y} are in the right relationship.*}
-apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec)
-apply (erule impE, blast intro: transM)
-txt{*We have an element of @{term Y}, so we have x, y, z*}
-apply (frule_tac y=z in transM, assumption, clarify)
-apply (simp add: vimage_closed restrict_closed restrict_Y_lemma [of A r H])
+ txt{*Show that elements of @{term Y} are in the right relationship.*}
+ apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec)
+ apply (erule impE, blast intro: transM)
+ txt{*We have an element of @{term Y}, so we have x, y, z*}
+ apply (frule_tac y=z in transM, assumption, clarify)
+ apply (simp add: restrict_Y_lemma [of r H])
txt{*one more case*}
-apply (simp add: vimage_closed restrict_closed )
+apply (simp)
apply (rule_tac x=x in bexI)
-prefer 2 apply blast
+ prefer 2 apply blast
apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI)
-apply (simp add: vimage_closed restrict_closed )
+apply (simp)
apply (drule_tac x1=x in spec [THEN mp], assumption, clarify)
apply (rule_tac x=f in exI)
-apply (simp add: restrict_Y_lemma [of A r H])
+apply (simp add: restrict_Y_lemma [of r H])
done
-
text{*Relativized version, when we have the (currently weaker) premise
- @{term "wellfounded_on(M,A,r)"}*}
+ @{term "wellfounded(M,r)"}*}
lemma (in M_axioms) wellfounded_exists_is_recfun:
- "[|wellfounded_on(M,A,r); trans[A](r); a\<in>A;
- separation(M, \<lambda>x. x \<in> A --> ~ (\<exists>f. M(f) \<and> is_recfun(r, x, H, f)));
+ "[|wellfounded(M,r); trans(r);
+ separation(M, \<lambda>x. ~ (\<exists>f. M(f) \<and> is_recfun(r, x, H, f)));
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
- M(A); M(r); r \<subseteq> A*A;
+ M(r); M(a);
\<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
-apply (rule wellfounded_on_induct2, assumption+, clarify)
+apply (rule wellfounded_induct, assumption+, clarify)
apply (rule exists_is_recfun_indstep, assumption+)
done
-lemma (in M_axioms) wf_exists_is_recfun:
- "[|wf[A](r); trans[A](r); a\<in>A;
+lemma (in M_axioms) wf_exists_is_recfun [rule_format]:
+ "[|wf(r); trans(r);
strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
- M(A); M(r); r \<subseteq> A*A;
+ M(r);
\<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
- ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
-apply (rule wf_on_induct2, assumption+)
-apply (frule wf_on_imp_relativized)
-apply (rule exists_is_recfun_indstep, assumption+)
+ ==> M(a) --> (\<exists>f. M(f) & is_recfun(r,a,H,f))"
+apply (rule wf_induct, assumption+)
+apply (frule wf_imp_relativized)
+apply (intro impI)
+apply (rule exists_is_recfun_indstep)
+ apply (blast dest: pair_components_in_M)+
done
constdefs
@@ -377,12 +378,10 @@
lemma (in M_recursion) exists_oadd:
"[| Ord(j); M(i); M(j) |]
==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
-apply (rule wf_exists_is_recfun)
-apply (rule wf_Memrel [THEN wf_imp_wf_on])
-apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)
-apply (rule succI1)
-apply (blast intro: oadd_strong_replacement')
-apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
+ apply (simp add: );
+ apply (blast intro: oadd_strong_replacement')
+ apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
done
lemma (in M_recursion) exists_oadd_fun:
@@ -491,12 +490,10 @@
lemma (in M_recursion) exists_omult:
"[| Ord(j); M(i); M(j) |]
==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
-apply (rule wf_exists_is_recfun)
-apply (rule wf_Memrel [THEN wf_imp_wf_on])
-apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)
-apply (rule succI1)
-apply (blast intro: omult_strong_replacement')
-apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
+ apply (simp add: );
+ apply (blast intro: omult_strong_replacement')
+ apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
apply (blast intro: the_omult_eqns_closed)
done