src/ZF/Constructible/WF_absolute.thy
changeset 13223 45be08fbdcff
child 13242 f96bd927dd37
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jun 19 11:48:01 2002 +0200
     1.3 @@ -0,0 +1,210 @@
     1.4 +theory WF_absolute = WF_extras + WFrec:
     1.5 +
     1.6 +
     1.7 +subsection{*Transitive closure without fixedpoints*}
     1.8 +
     1.9 +(*Ordinal.thy: just after succ_le_iff?*)
    1.10 +lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
    1.11 +apply (insert succ_le_iff [of i j]) 
    1.12 +apply (simp add: lt_def) 
    1.13 +done
    1.14 +
    1.15 +constdefs
    1.16 +  rtrancl_alt :: "[i,i]=>i"
    1.17 +    "rtrancl_alt(A,r) == 
    1.18 +       {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    1.19 +                 \<exists>x y. p = <x,y> &  f`0 = x & f`n = y &
    1.20 +                       (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
    1.21 +
    1.22 +lemma alt_rtrancl_lemma1 [rule_format]: 
    1.23 +    "n \<in> nat
    1.24 +     ==> \<forall>f \<in> succ(n) -> field(r). 
    1.25 +         (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
    1.26 +apply (induct_tac n) 
    1.27 +apply (simp_all add: apply_funtype rtrancl_refl, clarify) 
    1.28 +apply (rename_tac n f) 
    1.29 +apply (rule rtrancl_into_rtrancl) 
    1.30 + prefer 2 apply assumption
    1.31 +apply (drule_tac x="restrict(f,succ(n))" in bspec)
    1.32 + apply (blast intro: restrict_type2) 
    1.33 +apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    1.34 +done
    1.35 +
    1.36 +lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
    1.37 +apply (simp add: rtrancl_alt_def)
    1.38 +apply (blast intro: alt_rtrancl_lemma1 )  
    1.39 +done
    1.40 +
    1.41 +lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
    1.42 +apply (simp add: rtrancl_alt_def, clarify) 
    1.43 +apply (frule rtrancl_type [THEN subsetD], clarify) 
    1.44 +apply simp 
    1.45 +apply (erule rtrancl_induct) 
    1.46 + txt{*Base case, trivial*}
    1.47 + apply (rule_tac x=0 in bexI) 
    1.48 +  apply (rule_tac x="lam x:1. xa" in bexI) 
    1.49 +   apply simp_all 
    1.50 +txt{*Inductive step*}
    1.51 +apply clarify 
    1.52 +apply (rename_tac n f) 
    1.53 +apply (rule_tac x="succ(n)" in bexI) 
    1.54 + apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
    1.55 +  apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    1.56 +  apply (blast intro: mem_asym)  
    1.57 + apply typecheck 
    1.58 + apply auto 
    1.59 +done
    1.60 +
    1.61 +lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
    1.62 +by (blast del: subsetI
    1.63 +	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) 
    1.64 +
    1.65 +
    1.66 +text{*Relativized to M: Every well-founded relation is a subset of some
    1.67 +inverse image of an ordinal.  Key step is the construction (in M) of a 
    1.68 +rank function.*}
    1.69 +
    1.70 +
    1.71 +(*NEEDS RELATIVIZATION*)
    1.72 +locale M_recursion = M_axioms +
    1.73 +  assumes wfrank_separation':
    1.74 +     "[| M(r); M(a); r \<subseteq> A*A |] ==>
    1.75 +	separation
    1.76 +	   (M, \<lambda>x. x \<in> A --> 
    1.77 +		~(\<exists>f. M(f) \<and> 
    1.78 +		      is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f)))"
    1.79 + and wfrank_strong_replacement':
    1.80 +     "[| M(r); M(a); r \<subseteq> A*A |] ==>
    1.81 +      strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    1.82 +		  pair(M,x,y,z) & 
    1.83 +		  is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f) & 
    1.84 +		  y = (\<Union>y \<in> r-``{x}. succ(g`y)))"
    1.85 +
    1.86 +
    1.87 +constdefs (*????????????????NEEDED?*)
    1.88 + is_wfrank_fun :: "[i=>o,i,i,i] => o"
    1.89 +    "is_wfrank_fun(M,r,a,f) == 
    1.90 +       function(f) & domain(f) = r-``{a} & 
    1.91 +       (\<forall>x. M(x) --> <x,a> \<in> r --> f`x = (\<Union>y \<in> r-``{x}. succ(f`y)))"
    1.92 +
    1.93 +
    1.94 +
    1.95 +
    1.96 +lemma (in M_recursion) exists_wfrank:
    1.97 +    "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
    1.98 +     ==> \<exists>f. M(f) & is_recfun(r, a, %x g. (\<Union>y \<in> r-``{x}. succ(g`y)), f)"
    1.99 +apply (rule exists_is_recfun [of A r]) 
   1.100 +apply (erule wellfounded_imp_wellfounded_on) 
   1.101 +apply assumption; 
   1.102 +apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
   1.103 +apply (rule succI1) 
   1.104 +apply (blast intro: wfrank_separation') 
   1.105 +apply (blast intro: wfrank_strong_replacement') 
   1.106 +apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
   1.107 +done
   1.108 +
   1.109 +lemma (in M_recursion) exists_wfrank_fun:
   1.110 +    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f. M(f) & is_wfrank_fun(M,i,succ(j),f)"
   1.111 +apply (rule exists_wfrank [THEN exE])
   1.112 +apply (erule Ord_succ, assumption, simp) 
   1.113 +apply (rename_tac f, clarify) 
   1.114 +apply (frule is_recfun_type)
   1.115 +apply (rule_tac x=f in exI) 
   1.116 +apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   1.117 +                 is_wfrank_fun_eq Ord_trans [OF _ succI1])
   1.118 +done
   1.119 +
   1.120 +lemma (in M_recursion) is_wfrank_fun_apply:
   1.121 +    "[| x < j; M(i); M(j); M(f); is_wfrank_fun(M,r,a,f) |] 
   1.122 +     ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
   1.123 +apply (simp add: is_wfrank_fun_eq lt_Ord2) 
   1.124 +apply (frule lt_closed, simp) 
   1.125 +apply (subgoal_tac "x <= domain(f)")
   1.126 + apply (simp add: Ord_trans [OF _ succI1] image_function)
   1.127 + apply (blast intro: elim:); 
   1.128 +apply (blast intro: dest!: leI [THEN le_imp_subset] ) 
   1.129 +done
   1.130 +
   1.131 +lemma (in M_recursion) is_wfrank_fun_eq_wfrank [rule_format]:
   1.132 +    "[| is_wfrank_fun(M,i,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
   1.133 +     ==> j<J --> f`j = i++j"
   1.134 +apply (erule_tac i=j in trans_induct, clarify) 
   1.135 +apply (subgoal_tac "\<forall>k\<in>x. k<J")
   1.136 + apply (simp (no_asm_simp) add: is_wfrank_def wfrank_unfold is_wfrank_fun_apply)
   1.137 +apply (blast intro: lt_trans ltI lt_Ord) 
   1.138 +done
   1.139 +
   1.140 +lemma (in M_recursion) wfrank_abs_fun_apply_iff:
   1.141 +    "[| M(i); M(J); M(f); M(k); j<J; is_wfrank_fun(M,i,J,f) |] 
   1.142 +     ==> fun_apply(M,f,j,k) <-> f`j = k"
   1.143 +by (auto simp add: lt_def is_wfrank_fun_eq subsetD apply_abs) 
   1.144 +
   1.145 +lemma (in M_recursion) Ord_wfrank_abs:
   1.146 +    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
   1.147 +apply (simp add: is_wfrank_def wfrank_abs_fun_apply_iff is_wfrank_fun_eq_wfrank)
   1.148 +apply (frule exists_wfrank_fun [of j i], blast+)
   1.149 +done
   1.150 +
   1.151 +lemma (in M_recursion) wfrank_abs:
   1.152 +    "[| M(i); M(j); M(k) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
   1.153 +apply (case_tac "Ord(i) & Ord(j)")
   1.154 + apply (simp add: Ord_wfrank_abs)
   1.155 +apply (auto simp add: is_wfrank_def wfrank_eq_if_raw_wfrank)
   1.156 +done
   1.157 +
   1.158 +lemma (in M_recursion) wfrank_closed [intro]:
   1.159 +    "[| M(i); M(j) |] ==> M(i++j)"
   1.160 +apply (simp add: wfrank_eq_if_raw_wfrank, clarify) 
   1.161 +apply (simp add: raw_wfrank_eq_wfrank) 
   1.162 +apply (frule exists_wfrank_fun [of j i], auto)
   1.163 +apply (simp add: apply_closed is_wfrank_fun_eq_wfrank [symmetric]) 
   1.164 +done
   1.165 +
   1.166 +
   1.167 +
   1.168 +constdefs
   1.169 +  wfrank :: "[i,i]=>i"
   1.170 +    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
   1.171 +
   1.172 +constdefs
   1.173 +  wftype :: "i=>i"
   1.174 +    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
   1.175 +
   1.176 +lemma (in M_axioms) wfrank: "wellfounded(M,r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
   1.177 +by (subst wfrank_def [THEN def_wfrec], simp_all)
   1.178 +
   1.179 +lemma (in M_axioms) Ord_wfrank: "wellfounded(M,r) ==> Ord(wfrank(r,a))"
   1.180 +apply (rule_tac a="a" in wf_induct, assumption)
   1.181 +apply (subst wfrank, assumption)
   1.182 +apply (rule Ord_succ [THEN Ord_UN], blast) 
   1.183 +done
   1.184 +
   1.185 +lemma (in M_axioms) wfrank_lt: "[|wellfounded(M,r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
   1.186 +apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
   1.187 +apply (rule UN_I [THEN ltI])
   1.188 +apply (simp add: Ord_wfrank vimage_iff)+
   1.189 +done
   1.190 +
   1.191 +lemma (in M_axioms) Ord_wftype: "wellfounded(M,r) ==> Ord(wftype(r))"
   1.192 +by (simp add: wftype_def Ord_wfrank)
   1.193 +
   1.194 +lemma (in M_axioms) wftypeI: "\<lbrakk>wellfounded(M,r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
   1.195 +apply (simp add: wftype_def) 
   1.196 +apply (blast intro: wfrank_lt [THEN ltD]) 
   1.197 +done
   1.198 +
   1.199 +
   1.200 +lemma (in M_axioms) wf_imp_subset_rvimage:
   1.201 +     "[|wellfounded(M,r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   1.202 +apply (rule_tac x="wftype(r)" in exI) 
   1.203 +apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI) 
   1.204 +apply (simp add: Ord_wftype, clarify) 
   1.205 +apply (frule subsetD, assumption, clarify) 
   1.206 +apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
   1.207 +apply (blast intro: wftypeI  ) 
   1.208 +done
   1.209 +
   1.210 +
   1.211 +
   1.212 +
   1.213 +end