src/ZF/Constructible/WFrec.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 21404 eb85850d3eb7
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      ZF/Constructible/WFrec.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 header{*Relativized Well-Founded Recursion*}
     7 
     8 theory WFrec imports Wellorderings begin
     9 
    10 
    11 subsection{*General Lemmas*}
    12 
    13 (*Many of these might be useful in WF.thy*)
    14 
    15 lemma apply_recfun2:
    16     "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
    17 apply (frule apply_recfun) 
    18  apply (blast dest: is_recfun_type fun_is_rel) 
    19 apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
    20 done
    21 
    22 text{*Expresses @{text is_recfun} as a recursion equation*}
    23 lemma is_recfun_iff_equation:
    24      "is_recfun(r,a,H,f) <->
    25 	   f \<in> r -`` {a} \<rightarrow> range(f) &
    26 	   (\<forall>x \<in> r-``{a}. f`x = H(x, restrict(f, r-``{x})))"  
    27 apply (rule iffI) 
    28  apply (simp add: is_recfun_type apply_recfun Ball_def vimage_singleton_iff, 
    29         clarify)  
    30 apply (simp add: is_recfun_def) 
    31 apply (rule fun_extension) 
    32   apply assumption
    33  apply (fast intro: lam_type, simp) 
    34 done
    35 
    36 lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r"
    37 by (blast dest: is_recfun_type fun_is_rel)
    38 
    39 lemma trans_Int_eq:
    40       "[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
    41 by (blast intro: transD) 
    42 
    43 lemma is_recfun_restrict_idem:
    44      "is_recfun(r,a,H,f) ==> restrict(f, r -`` {a}) = f"
    45 apply (drule is_recfun_type)
    46 apply (auto simp add: Pi_iff subset_Sigma_imp_relation restrict_idem)  
    47 done
    48 
    49 lemma is_recfun_cong_lemma:
    50   "[| is_recfun(r,a,H,f); r = r'; a = a'; f = f'; 
    51       !!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |] 
    52              ==> H(x,g) = H'(x,g) |]
    53    ==> is_recfun(r',a',H',f')"
    54 apply (simp add: is_recfun_def) 
    55 apply (erule trans) 
    56 apply (rule lam_cong) 
    57 apply (simp_all add: vimage_singleton_iff Int_lower2)  
    58 done
    59 
    60 text{*For @{text is_recfun} we need only pay attention to functions
    61       whose domains are initial segments of @{term r}.*}
    62 lemma is_recfun_cong:
    63   "[| r = r'; a = a'; f = f'; 
    64       !!x g. [| <x,a'> \<in> r'; relation(g); domain(g) <= r' -``{x} |] 
    65              ==> H(x,g) = H'(x,g) |]
    66    ==> is_recfun(r,a,H,f) <-> is_recfun(r',a',H',f')"
    67 apply (rule iffI)
    68 txt{*Messy: fast and blast don't work for some reason*}
    69 apply (erule is_recfun_cong_lemma, auto) 
    70 apply (erule is_recfun_cong_lemma)
    71 apply (blast intro: sym)+
    72 done
    73 
    74 subsection{*Reworking of the Recursion Theory Within @{term M}*}
    75 
    76 lemma (in M_basic) is_recfun_separation':
    77     "[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
    78         M(r); M(f); M(g); M(a); M(b) |] 
    79      ==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))"
    80 apply (insert is_recfun_separation [of r f g a b]) 
    81 apply (simp add: vimage_singleton_iff)
    82 done
    83 
    84 text{*Stated using @{term "trans(r)"} rather than
    85       @{term "transitive_rel(M,A,r)"} because the latter rewrites to
    86       the former anyway, by @{text transitive_rel_abs}.
    87       As always, theorems should be expressed in simplified form.
    88       The last three M-premises are redundant because of @{term "M(r)"}, 
    89       but without them we'd have to undertake
    90       more work to set up the induction formula.*}
    91 lemma (in M_basic) is_recfun_equal [rule_format]: 
    92     "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
    93        wellfounded(M,r);  trans(r);
    94        M(f); M(g); M(r); M(x); M(a); M(b) |] 
    95      ==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x"
    96 apply (frule_tac f=f in is_recfun_type) 
    97 apply (frule_tac f=g in is_recfun_type) 
    98 apply (simp add: is_recfun_def)
    99 apply (erule_tac a=x in wellfounded_induct, assumption+)
   100 txt{*Separation to justify the induction*}
   101  apply (blast intro: is_recfun_separation') 
   102 txt{*Now the inductive argument itself*}
   103 apply clarify 
   104 apply (erule ssubst)+
   105 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
   106 apply (rename_tac x1)
   107 apply (rule_tac t="%z. H(x1,z)" in subst_context) 
   108 apply (subgoal_tac "\<forall>y \<in> r-``{x1}. ALL z. <y,z>\<in>f <-> <y,z>\<in>g")
   109  apply (blast intro: transD) 
   110 apply (simp add: apply_iff) 
   111 apply (blast intro: transD sym) 
   112 done
   113 
   114 lemma (in M_basic) is_recfun_cut: 
   115     "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
   116        wellfounded(M,r); trans(r); 
   117        M(f); M(g); M(r); <b,a> \<in> r |]   
   118       ==> restrict(f, r-``{b}) = g"
   119 apply (frule_tac f=f in is_recfun_type) 
   120 apply (rule fun_extension) 
   121 apply (blast intro: transD restrict_type2) 
   122 apply (erule is_recfun_type, simp) 
   123 apply (blast intro: is_recfun_equal transD dest: transM) 
   124 done
   125 
   126 lemma (in M_basic) is_recfun_functional:
   127      "[|is_recfun(r,a,H,f);  is_recfun(r,a,H,g);  
   128        wellfounded(M,r); trans(r); M(f); M(g); M(r) |] ==> f=g"
   129 apply (rule fun_extension)
   130 apply (erule is_recfun_type)+
   131 apply (blast intro!: is_recfun_equal dest: transM) 
   132 done 
   133 
   134 text{*Tells us that @{text is_recfun} can (in principle) be relativized.*}
   135 lemma (in M_basic) is_recfun_relativize:
   136   "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   137    ==> is_recfun(r,a,H,f) <->
   138        (\<forall>z[M]. z \<in> f <-> 
   139         (\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))";
   140 apply (simp add: is_recfun_def lam_def)
   141 apply (safe intro!: equalityI) 
   142    apply (drule equalityD1 [THEN subsetD], assumption) 
   143    apply (blast dest: pair_components_in_M) 
   144   apply (blast elim!: equalityE dest: pair_components_in_M)
   145  apply (frule transM, assumption) 
   146  apply simp  
   147  apply blast
   148 apply (subgoal_tac "is_function(M,f)")
   149  txt{*We use @{term "is_function"} rather than @{term "function"} because
   150       the subgoal's easier to prove with relativized quantifiers!*}
   151  prefer 2 apply (simp add: is_function_def) 
   152 apply (frule pair_components_in_M, assumption) 
   153 apply (simp add: is_recfun_imp_function function_restrictI) 
   154 done
   155 
   156 lemma (in M_basic) is_recfun_restrict:
   157      "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; 
   158        M(r); M(f); 
   159        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
   160        ==> is_recfun(r, y, H, restrict(f, r -`` {y}))"
   161 apply (frule pair_components_in_M, assumption, clarify) 
   162 apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff
   163            trans_Int_eq)
   164 apply safe
   165   apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff]) 
   166   apply (frule_tac x=xa in pair_components_in_M, assumption)
   167   apply (frule_tac x=xa in apply_recfun, blast intro: transD)  
   168   apply (simp add: is_recfun_type [THEN apply_iff] 
   169                    is_recfun_imp_function function_restrictI)
   170 apply (blast intro: apply_recfun dest: transD)
   171 done
   172  
   173 lemma (in M_basic) restrict_Y_lemma:
   174    "[| wellfounded(M,r); trans(r); M(r);
   175        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(Y);
   176        \<forall>b[M]. 
   177 	   b \<in> Y <->
   178 	   (\<exists>x[M]. <x,a1> \<in> r &
   179             (\<exists>y[M]. b = \<langle>x,y\<rangle> & (\<exists>g[M]. is_recfun(r,x,H,g) \<and> y = H(x,g))));
   180           \<langle>x,a1\<rangle> \<in> r; is_recfun(r,x,H,f); M(f) |]
   181        ==> restrict(Y, r -`` {x}) = f"
   182 apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y <-> <y,z>:f") 
   183  apply (simp (no_asm_simp) add: restrict_def) 
   184  apply (thin_tac "rall(M,?P)")+  --{*essential for efficiency*}
   185  apply (frule is_recfun_type [THEN fun_is_rel], blast)
   186 apply (frule pair_components_in_M, assumption, clarify) 
   187 apply (rule iffI)
   188  apply (frule_tac y="<y,z>" in transM, assumption)
   189  apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
   190 			   apply_recfun is_recfun_cut) 
   191 txt{*Opposite inclusion: something in f, show in Y*}
   192 apply (frule_tac y="<y,z>" in transM, assumption)  
   193 apply (simp add: vimage_singleton_iff) 
   194 apply (rule conjI) 
   195  apply (blast dest: transD) 
   196 apply (rule_tac x="restrict(f, r -`` {y})" in rexI) 
   197 apply (simp_all add: is_recfun_restrict
   198                      apply_recfun is_recfun_type [THEN apply_iff]) 
   199 done
   200 
   201 text{*For typical applications of Replacement for recursive definitions*}
   202 lemma (in M_basic) univalent_is_recfun:
   203      "[|wellfounded(M,r); trans(r); M(r)|]
   204       ==> univalent (M, A, \<lambda>x p. 
   205               \<exists>y[M]. p = \<langle>x,y\<rangle> & (\<exists>f[M]. is_recfun(r,x,H,f) & y = H(x,f)))"
   206 apply (simp add: univalent_def) 
   207 apply (blast dest: is_recfun_functional) 
   208 done
   209 
   210 
   211 text{*Proof of the inductive step for @{text exists_is_recfun}, since
   212       we must prove two versions.*}
   213 lemma (in M_basic) exists_is_recfun_indstep:
   214     "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f[M]. is_recfun(r, y, H, f)); 
   215        wellfounded(M,r); trans(r); M(r); M(a1);
   216        strong_replacement(M, \<lambda>x z. 
   217               \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   218        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]   
   219       ==> \<exists>f[M]. is_recfun(r,a1,H,f)"
   220 apply (drule_tac A="r-``{a1}" in strong_replacementD)
   221   apply blast 
   222  txt{*Discharge the "univalent" obligation of Replacement*}
   223  apply (simp add: univalent_is_recfun) 
   224 txt{*Show that the constructed object satisfies @{text is_recfun}*} 
   225 apply clarify 
   226 apply (rule_tac x=Y in rexI)  
   227 txt{*Unfold only the top-level occurrence of @{term is_recfun}*}
   228 apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1])
   229 txt{*The big iff-formula defining @{term Y} is now redundant*}
   230 apply safe 
   231  apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H _ a1]) 
   232 txt{*one more case*}
   233 apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff)
   234 apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 
   235 apply (rename_tac f) 
   236 apply (rule_tac x=f in rexI) 
   237 apply (simp_all add: restrict_Y_lemma [of r H])
   238 txt{*FIXME: should not be needed!*}
   239 apply (subst restrict_Y_lemma [of r H])
   240 apply (simp add: vimage_singleton_iff)+
   241 apply blast+
   242 done
   243 
   244 text{*Relativized version, when we have the (currently weaker) premise
   245       @{term "wellfounded(M,r)"}*}
   246 lemma (in M_basic) wellfounded_exists_is_recfun:
   247     "[|wellfounded(M,r);  trans(r);  
   248        separation(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r, x, H, f)));
   249        strong_replacement(M, \<lambda>x z. 
   250           \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   251        M(r);  M(a);  
   252        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]   
   253       ==> \<exists>f[M]. is_recfun(r,a,H,f)"
   254 apply (rule wellfounded_induct, assumption+, clarify)
   255 apply (rule exists_is_recfun_indstep, assumption+)
   256 done
   257 
   258 lemma (in M_basic) wf_exists_is_recfun [rule_format]:
   259     "[|wf(r);  trans(r);  M(r);  
   260        strong_replacement(M, \<lambda>x z. 
   261          \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   262        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]   
   263       ==> M(a) --> (\<exists>f[M]. is_recfun(r,a,H,f))"
   264 apply (rule wf_induct, assumption+)
   265 apply (frule wf_imp_relativized)
   266 apply (intro impI)
   267 apply (rule exists_is_recfun_indstep) 
   268       apply (blast dest: transM del: rev_rallE, assumption+)
   269 done
   270 
   271 
   272 subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
   273 
   274 definition
   275   M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where
   276    "M_is_recfun(M,MH,r,a,f) == 
   277      \<forall>z[M]. z \<in> f <-> 
   278             (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
   279 	       pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
   280                pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
   281                xa \<in> r & MH(x, f_r_sx, y))"
   282 
   283 definition
   284   is_wfrec :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where
   285    "is_wfrec(M,MH,r,a,z) == 
   286       \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)"
   287 
   288 definition
   289   wfrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o" where
   290    "wfrec_replacement(M,MH,r) ==
   291         strong_replacement(M, 
   292              \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & is_wfrec(M,MH,r,x,y))"
   293 
   294 lemma (in M_basic) is_recfun_abs:
   295      "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(r); M(a); M(f); 
   296          relation2(M,MH,H) |] 
   297       ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)"
   298 apply (simp add: M_is_recfun_def relation2_def is_recfun_relativize)
   299 apply (rule rall_cong)
   300 apply (blast dest: transM)
   301 done
   302 
   303 lemma M_is_recfun_cong [cong]:
   304      "[| r = r'; a = a'; f = f'; 
   305        !!x g y. [| M(x); M(g); M(y) |] ==> MH(x,g,y) <-> MH'(x,g,y) |]
   306       ==> M_is_recfun(M,MH,r,a,f) <-> M_is_recfun(M,MH',r',a',f')"
   307 by (simp add: M_is_recfun_def) 
   308 
   309 lemma (in M_basic) is_wfrec_abs:
   310      "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
   311          relation2(M,MH,H);  M(r); M(a); M(z) |]
   312       ==> is_wfrec(M,MH,r,a,z) <-> 
   313           (\<exists>g[M]. is_recfun(r,a,H,g) & z = H(a,g))"
   314 by (simp add: is_wfrec_def relation2_def is_recfun_abs)
   315 
   316 text{*Relating @{term wfrec_replacement} to native constructs*}
   317 lemma (in M_basic) wfrec_replacement':
   318   "[|wfrec_replacement(M,MH,r);
   319      \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
   320      relation2(M,MH,H);  M(r)|] 
   321    ==> strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
   322                 pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g)))"
   323 by (simp add: wfrec_replacement_def is_wfrec_abs) 
   324 
   325 lemma wfrec_replacement_cong [cong]:
   326      "[| !!x y z. [| M(x); M(y); M(z) |] ==> MH(x,y,z) <-> MH'(x,y,z);
   327          r=r' |] 
   328       ==> wfrec_replacement(M, %x y. MH(x,y), r) <-> 
   329           wfrec_replacement(M, %x y. MH'(x,y), r')" 
   330 by (simp add: is_wfrec_def wfrec_replacement_def) 
   331 
   332 
   333 end
   334