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