--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Datatype_absolute.thy Mon Jul 01 18:16:18 2002 +0200
@@ -0,0 +1,173 @@
+theory Datatype_absolute = WF_absolute:
+
+(*Epsilon.thy*)
+lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
+apply (insert arg_subset_eclose [of "{i}"], simp)
+apply (frule eclose_subset, blast)
+done
+
+lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
+apply (rule equalityI)
+apply (erule eclose_sing_Ord)
+apply (rule succ_subset_eclose_sing)
+done
+
+(*Ordinal.thy*)
+lemma relation_Memrel: "relation(Memrel(A))"
+by (simp add: relation_def Memrel_def, blast)
+
+lemma (in M_axioms) nat_case_closed:
+ "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
+apply (case_tac "k=0", simp)
+apply (case_tac "\<exists>m. k = succ(m)")
+apply force
+apply (simp add: nat_case_def)
+done
+
+
+subsection{*The lfp of a continuous function can be expressed as a union*}
+
+constdefs
+ contin :: "[i=>i]=>o"
+ "contin(h) == (\<forall>A. A\<noteq>0 --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"
+
+lemma bnd_mono_iterates_subset: "[|bnd_mono(D, h); n \<in> nat|] ==> h^n (0) <= D"
+apply (induct_tac n)
+ apply (simp_all add: bnd_mono_def, blast)
+done
+
+
+lemma contin_iterates_eq:
+ "contin(h) \<Longrightarrow> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
+apply (simp add: contin_def)
+apply (rule trans)
+apply (rule equalityI)
+ apply (simp_all add: UN_subset_iff)
+ apply safe
+ apply (erule_tac [2] natE)
+ apply (rule_tac a="succ(x)" in UN_I)
+ apply simp_all
+apply blast
+done
+
+lemma lfp_subset_Union:
+ "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) <= (\<Union>n\<in>nat. h^n(0))"
+apply (rule lfp_lowerbound)
+ apply (simp add: contin_iterates_eq)
+apply (simp add: contin_def bnd_mono_iterates_subset UN_subset_iff)
+done
+
+lemma Union_subset_lfp:
+ "bnd_mono(D,h) ==> (\<Union>n\<in>nat. h^n(0)) <= lfp(D,h)"
+apply (simp add: UN_subset_iff)
+apply (rule ballI)
+apply (induct_tac x, simp_all)
+apply (rule subset_trans [of _ "h(lfp(D,h))"])
+ apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] )
+apply (erule lfp_lemma2)
+done
+
+lemma lfp_eq_Union:
+ "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) = (\<Union>n\<in>nat. h^n(0))"
+by (blast del: subsetI
+ intro: lfp_subset_Union Union_subset_lfp)
+
+
+subsection {*lists without univ*}
+
+lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ
+ Pair_in_univ zero_in_univ
+
+lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
+apply (rule bnd_monoI)
+ apply (intro subset_refl zero_subset_univ A_subset_univ
+ sum_subset_univ Sigma_subset_univ)
+ apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI)
+done
+
+lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
+by (simp add: contin_def, blast)
+
+text{*Re-expresses lists using sum and product*}
+lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
+apply (simp add: list_def)
+apply (rule equalityI)
+ apply (rule lfp_lowerbound)
+ prefer 2 apply (rule lfp_subset)
+ apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
+ apply (simp add: Nil_def Cons_def)
+ apply blast
+txt{*Opposite inclusion*}
+apply (rule lfp_lowerbound)
+ prefer 2 apply (rule lfp_subset)
+apply (clarify, subst lfp_unfold [OF list.bnd_mono])
+apply (simp add: Nil_def Cons_def)
+apply (blast intro: datatype_univs
+ dest: lfp_subset [THEN subsetD])
+done
+
+text{*Re-expresses lists using "iterates", no univ.*}
+lemma list_eq_Union:
+ "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
+by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
+
+
+subsection {*Absoluteness for "Iterates"*}
+
+lemma (in M_trancl) iterates_relativize:
+ "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
+ strong_replacement(M,
+ \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
+ is_recfun (Memrel(succ(n)), x,
+ \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
+ y = nat_case(v, \<lambda>m. F(g`m), x))|]
+ ==> iterates(F,n,v) = z <->
+ (\<exists>g[M]. is_recfun(Memrel(succ(n)), n,
+ \<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n), g) &
+ z = nat_case(v, \<lambda>m. F(g`m), n))"
+by (simp add: iterates_nat_def recursor_def transrec_def
+ eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M
+ wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
+
+
+lemma (in M_wfrank) iterates_closed [intro,simp]:
+ "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
+ strong_replacement(M,
+ \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
+ is_recfun (Memrel(succ(n)), x,
+ \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
+ y = nat_case(v, \<lambda>m. F(g`m), x))|]
+ ==> M(iterates(F,n,v))"
+by (simp add: iterates_nat_def recursor_def transrec_def
+ eclose_sing_Ord_eq trans_wfrec_closed nat_into_M
+ wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
+
+
+locale M_datatypes = M_wfrank +
+(*THEY NEED RELATIVIZATION*)
+ assumes list_replacement1:
+ "[|M(A); n \<in> nat|] ==>
+ strong_replacement(M,
+ \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
+ is_recfun (Memrel(succ(n)), x,
+ \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
+ y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
+ and list_replacement2':
+ "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
+
+
+lemma (in M_datatypes) list_replacement1':
+ "[|M(A); n \<in> nat|]
+ ==> strong_replacement
+ (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> &
+ is_recfun (Memrel(succ(n)), x,
+ \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) &
+ z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
+by (insert list_replacement1, simp)
+
+
+lemma (in M_datatypes) list_closed [intro,simp]:
+ "M(A) ==> M(list(A))"
+by (simp add: list_eq_Union list_replacement1' list_replacement2')
+
+end
--- a/src/ZF/Constructible/L_axioms.thy Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Mon Jul 01 18:16:18 2002 +0200
@@ -62,8 +62,7 @@
lemma replacement: "replacement(L,P)"
apply (simp add: replacement_def, clarify)
-apply (frule LReplace_in_L, assumption+)
-apply clarify
+apply (frule LReplace_in_L, assumption+, clarify)
apply (rule_tac x=Y in exI)
apply (simp add: Replace_iff univalent_def, blast)
done
--- a/src/ZF/Constructible/Normal.thy Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/Normal.thy Mon Jul 01 18:16:18 2002 +0200
@@ -316,8 +316,7 @@
--"this lemma is @{thm increasing_LimitI [no_vars]}"
apply (blast intro: UN_upper_lt [of "1"] Normal_imp_Ord
Ord_UN Ord_iterates lt_imp_0_lt
- iterates_Normal_increasing)
-apply clarify
+ iterates_Normal_increasing, clarify)
apply (rule bexI)
apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal])
apply (rule UN_I, erule nat_succI)
--- a/src/ZF/Constructible/ROOT.ML Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/ROOT.ML Mon Jul 01 18:16:18 2002 +0200
@@ -9,3 +9,4 @@
use_thy "Reflection";
use_thy "WF_absolute";
use_thy "L_axioms";
+use_thy "Datatype_absolute";
--- a/src/ZF/Constructible/Reflection.thy Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/Reflection.thy Mon Jul 01 18:16:18 2002 +0200
@@ -55,7 +55,7 @@
theorem (in reflection) Not_reflection [intro]:
"Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
-by (simp add: Reflects_def);
+by (simp add: Reflects_def)
theorem (in reflection) And_reflection [intro]:
"[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
--- a/src/ZF/Constructible/Relative.thy Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Mon Jul 01 18:16:18 2002 +0200
@@ -2,6 +2,11 @@
theory Relative = Main:
+(*func.thy*)
+lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
+by (simp add: succ_def mem_not_refl cons_fun_eq)
+
+
subsection{* Relativized versions of standard set-theoretic concepts *}
constdefs
@@ -96,6 +101,10 @@
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
(\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
+ is_funspace :: "[i=>o,i,i,i] => o"
+ "is_funspace(M,A,B,F) ==
+ \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
+
composition :: "[i=>o,i,i,i] => o"
"composition(M,r,s,t) ==
\<forall>p. M(p) --> (p \<in> t <->
@@ -385,29 +394,28 @@
and Union_ax: "Union_ax(M)"
and power_ax: "power_ax(M)"
and replacement: "replacement(M,P)"
- and M_nat: "M(nat)" (*i.e. the axiom of infinity*)
+ and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*)
and Inter_separation:
- "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
+ "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
and cartprod_separation:
"[| M(A); M(B) |]
==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"
and image_separation:
"[| M(A); M(r) |]
- ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & (\<exists>x\<in>A. M(x) & pair(M,x,y,p)))"
+ ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
and vimage_separation:
"[| M(A); M(r) |]
- ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
+ ==> separation(M, \<lambda>x. \<exists>p[M]. p\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,p)))"
and converse_separation:
"M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r.
M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
and restrict_separation:
- "M(A)
- ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
+ "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
and comp_separation:
"[| M(r); M(s) |]
- ==> separation(M, \<lambda>xz. \<exists>x y z. M(x) & M(y) & M(z) &
- (\<exists>xy\<in>s. \<exists>yz\<in>r. M(xy) & M(yz) &
- pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
+ ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
+ pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &
+ xy\<in>s & yz\<in>r)"
and pred_separation:
"[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
and Memrel_separation:
@@ -418,6 +426,10 @@
==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &
ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
order_isomorphism(M,par,r,x,mx,g))"
+ and funspace_succ_replacement:
+ "M(n) ==>
+ strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M].
+ pair(M,f,b,p) & pair(M,n,b,nb) & z = {cons(nb,f)})"
and well_ord_iso_separation:
"[| M(A); M(f); M(r) |]
==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) & (\<exists>p. M(p) &
@@ -440,15 +452,23 @@
ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
-lemma (in M_axioms) Ball_abs [simp]:
+lemma (in M_axioms) ball_abs [simp]:
"M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))"
by (blast intro: transM)
-lemma (in M_axioms) Bex_abs [simp]:
+lemma (in M_axioms) rall_abs [simp]:
+ "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))"
+by (blast intro: transM)
+
+lemma (in M_axioms) bex_abs [simp]:
"M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))"
by (blast intro: transM)
-lemma (in M_axioms) Ball_iff_equiv:
+lemma (in M_axioms) rex_abs [simp]:
+ "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))"
+by (blast intro: transM)
+
+lemma (in M_axioms) ball_iff_equiv:
"M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <->
(\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"
by (blast intro: transM)
@@ -570,11 +590,9 @@
"[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
==> strong_replacement(M,P)"
apply (simp add: strong_replacement_def, clarify)
-apply (frule replacementD [OF replacement], assumption)
-apply clarify
+apply (frule replacementD [OF replacement], assumption, clarify)
apply (drule_tac x=A in spec, clarify)
-apply (drule_tac z=Y in separationD, assumption)
-apply clarify
+apply (drule_tac z=Y in separationD, assumption, clarify)
apply (blast dest: transM)
done
@@ -692,6 +710,10 @@
"[| M(A); M(B) |] ==> M(A*B)"
by (frule cartprod_closed_lemma, assumption, force)
+lemma (in M_axioms) sum_closed [intro,simp]:
+ "[| M(A); M(B) |] ==> M(A+B)"
+by (simp add: sum_def)
+
lemma (in M_axioms) image_closed [intro,simp]:
"[| M(A); M(r) |] ==> M(r``A)"
apply (simp add: image_iff_Collect)
@@ -758,9 +780,9 @@
"[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
apply (simp add: is_converse_def)
apply (rule iffI)
- prefer 2 apply (blast intro: elim:);
+ prefer 2 apply blast
apply (rule M_equalityI)
- apply (simp add: )
+ apply simp
apply (blast dest: transM)+
done
@@ -819,20 +841,20 @@
"[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
==> function(z)"
apply (rotate_tac 1)
-apply (simp add: restriction_def Ball_iff_equiv)
+apply (simp add: restriction_def ball_iff_equiv)
apply (unfold function_def, blast)
done
lemma (in M_axioms) restriction_abs [simp]:
"[| M(f); M(A); M(z) |]
==> restriction(M,f,A,z) <-> z = restrict(f,A)"
-apply (simp add: Ball_iff_equiv restriction_def restrict_def)
+apply (simp add: ball_iff_equiv restriction_def restrict_def)
apply (blast intro!: equalityI dest: transM)
done
lemma (in M_axioms) M_restrict_iff:
- "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
+ "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
by (simp add: restrict_def, blast dest: transM)
lemma (in M_axioms) restrict_closed [intro,simp]:
@@ -845,8 +867,7 @@
"[| M(r); M(s) |]
==> r O s =
{xz \<in> domain(s) * range(r).
- \<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) &
- xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))}"
+ \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r}"
apply (simp add: comp_def)
apply (rule equalityI)
apply clarify
@@ -902,6 +923,8 @@
apply (frule Inter_closed, force+)
done
+subsection{*Functions and function space*}
+
text{*M contains all finite functions*}
lemma (in M_axioms) finite_fun_closed_lemma [rule_format]:
"[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
@@ -919,6 +942,39 @@
"[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
by (blast intro: finite_fun_closed_lemma)
+text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
+all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
+lemma (in M_axioms) is_funspace_abs [simp]:
+ "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
+apply (simp add: is_funspace_def)
+apply (rule iffI)
+ prefer 2 apply blast
+apply (rule M_equalityI)
+ apply simp_all
+done
+
+lemma (in M_axioms) succ_fun_eq2:
+ "[|M(B); M(n->B)|] ==>
+ succ(n) -> B =
+ \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
+apply (simp add: succ_fun_eq)
+apply (blast dest: transM)
+done
+
+lemma (in M_axioms) funspace_succ:
+ "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
+apply (insert funspace_succ_replacement [of n])
+apply (force simp add: succ_fun_eq2 univalent_def)
+done
+
+text{*@{term M} contains all finite function spaces. Needed to prove the
+absoluteness of transitive closure.*}
+lemma (in M_axioms) finite_funspace_closed [intro,simp]:
+ "[|n\<in>nat; M(B)|] ==> M(n->B)"
+apply (induct_tac n, simp)
+apply (simp add: funspace_succ nat_into_M)
+done
+
subsection{*Absoluteness for ordinals*}
text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
--- a/src/ZF/Constructible/WF_absolute.thy Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Mon Jul 01 18:16:18 2002 +0200
@@ -1,5 +1,20 @@
theory WF_absolute = WFrec:
+(*????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)
+
+
subsection{*Every well-founded relation is a subset of some inverse image of
an ordinal*}
@@ -127,7 +142,7 @@
tran_closure :: "[i=>o,i,i] => o"
"tran_closure(M,r,t) ==
- \<exists>s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)"
+ \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
locale M_trancl = M_axioms +
@@ -135,11 +150,14 @@
assumes rtrancl_separation:
"[| M(r); M(A) |] ==>
separation
- (M, \<lambda>p. \<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))"
+ (M, \<lambda>p. \<exists>n[M]. n\<in>nat &
+ (\<exists>f[M].
+ f \<in> succ(n) -> A &
+ (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) &
+ f`0 = x & f`n = y) &
+ (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
and wellfounded_trancl_separation:
- "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z)"
+ "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+)"
lemma (in M_trancl) rtran_closure_rtrancl:
@@ -165,7 +183,7 @@
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
+ Ord_succ_mem_iff M_nat nat_into_M
nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
done
@@ -215,11 +233,10 @@
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})")
+apply (subgoal_tac "M({x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+})")
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 intro: wellfounded_trancl_separation)
+apply (drule_tac x = "{x\<in>A. \<exists>w[M]. w \<in> Z & \<langle>w,x\<rangle> \<in> r^+}" in spec, safe)
apply (blast dest: transM, simp)
apply (rename_tac y w)
apply (drule_tac x=w in bspec, assumption, clarify)
@@ -228,22 +245,6 @@
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)
@@ -259,14 +260,14 @@
(*NEEDS RELATIVIZATION*)
-locale M_recursion = M_trancl +
+locale M_wfrank = M_trancl +
assumes wfrank_separation':
"M(r) ==>
separation
- (M, \<lambda>x. ~ (\<exists>f. M(f) & is_recfun(r^+, x, %x f. range(f), f)))"
+ (M, \<lambda>x. ~ (\<exists>f[M]. 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) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M].
pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
y = range(f))"
and Ord_wfrank_separation:
@@ -279,13 +280,13 @@
constdefs
wellfoundedrank :: "[i=>o,i,i] => i"
"wellfoundedrank(M,r,A) ==
- {p. x\<in>A, \<exists>y f. M(y) & M(f) &
+ {p. x\<in>A, \<exists>y[M]. \<exists>f[M].
p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
y = range(f)}"
-lemma (in M_recursion) exists_wfrank:
+lemma (in M_wfrank) exists_wfrank:
"[| wellfounded(M,r); M(a); M(r) |]
- ==> \<exists>f. M(f) & is_recfun(r^+, a, %x f. range(f), f)"
+ ==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)"
apply (rule wellfounded_exists_is_recfun)
apply (blast intro: wellfounded_trancl)
apply (rule trans_trancl)
@@ -294,7 +295,7 @@
apply (simp_all add: trancl_subset_times)
done
-lemma (in M_recursion) M_wellfoundedrank:
+lemma (in M_wfrank) M_wellfoundedrank:
"[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
apply (insert wfrank_strong_replacement' [of r])
apply (simp add: wellfoundedrank_def)
@@ -306,7 +307,7 @@
apply (simp add: trancl_subset_times, blast)
done
-lemma (in M_recursion) Ord_wfrank_range [rule_format]:
+lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
"[| 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 (drule wellfounded_trancl, assumption)
@@ -337,7 +338,7 @@
apply (blast dest: pair_components_in_M)
done
-lemma (in M_recursion) Ord_range_wellfoundedrank:
+lemma (in M_wfrank) Ord_range_wellfoundedrank:
"[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |]
==> Ord (range(wellfoundedrank(M,r,A)))"
apply (frule wellfounded_trancl, assumption)
@@ -349,23 +350,23 @@
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 (rename_tac x f i 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_trancl dest: apply_recfun2)
- apply blast
+ apply (rule_tac x=i in rexI, simp)
+ apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
+ apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
+ apply (simp, simp, blast)
txt{*Unicity requirement of Replacement*}
apply clarify
apply (frule apply_recfun2, assumption)
apply (simp add: trans_trancl is_recfun_cut)+
done
-lemma (in M_recursion) function_wellfoundedrank:
+lemma (in M_wfrank) function_wellfoundedrank:
"[| wellfounded(M,r); M(r); M(A)|]
==> function(wellfoundedrank(M,r,A))"
apply (simp add: wellfoundedrank_def function_def, clarify)
@@ -375,7 +376,7 @@
apply (simp_all add: trancl_subset_times trans_trancl)
done
-lemma (in M_recursion) domain_wellfoundedrank:
+lemma (in M_wfrank) domain_wellfoundedrank:
"[| wellfounded(M,r); M(r); M(A)|]
==> domain(wellfoundedrank(M,r,A)) = A"
apply (simp add: wellfoundedrank_def function_def)
@@ -384,9 +385,9 @@
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 (rule_tac x="range(f)" in rexI)
apply simp
- apply (rule_tac x=f in exI, blast, assumption)
+ apply (rule_tac x=f in rexI, blast, simp_all)
txt{*Uniqueness (for Replacement): repeated above!*}
apply clarify
apply (drule is_recfun_functional, assumption)
@@ -394,7 +395,7 @@
apply (simp_all add: trancl_subset_times trans_trancl)
done
-lemma (in M_recursion) wellfoundedrank_type:
+lemma (in M_wfrank) wellfoundedrank_type:
"[| wellfounded(M,r); M(r); M(A)|]
==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
apply (frule function_wellfoundedrank [of r A], assumption+)
@@ -404,13 +405,13 @@
apply (simp add: domain_wellfoundedrank)
done
-lemma (in M_recursion) Ord_wellfoundedrank:
+lemma (in M_wfrank) Ord_wellfoundedrank:
"[| 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:
+lemma (in M_wfrank) wellfoundedrank_eq:
"[| is_recfun(r^+, a, %x. range, f);
wellfounded(M,r); a \<in> A; M(f); M(r); M(A)|]
==> wellfoundedrank(M,r,A) ` a = range(f)"
@@ -418,9 +419,9 @@
prefer 2 apply (blast intro: wellfoundedrank_type)
apply (simp add: wellfoundedrank_def)
apply (rule ReplaceI)
- apply (rule_tac x="range(f)" in exI)
+ apply (rule_tac x="range(f)" in rexI)
apply blast
- apply assumption
+ apply simp_all
txt{*Unicity requirement of Replacement*}
apply clarify
apply (drule is_recfun_functional, assumption)
@@ -429,7 +430,7 @@
done
-lemma (in M_recursion) wellfoundedrank_lt:
+lemma (in M_wfrank) wellfoundedrank_lt:
"[| <a,b> \<in> r;
wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
@@ -454,7 +455,7 @@
done
-lemma (in M_recursion) wellfounded_imp_subset_rvimage:
+lemma (in M_wfrank) wellfounded_imp_subset_rvimage:
"[|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)
@@ -465,12 +466,12 @@
apply (blast intro: apply_rangeI wellfoundedrank_type)
done
-lemma (in M_recursion) wellfounded_imp_wf:
+lemma (in M_wfrank) 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:
+lemma (in M_wfrank) 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)
@@ -478,11 +479,11 @@
done
-theorem (in M_recursion) wf_abs [simp]:
+theorem (in M_wfrank) wf_abs [simp]:
"[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
by (blast intro: wellfounded_imp_wf wf_imp_relativized)
-theorem (in M_recursion) wf_on_abs [simp]:
+theorem (in M_wfrank) 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)
@@ -493,20 +494,20 @@
lemma (in M_trancl) wfrec_relativize:
"[|wf(r); M(a); M(r);
- strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
pair(M,x,y,z) &
is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) &
y = H(x, restrict(g, r -`` {x})));
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> wfrec(r,a,H) = z <->
- (\<exists>f. M(f) & is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) &
+ (\<exists>f[M]. is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) &
z = H(a,restrict(f,r-``{a})))"
apply (frule wf_trancl)
apply (simp add: wftrec_def wfrec_def, safe)
apply (frule wf_exists_is_recfun
[of concl: "r^+" a "\<lambda>x f. H(x, restrict(f, r -`` {x}))"])
apply (simp_all add: trans_trancl function_restrictI trancl_subset_times)
- apply (clarify, rule_tac x=f in exI)
+ apply (clarify, rule_tac x=x in rexI)
apply (simp_all add: the_recfun_eq trans_trancl trancl_subset_times)
done
@@ -516,10 +517,10 @@
before we can replace @{term "r^+"} by @{term r}. *}
theorem (in M_trancl) trans_wfrec_relativize:
"[|wf(r); trans(r); relation(r); M(r); M(a);
- strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
- ==> wfrec(r,a,H) = z <-> (\<exists>f. M(f) & is_recfun(r,a,H,f) & z = H(a,f))"
+ ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))"
by (simp cong: is_recfun_cong
add: wfrec_relativize trancl_eq_r
is_recfun_restrict_idem domain_restrict_idem)
@@ -527,11 +528,11 @@
lemma (in M_trancl) trans_eq_pair_wfrec_iff:
"[|wf(r); trans(r); relation(r); M(r); M(y);
- strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> y = <x, wfrec(r, x, H)> <->
- (\<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
+ (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
apply safe
apply (simp add: trans_wfrec_relativize [THEN iff_sym])
txt{*converse direction*}
@@ -543,7 +544,7 @@
subsection{*M is closed under well-founded recursion*}
text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
-lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
+lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
"[|wf(r); M(r);
strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
@@ -557,20 +558,20 @@
done
text{*Eliminates one instance of replacement.*}
-lemma (in M_recursion) wfrec_replacement_iff:
- "strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+lemma (in M_wfrank) wfrec_replacement_iff:
+ "strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <->
strong_replacement(M,
- \<lambda>x y. \<exists>f. M(f) & is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
+ \<lambda>x y. \<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
apply simp
apply (rule strong_replacement_cong, blast)
done
text{*Useful version for transitive relations*}
-theorem (in M_recursion) trans_wfrec_closed:
+theorem (in M_wfrank) trans_wfrec_closed:
"[|wf(r); trans(r); relation(r); M(r); M(a);
strong_replacement(M,
- \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ \<lambda>x z. \<exists>y[M]. \<exists>g[M].
pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
==> M(wfrec(r,a,H))"
@@ -582,13 +583,13 @@
section{*Absoluteness without assuming transitivity*}
lemma (in M_trancl) eq_pair_wfrec_iff:
"[|wf(r); M(r); M(y);
- strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
pair(M,x,y,z) &
is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) &
y = H(x, restrict(g, r -`` {x})));
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> y = <x, wfrec(r, x, H)> <->
- (\<exists>f. M(f) & is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) &
+ (\<exists>f[M]. is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) &
y = <x, H(x,restrict(f,r-``{x}))>)"
apply safe
apply (simp add: wfrec_relativize [THEN iff_sym])
@@ -597,7 +598,7 @@
apply (simp add: wfrec_relativize, blast)
done
-lemma (in M_recursion) wfrec_closed_lemma [rule_format]:
+lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
"[|wf(r); M(r);
strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
@@ -611,9 +612,9 @@
done
text{*Full version not assuming transitivity, but maybe not very useful.*}
-theorem (in M_recursion) wfrec_closed:
+theorem (in M_wfrank) wfrec_closed:
"[|wf(r); M(r); M(a);
- strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
pair(M,x,y,z) &
is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) &
y = H(x, restrict(g, r -`` {x})));
--- a/src/ZF/Constructible/WFrec.thy Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Mon Jul 01 18:16:18 2002 +0200
@@ -117,9 +117,7 @@
lemma (in M_axioms) is_recfun_functional:
"[|is_recfun(r,a,H,f); is_recfun(r,a,H,g);
- wellfounded(M,r); trans(r);
- M(f); M(g); M(r) |]
- ==> f=g"
+ 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 dest: transM)
@@ -183,9 +181,8 @@
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); M(Y);
\<forall>b. M(b) -->
b \<in> Y <->
- (\<exists>x\<in>r -`` {a1}.
- \<exists>y. M(y) \<and>
- (\<exists>g. M(g) \<and> b = \<langle>x,y\<rangle> \<and> is_recfun(r,x,H,g) \<and> y = H(x,g)));
+ (\<exists>x\<in>r -`` {a1}. \<exists>y[M]. \<exists>g[M].
+ b = \<langle>x,y\<rangle> & 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 "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y <-> <y,z>:f")
@@ -203,17 +200,17 @@
apply (frule_tac y="<y,z>" in transM, assumption, simp)
apply (rule_tac x=y in bexI)
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])
+apply (rule_tac x=z in rexI)
+apply (rule_tac x="restrict(f, r -`` {y})" in rexI)
+apply (simp_all add: is_recfun_restrict
+ apply_recfun is_recfun_type [THEN apply_iff])
done
text{*For typical applications of Replacement for recursive definitions*}
lemma (in M_axioms) univalent_is_recfun:
"[|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)))"
+ ==> univalent (M, A, \<lambda>x p.
+ \<exists>y[M]. \<exists>f[M]. p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f))"
apply (simp add: univalent_def)
apply (blast dest: is_recfun_functional)
done
@@ -221,60 +218,60 @@
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:
- "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f));
+ "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f[M]. 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));
+ strong_replacement(M, \<lambda>x z.
+ \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
- ==> \<exists>f. M(f) & is_recfun(r,a1,H,f)"
+ ==> \<exists>f[M]. is_recfun(r,a1,H,f)"
apply (drule_tac A="r-``{a1}" in strong_replacementD)
apply blast
txt{*Discharge the "univalent" obligation of Replacement*}
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 (rule_tac x=Y in rexI)
txt{*Unfold only the top-level occurrence of @{term is_recfun}*}
apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1])
-txt{*The big iff-formula defininng @{term Y} is now redundant*}
+txt{*The big iff-formula defining @{term Y} is now redundant*}
apply safe
apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H])
txt{*one more case*}
apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff)
apply (rename_tac x)
apply (rule_tac x=x in exI, simp)
-apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI)
+apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in rexI)
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 r H])
+apply (rename_tac f)
+apply (rule_tac x=f in rexI)
+apply (simp add: restrict_Y_lemma [of r H], simp_all)
done
text{*Relativized version, when we have the (currently weaker) premise
@{term "wellfounded(M,r)"}*}
lemma (in M_axioms) wellfounded_exists_is_recfun:
"[|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));
+ separation(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r, x, H, f)));
+ strong_replacement(M, \<lambda>x z.
+ \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
M(r); M(a);
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
- ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
+ ==> \<exists>f[M]. is_recfun(r,a,H,f)"
apply (rule wellfounded_induct, assumption+, clarify)
apply (rule exists_is_recfun_indstep, assumption+)
done
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(r);
+ "[|wf(r); trans(r); M(r);
+ strong_replacement(M, \<lambda>x z.
+ \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
- ==> M(a) --> (\<exists>f. M(f) & is_recfun(r,a,H,f))"
+ ==> M(a) --> (\<exists>f[M]. 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)+
+apply (rule exists_is_recfun_indstep)
+ apply (blast dest: transM del: rev_rallE, assumption+)
done
constdefs
@@ -346,24 +343,23 @@
fun_apply(M,f,j,fj) & fj = k"
-locale M_recursion = M_axioms +
+locale M_ord_arith = M_axioms +
assumes oadd_strong_replacement:
"[| M(i); M(j) |] ==>
strong_replacement(M,
- \<lambda>x z. \<exists>y f fx. M(y) & M(f) & M(fx) &
- pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) &
- image(M,f,x,fx) & y = i Un fx)"
+ \<lambda>x z. \<exists>y[M]. \<exists>f[M]. \<exists>fx[M]. pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) &
+ image(M,f,x,fx) & y = i Un fx)"
and omult_strong_replacement':
"[| M(i); M(j) |] ==>
- strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
- pair(M,x,y,z) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
+ z = <x,y> &
is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) &
y = (THE z. omult_eqns(i, x, g, z)))"
text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*}
-lemma (in M_recursion) is_oadd_fun_iff:
+lemma (in M_ord_arith) is_oadd_fun_iff:
"[| a\<le>j; M(i); M(j); M(a); M(f) |]
==> is_oadd_fun(M,i,j,a,f) <->
f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
@@ -377,10 +373,10 @@
done
-lemma (in M_recursion) oadd_strong_replacement':
+lemma (in M_ord_arith) oadd_strong_replacement':
"[| M(i); M(j) |] ==>
- strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
- pair(M,x,y,z) &
+ strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
+ z = <x,y> &
is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) &
y = i Un g``x)"
apply (insert oadd_strong_replacement [of i j])
@@ -389,28 +385,25 @@
done
-lemma (in M_recursion) exists_oadd:
+lemma (in M_ord_arith) 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)"
+ ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
- apply simp
- apply (blast intro: oadd_strong_replacement')
- apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+ apply (simp_all add: Memrel_type oadd_strong_replacement')
+done
+
+lemma (in M_ord_arith) exists_oadd_fun:
+ "[| Ord(j); M(i); M(j) |] ==> \<exists>f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)"
+apply (rule exists_oadd [THEN rexE])
+apply (erule Ord_succ, assumption, simp)
+apply (rename_tac f)
+apply (frule is_recfun_type)
+apply (rule_tac x=f in rexI)
+ apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
+ is_oadd_fun_iff Ord_trans [OF _ succI1], assumption)
done
-lemma (in M_recursion) exists_oadd_fun:
- "[| Ord(j); M(i); M(j) |]
- ==> \<exists>f. M(f) & is_oadd_fun(M,i,succ(j),succ(j),f)"
-apply (rule exists_oadd [THEN exE])
-apply (erule Ord_succ, assumption, simp)
-apply (rename_tac f, clarify)
-apply (frule is_recfun_type)
-apply (rule_tac x=f in exI)
-apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
- is_oadd_fun_iff Ord_trans [OF _ succI1])
-done
-
-lemma (in M_recursion) is_oadd_fun_apply:
+lemma (in M_ord_arith) is_oadd_fun_apply:
"[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |]
==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
apply (simp add: is_oadd_fun_iff lt_Ord2, clarify)
@@ -419,7 +412,7 @@
apply (simp add: image_fun, blast)
done
-lemma (in M_recursion) is_oadd_fun_iff_oadd [rule_format]:
+lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]:
"[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |]
==> j<J --> f`j = i++j"
apply (erule_tac i=j in trans_induct, clarify)
@@ -428,25 +421,25 @@
apply (blast intro: lt_trans ltI lt_Ord)
done
-lemma (in M_recursion) oadd_abs_fun_apply_iff:
+lemma (in M_ord_arith) oadd_abs_fun_apply_iff:
"[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |]
==> fun_apply(M,f,j,k) <-> f`j = k"
by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs)
-lemma (in M_recursion) Ord_oadd_abs:
+lemma (in M_ord_arith) Ord_oadd_abs:
"[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd)
apply (frule exists_oadd_fun [of j i], blast+)
done
-lemma (in M_recursion) oadd_abs:
+lemma (in M_ord_arith) oadd_abs:
"[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
apply (case_tac "Ord(i) & Ord(j)")
apply (simp add: Ord_oadd_abs)
apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
done
-lemma (in M_recursion) oadd_closed [intro,simp]:
+lemma (in M_ord_arith) oadd_closed [intro,simp]:
"[| M(i); M(j) |] ==> M(i++j)"
apply (simp add: oadd_eq_if_raw_oadd, clarify)
apply (simp add: raw_oadd_eq_oadd)
@@ -490,7 +483,7 @@
by (simp add: omult_eqns_def)
-lemma (in M_recursion) the_omult_eqns_closed:
+lemma (in M_ord_arith) the_omult_eqns_closed:
"[| M(i); M(x); M(g); function(g) |]
==> M(THE z. omult_eqns(i, x, g, z))"
apply (case_tac "Ord(x)")
@@ -501,39 +494,37 @@
apply (simp add: omult_eqns_Limit)
done
-lemma (in M_recursion) exists_omult:
+lemma (in M_ord_arith) 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)"
+ ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
- apply simp
- apply (blast intro: omult_strong_replacement')
- apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+ apply (simp_all add: Memrel_type omult_strong_replacement')
apply (blast intro: the_omult_eqns_closed)
done
-lemma (in M_recursion) exists_omult_fun:
- "[| Ord(j); M(i); M(j) |] ==> \<exists>f. M(f) & is_omult_fun(M,i,succ(j),f)"
-apply (rule exists_omult [THEN exE])
+lemma (in M_ord_arith) exists_omult_fun:
+ "[| Ord(j); M(i); M(j) |] ==> \<exists>f[M]. is_omult_fun(M,i,succ(j),f)"
+apply (rule exists_omult [THEN rexE])
apply (erule Ord_succ, assumption, simp)
-apply (rename_tac f, clarify)
+apply (rename_tac f)
apply (frule is_recfun_type)
-apply (rule_tac x=f in exI)
+apply (rule_tac x=f in rexI)
apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
is_omult_fun_def Ord_trans [OF _ succI1])
-apply (force dest: Ord_in_Ord'
- simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
- the_omult_eqns_Limit)
+ apply (force dest: Ord_in_Ord'
+ simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
+ the_omult_eqns_Limit, assumption)
done
-lemma (in M_recursion) is_omult_fun_apply_0:
+lemma (in M_ord_arith) is_omult_fun_apply_0:
"[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
-lemma (in M_recursion) is_omult_fun_apply_succ:
+lemma (in M_ord_arith) is_omult_fun_apply_succ:
"[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast)
-lemma (in M_recursion) is_omult_fun_apply_Limit:
+lemma (in M_ord_arith) is_omult_fun_apply_Limit:
"[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |]
==> f ` x = (\<Union>y\<in>x. f`y)"
apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
@@ -541,7 +532,7 @@
apply (simp add: ball_conj_distrib omult_Limit image_function)
done
-lemma (in M_recursion) is_omult_fun_eq_omult:
+lemma (in M_ord_arith) is_omult_fun_eq_omult:
"[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |]
==> j<J --> f`j = i**j"
apply (erule_tac i=j in trans_induct3)
@@ -555,12 +546,12 @@
apply (blast intro: lt_trans ltI lt_Ord)
done
-lemma (in M_recursion) omult_abs_fun_apply_iff:
+lemma (in M_ord_arith) omult_abs_fun_apply_iff:
"[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |]
==> fun_apply(M,f,j,k) <-> f`j = k"
by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs)
-lemma (in M_recursion) omult_abs:
+lemma (in M_ord_arith) omult_abs:
"[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult)
apply (frule exists_omult_fun [of j i], blast+)