*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Well-foundedness of Relational Composition*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Mon, 27 Apr 2015 23:46:12 +1000*Authentication-results*: lists.cam.ac.uk; dkim=none (message not signed) header.d=none;*In-reply-to*: <553E084A.3020303@gmail.com>*References*: <1429885969.5902.26.camel@weber> <553C929B.208@in.tum.de> <1430056276.6087.7.camel@weber> <553E084A.3020303@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.3.0

Hi Tjark / Christian, I'm confused by the notation here. Firstly, R O S:

Secondly, wf R - doesn't this mean that there is no infinite chain ..... an ... a1 a0 such that each (a_{n+1}, a_n) in R ? So using this notation, let R = (n, n+1) for all n (naturals) let S = (n+1, n) for all n Then R O S = {(n, n) | n >= 1} S O R = {(n, n) | n >= 0} Anyhow, in http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/WfUn.{thy,ML} I have proofs of "(s O r <= r O s^*) --> wf r --> wf (r O s^*)" and "(s O r <= r O s^*) --> wf r --> wf (s^* O r)" (they're called wf_movl_comp and wf_movl_comp2) (obviously, wf (r O s) = wf (s O r)) (proofs are in Isabelle2005) I now see in that file I have a note: (* note - can't get result "(r O s <= s^* O r) ==> wf r ==> wf (s^* O r)", eg E = {(x, y) | x >= 0, 0 <= y <= x} (x, y) >_r (x, y+1) - so r is wf (x, y) >_s (x+1, y) - so r O s, s O r not wf In r O s, (x, y) > (x+1, y+1) but only if y < x In s O r, (x, y) > (x+1, y+1) always So (r O s <= s O r) *)

RS RS ... means x0 >R x1 >S x2 >R x3 >S x4 ... in which case wf R means R R R R ... is not possible, but then haven't you actually applied SR <= RS, not RS <= SR?

Cheers, Jeremy On 27/04/15 19:58, Christian Sternagel wrote:

Dear Tjark and Tobias, This is my first impression: I've definitely seen this fact applied (although implicitly) and think it counts as, as they say, "folklore". Especially so, since the paper "proof" is trivial ;): Assume: RS RS RS RS RS RS ... Rearrange into: R SR SR SR SR SR ... Apply "RS <= SR": R RS RS RS RS RS ... Repeat this process to obtain: R R R R R R ... Contradiction. I checked IsaFoR by hypersearch but didn't find anything that looks alike immediately. That is, I'm not aware of any formalized proof. After investigating a little further, I found some relevant literature. Commutation has been investigated by Rosen [3], but as far as I can tell on a short glance only w.r.t. confluence. Bachmair and Dershowitz [2] pronounce "RS <= SR" as "R *commutes over* S" (whereas "commutation" without "over" would result in a "diamond" diagram). And Geser [1] (which was the reference I started from) at least comments about something similar to your lemma on page 38: If R is Noetherian, it is more convenient to check for strict local commutation than for quasi-commutation: They are equivalent, and checking for strict local commutation is less complex ... But also here I did not find a proof by skimming through. Maybe a closer look would reveal something. [1] Alfons Geser. Relative Termination. PhD-Thesis. 1990. [2] Leo Bachmair, Nachum Dershowitz. Commutation, Transformation, and Termination. CADE. 1986. http://dx.doi.org/10.1007/3-540-16780-3_76 [3] Barry K. Rosen. Tree-Manipulating Systems and Church-Rosser Theorems. J. ACM (JACM) 20(1):160-187 (1973). http://doi.acm.org/10.1145/321738.321750 cheers chris On 04/26/2015 03:51 PM, Tjark Weber wrote:Tobias, On Sun, 2015-04-26 at 09:24 +0200, Tobias Nipkow wrote:I'll be happy to include it in HOL/Wellfounded.thy if you do me the favour of getting rid of metis - it is not available at that theory yet.Certainly. A proof that uses only simp and blast is attached.Maybe somebody can also think of a more telling name suffix than "_compatible".This was inspired by the existing lemma wf_union_compatible. Of course, it is a terrible name. 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 (simp add: Image_mono) also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A" using assms(2) by (simp add: Image_mono O_assoc relcomp_Image[symmetric] relcomp_mono) finally show ?case by (simp add: relcomp_Image) 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 (simp only: wfE_pf) then show "A = {}" using relpow.simps(1) by blast qed

**Follow-Ups**:**Re: [isabelle] Well-foundedness of Relational Composition***From:*Christian Sternagel

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

**Re: [isabelle] Well-foundedness of Relational Composition***From:*Tobias Nipkow

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

**Re: [isabelle] Well-foundedness of Relational Composition***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Well-foundedness of Relational Composition
- Next by Date: Re: [isabelle] Well-foundedness of Relational Composition
- Previous by Thread: Re: [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