src/ZF/Constructible/WF_absolute.thy
author paulson
Wed Jun 19 11:48:01 2002 +0200 (2002-06-19)
changeset 13223 45be08fbdcff
child 13242 f96bd927dd37
permissions -rw-r--r--
new theory of inner models
     1 theory WF_absolute = WF_extras + WFrec:
     2 
     3 
     4 subsection{*Transitive closure without fixedpoints*}
     5 
     6 (*Ordinal.thy: just after succ_le_iff?*)
     7 lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
     8 apply (insert succ_le_iff [of i j]) 
     9 apply (simp add: lt_def) 
    10 done
    11 
    12 constdefs
    13   rtrancl_alt :: "[i,i]=>i"
    14     "rtrancl_alt(A,r) == 
    15        {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    16                  \<exists>x y. p = <x,y> &  f`0 = x & f`n = y &
    17                        (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
    18 
    19 lemma alt_rtrancl_lemma1 [rule_format]: 
    20     "n \<in> nat
    21      ==> \<forall>f \<in> succ(n) -> field(r). 
    22          (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
    23 apply (induct_tac n) 
    24 apply (simp_all add: apply_funtype rtrancl_refl, clarify) 
    25 apply (rename_tac n f) 
    26 apply (rule rtrancl_into_rtrancl) 
    27  prefer 2 apply assumption
    28 apply (drule_tac x="restrict(f,succ(n))" in bspec)
    29  apply (blast intro: restrict_type2) 
    30 apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    31 done
    32 
    33 lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
    34 apply (simp add: rtrancl_alt_def)
    35 apply (blast intro: alt_rtrancl_lemma1 )  
    36 done
    37 
    38 lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
    39 apply (simp add: rtrancl_alt_def, clarify) 
    40 apply (frule rtrancl_type [THEN subsetD], clarify) 
    41 apply simp 
    42 apply (erule rtrancl_induct) 
    43  txt{*Base case, trivial*}
    44  apply (rule_tac x=0 in bexI) 
    45   apply (rule_tac x="lam x:1. xa" in bexI) 
    46    apply simp_all 
    47 txt{*Inductive step*}
    48 apply clarify 
    49 apply (rename_tac n f) 
    50 apply (rule_tac x="succ(n)" in bexI) 
    51  apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
    52   apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    53   apply (blast intro: mem_asym)  
    54  apply typecheck 
    55  apply auto 
    56 done
    57 
    58 lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
    59 by (blast del: subsetI
    60 	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) 
    61 
    62 
    63 text{*Relativized to M: Every well-founded relation is a subset of some
    64 inverse image of an ordinal.  Key step is the construction (in M) of a 
    65 rank function.*}
    66 
    67 
    68 (*NEEDS RELATIVIZATION*)
    69 locale M_recursion = M_axioms +
    70   assumes wfrank_separation':
    71      "[| M(r); M(a); r \<subseteq> A*A |] ==>
    72 	separation
    73 	   (M, \<lambda>x. x \<in> A --> 
    74 		~(\<exists>f. M(f) \<and> 
    75 		      is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f)))"
    76  and wfrank_strong_replacement':
    77      "[| M(r); M(a); r \<subseteq> A*A |] ==>
    78       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    79 		  pair(M,x,y,z) & 
    80 		  is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f) & 
    81 		  y = (\<Union>y \<in> r-``{x}. succ(g`y)))"
    82 
    83 
    84 constdefs (*????????????????NEEDED?*)
    85  is_wfrank_fun :: "[i=>o,i,i,i] => o"
    86     "is_wfrank_fun(M,r,a,f) == 
    87        function(f) & domain(f) = r-``{a} & 
    88        (\<forall>x. M(x) --> <x,a> \<in> r --> f`x = (\<Union>y \<in> r-``{x}. succ(f`y)))"
    89 
    90 
    91 
    92 
    93 lemma (in M_recursion) exists_wfrank:
    94     "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
    95      ==> \<exists>f. M(f) & is_recfun(r, a, %x g. (\<Union>y \<in> r-``{x}. succ(g`y)), f)"
    96 apply (rule exists_is_recfun [of A r]) 
    97 apply (erule wellfounded_imp_wellfounded_on) 
    98 apply assumption; 
    99 apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
   100 apply (rule succI1) 
   101 apply (blast intro: wfrank_separation') 
   102 apply (blast intro: wfrank_strong_replacement') 
   103 apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
   104 done
   105 
   106 lemma (in M_recursion) exists_wfrank_fun:
   107     "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f. M(f) & is_wfrank_fun(M,i,succ(j),f)"
   108 apply (rule exists_wfrank [THEN exE])
   109 apply (erule Ord_succ, assumption, simp) 
   110 apply (rename_tac f, clarify) 
   111 apply (frule is_recfun_type)
   112 apply (rule_tac x=f in exI) 
   113 apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   114                  is_wfrank_fun_eq Ord_trans [OF _ succI1])
   115 done
   116 
   117 lemma (in M_recursion) is_wfrank_fun_apply:
   118     "[| x < j; M(i); M(j); M(f); is_wfrank_fun(M,r,a,f) |] 
   119      ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
   120 apply (simp add: is_wfrank_fun_eq lt_Ord2) 
   121 apply (frule lt_closed, simp) 
   122 apply (subgoal_tac "x <= domain(f)")
   123  apply (simp add: Ord_trans [OF _ succI1] image_function)
   124  apply (blast intro: elim:); 
   125 apply (blast intro: dest!: leI [THEN le_imp_subset] ) 
   126 done
   127 
   128 lemma (in M_recursion) is_wfrank_fun_eq_wfrank [rule_format]:
   129     "[| is_wfrank_fun(M,i,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
   130      ==> j<J --> f`j = i++j"
   131 apply (erule_tac i=j in trans_induct, clarify) 
   132 apply (subgoal_tac "\<forall>k\<in>x. k<J")
   133  apply (simp (no_asm_simp) add: is_wfrank_def wfrank_unfold is_wfrank_fun_apply)
   134 apply (blast intro: lt_trans ltI lt_Ord) 
   135 done
   136 
   137 lemma (in M_recursion) wfrank_abs_fun_apply_iff:
   138     "[| M(i); M(J); M(f); M(k); j<J; is_wfrank_fun(M,i,J,f) |] 
   139      ==> fun_apply(M,f,j,k) <-> f`j = k"
   140 by (auto simp add: lt_def is_wfrank_fun_eq subsetD apply_abs) 
   141 
   142 lemma (in M_recursion) Ord_wfrank_abs:
   143     "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
   144 apply (simp add: is_wfrank_def wfrank_abs_fun_apply_iff is_wfrank_fun_eq_wfrank)
   145 apply (frule exists_wfrank_fun [of j i], blast+)
   146 done
   147 
   148 lemma (in M_recursion) wfrank_abs:
   149     "[| M(i); M(j); M(k) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
   150 apply (case_tac "Ord(i) & Ord(j)")
   151  apply (simp add: Ord_wfrank_abs)
   152 apply (auto simp add: is_wfrank_def wfrank_eq_if_raw_wfrank)
   153 done
   154 
   155 lemma (in M_recursion) wfrank_closed [intro]:
   156     "[| M(i); M(j) |] ==> M(i++j)"
   157 apply (simp add: wfrank_eq_if_raw_wfrank, clarify) 
   158 apply (simp add: raw_wfrank_eq_wfrank) 
   159 apply (frule exists_wfrank_fun [of j i], auto)
   160 apply (simp add: apply_closed is_wfrank_fun_eq_wfrank [symmetric]) 
   161 done
   162 
   163 
   164 
   165 constdefs
   166   wfrank :: "[i,i]=>i"
   167     "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
   168 
   169 constdefs
   170   wftype :: "i=>i"
   171     "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
   172 
   173 lemma (in M_axioms) wfrank: "wellfounded(M,r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
   174 by (subst wfrank_def [THEN def_wfrec], simp_all)
   175 
   176 lemma (in M_axioms) Ord_wfrank: "wellfounded(M,r) ==> Ord(wfrank(r,a))"
   177 apply (rule_tac a="a" in wf_induct, assumption)
   178 apply (subst wfrank, assumption)
   179 apply (rule Ord_succ [THEN Ord_UN], blast) 
   180 done
   181 
   182 lemma (in M_axioms) wfrank_lt: "[|wellfounded(M,r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
   183 apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
   184 apply (rule UN_I [THEN ltI])
   185 apply (simp add: Ord_wfrank vimage_iff)+
   186 done
   187 
   188 lemma (in M_axioms) Ord_wftype: "wellfounded(M,r) ==> Ord(wftype(r))"
   189 by (simp add: wftype_def Ord_wfrank)
   190 
   191 lemma (in M_axioms) wftypeI: "\<lbrakk>wellfounded(M,r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
   192 apply (simp add: wftype_def) 
   193 apply (blast intro: wfrank_lt [THEN ltD]) 
   194 done
   195 
   196 
   197 lemma (in M_axioms) wf_imp_subset_rvimage:
   198      "[|wellfounded(M,r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   199 apply (rule_tac x="wftype(r)" in exI) 
   200 apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI) 
   201 apply (simp add: Ord_wftype, clarify) 
   202 apply (frule subsetD, assumption, clarify) 
   203 apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
   204 apply (blast intro: wftypeI  ) 
   205 done
   206 
   207 
   208 
   209 
   210 end