src/ZF/Constructible/WF_absolute.thy
changeset 13247 e3c289f0724b
parent 13242 f96bd927dd37
child 13251 74cb2af8811e
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Mon Jun 24 16:33:43 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jun 26 10:25:36 2002 +0200
     1.3 @@ -1,5 +1,60 @@
     1.4  theory WF_absolute = WFrec:
     1.5  
     1.6 +subsection{*Every well-founded relation is a subset of some inverse image of 
     1.7 +      an ordinal*}
     1.8 +
     1.9 +lemma wf_rvimage_Ord: "Ord(i) \<Longrightarrow> wf(rvimage(A, f, Memrel(i)))"
    1.10 +by (blast intro: wf_rvimage wf_Memrel )
    1.11 +
    1.12 +
    1.13 +constdefs
    1.14 +  wfrank :: "[i,i]=>i"
    1.15 +    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
    1.16 +
    1.17 +constdefs
    1.18 +  wftype :: "i=>i"
    1.19 +    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
    1.20 +
    1.21 +lemma wfrank: "wf(r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
    1.22 +by (subst wfrank_def [THEN def_wfrec], simp_all)
    1.23 +
    1.24 +lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
    1.25 +apply (rule_tac a="a" in wf_induct, assumption)
    1.26 +apply (subst wfrank, assumption)
    1.27 +apply (rule Ord_succ [THEN Ord_UN], blast) 
    1.28 +done
    1.29 +
    1.30 +lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
    1.31 +apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
    1.32 +apply (rule UN_I [THEN ltI])
    1.33 +apply (simp add: Ord_wfrank vimage_iff)+
    1.34 +done
    1.35 +
    1.36 +lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))"
    1.37 +by (simp add: wftype_def Ord_wfrank)
    1.38 +
    1.39 +lemma wftypeI: "\<lbrakk>wf(r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
    1.40 +apply (simp add: wftype_def) 
    1.41 +apply (blast intro: wfrank_lt [THEN ltD]) 
    1.42 +done
    1.43 +
    1.44 +
    1.45 +lemma wf_imp_subset_rvimage:
    1.46 +     "[|wf(r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
    1.47 +apply (rule_tac x="wftype(r)" in exI) 
    1.48 +apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI) 
    1.49 +apply (simp add: Ord_wftype, clarify) 
    1.50 +apply (frule subsetD, assumption, clarify) 
    1.51 +apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
    1.52 +apply (blast intro: wftypeI  ) 
    1.53 +done
    1.54 +
    1.55 +theorem wf_iff_subset_rvimage:
    1.56 +  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))"
    1.57 +by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
    1.58 +          intro: wf_rvimage_Ord [THEN wf_subset])
    1.59 +
    1.60 +
    1.61  subsection{*Transitive closure without fixedpoints*}
    1.62  
    1.63  constdefs
    1.64 @@ -127,8 +182,7 @@
    1.65   prefer 2 apply assumption
    1.66   prefer 2 apply blast
    1.67  apply (rule iffI, clarify) 
    1.68 -apply (simp add: nat_0_le [THEN ltD]  apply_funtype, blast, clarify)  
    1.69 -apply simp 
    1.70 +apply (simp add: nat_0_le [THEN ltD]  apply_funtype, blast, clarify, simp) 
    1.71   apply (rename_tac n f) 
    1.72   apply (rule_tac x=n in bexI) 
    1.73    apply (rule_tac x=f in exI)
    1.74 @@ -274,8 +328,7 @@
    1.75   txt{*by our previous result the range consists of ordinals.*} 
    1.76   apply (blast intro: Ord_wfrank_range) 
    1.77  txt{*We still must show that the range is a transitive set.*}
    1.78 -apply (simp add: Transset_def, clarify)
    1.79 -apply simp
    1.80 +apply (simp add: Transset_def, clarify, simp)
    1.81  apply (rename_tac x i f u)   
    1.82  apply (frule is_recfun_imp_in_r, assumption) 
    1.83  apply (subgoal_tac "M(u) & M(i) & M(x)") 
    1.84 @@ -310,14 +363,12 @@
    1.85  apply (simp add: wellfoundedrank_def function_def) 
    1.86  apply (rule equalityI, auto)
    1.87  apply (frule transM, assumption)  
    1.88 -apply (frule exists_wfrank, assumption+)
    1.89 -apply clarify 
    1.90 +apply (frule exists_wfrank, assumption+, clarify) 
    1.91  apply (rule domainI) 
    1.92  apply (rule ReplaceI)
    1.93  apply (rule_tac x="range(f)" in exI)
    1.94  apply simp  
    1.95 -apply (rule_tac x=f in exI, blast)
    1.96 -apply assumption
    1.97 +apply (rule_tac x=f in exI, blast, assumption)
    1.98  txt{*Uniqueness (for Replacement): repeated above!*}
    1.99  apply clarify
   1.100  apply (drule is_recfun_functional, assumption)
   1.101 @@ -362,4 +413,64 @@
   1.102  apply (blast dest: transM) 
   1.103  done
   1.104  
   1.105 +
   1.106 +lemma (in M_recursion) wellfoundedrank_lt:
   1.107 +     "[| <a,b> \<in> r;
   1.108 +         wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|] 
   1.109 +      ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
   1.110 +apply (subgoal_tac "wellfounded_on(M, A, r^+)") 
   1.111 + prefer 2
   1.112 + apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   1.113 +apply (subgoal_tac "a\<in>A & b\<in>A")
   1.114 + prefer 2 apply blast
   1.115 +apply (simp add: lt_def Ord_wellfoundedrank, clarify)   
   1.116 +apply (frule exists_wfrank [of concl: _ b], assumption+, clarify) 
   1.117 +apply (rename_tac fb)
   1.118 +apply (frule is_recfun_restrict [of concl: _ a])
   1.119 +    apply (rule trans_on_trancl, assumption)
   1.120 +   apply (simp_all add: r_into_trancl trancl_subset_times) 
   1.121 +txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
   1.122 +apply (simp add: wellfoundedrank_eq) 
   1.123 +apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
   1.124 +   apply (simp_all add: transM [of a])
   1.125 +txt{*We have used equations for wellfoundedrank and now must use some
   1.126 +    for  @{text is_recfun}. *}
   1.127 +apply (rule_tac a=a in rangeI) 
   1.128 +apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff 
   1.129 +                 r_into_trancl apply_recfun r_into_trancl)  
   1.130 +done
   1.131 +
   1.132 +
   1.133 +lemma (in M_recursion) wellfounded_imp_subset_rvimage:
   1.134 +     "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|] 
   1.135 +      ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   1.136 +apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
   1.137 +apply (rule_tac x="wellfoundedrank(M,r,A)" in exI)
   1.138 +apply (simp add: Ord_range_wellfoundedrank, clarify) 
   1.139 +apply (frule subsetD, assumption, clarify) 
   1.140 +apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD])
   1.141 +apply (blast intro: apply_rangeI wellfoundedrank_type) 
   1.142 +done
   1.143 +
   1.144 +lemma (in M_recursion) wellfounded_imp_wf: 
   1.145 +     "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)" 
   1.146 +by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
   1.147 +          intro: wf_rvimage_Ord [THEN wf_subset])
   1.148 +
   1.149 +lemma (in M_recursion) wellfounded_on_imp_wf_on: 
   1.150 +     "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)" 
   1.151 +apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) 
   1.152 +apply (rule wellfounded_imp_wf)
   1.153 +apply (simp_all add: relation_def)  
   1.154 +done
   1.155 +
   1.156 +
   1.157 +theorem (in M_recursion) wf_abs [simp]: 
   1.158 +     "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
   1.159 +by (blast intro: wellfounded_imp_wf wf_imp_relativized) 
   1.160 +
   1.161 +theorem (in M_recursion) wf_on_abs [simp]: 
   1.162 +     "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
   1.163 +by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) 
   1.164 +
   1.165  end