src/ZF/Constructible/WF_absolute.thy
author paulson
Mon Jun 24 11:57:23 2002 +0200 (2002-06-24)
changeset 13242 f96bd927dd37
parent 13223 45be08fbdcff
child 13247 e3c289f0724b
permissions -rw-r--r--
towards absoluteness of wf
     1 theory WF_absolute = WFrec:
     2 
     3 subsection{*Transitive closure without fixedpoints*}
     4 
     5 constdefs
     6   rtrancl_alt :: "[i,i]=>i"
     7     "rtrancl_alt(A,r) == 
     8        {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
     9                  (\<exists>x y. p = <x,y> &  f`0 = x & f`n = y) &
    10                        (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
    11 
    12 lemma alt_rtrancl_lemma1 [rule_format]: 
    13     "n \<in> nat
    14      ==> \<forall>f \<in> succ(n) -> field(r). 
    15          (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
    16 apply (induct_tac n) 
    17 apply (simp_all add: apply_funtype rtrancl_refl, clarify) 
    18 apply (rename_tac n f) 
    19 apply (rule rtrancl_into_rtrancl) 
    20  prefer 2 apply assumption
    21 apply (drule_tac x="restrict(f,succ(n))" in bspec)
    22  apply (blast intro: restrict_type2) 
    23 apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    24 done
    25 
    26 lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
    27 apply (simp add: rtrancl_alt_def)
    28 apply (blast intro: alt_rtrancl_lemma1 )  
    29 done
    30 
    31 lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
    32 apply (simp add: rtrancl_alt_def, clarify) 
    33 apply (frule rtrancl_type [THEN subsetD], clarify, simp) 
    34 apply (erule rtrancl_induct) 
    35  txt{*Base case, trivial*}
    36  apply (rule_tac x=0 in bexI) 
    37   apply (rule_tac x="lam x:1. xa" in bexI) 
    38    apply simp_all 
    39 txt{*Inductive step*}
    40 apply clarify 
    41 apply (rename_tac n f) 
    42 apply (rule_tac x="succ(n)" in bexI) 
    43  apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
    44   apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    45   apply (blast intro: mem_asym)  
    46  apply typecheck 
    47  apply auto 
    48 done
    49 
    50 lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
    51 by (blast del: subsetI
    52 	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) 
    53 
    54 
    55 constdefs
    56 
    57   rtran_closure :: "[i=>o,i,i] => o"
    58     "rtran_closure(M,r,s) == 
    59         \<forall>A. M(A) --> is_field(M,r,A) -->
    60  	 (\<forall>p. M(p) --> 
    61           (p \<in> s <-> 
    62            (\<exists>n\<in>nat. M(n) & 
    63             (\<exists>n'. M(n') & successor(M,n,n') &
    64              (\<exists>f. M(f) & typed_function(M,n',A,f) &
    65               (\<exists>x\<in>A. M(x) & (\<exists>y\<in>A. M(y) & pair(M,x,y,p) &  
    66                    fun_apply(M,f,0,x) & fun_apply(M,f,n,y))) &
    67               (\<forall>i\<in>n. M(i) -->
    68                 (\<forall>i'. M(i') --> successor(M,i,i') -->
    69                  (\<forall>fi. M(fi) --> fun_apply(M,f,i,fi) -->
    70                   (\<forall>fi'. M(fi') --> fun_apply(M,f,i',fi') -->
    71                    (\<forall>q. M(q) --> pair(M,fi,fi',q) --> q \<in> r))))))))))"
    72 
    73   tran_closure :: "[i=>o,i,i] => o"
    74     "tran_closure(M,r,t) == 
    75          \<exists>s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)"
    76 
    77 
    78 locale M_trancl = M_axioms +
    79 (*THEY NEED RELATIVIZATION*)
    80   assumes rtrancl_separation:
    81      "[| M(r); M(A) |] ==>
    82 	separation
    83 	   (M, \<lambda>p. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    84                     (\<exists>x y. p = <x,y> &  f`0 = x & f`n = y) &
    85                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r))"
    86       and wellfounded_trancl_separation:
    87      "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z)"
    88 
    89 
    90 lemma (in M_trancl) rtran_closure_rtrancl: 
    91      "M(r) ==> rtran_closure(M,r,rtrancl(r))"
    92 apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] 
    93                  rtrancl_alt_def field_closed typed_apply_abs apply_closed
    94                  Ord_succ_mem_iff M_nat  nat_0_le [THEN ltD], clarify) 
    95 apply (rule iffI) 
    96  apply clarify 
    97  apply simp 
    98  apply (rename_tac n f) 
    99  apply (rule_tac x=n in bexI) 
   100   apply (rule_tac x=f in exI) 
   101   apply simp
   102   apply (blast dest: finite_fun_closed dest: transM)
   103  apply assumption
   104 apply clarify
   105 apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast)  
   106 done
   107 
   108 lemma (in M_trancl) rtrancl_closed [intro,simp]: 
   109      "M(r) ==> M(rtrancl(r))"
   110 apply (insert rtrancl_separation [of r "field(r)"]) 
   111 apply (simp add: rtrancl_alt_eq_rtrancl [symmetric] 
   112                  rtrancl_alt_def field_closed typed_apply_abs apply_closed
   113                  Ord_succ_mem_iff M_nat
   114                  nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
   115 done
   116 
   117 lemma (in M_trancl) rtrancl_abs [simp]: 
   118      "[| M(r); M(z) |] ==> rtran_closure(M,r,z) <-> z = rtrancl(r)"
   119 apply (rule iffI)
   120  txt{*Proving the right-to-left implication*}
   121  prefer 2 apply (blast intro: rtran_closure_rtrancl) 
   122 apply (rule M_equalityI)
   123 apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] 
   124                  rtrancl_alt_def field_closed typed_apply_abs apply_closed
   125                  Ord_succ_mem_iff M_nat
   126                  nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) 
   127  prefer 2 apply assumption
   128  prefer 2 apply blast
   129 apply (rule iffI, clarify) 
   130 apply (simp add: nat_0_le [THEN ltD]  apply_funtype, blast, clarify)  
   131 apply simp 
   132  apply (rename_tac n f) 
   133  apply (rule_tac x=n in bexI) 
   134   apply (rule_tac x=f in exI)
   135   apply (blast dest!: finite_fun_closed, assumption)
   136 done
   137 
   138 
   139 lemma (in M_trancl) trancl_closed [intro,simp]: 
   140      "M(r) ==> M(trancl(r))"
   141 by (simp add: trancl_def comp_closed rtrancl_closed) 
   142 
   143 lemma (in M_trancl) trancl_abs [simp]: 
   144      "[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)"
   145 by (simp add: tran_closure_def trancl_def) 
   146 
   147 
   148 text{*Alternative proof of @{text wf_on_trancl}; inspiration for the 
   149       relativized version.  Original version is on theory WF.*}
   150 lemma "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
   151 apply (simp add: wf_on_def wf_def) 
   152 apply (safe intro!: equalityI)
   153 apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec) 
   154 apply (blast elim: tranclE) 
   155 done
   156 
   157 
   158 lemma (in M_trancl) wellfounded_on_trancl:
   159      "[| wellfounded_on(M,A,r);  r-``A <= A; M(r); M(A) |]
   160       ==> wellfounded_on(M,A,r^+)" 
   161 apply (simp add: wellfounded_on_def) 
   162 apply (safe intro!: equalityI)
   163 apply (rename_tac Z x)
   164 apply (subgoal_tac "M({x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z})") 
   165  prefer 2 
   166  apply (simp add: wellfounded_trancl_separation) 
   167 apply (drule_tac x = "{x\<in>A. \<exists>w. M(w) & \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec) 
   168 apply safe
   169 apply (blast dest: transM, simp) 
   170 apply (rename_tac y w) 
   171 apply (drule_tac x=w in bspec, assumption, clarify)
   172 apply (erule tranclE)
   173   apply (blast dest: transM)   (*transM is needed to prove M(xa)*)
   174  apply blast 
   175 done
   176 
   177 
   178 text{*Relativized to M: Every well-founded relation is a subset of some
   179 inverse image of an ordinal.  Key step is the construction (in M) of a 
   180 rank function.*}
   181 
   182 
   183 (*NEEDS RELATIVIZATION*)
   184 locale M_recursion = M_trancl +
   185   assumes wfrank_separation':
   186      "[| M(r); M(A) |] ==>
   187 	separation
   188 	   (M, \<lambda>x. x \<in> A --> 
   189 		~(\<exists>f. M(f) \<and> is_recfun(r^+, x, %x f. range(f), f)))"
   190  and wfrank_strong_replacement':
   191      "M(r) ==>
   192       strong_replacement(M, \<lambda>x z. \<exists>y f. M(y) & M(f) &
   193 		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & 
   194 		  y = range(f))"
   195  and Ord_wfrank_separation:
   196      "[| M(r); M(A) |] ==>
   197       separation (M, \<lambda>x. x \<in> A \<longrightarrow>
   198                 \<not> (\<forall>f. M(f) \<longrightarrow>
   199                        is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))"
   200 
   201 constdefs 
   202  wellfoundedrank :: "[i=>o,i,i] => i"
   203     "wellfoundedrank(M,r,A) == 
   204         {p. x\<in>A, \<exists>y f. M(y) & M(f) & 
   205                        p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) & 
   206                        y = range(f)}"
   207 
   208 lemma (in M_recursion) exists_wfrank:
   209     "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
   210      ==> \<exists>f. M(f) & is_recfun(r^+, a, %x f. range(f), f)"
   211 apply (rule wellfounded_exists_is_recfun [of A]) 
   212 apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   213 apply (rule trans_trancl [THEN trans_imp_trans_on], assumption+)
   214 apply (simp_all add: trancl_subset_times) 
   215 done
   216 
   217 lemma (in M_recursion) M_wellfoundedrank:
   218     "[| wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) |] 
   219      ==> M(wellfoundedrank(M,r,A))"
   220 apply (insert wfrank_strong_replacement' [of r]) 
   221 apply (simp add: wellfoundedrank_def) 
   222 apply (rule strong_replacement_closed) 
   223    apply assumption+
   224  apply (rule univalent_is_recfun) 
   225      apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   226     apply (rule trans_on_trancl) 
   227    apply (simp add: trancl_subset_times) 
   228   apply blast+
   229 done
   230 
   231 lemma (in M_recursion) Ord_wfrank_range [rule_format]:
   232     "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
   233      ==> \<forall>f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
   234 apply (subgoal_tac "wellfounded_on(M, A, r^+)") 
   235  prefer 2
   236  apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   237 apply (erule wellfounded_on_induct2, assumption+)
   238 apply (simp add: trancl_subset_times) 
   239 apply (blast intro: Ord_wfrank_separation, clarify)
   240 txt{*The reasoning in both cases is that we get @{term y} such that
   241    @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that 
   242    @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
   243 apply (rule OrdI [OF _ Ord_is_Transset])
   244  txt{*An ordinal is a transitive set...*}
   245  apply (simp add: Transset_def) 
   246  apply clarify
   247  apply (frule apply_recfun2, assumption) 
   248  apply (force simp add: restrict_iff)
   249 txt{*...of ordinals.  This second case requires the induction hyp.*} 
   250 apply clarify 
   251 apply (rename_tac i y)
   252 apply (frule apply_recfun2, assumption) 
   253 apply (frule is_recfun_imp_in_r, assumption) 
   254 apply (frule is_recfun_restrict) 
   255     (*simp_all won't work*)
   256     apply (simp add: trans_on_trancl trancl_subset_times)+  
   257 apply (drule spec [THEN mp], assumption)
   258 apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
   259  apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec) 
   260  apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
   261 apply (blast dest: pair_components_in_M)
   262 done
   263 
   264 lemma (in M_recursion) Ord_range_wellfoundedrank:
   265     "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |] 
   266      ==> Ord (range(wellfoundedrank(M,r,A)))"
   267 apply (subgoal_tac "wellfounded_on(M, A, r^+)") 
   268  prefer 2
   269  apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   270 apply (frule trancl_subset_times) 
   271 apply (simp add: wellfoundedrank_def)
   272 apply (rule OrdI [OF _ Ord_is_Transset])
   273  prefer 2
   274  txt{*by our previous result the range consists of ordinals.*} 
   275  apply (blast intro: Ord_wfrank_range) 
   276 txt{*We still must show that the range is a transitive set.*}
   277 apply (simp add: Transset_def, clarify)
   278 apply simp
   279 apply (rename_tac x i f u)   
   280 apply (frule is_recfun_imp_in_r, assumption) 
   281 apply (subgoal_tac "M(u) & M(i) & M(x)") 
   282  prefer 2 apply (blast dest: transM, clarify) 
   283 apply (rule_tac a=u in rangeI) 
   284 apply (rule ReplaceI) 
   285   apply (rule_tac x=i in exI, simp) 
   286   apply (rule_tac x="restrict(f, r^+ -`` {u})" in exI)
   287   apply (blast intro: is_recfun_restrict trans_on_trancl dest: apply_recfun2)
   288  apply blast
   289 txt{*Unicity requirement of Replacement*} 
   290 apply clarify
   291 apply (frule apply_recfun2, assumption) 
   292 apply (simp add: trans_on_trancl is_recfun_cut)+
   293 done
   294 
   295 lemma (in M_recursion) function_wellfoundedrank:
   296     "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   297      ==> function(wellfoundedrank(M,r,A))"
   298 apply (simp add: wellfoundedrank_def function_def, clarify) 
   299 txt{*Uniqueness: repeated below!*}
   300 apply (drule is_recfun_functional, assumption)
   301     apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   302     apply (simp_all add: trancl_subset_times 
   303                          trans_trancl [THEN trans_imp_trans_on]) 
   304 apply (blast dest: transM) 
   305 done
   306 
   307 lemma (in M_recursion) domain_wellfoundedrank:
   308     "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   309      ==> domain(wellfoundedrank(M,r,A)) = A"
   310 apply (simp add: wellfoundedrank_def function_def) 
   311 apply (rule equalityI, auto)
   312 apply (frule transM, assumption)  
   313 apply (frule exists_wfrank, assumption+)
   314 apply clarify 
   315 apply (rule domainI) 
   316 apply (rule ReplaceI)
   317 apply (rule_tac x="range(f)" in exI)
   318 apply simp  
   319 apply (rule_tac x=f in exI, blast)
   320 apply assumption
   321 txt{*Uniqueness (for Replacement): repeated above!*}
   322 apply clarify
   323 apply (drule is_recfun_functional, assumption)
   324     apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   325     apply (simp_all add: trancl_subset_times 
   326                          trans_trancl [THEN trans_imp_trans_on]) 
   327 done
   328 
   329 lemma (in M_recursion) wellfoundedrank_type:
   330     "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   331      ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
   332 apply (frule function_wellfoundedrank, assumption+) 
   333 apply (frule function_imp_Pi) 
   334  apply (simp add: wellfoundedrank_def relation_def) 
   335  apply blast  
   336 apply (simp add: domain_wellfoundedrank)
   337 done
   338 
   339 lemma (in M_recursion) Ord_wellfoundedrank:
   340     "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |] 
   341      ==> Ord(wellfoundedrank(M,r,A) ` a)"
   342 by (blast intro: apply_funtype [OF wellfoundedrank_type]
   343                  Ord_in_Ord [OF Ord_range_wellfoundedrank])
   344 
   345 lemma (in M_recursion) wellfoundedrank_eq:
   346      "[| is_recfun(r^+, a, %x. range, f);
   347          wellfounded(M,r);  a \<in> A; r \<subseteq> A*A;  M(f); M(r); M(A)|] 
   348       ==> wellfoundedrank(M,r,A) ` a = range(f)"
   349 apply (rule apply_equality) 
   350  prefer 2 apply (blast intro: wellfoundedrank_type ) 
   351 apply (simp add: wellfoundedrank_def)
   352 apply (rule ReplaceI)
   353   apply (rule_tac x="range(f)" in exI) 
   354   apply blast 
   355  apply assumption
   356 txt{*Unicity requirement of Replacement*} 
   357 apply clarify
   358 apply (drule is_recfun_functional, assumption)
   359     apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on)
   360     apply (simp_all add: trancl_subset_times 
   361                          trans_trancl [THEN trans_imp_trans_on])
   362 apply (blast dest: transM) 
   363 done
   364 
   365 end