section‹Some enhanced theorems on recursion› theory Recursion_Thms imports "Eclose_Absolute" begin hide_const (open) Order.pred ― ‹Removing arities from inherited simpset› declare arity_And [simp del] arity_Or[simp del] arity_Implies[simp del] arity_Exists[simp del] arity_Iff[simp del] arity_subset_fm [simp del] arity_ordinal_fm[simp del] arity_transset_fm[simp del] text‹We prove results concerning definitions by well-founded recursion on some relation \<^term>‹R› and its transitive closure \<^term>‹R^*›› lemma fld_restrict_eq : "a ∈ A ⟹ (r ∩ A×A)-``{a} = (r-``{a} ∩ A)" by(force) lemma fld_restrict_mono : "relation(r) ⟹ A ⊆ B ⟹ r ∩ A×A ⊆ r ∩ B×B" by(auto) lemma fld_restrict_dom : assumes "relation(r)" "domain(r) ⊆ A" "range(r)⊆ A" shows "r∩ A×A = r" proof (rule equalityI,blast,rule subsetI) { fix x assume xr: "x ∈ r" from xr assms have "∃ a b . x = ⟨a,b⟩" by (simp add: relation_def) then obtain a b where "⟨a,b⟩ ∈ r" "⟨a,b⟩ ∈ r∩A×A" "x ∈ r∩A×A" using assms xr by force then have "x∈ r ∩ A×A" by simp } then show "x ∈ r ⟹ x∈ r∩A×A" for x . qed definition tr_down :: "[i,i] ⇒ i" where "tr_down(r,a) = (r^+)-``{a}" lemma tr_downD : "x ∈ tr_down(r,a) ⟹ ⟨x,a⟩ ∈ r^+" by (simp add: tr_down_def vimage_singleton_iff) lemma pred_down : "relation(r) ⟹ r-``{a} ⊆ tr_down(r,a)" by(simp add: tr_down_def vimage_mono r_subset_trancl) lemma tr_down_mono : "relation(r) ⟹ x ∈ r-``{a} ⟹ tr_down(r,x) ⊆ tr_down(r,a)" by(rule subsetI,simp add:tr_down_def,auto dest: underD,force simp add: underI r_into_trancl trancl_trans) lemma rest_eq : assumes "relation(r)" and "r-``{a} ⊆ B" and "a ∈ B" shows "r-``{a} = (r∩B×B)-``{a}" proof (intro equalityI subsetI) fix x assume "x ∈ r-``{a}" then have "x ∈ B" using assms by (simp add: subsetD) from ‹x∈ r-``{a}› have "⟨x,a⟩ ∈ r" using underD by simp then show "x ∈ (r∩B×B)-``{a}" using ‹x∈B› ‹a∈B› underI by simp next from assms show "x ∈ r -`` {a}" if "x ∈ (r ∩ B×B) -`` {a}" for x using vimage_mono that by auto qed lemma wfrec_restr_eq : "r' = r ∩ A×A ⟹ wfrec[A](r,a,H) = wfrec(r',a,H)" by(simp add:wfrec_on_def) lemma wfrec_restr : assumes rr: "relation(r)" and wfr:"wf(r)" shows "a ∈ A ⟹ tr_down(r,a) ⊆ A ⟹ wfrec(r,a,H) = wfrec[A](r,a,H)" proof (induct a arbitrary:A rule:wf_induct_raw[OF wfr] ) case (1 a) have wfRa : "wf[A](r)" using wf_subset wfr wf_on_def Int_lower1 by simp from pred_down rr have "r -`` {a} ⊆ tr_down(r, a)" . with 1 have "r-``{a} ⊆ A" by (force simp add: subset_trans) { fix x assume x_a : "x ∈ r-``{a}" with ‹r-``{a} ⊆ A› have "x ∈ A" .. from pred_down rr have b : "r -``{x} ⊆ tr_down(r,x)" . then have "tr_down(r,x) ⊆ tr_down(r,a)" using tr_down_mono x_a rr by simp with 1 have "tr_down(r,x) ⊆ A" using subset_trans by force have "⟨x,a⟩ ∈ r" using x_a underD by simp with 1 ‹tr_down(r,x) ⊆ A› ‹x ∈ A› have "wfrec(r,x,H) = wfrec[A](r,x,H)" by simp } then have "x∈ r-``{a} ⟹ wfrec(r,x,H) = wfrec[A](r,x,H)" for x . then have Eq1 :"(λ x ∈ r-``{a} . wfrec(r,x,H)) = (λ x ∈ r-``{a} . wfrec[A](r,x,H))" using lam_cong by simp from assms have "wfrec(r,a,H) = H(a,λ x ∈ r-``{a} . wfrec(r,x,H))" by (simp add:wfrec) also have "... = H(a,λ x ∈ r-``{a} . wfrec[A](r,x,H))" using assms Eq1 by simp also from 1 ‹r-``{a} ⊆ A› have "... = H(a,λ x ∈ (r∩A×A)-``{a} . wfrec[A](r,x,H))" using assms rest_eq by simp also from ‹a∈A› have "... = H(a,λ x ∈ (r-``{a})∩A . wfrec[A](r,x,H))" using fld_restrict_eq by simp also from ‹a∈A› ‹wf[A](r)› have "... = wfrec[A](r,a,H)" using wfrec_on by simp finally show ?case . qed lemmas wfrec_tr_down = wfrec_restr[OF _ _ _ subset_refl] lemma wfrec_trans_restr : "relation(r) ⟹ wf(r) ⟹ trans(r) ⟹ r-``{a}⊆A ⟹ a ∈ A ⟹ wfrec(r, a, H) = wfrec[A](r, a, H)" by(subgoal_tac "tr_down(r,a) ⊆ A",auto simp add : wfrec_restr tr_down_def trancl_eq_r) lemma field_trancl : "field(r^+) = field(r)" by (blast intro: r_into_trancl dest!: trancl_type [THEN subsetD]) definition Rrel :: "[i⇒i⇒o,i] ⇒ i" where "Rrel(R,A) ≡ {z∈A×A. ∃x y. z = ⟨x, y⟩ ∧ R(x,y)}" lemma RrelI : "x ∈ A ⟹ y ∈ A ⟹ R(x,y) ⟹ ⟨x,y⟩ ∈ Rrel(R,A)" unfolding Rrel_def by simp lemma Rrel_mem: "Rrel(mem,x) = Memrel(x)" unfolding Rrel_def Memrel_def .. lemma relation_Rrel: "relation(Rrel(R,d))" unfolding Rrel_def relation_def by simp lemma field_Rrel: "field(Rrel(R,d)) ⊆ d" unfolding Rrel_def by auto lemma Rrel_mono : "A ⊆ B ⟹ Rrel(R,A) ⊆ Rrel(R,B)" unfolding Rrel_def by blast lemma Rrel_restr_eq : "Rrel(R,A) ∩ B×B = Rrel(R,A∩B)" unfolding Rrel_def by blast ― ‹We obtain this lemmas as a consequence of the previous one; alternatively it can be obtained using @{thm [source] Ordinal.Memrel_type}› lemma field_Memrel : "field(Memrel(A)) ⊆ A" using Rrel_mem field_Rrel by blast lemma restrict_trancl_Rrel: assumes "R(w,y)" shows "restrict(f,Rrel(R,d)-``{y})`w = restrict(f,(Rrel(R,d)^+)-``{y})`w" proof (cases "y∈d") let ?r="Rrel(R,d)" and ?s="(Rrel(R,d))^+" case True show ?thesis proof (cases "w∈d") case True with ‹y∈d› assms have "⟨w,y⟩∈?r" unfolding Rrel_def by blast then have "⟨w,y⟩∈?s" using r_subset_trancl[of ?r] relation_Rrel[of R d] by blast with ‹⟨w,y⟩∈?r› have "w∈?r-``{y}" "w∈?s-``{y}" using vimage_singleton_iff by simp_all then show ?thesis by simp next case False then have "w∉domain(restrict(f,?r-``{y}))" using subsetD[OF field_Rrel[of R d]] by auto moreover from ‹w∉d› have "w∉domain(restrict(f,?s-``{y}))" using subsetD[OF field_Rrel[of R d], of w] field_trancl[of ?r] fieldI1[of w y ?s] by auto ultimately have "restrict(f,?r-``{y})`w = 0" "restrict(f,?s-``{y})`w = 0" unfolding apply_def by auto then show ?thesis by simp qed next let ?r="Rrel(R,d)" let ?s="?r^+" case False then have "?r-``{y}=0" unfolding Rrel_def by blast then have "w∉?r-``{y}" by simp with ‹y∉d› assms have "y∉field(?s)" using field_trancl subsetD[OF field_Rrel[of R d]] by force then have "w∉?s-``{y}" using vimage_singleton_iff by blast with ‹w∉?r-``{y}› show ?thesis by simp qed lemma restrict_trans_eq: assumes "w ∈ y" shows "restrict(f,Memrel(eclose({x}))-``{y})`w = restrict(f,(Memrel(eclose({x}))^+)-``{y})`w" using assms restrict_trancl_Rrel[of mem ] Rrel_mem by (simp) lemma wf_eq_trancl: assumes "⋀ f y . H(y,restrict(f,R-``{y})) = H(y,restrict(f,R^+-``{y}))" shows "wfrec(R, x, H) = wfrec(R^+, x, H)" (is "wfrec(?r,_,_) = wfrec(?r',_,_)") proof - have "wfrec(R, x, H) = wftrec(?r^+, x, λy f. H(y, restrict(f,?r-``{y})))" unfolding wfrec_def .. also have " ... = wftrec(?r^+, x, λy f. H(y, restrict(f,(?r^+)-``{y})))" using assms by simp also have " ... = wfrec(?r^+, x, H)" unfolding wfrec_def using trancl_eq_r[OF relation_trancl trans_trancl] by simp finally show ?thesis . qed lemma transrec_equal_on_Ord: assumes "⋀x f . Ord(x) ⟹ foo(x,f) = bar(x,f)" "Ord(α)" shows "transrec(α, foo) = transrec(α, bar)" proof - have "transrec(β,foo) = transrec(β,bar)" if "Ord(β)" for β using that proof (induct rule:trans_induct) case (step β) have "transrec(β, foo) = foo(β, λx∈β. transrec(x, foo))" using def_transrec[of "λx. transrec(x, foo)" foo] by blast also from assms and step have " … = bar(β, λx∈β. transrec(x, foo))" by simp also from step have " … = bar(β, λx∈β. transrec(x, bar))" by (auto) also have " … = transrec(β, bar)" using def_transrec[of "λx. transrec(x, bar)" bar, symmetric] by blast finally show "transrec(β, foo) = transrec(β, bar)" . qed with assms show ?thesis by simp qed ― ‹Next theorem is very similar to @{thm [source] transrec_equal_on_Ord}› lemma (in M_eclose) transrec_equal_on_M: assumes "⋀x f . M(x) ⟹ M(f) ⟹ foo(x,f) = bar(x,f)" "⋀β. M(β) ⟹ transrec_replacement(M,is_foo,β)" "relation2(M,is_foo,foo)" "strong_replacement(M, λx y. y = ⟨x, transrec(x, foo)⟩)" "∀x[M]. ∀g[M]. function(g) ⟶ M(foo(x,g))" "M(α)" "Ord(α)" shows "transrec(α, foo) = transrec(α, bar)" proof - have "M(transrec(x, foo))" if "Ord(x)" and "M(x)" for x using that assms transrec_closed[of is_foo] by simp have "transrec(β,foo) = transrec(β,bar)" "M(transrec(β,foo))" if "Ord(β)" "M(β)" for β using that proof (induct rule:trans_induct) case (step β) moreover assume "M(β)" moreover note ‹Ord(β)⟹ M(β) ⟹ M(transrec(β, foo))› ultimately show "M(transrec(β, foo))" by blast with step ‹M(β)› ‹⋀x. Ord(x)⟹ M(x) ⟹ M(transrec(x, foo))› ‹strong_replacement(M, λx y. y = ⟨x, transrec(x, foo)⟩)› have "M(λx∈β. transrec(x, foo))" using Ord_in_Ord transM[of _ β] by (rule_tac lam_closed) auto have "transrec(β, foo) = foo(β, λx∈β. transrec(x, foo))" using def_transrec[of "λx. transrec(x, foo)" foo] by blast also from assms and ‹M(λx∈β. transrec(x, foo))› ‹M(β)› have " … = bar(β, λx∈β. transrec(x, foo))" by simp also from step and ‹M(β)› have " … = bar(β, λx∈β. transrec(x, bar))" using transM[of _ β] by (auto) also have " … = transrec(β, bar)" using def_transrec[of "λx. transrec(x, bar)" bar, symmetric] by blast finally show "transrec(β, foo) = transrec(β, bar)" . qed with assms show ?thesis by simp qed lemma ordermap_restr_eq: assumes "well_ord(X,r)" shows "ordermap(X, r) = ordermap(X, r ∩ X×X)" proof - let ?A="λx . Order.pred(X, x, r)" let ?B="λx . Order.pred(X, x, r ∩ X × X)" let ?F="λx f. f `` ?A(x)" let ?G="λx f. f `` ?B(x)" let ?P="λ z. z∈X ⟶ wfrec(r ∩ X × X,z,λx f. f `` ?A(x)) = wfrec(r ∩ X × X,z,λx f. f `` ?B(x))" have pred_eq: "Order.pred(X, x, r ∩ X × X) = Order.pred(X, x, r)" if "x∈X" for x unfolding Order.pred_def using that by auto from assms have wf_onX:"wf(r ∩ X × X)" unfolding well_ord_def wf_on_def by simp { have "?P(z)" for z proof(induct rule:wf_induct[where P="?P",OF wf_onX]) case (1 x) { assume "x∈X" from 1 have lam_eq: "(λw∈(r ∩ X × X) -`` {x}. wfrec(r ∩ X × X, w, ?F)) = (λw∈(r ∩ X × X) -`` {x}. wfrec(r ∩ X × X, w, ?G))" (is "?L=?R") proof - have "wfrec(r ∩ X × X, w, ?F) = wfrec(r ∩ X × X, w, ?G)" if "w∈(r∩X×X)-``{x}" for w using 1 that by auto then show ?thesis using lam_cong[OF refl] by simp qed then have "wfrec(r ∩ X × X, x, ?F) = ?L `` ?A(x)" using wfrec[OF wf_onX,of x ?F] by simp also have "... = ?R `` ?B(x)" using lam_eq pred_eq[OF ‹x∈_›] by simp also have "... = wfrec(r ∩ X × X, x, ?G)" using wfrec[OF wf_onX,of x ?G] by simp finally have "wfrec(r ∩ X × X, x, ?F) = wfrec(r ∩ X × X, x, ?G)" by simp } then show ?case by simp qed } then show ?thesis unfolding ordermap_def wfrec_on_def using Int_ac by simp qed end