1(* Title: ZF/Constructible/WFrec.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3*) 4 5section\<open>Relativized Well-Founded Recursion\<close> 6 7theory WFrec imports Wellorderings begin 8 9 10subsection\<open>General Lemmas\<close> 11 12(*Many of these might be useful in WF.thy*) 13 14lemma apply_recfun2: 15 "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))" 16apply (frule apply_recfun) 17 apply (blast dest: is_recfun_type fun_is_rel) 18apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) 19done 20 21text\<open>Expresses \<open>is_recfun\<close> as a recursion equation\<close> 22lemma 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})))" 26apply (rule iffI) 27 apply (simp add: is_recfun_type apply_recfun Ball_def vimage_singleton_iff, 28 clarify) 29apply (simp add: is_recfun_def) 30apply (rule fun_extension) 31 apply assumption 32 apply (fast intro: lam_type, simp) 33done 34 35lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r" 36by (blast dest: is_recfun_type fun_is_rel) 37 38lemma trans_Int_eq: 39 "[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}" 40by (blast intro: transD) 41 42lemma is_recfun_restrict_idem: 43 "is_recfun(r,a,H,f) ==> restrict(f, r -`` {a}) = f" 44apply (drule is_recfun_type) 45apply (auto simp add: Pi_iff subset_Sigma_imp_relation restrict_idem) 46done 47 48lemma 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')" 53apply (simp add: is_recfun_def) 54apply (erule trans) 55apply (rule lam_cong) 56apply (simp_all add: vimage_singleton_iff Int_lower2) 57done 58 59text\<open>For \<open>is_recfun\<close> we need only pay attention to functions 60 whose domains are initial segments of \<^term>\<open>r\<close>.\<close> 61lemma 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')" 66apply (rule iffI) 67txt\<open>Messy: fast and blast don't work for some reason\<close> 68apply (erule is_recfun_cong_lemma, auto) 69apply (erule is_recfun_cong_lemma) 70apply (blast intro: sym)+ 71done 72 73subsection\<open>Reworking of the Recursion Theory Within \<^term>\<open>M\<close>\<close> 74 75lemma (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))" 79apply (insert is_recfun_separation [of r f g a b]) 80apply (simp add: vimage_singleton_iff) 81done 82 83text\<open>Stated using \<^term>\<open>trans(r)\<close> rather than 84 \<^term>\<open>transitive_rel(M,A,r)\<close> 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>\<open>M(r)\<close>, 88 but without them we'd have to undertake 89 more work to set up the induction formula.\<close> 90lemma (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" 95apply (frule_tac f=f in is_recfun_type) 96apply (frule_tac f=g in is_recfun_type) 97apply (simp add: is_recfun_def) 98apply (erule_tac a=x in wellfounded_induct, assumption+) 99txt\<open>Separation to justify the induction\<close> 100 apply (blast intro: is_recfun_separation') 101txt\<open>Now the inductive argument itself\<close> 102apply clarify 103apply (erule ssubst)+ 104apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) 105apply (rename_tac x1) 106apply (rule_tac t="%z. H(x1,z)" in subst_context) 107apply (subgoal_tac "\<forall>y \<in> r-``{x1}. \<forall>z. <y,z>\<in>f \<longleftrightarrow> <y,z>\<in>g") 108 apply (blast intro: transD) 109apply (simp add: apply_iff) 110apply (blast intro: transD sym) 111done 112 113lemma (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" 118apply (frule_tac f=f in is_recfun_type) 119apply (rule fun_extension) 120apply (blast intro: transD restrict_type2) 121apply (erule is_recfun_type, simp) 122apply (blast intro: is_recfun_equal transD dest: transM) 123done 124 125lemma (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" 128apply (rule fun_extension) 129apply (erule is_recfun_type)+ 130apply (blast intro!: is_recfun_equal dest: transM) 131done 132 133text\<open>Tells us that \<open>is_recfun\<close> can (in principle) be relativized.\<close> 134lemma (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}))>))" 139apply (simp add: is_recfun_def lam_def) 140apply (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 147apply (subgoal_tac "is_function(M,f)") 148 txt\<open>We use \<^term>\<open>is_function\<close> rather than \<^term>\<open>function\<close> because 149 the subgoal's easier to prove with relativized quantifiers!\<close> 150 prefer 2 apply (simp add: is_function_def) 151apply (frule pair_components_in_M, assumption) 152apply (simp add: is_recfun_imp_function function_restrictI) 153done 154 155lemma (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}))" 160apply (frule pair_components_in_M, assumption, clarify) 161apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff 162 trans_Int_eq) 163apply 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) 169apply (blast intro: apply_recfun dest: transD) 170done 171 172lemma (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" 181apply (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) 185apply (frule pair_components_in_M, assumption, clarify) 186apply (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) 190txt\<open>Opposite inclusion: something in f, show in Y\<close> 191apply (frule_tac y="<y,z>" in transM, assumption) 192apply (simp add: vimage_singleton_iff) 193apply (rule conjI) 194 apply (blast dest: transD) 195apply (rule_tac x="restrict(f, r -`` {y})" in rexI) 196apply (simp_all add: is_recfun_restrict 197 apply_recfun is_recfun_type [THEN apply_iff]) 198done 199 200text\<open>For typical applications of Replacement for recursive definitions\<close> 201lemma (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)))" 205apply (simp add: univalent_def) 206apply (blast dest: is_recfun_functional) 207done 208 209 210text\<open>Proof of the inductive step for \<open>exists_is_recfun\<close>, since 211 we must prove two versions.\<close> 212lemma (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)" 219apply (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) 223txt\<open>Show that the constructed object satisfies \<open>is_recfun\<close>\<close> 224apply clarify 225apply (rule_tac x=Y in rexI) 226txt\<open>Unfold only the top-level occurrence of \<^term>\<open>is_recfun\<close>\<close> 227apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1]) 228txt\<open>The big iff-formula defining \<^term>\<open>Y\<close> is now redundant\<close> 229apply safe 230 apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H _ a1]) 231txt\<open>one more case\<close> 232apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff) 233apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 234apply (rename_tac f) 235apply (rule_tac x=f in rexI) 236apply (simp_all add: restrict_Y_lemma [of r H]) 237txt\<open>FIXME: should not be needed!\<close> 238apply (subst restrict_Y_lemma [of r H]) 239apply (simp add: vimage_singleton_iff)+ 240apply blast+ 241done 242 243text\<open>Relativized version, when we have the (currently weaker) premise 244 \<^term>\<open>wellfounded(M,r)\<close>\<close> 245lemma (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)" 253apply (rule wellfounded_induct, assumption+, clarify) 254apply (rule exists_is_recfun_indstep, assumption+) 255done 256 257lemma (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))" 263apply (rule wf_induct, assumption+) 264apply (frule wf_imp_relativized) 265apply (intro impI) 266apply (rule exists_is_recfun_indstep) 267 apply (blast dest: transM del: rev_rallE, assumption+) 268done 269 270 271subsection\<open>Relativization of the ZF Predicate \<^term>\<open>is_recfun\<close>\<close> 272 273definition 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 282definition 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 287definition 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 293lemma (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)" 297apply (simp add: M_is_recfun_def relation2_def is_recfun_relativize) 298apply (rule rall_cong) 299apply (blast dest: transM) 300done 301 302lemma 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')" 306by (simp add: M_is_recfun_def) 307 308lemma (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))" 313by (simp add: is_wfrec_def relation2_def is_recfun_abs) 314 315text\<open>Relating \<^term>\<open>wfrec_replacement\<close> to native constructs\<close> 316lemma (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)))" 322by (simp add: wfrec_replacement_def is_wfrec_abs) 323 324lemma 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')" 329by (simp add: is_wfrec_def wfrec_replacement_def) 330 331 332end 333 334