--- a/src/ZF/Constructible/Relative.thy Mon Jun 24 16:33:43 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Wed Jun 26 10:25:36 2002 +0200
@@ -569,16 +569,12 @@
lemma (in M_axioms) strong_replacementI [rule_format]:
"[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
==> strong_replacement(M,P)"
-apply (simp add: strong_replacement_def)
-apply (clarify );
-apply (frule replacementD [OF replacement])
-apply assumption
-apply (clarify );
-apply (drule_tac x=A in spec)
-apply (clarify );
-apply (drule_tac z=Y in separationD)
-apply assumption;
-apply (clarify );
+apply (simp add: strong_replacement_def, clarify)
+apply (frule replacementD [OF replacement], assumption)
+apply clarify
+apply (drule_tac x=A in spec, clarify)
+apply (drule_tac z=Y in separationD, assumption)
+apply clarify
apply (blast dest: transM)
done
@@ -586,17 +582,16 @@
(*The last premise expresses that P takes M to M*)
lemma (in M_axioms) strong_replacement_closed [intro,simp]:
"[| strong_replacement(M,P); M(A); univalent(M,A,P);
- !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
+ !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
apply (simp add: strong_replacement_def)
apply (drule spec [THEN mp], auto)
apply (subgoal_tac "Replace(A,P) = Y")
- apply (simp add: );
+ apply simp
apply (rule equality_iffI)
-apply (simp add: Replace_iff)
-apply safe;
+apply (simp add: Replace_iff, safe)
apply (blast dest: transM)
apply (frule transM, assumption)
- apply (simp add: univalent_def);
+ apply (simp add: univalent_def)
apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
apply (blast dest: transM)
done
@@ -609,13 +604,18 @@
even for f : M -> M.
*)
lemma (in M_axioms) RepFun_closed [intro,simp]:
- "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
+ "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
==> M(RepFun(A,f))"
apply (simp add: RepFun_def)
apply (rule strong_replacement_closed)
apply (auto dest: transM simp add: univalent_def)
done
+lemma (in M_axioms) lam_closed [intro,simp]:
+ "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
+ ==> 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)
@@ -800,7 +800,7 @@
lemma (in M_axioms) injection_abs [simp]:
"[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
apply (simp add: injection_def apply_iff inj_def apply_closed)
-apply (blast dest: transM [of _ A]);
+apply (blast dest: transM [of _ A])
done
lemma (in M_axioms) surjection_abs [simp]:
@@ -846,8 +846,8 @@
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 );
- apply (simp add: );
+ apply clarify
+ apply simp
apply (blast dest: transM)+
done
@@ -860,7 +860,7 @@
lemma (in M_axioms) composition_abs [simp]:
"[| M(r); M(s); M(t) |]
==> composition(M,r,s,t) <-> t = r O s"
-apply safe;
+apply safe
txt{*Proving @{term "composition(M, r, s, r O s)"}*}
prefer 2
apply (simp add: composition_def comp_def)
@@ -896,7 +896,7 @@
lemma (in M_axioms) Int_closed [intro,simp]:
"[| M(A); M(B) |] ==> M(A Int B)"
apply (subgoal_tac "M({A,B})")
-apply (frule Inter_closed, force+);
+apply (frule Inter_closed, force+)
done
text{*M contains all finite functions*}
--- a/src/ZF/Constructible/WF_absolute.thy Mon Jun 24 16:33:43 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Wed Jun 26 10:25:36 2002 +0200
@@ -1,5 +1,60 @@
theory WF_absolute = WFrec:
+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 )
+
+
+constdefs
+ wfrank :: "[i,i]=>i"
+ "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
+
+constdefs
+ wftype :: "i=>i"
+ "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
+
+lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
+by (subst wfrank_def [THEN def_wfrec], simp_all)
+
+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)
+done
+
+lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
+apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
+apply (rule UN_I [THEN ltI])
+apply (simp add: Ord_wfrank vimage_iff)+
+done
+
+lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))"
+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])
+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 (simp add: rvimage_iff wfrank_lt [THEN ltD])
+apply (blast intro: wftypeI )
+done
+
+theorem wf_iff_subset_rvimage:
+ "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))"
+by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
+ intro: wf_rvimage_Ord [THEN wf_subset])
+
+
subsection{*Transitive closure without fixedpoints*}
constdefs
@@ -127,8 +182,7 @@
prefer 2 apply assumption
prefer 2 apply blast
apply (rule iffI, clarify)
-apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast, clarify)
-apply simp
+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)
@@ -274,8 +328,7 @@
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)
-apply simp
+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)")
@@ -310,14 +363,12 @@
apply (simp add: wellfoundedrank_def function_def)
apply (rule equalityI, auto)
apply (frule transM, assumption)
-apply (frule exists_wfrank, assumption+)
-apply clarify
+apply (frule 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)
-apply assumption
+apply (rule_tac x=f in exI, blast, assumption)
txt{*Uniqueness (for Replacement): repeated above!*}
apply clarify
apply (drule is_recfun_functional, assumption)
@@ -362,4 +413,64 @@
apply (blast dest: transM)
done
+
+lemma (in M_recursion) 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"
+apply (subgoal_tac "wellfounded_on(M, A, r^+)")
+ prefer 2
+ apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
+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 (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)
+txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
+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)
+done
+
+
+lemma (in M_recursion) 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)
+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: rvimage_iff wellfoundedrank_lt [THEN ltD])
+apply (blast intro: apply_rangeI wellfoundedrank_type)
+done
+
+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)
+apply (rule wellfounded_imp_wf)
+apply (simp_all add: relation_def)
+done
+
+
+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)
+
+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)
+
end
--- a/src/ZF/Constructible/WFrec.thy Mon Jun 24 16:33:43 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Wed Jun 26 10:25:36 2002 +0200
@@ -141,15 +141,13 @@
\<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)); r \<subseteq> A * A |]
==> 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 vimage_closed restrict_closed
- restrict_iff)
+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 (simp add: is_recfun_type [THEN apply_iff])
- (*???COMBINE*)
- apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed)
+ apply (simp add: is_recfun_type [THEN apply_iff]
+ is_recfun_imp_function function_restrictI)
apply (blast intro: apply_recfun dest: trans_onD)+
done
@@ -261,23 +259,6 @@
apply (rule exists_is_recfun_indstep, assumption+)
done
- (*????????????????NOT USED????????????????*)
- constdefs
- M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
- "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
-
- (*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
- lemma (in M_axioms) M_is_the_recfun:
- "[|is_recfun(r,a,H,f);
- wellfounded_on(M,A,r); trans[A](r);
- M(A); M(f); M(a); r \<subseteq> A*A |]
- ==> M(M_the_recfun(M,r,a,H)) &
- is_recfun(r, a, H, M_the_recfun(M,r,a,H))"
- apply (unfold M_the_recfun_def)
- apply (rule ex1I [THEN theI2], fast)
- apply (blast intro: is_recfun_functional, blast)
- 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) ==
--- a/src/ZF/Constructible/Wellorderings.thy Mon Jun 24 16:33:43 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Wed Jun 26 10:25:36 2002 +0200
@@ -81,6 +81,10 @@
apply (drule_tac x=x in spec, blast)
done
+lemma (in M_axioms) wellfounded_on_imp_wellfounded:
+ "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
+by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
+
lemma (in M_axioms) wellfounded_on_induct:
"[| a\<in>A; wellfounded_on(M,A,r); M(A);
separation(M, \<lambda>x. x\<in>A --> ~P(x));