Theory Wellfounded_Transitive_Recursion
subsection ‹Well-Founded Transitive Recursion›
theory Wellfounded_Transitive_Recursion
imports
Binary_Relations_Transitive
Binary_Relations_Wellfounded
Binary_Relation_Functions
Functions_Restrict
begin
paragraph ‹Summary›
text ‹Well-founded recursion on transitive, well-founded relations. One can extend this to
well-founded recursion on non-transitive, well-founded relations since the transitive closure of a
well-founded relation is well-founded.›
context
includes fun_restrict_syntax and no rel_restrict_syntax
begin
definition "fun_rel_restrict f R y ≡ f↾⇘R¯ y :: 'a ⇒ bool⇙"
lemma fun_rel_restrict_eq [simp]:
assumes "R x y"
shows "fun_rel_restrict f R y x = f x"
using assms unfolding fun_rel_restrict_def by auto
lemma fun_rel_restrict_if_not [simp]:
assumes "¬(R x y)"
shows "fun_rel_restrict f R y x = undefined"
using assms unfolding fun_rel_restrict_def by auto
lemma fun_rel_restrict_eq_fun_restrict: "fun_rel_restrict f R y = f↾⇘R¯ y⇙"
unfolding fun_rel_restrict_def by auto
lemma fun_rel_restrict_cong [cong]:
assumes "y = y'"
and "⋀x. R x y' ⟷ R' x y'"
and "⋀x. R' x y' ⟹ f x = g x"
shows "fun_rel_restrict f R y = fun_rel_restrict g R' y"
using assms by (intro ext) (auto simp: fun_rel_restrict_eq_fun_restrict fun_restrict_eq_if)
lemma fun_rel_restrict_rel_restrict_eq_fun_restrict_fun_rel_restrictI [simp]:
assumes "P x"
shows "fun_rel_restrict f (rel_restrict R P) x = (fun_rel_restrict f R x)↾⇘P⇙"
using assms unfolding fun_rel_restrict_eq_fun_restrict fun_restrict_eq_if by fastforce
context
fixes R :: "'a ⇒ 'a ⇒ bool" and step :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b"
begin
definition "wf_rec_step f x = step (fun_rel_restrict (f x) R x) x"
lemma wf_rec_step_eq: "wf_rec_step f x = step (fun_rel_restrict (f x) R x) x"
unfolding wf_rec_step_def by simp
definition "is_recfun X f ≡ f = fun_rel_restrict (wf_rec_step (λ_. f)) R X"
definition "the_recfun X = (THE f. is_recfun X f)"
lemma is_recfunI [intro]:
assumes "⋀x. R x X ⟹ f x = wf_rec_step (λ_. f) x"
and "⋀x. ¬(R x X) ⟹ f x = undefined"
shows "is_recfun X f"
using assms unfolding is_recfun_def wf_rec_step_eq fun_rel_restrict_eq_fun_restrict fun_restrict_eq_if
by (intro ext) simp
lemma is_recfunE [elim]:
assumes "is_recfun X f"
obtains "⋀x. R x X ⟹ f x = wf_rec_step (λ_. f) x"
"⋀x. ¬(R x X) ⟹ f x = undefined"
using assms[unfolded is_recfun_def, THEN fun_cong]
unfolding fun_rel_restrict_eq_fun_restrict fun_restrict_eq_if
by simp
lemma eq_if_rel_if_is_recfun:
assumes "is_recfun X f"
and "R x X"
shows "f x = wf_rec_step (λ_. f) x"
using assms by auto
lemma eq_if_not_rel_if_is_recfun:
assumes "is_recfun X f"
and "¬(R x X)"
shows "f x = undefined"
using assms by auto
context
assumes wf: "wellfounded R"
and trans: "transitive R"
begin
lemma app_eq_app_if_is_recfunI:
assumes "is_recfun X f" "is_recfun Y g"
and "R Z X" "R Z Y"
shows "f Z = g Z"
using wf ‹R Z X› ‹R Z Y›
proof (induction Z rule: wellfounded_induct)
case (step Z)
then have "f z = g z" if "R z Z" for z using that trans by auto
moreover have "f Z = wf_rec_step (λ_. f) Z" "g Z = wf_rec_step (λ_. g) Z" using assms step.prems by auto
ultimately show ?case by (auto simp: wf_rec_step_eq)
qed
corollary eq_if_is_recfunI:
assumes "is_recfun X f" "is_recfun X g"
shows "f = g"
proof (intro ext)
fix x from assms app_eq_app_if_is_recfunI show "f x = g x" by (cases "R x X") force+
qed
corollary is_recfun_the_recfun_if_is_recfunI:
assumes "is_recfun X f"
shows "is_recfun X (the_recfun X)"
proof -
from assms eq_if_is_recfunI have "∃!g. is_recfun X g" by auto
from theI'[OF this] show ?thesis unfolding the_recfun_def by auto
qed
corollary fun_rel_restrict_eq_fun_rel_restrict_if_is_recfunI:
assumes recfuns: "is_recfun x f" "is_recfun X g"
and "R x X"
shows "fun_rel_restrict f R x = fun_rel_restrict g R x"
proof -
have "f y = g y" if "R y x" for y
using app_eq_app_if_is_recfunI[OF recfuns] ‹R y x› ‹R x X› trans by blast
then show ?thesis by auto
qed
definition "wft_rec ≡ wf_rec_step the_recfun"
lemma ex_is_recfunI: "∃f. is_recfun X f"
using wf
proof (induction X rule: wellfounded_induct)
case (step X)
then have is_recfun: "is_recfun x (the_recfun x)" if "R x X" for x
using is_recfun_the_recfun_if_is_recfunI that by blast
define f where "f ≡ fun_rel_restrict wft_rec R X"
have "fun_rel_restrict f R x = fun_rel_restrict (the_recfun x) R x" if "R x X" for x
proof -
have "f y = (the_recfun x) y" if "R y x" for y
proof -
have "is_recfun y (the_recfun y)" "is_recfun x (the_recfun x)"
using is_recfun ‹R x X› ‹R y x› trans by auto
with fun_rel_restrict_eq_fun_rel_restrict_if_is_recfunI have
"fun_rel_restrict (the_recfun y) R y = fun_rel_restrict (the_recfun x) R y"
using ‹R y x› by auto
moreover have "f y = wft_rec y"
unfolding f_def using ‹R y x› ‹R x X› trans by auto
moreover have "wf_rec_step (λ_. the_recfun x) y = (the_recfun x) y"
using ‹R y x› ‹R x X› is_recfun by fastforce
ultimately show ?thesis by (auto simp: wft_rec_def wf_rec_step_eq)
qed
then show ?thesis by auto
qed
then have "is_recfun X f" unfolding f_def by (auto simp: wft_rec_def wf_rec_step_eq)
then show ?case by auto
qed
corollary is_recfun_the_recfunI: "is_recfun X (the_recfun X)"
using is_recfun_the_recfun_if_is_recfunI ex_is_recfunI by blast
theorem wft_rec_eq_wf_rec_stepI: "wft_rec X = wf_rec_step (λ_. wft_rec) X"
proof -
have "(the_recfun X) x = wf_rec_step the_recfun x" if "R x X" for x
proof -
have "(the_recfun X) x = wf_rec_step (λ_. the_recfun X) x"
using is_recfun_the_recfunI ‹R x X› by auto
moreover have "fun_rel_restrict (the_recfun x) R x = fun_rel_restrict (the_recfun X) R x"
using fun_rel_restrict_eq_fun_rel_restrict_if_is_recfunI is_recfun_the_recfunI ‹R x X›
by blast
ultimately show ?thesis by (auto simp: wf_rec_step_eq)
qed
then have "fun_rel_restrict (the_recfun X) R X = fun_rel_restrict (wf_rec_step the_recfun) R X" by simp
then show ?thesis by (simp add: wft_rec_def wf_rec_step_eq)
qed
end
end
end
end