section‹Some enhanced theorems on recursion›
theory Recursion_Thms imports ZF.Epsilon begin
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
{ fix x
assume "x ∈ r-``{a}"
then have "x ∈ B" using assms by (simp add: subsetD)
from ‹x∈ r-``{a}› underD have "<x,a> ∈ r" by simp
then have "x ∈ (r∩B*B)-``{a}" using ‹x ∈ B› ‹a∈B› underI by simp
}
then show "r -`` {a} ⊆ (r∩B*B)-`` {a}" by auto
next
from vimage_mono assms
show "(r∩B*B) -`` {a} ⊆ r -`` {a}" 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)
from wf_subset wfr wf_on_def Int_lower1 have wfRa : "wf[A](r)" by simp
from pred_down rr have "r -`` {a} ⊆ tr_down(r, a)" .
then have "r-``{a} ⊆ A" using 1 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
then have "tr_down(r,x) ⊆ A" using 1 subset_trans by force
have "<x,a> ∈ r" using x_a underD by simp
then have "wfrec(r,x,H) = wfrec[A](r,x,H)"
using 1 ‹tr_down(r,x) ⊆ A› ‹x ∈ A› 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 have "... = H(a,λ x ∈ (r∩A*A)-``{a} . wfrec[A](r,x,H))"
using 1 assms rest_eq ‹r-``{a} ⊆ A› by simp
also have "... = H(a,λ x ∈ (r-``{a})∩A . wfrec[A](r,x,H))"
using ‹a∈A› fld_restrict_eq by simp
also have "... = wfrec[A](r,a,H)" using ‹wf[A](r)› ‹a∈A› 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
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
end