--- a/src/ZF/Constructible/WFrec.thy Fri Aug 16 16:41:48 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Fri Aug 16 17:19:43 2002 +0200
@@ -9,6 +9,8 @@
theory WFrec = Wellorderings:
+subsection{*General Lemmas*}
+
(*Many of these might be useful in WF.thy*)
lemma apply_recfun2:
@@ -70,6 +72,8 @@
apply (blast intro: sym)+
done
+subsection{*Reworking of the Recursion Theory Within @{term M}*}
+
lemma (in M_axioms) is_recfun_separation':
"[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
M(r); M(f); M(g); M(a); M(b) |]
@@ -150,20 +154,6 @@
apply (simp add: is_recfun_imp_function function_restrictI)
done
-(* ideas for further weaking the H-closure premise:
-apply (drule spec [THEN spec])
-apply (erule mp)
-apply (intro conjI)
-apply (blast dest!: pair_components_in_M)
-apply (blast intro!: function_restrictI dest!: pair_components_in_M)
-apply (blast intro!: function_restrictI dest!: pair_components_in_M)
-apply (simp only: subset_iff domain_iff restrict_iff vimage_iff)
-apply (simp add: vimage_singleton_iff)
-apply (intro allI impI conjI)
-apply (blast intro: transM dest!: pair_components_in_M)
-prefer 4;apply blast
-*)
-
lemma (in M_axioms) is_recfun_restrict:
"[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r;
M(r); M(f);
@@ -280,6 +270,9 @@
apply (blast dest: transM del: rev_rallE, assumption+)
done
+
+subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
+
constdefs
M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
"M_is_recfun(M,MH,r,a,f) ==
@@ -339,6 +332,10 @@
by (simp add: is_wfrec_def wfrec_replacement_def)
+subsection{*Ordinal Arithmetic: Two Examples of Recursion*}
+
+subsubsection{*Ordinal Addition*}
+
(*FIXME: update to use new techniques!!*)
constdefs
(*This expresses ordinal addition in the language of ZF. It also
@@ -485,7 +482,7 @@
done
-text{*Ordinal Multiplication*}
+subsubsection{*Ordinal Multiplication*}
lemma omult_eqns_unique:
"[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";