--- a/src/ZF/Constructible/ROOT.ML Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/ROOT.ML Fri Jun 28 11:25:46 2002 +0200
@@ -7,5 +7,5 @@
*)
use_thy "Reflection";
-use_thy "WFrec";
+use_thy "WF_absolute";
use_thy "L_axioms";
--- a/src/ZF/Constructible/Relative.thy Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Fri Jun 28 11:25:46 2002 +0200
@@ -6,7 +6,7 @@
constdefs
empty :: "[i=>o,i] => o"
- "empty(M,z) == \<forall>x. M(x) --> x \<notin> z"
+ "empty(M,z) == \<forall>x[M]. x \<notin> z"
subset :: "[i=>o,i,i] => o"
"subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
@@ -15,42 +15,42 @@
"upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
pair :: "[i=>o,i,i,i] => o"
- "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) &
- (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
+ "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &
+ (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
union :: "[i=>o,i,i,i] => o"
- "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
+ "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
successor :: "[i=>o,i,i] => o"
- "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
+ "successor(M,a,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,a,z)"
powerset :: "[i=>o,i,i] => o"
- "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
+ "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
inter :: "[i=>o,i,i,i] => o"
- "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
+ "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
setdiff :: "[i=>o,i,i,i] => o"
- "setdiff(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<notin> b)"
+ "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
big_union :: "[i=>o,i,i] => o"
- "big_union(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y))"
+ "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y)"
big_inter :: "[i=>o,i,i] => o"
"big_inter(M,A,z) ==
(A=0 --> z=0) &
- (A\<noteq>0 --> (\<forall>x. M(x) --> (x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y))))"
+ (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y)))"
cartprod :: "[i=>o,i,i,i] => o"
"cartprod(M,A,B,z) ==
- \<forall>u. M(u) --> (u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u))))"
+ \<forall>u[M]. u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u)))"
is_converse :: "[i=>o,i,i] => o"
"is_converse(M,r,z) ==
\<forall>x. M(x) -->
(x \<in> z <->
(\<exists>w\<in>r. M(w) &
- (\<exists>u v. M(u) & M(v) & pair(M,u,v,w) & pair(M,v,u,x))))"
+ (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"
pre_image :: "[i=>o,i,i,i] => o"
"pre_image(M,r,A,z) ==
@@ -224,17 +224,17 @@
by (blast intro: univ0_downwards_mem)
text{*Congruence rule for separation: can assume the variable is in @{text M}*}
-lemma [cong]:
+lemma separation_cong [cong]:
"(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
by (simp add: separation_def)
text{*Congruence rules for replacement*}
-lemma [cong]:
+lemma univalent_cong [cong]:
"[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
==> univalent(M,A,P) <-> univalent(M,A',P')"
by (simp add: univalent_def)
-lemma [cong]:
+lemma strong_replacement_cong [cong]:
"[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
==> strong_replacement(M,P) <-> strong_replacement(M,P')"
by (simp add: strong_replacement_def)
@@ -398,8 +398,8 @@
"[| 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)))"
and converse_separation:
- "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) &
- pair(M,x,y,p) & pair(M,y,x,z)))"
+ "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)))"
@@ -507,7 +507,7 @@
"[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
apply (simp add: cartprod_def)
apply (rule iffI)
-apply (blast intro!: equalityI intro: transM dest!: spec)
+ apply (blast intro!: equalityI intro: transM dest!: rspec)
apply (blast dest: transM)
done
@@ -616,15 +616,6 @@
==> M(\<lambda>x\<in>A. b(x))"
by (simp add: lam_def, blast dest: transM)
-lemma (in M_axioms) converse_abs [simp]:
- "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
-apply (simp add: is_converse_def)
-apply (rule iffI)
- apply (rule equalityI)
- apply (blast dest: transM)
- apply (clarify, frule transM, assumption, simp, blast)
-done
-
lemma (in M_axioms) image_abs [simp]:
"[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
apply (simp add: image_def)
@@ -648,11 +639,14 @@
done
lemma (in M_axioms) cartprod_iff_lemma:
- "[| M(C); \<forall>u. M(u) --> u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
- powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
+ "[| M(C); \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
+ powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
apply (simp add: powerset_def)
-apply (rule equalityI, clarify, simp)
+apply (rule equalityI, clarify, simp)
+
+ apply (frule transM, assumption)
+
apply (frule transM, assumption, simp)
apply blast
apply clarify
@@ -751,8 +745,7 @@
lemma (in M_axioms) M_converse_iff:
"M(r) ==>
converse(r) =
- {z \<in> range(r) * domain(r).
- \<exists>p\<in>r. \<exists>x. M(x) & (\<exists>y. M(y) & p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>)}"
+ {z \<in> range(r) * domain(r). \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
by (blast dest: transM)
lemma (in M_axioms) converse_closed [intro,simp]:
@@ -761,6 +754,16 @@
apply (insert converse_separation [of r], simp)
done
+lemma (in M_axioms) converse_abs [simp]:
+ "[| 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:);
+apply (rule M_equalityI)
+ apply (simp add: )
+ apply (blast dest: transM)+
+done
+
lemma (in M_axioms) relation_abs [simp]:
"M(r) ==> is_relation(M,r) <-> relation(r)"
apply (simp add: is_relation_def relation_def)
--- a/src/ZF/Constructible/WF_absolute.thy Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Fri Jun 28 11:25:46 2002 +0200
@@ -303,8 +303,7 @@
apply (rule univalent_is_recfun)
apply (blast intro: wellfounded_trancl)
apply (rule trans_trancl)
- apply (simp add: trancl_subset_times)
-apply blast
+ apply (simp add: trancl_subset_times, blast)
done
lemma (in M_recursion) Ord_wfrank_range [rule_format]:
@@ -312,9 +311,8 @@
==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
apply (drule wellfounded_trancl, assumption)
apply (rule wellfounded_induct, assumption+)
- apply (simp add:);
- apply (blast intro: Ord_wfrank_separation);
-apply (clarify)
+ apply simp
+ apply (blast intro: Ord_wfrank_separation, 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 "f`y = restrict(f, r^+ -`` {y})"}. *}
@@ -488,4 +486,142 @@
"[|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)
+
+text{*absoluteness for wfrec-defined functions.*}
+
+(*first use is_recfun, then M_is_recfun*)
+
+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) &
+ 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) &
+ 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 (simp_all add: the_recfun_eq trans_trancl trancl_subset_times)
+done
+
+
+text{*Assuming @{term r} is transitive simplifies the occurrences of @{text H}.
+ The premise @{term "relation(r)"} is necessary
+ 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) &
+ 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))"
+by (simp cong: is_recfun_cong
+ add: wfrec_relativize trancl_eq_r
+ is_recfun_restrict_idem domain_restrict_idem)
+
+
+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) &
+ 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)>)"
+apply safe
+ apply (simp add: trans_wfrec_relativize [THEN iff_sym])
+txt{*converse direction*}
+apply (rule sym)
+apply (simp add: trans_wfrec_relativize, blast)
+done
+
+
+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]:
+ "[|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)) |]
+ ==> M(a) --> M(wfrec(r,a,H))"
+apply (rule_tac a=a in wf_induct, assumption+)
+apply (subst wfrec, assumption, clarify)
+apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)"
+ in rspec [THEN rspec])
+apply (simp_all add: function_lam)
+apply (blast intro: dest: pair_components_in_M )
+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) &
+ 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)>)"
+apply simp
+apply (rule strong_replacement_cong, blast)
+done
+
+text{*Useful version for transitive relations*}
+theorem (in M_recursion) 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) &
+ 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))"
+apply (frule wfrec_replacement_iff [THEN iffD1])
+apply (rule wfrec_closed_lemma, assumption+)
+apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff)
+done
+
+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) &
+ 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) &
+ y = <x, H(x,restrict(f,r-``{x}))>)"
+apply safe
+ apply (simp add: wfrec_relativize [THEN iff_sym])
+txt{*converse direction*}
+apply (rule sym)
+apply (simp add: wfrec_relativize, blast)
+done
+
+lemma (in M_recursion) 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)) |]
+ ==> M(a) --> M(wfrec(r,a,H))"
+apply (rule_tac a=a in wf_induct, assumption+)
+apply (subst wfrec, assumption, clarify)
+apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)"
+ in rspec [THEN rspec])
+apply (simp_all add: function_lam)
+apply (blast intro: dest: pair_components_in_M )
+done
+
+text{*Full version not assuming transitivity, but maybe not very useful.*}
+theorem (in M_recursion) wfrec_closed:
+ "[|wf(r); M(r); M(a);
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ 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)) |]
+ ==> M(wfrec(r,a,H))"
+apply (frule wfrec_replacement_iff [THEN iffD1])
+apply (rule wfrec_closed_lemma, assumption+)
+apply (simp_all add: eq_pair_wfrec_iff)
+done
+
end
--- a/src/ZF/Constructible/WFrec.thy Fri Jun 28 11:24:36 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Fri Jun 28 11:25:46 2002 +0200
@@ -1,7 +1,7 @@
theory WFrec = Wellorderings:
-(*FIXME: could move these to WF.thy*)
+(*Many of these might be useful in WF.thy*)
lemma is_recfunI:
"f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
@@ -37,16 +37,40 @@
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
done
-(*????GET RID OF [simp]*)
-lemma trans_Int_eq [simp]:
- "[| trans(r); <y,x> \<in> r |]
- ==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
+lemma trans_Int_eq:
+ "[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
by (blast intro: transD)
-lemma trans_Int_eq2 [simp]:
- "[| trans(r); <y,x> \<in> r |]
- ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
-by (blast intro: transD)
+lemma is_recfun_restrict_idem:
+ "is_recfun(r,a,H,f) ==> restrict(f, r -`` {a}) = f"
+apply (drule is_recfun_type)
+apply (auto simp add: Pi_iff subset_Sigma_imp_relation restrict_idem)
+done
+
+lemma is_recfun_cong_lemma:
+ "[| is_recfun(r,a,H,f); r = r'; a = a'; f = f';
+ !!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |]
+ ==> H(x,g) = H'(x,g) |]
+ ==> is_recfun(r',a',H',f')"
+apply (simp add: is_recfun_def)
+apply (erule trans)
+apply (rule lam_cong)
+apply (simp_all add: vimage_singleton_iff Int_lower2)
+done
+
+text{*For @{text is_recfun} we need only pay attention to functions
+ whose domains are initial segments of @{term r}.*}
+lemma is_recfun_cong:
+ "[| r = r'; a = a'; f = f';
+ !!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |]
+ ==> H(x,g) = H'(x,g) |]
+ ==> is_recfun(r,a,H,f) <-> is_recfun(r',a',H',f')"
+apply (rule iffI)
+txt{*Messy: fast and blast don't work for some reason*}
+apply (erule is_recfun_cong_lemma, auto)
+apply (erule is_recfun_cong_lemma)
+apply (blast intro: sym)+
+done
text{*Stated using @{term "trans(r)"} rather than
@@ -64,12 +88,11 @@
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_tac a=x in wellfounded_induct)
-apply assumption+
+apply (erule_tac a=x in wellfounded_induct, assumption+)
txt{*Separation to justify the induction*}
apply (force intro: is_recfun_separation)
txt{*Now the inductive argument itself*}
-apply (clarify );
+apply clarify
apply (erule ssubst)+
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
apply (rename_tac x1)
@@ -100,29 +123,28 @@
apply (rule fun_extension)
apply (erule is_recfun_type)+
apply (blast intro!: is_recfun_equal dest: transM)
-done
+done
text{*Tells us that is_recfun can (in principle) be relativized.*}
lemma (in M_axioms) is_recfun_relativize:
- "[| M(r); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
+ "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. 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)
+ (\<forall>z[M]. z \<in> f <->
+ (\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))";
+apply (simp add: is_recfun_def lam_def)
apply (safe intro!: equalityI)
- apply (drule equalityD1 [THEN subsetD], assumption)
- apply clarify
- apply (rule_tac x=x in exI)
- apply (blast dest: pair_components_in_M)
- apply (blast elim!: equalityE dest: pair_components_in_M)
+ apply (drule equalityD1 [THEN subsetD], assumption)
+ apply (blast dest: pair_components_in_M)
+ apply (blast elim!: equalityE dest: pair_components_in_M)
+ apply (frule transM, assumption, rotate_tac -1)
apply simp
apply blast
- apply simp
-apply (subgoal_tac "function(f)")
- prefer 2
- apply (simp add: function_def)
+apply (subgoal_tac "is_function(M,f)")
+ txt{*We use @{term "is_function"} rather than @{term "function"} because
+ the subgoal's easier to prove with relativized quantifiers!*}
+ prefer 2 apply (simp add: is_function_def)
apply (frule pair_components_in_M, assumption)
- apply (simp add: is_recfun_imp_function function_restrictI)
+apply (simp add: is_recfun_imp_function function_restrictI)
done
(* ideas for further weaking the H-closure premise:
@@ -142,10 +164,11 @@
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);
- \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
+ \<forall>x[M]. \<forall>g[M]. 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 (simp (no_asm_simp) add: is_recfun_relativize restrict_iff
+ trans_Int_eq)
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)
@@ -157,7 +180,7 @@
lemma (in M_axioms) restrict_Y_lemma:
"[| wellfounded(M,r); trans(r); M(r);
- \<forall>x g. M(x) \<and> M(g) & function(g) --> M(H(x,g)); M(Y);
+ \<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}.
@@ -167,6 +190,7 @@
==> restrict(Y, r -`` {x}) = f"
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 "rall(M,?P)")+ --{*essential for efficiency*}
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)
@@ -201,7 +225,7 @@
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));
- \<forall>x g. M(x) & M(g) & function(g) --> M(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)"
apply (drule_tac A="r-``{a1}" in strong_replacementD)
apply blast
@@ -210,23 +234,16 @@
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)
-(*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: restrict_Y_lemma [of r H])
+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*}
+apply safe
+ apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H])
txt{*one more case*}
-apply (simp)
-apply (rule_tac x=x in bexI)
- prefer 2 apply blast
+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 (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 r H])
@@ -240,7 +257,7 @@
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); M(a);
- \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
+ \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
apply (rule wellfounded_induct, assumption+, clarify)
apply (rule exists_is_recfun_indstep, assumption+)
@@ -251,7 +268,7 @@
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);
- \<forall>x g. M(x) & M(g) & function(g) --> M(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))"
apply (rule wf_induct, assumption+)
apply (frule wf_imp_relativized)
@@ -261,24 +278,21 @@
done
constdefs
- M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
- "M_is_recfun(M,r,a,MH,f) ==
- \<forall>z. M(z) -->
- (z \<in> f <->
- (\<exists>x y xa sx r_sx f_r_sx.
- M(x) & M(y) & M(xa) & M(sx) & M(r_sx) & M(f_r_sx) &
- pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
- pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
- xa \<in> r & MH(M, x, f_r_sx, y)))"
+ M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
+ "M_is_recfun(M,r,a,MH,f) ==
+ \<forall>z[M]. z \<in> f <->
+ (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
+ pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
+ pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
+ xa \<in> r & MH(M, x, f_r_sx, y))"
lemma (in M_axioms) is_recfun_iff_M:
- "[| M(r); M(a); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g));
+ "[| M(r); M(a); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));
\<forall>x g y. M(x) --> M(g) --> M(y) --> MH(M,x,g,y) <-> y = H(x,g) |] ==>
is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)"
-apply (simp add: vimage_closed restrict_closed M_is_recfun_def is_recfun_relativize)
-apply (rule all_cong, safe)
- apply (thin_tac "\<forall>x. ?P(x)")+
- apply (blast dest: transM) (*or del: allE*)
+apply (simp add: M_is_recfun_def is_recfun_relativize)
+apply (rule rall_cong)
+apply (blast dest: transM)
done
lemma M_is_recfun_cong [cong]:
@@ -379,7 +393,7 @@
"[| 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 [OF wf_Memrel trans_Memrel])
- apply (simp add: );
+ apply simp
apply (blast intro: oadd_strong_replacement')
apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
done
@@ -491,7 +505,7 @@
"[| 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 [OF wf_Memrel trans_Memrel])
- apply (simp add: );
+ apply simp
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)