# [isabelle] Well-foundedness of Relational Composition

The attached lemma about well-foundedness of relational composition
featured prominently in a recent termination proof of mine. If the
lemma is not available already, I would like to propose it for
inclusion in HOL/Wellfounded.thy (or some derived theory).
I discovered the lemma and proof myself, but I suspect that the result
is well-known. Pointers to the literature would be appreciated.
Best,
Tjark
===== 8< =====
lemma wf_relcomp_compatible:
assumes "wf R" and "R O S \<subseteq> S O R"
shows "wf (S O R)"
proof (rule wfI_pf)
fix A assume A: "A \<subseteq> (S O R) `` A"
{
fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
proof (induction n)
case 0 show ?case
using A by (simp add: relcomp_Image)
next
case (Suc n)
then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n)
`` A"
by (metis Image_mono subsetCI)
also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A"
using assms(2) by (metis (no_types, hide_lams) Image_mono
order_refl relcomp_Image)
finally show ?case
by (metis relcomp_Image relpow.simps(2))
qed
}
then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S
^^ n) `` A)"
by blast
then have "(\<Union>n. (S ^^ n) `` A) = {}"
using assms(1) by (metis wfE_pf)
then show "A = {}"
using relpow.simps(1) by blast
qed

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*