*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Well-foundedness of Relational Composition*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 26 Apr 2015 09:24:11 +0200*In-reply-to*: <1429885969.5902.26.camel@weber>*References*: <1429885969.5902.26.camel@weber>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Thanks Tobias On 24/04/2015 16:32, Tjark Weber wrote:

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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Well-foundedness of Relational Composition***From:*Tjark Weber

**References**:**[isabelle] Well-foundedness of Relational Composition***From:*Tjark Weber

- Previous by Date: Re: [isabelle] What is sumC?
- Next by Date: [isabelle] How to "code abstract" over nested types
- Previous by Thread: [isabelle] Well-foundedness of Relational Composition
- Next by Thread: Re: [isabelle] Well-foundedness of Relational Composition
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list