# HG changeset patch
# User paulson
# Date 1025079936 -7200
# Node ID e3c289f0724b7d43722255a2a9e982f52df11b08
# Parent  e51efc2029e92759179c57fd8ff9688b8fa36a4c
towards absoluteness of wfrec-defined functions

diff -r e51efc2029e9 -r e3c289f0724b src/ZF/Constructible/Relative.thy
--- 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*}
diff -r e51efc2029e9 -r e3c289f0724b src/ZF/Constructible/WF_absolute.thy
--- 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
diff -r e51efc2029e9 -r e3c289f0724b src/ZF/Constructible/WFrec.thy
--- 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) == 
diff -r e51efc2029e9 -r e3c289f0724b src/ZF/Constructible/Wellorderings.thy
--- 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));