--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/WF_absolute.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,210 @@
+theory WF_absolute = WF_extras + WFrec:
+
+
+subsection{*Transitive closure without fixedpoints*}
+
+(*Ordinal.thy: just after succ_le_iff?*)
+lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
+apply (insert succ_le_iff [of i j])
+apply (simp add: lt_def)
+done
+
+constdefs
+ rtrancl_alt :: "[i,i]=>i"
+ "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]:
+ "n \<in> nat
+ ==> \<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)
+ 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)
+done
+
+lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
+apply (simp add: rtrancl_alt_def)
+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)
+apply 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
+txt{*Inductive step*}
+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
+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)
+
+
+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
+rank function.*}
+
+
+(*NEEDS RELATIVIZATION*)
+locale M_recursion = M_axioms +
+ assumes wfrank_separation':
+ "[| M(r); M(a); r \<subseteq> A*A |] ==>
+ separation
+ (M, \<lambda>x. x \<in> A -->
+ ~(\<exists>f. M(f) \<and>
+ is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f)))"
+ and wfrank_strong_replacement':
+ "[| M(r); M(a); r \<subseteq> A*A |] ==>
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ pair(M,x,y,z) &
+ is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f) &
+ y = (\<Union>y \<in> r-``{x}. succ(g`y)))"
+
+
+constdefs (*????????????????NEEDED?*)
+ is_wfrank_fun :: "[i=>o,i,i,i] => o"
+ "is_wfrank_fun(M,r,a,f) ==
+ function(f) & domain(f) = r-``{a} &
+ (\<forall>x. M(x) --> <x,a> \<in> r --> f`x = (\<Union>y \<in> r-``{x}. succ(f`y)))"
+
+
+
+
+lemma (in M_recursion) exists_wfrank:
+ "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
+ ==> \<exists>f. M(f) & is_recfun(r, a, %x g. (\<Union>y \<in> r-``{x}. succ(g`y)), f)"
+apply (rule exists_is_recfun [of A r])
+apply (erule wellfounded_imp_wellfounded_on)
+apply assumption;
+apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)
+apply (rule succI1)
+apply (blast intro: wfrank_separation')
+apply (blast intro: wfrank_strong_replacement')
+apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+done
+
+lemma (in M_recursion) exists_wfrank_fun:
+ "[| Ord(j); M(i); M(j) |] ==> \<exists>f. M(f) & is_wfrank_fun(M,i,succ(j),f)"
+apply (rule exists_wfrank [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_wfrank_fun_eq Ord_trans [OF _ succI1])
+done
+
+lemma (in M_recursion) is_wfrank_fun_apply:
+ "[| x < j; M(i); M(j); M(f); is_wfrank_fun(M,r,a,f) |]
+ ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
+apply (simp add: is_wfrank_fun_eq lt_Ord2)
+apply (frule lt_closed, simp)
+apply (subgoal_tac "x <= domain(f)")
+ apply (simp add: Ord_trans [OF _ succI1] image_function)
+ apply (blast intro: elim:);
+apply (blast intro: dest!: leI [THEN le_imp_subset] )
+done
+
+lemma (in M_recursion) is_wfrank_fun_eq_wfrank [rule_format]:
+ "[| is_wfrank_fun(M,i,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)
+apply (subgoal_tac "\<forall>k\<in>x. k<J")
+ apply (simp (no_asm_simp) add: is_wfrank_def wfrank_unfold is_wfrank_fun_apply)
+apply (blast intro: lt_trans ltI lt_Ord)
+done
+
+lemma (in M_recursion) wfrank_abs_fun_apply_iff:
+ "[| M(i); M(J); M(f); M(k); j<J; is_wfrank_fun(M,i,J,f) |]
+ ==> fun_apply(M,f,j,k) <-> f`j = k"
+by (auto simp add: lt_def is_wfrank_fun_eq subsetD apply_abs)
+
+lemma (in M_recursion) Ord_wfrank_abs:
+ "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
+apply (simp add: is_wfrank_def wfrank_abs_fun_apply_iff is_wfrank_fun_eq_wfrank)
+apply (frule exists_wfrank_fun [of j i], blast+)
+done
+
+lemma (in M_recursion) wfrank_abs:
+ "[| M(i); M(j); M(k) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
+apply (case_tac "Ord(i) & Ord(j)")
+ apply (simp add: Ord_wfrank_abs)
+apply (auto simp add: is_wfrank_def wfrank_eq_if_raw_wfrank)
+done
+
+lemma (in M_recursion) wfrank_closed [intro]:
+ "[| M(i); M(j) |] ==> M(i++j)"
+apply (simp add: wfrank_eq_if_raw_wfrank, clarify)
+apply (simp add: raw_wfrank_eq_wfrank)
+apply (frule exists_wfrank_fun [of j i], auto)
+apply (simp add: apply_closed is_wfrank_fun_eq_wfrank [symmetric])
+done
+
+
+
+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 (in M_axioms) wfrank: "wellfounded(M,r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
+by (subst wfrank_def [THEN def_wfrec], simp_all)
+
+lemma (in M_axioms) Ord_wfrank: "wellfounded(M,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 (in M_axioms) wfrank_lt: "[|wellfounded(M,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 (in M_axioms) Ord_wftype: "wellfounded(M,r) ==> Ord(wftype(r))"
+by (simp add: wftype_def Ord_wfrank)
+
+lemma (in M_axioms) wftypeI: "\<lbrakk>wellfounded(M,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 (in M_axioms) wf_imp_subset_rvimage:
+ "[|wellfounded(M,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
+
+
+
+
+end