*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Proofs that hang*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Mon, 14 Apr 2008 10:52:00 +0200*Cc*: Jesper Bengtson <jesperb at it.uu.se>*In-reply-to*: <0EC30DE4-4042-4B39-96EB-9AE6CC5EC83C@it.uu.se>*References*: <0EC30DE4-4042-4B39-96EB-9AE6CC5EC83C@it.uu.se>*User-agent*: KMail/1.8

Jesper, On Sunday 13 April 2008 13:35, Jesper Bengtson wrote: > In my current formalisation I have a relation which is created through > some quite trivial rules. It's an equivalence relation, it is a > congruence, it's idempotent and it has one or two more obscure rules. > The problem is that these rules are inherently symmetric -- especially > rules regarding associativity and commutativity of one of the > operators and I am having a hard time to have Isabelel automatically > verify proofs even though they are seemingly quite simple. Doing it by > hand works, but it's a bit of a pain. > > My question is basically if there is a way to reason about these types > of relations automatically in Isabelle where the automatic tactics get > stuck on symmetries. Isabelle uses ordered rewriting. Permutative rules, e.g. commutativity, are applied only if this results in a "smaller" (with respect to some fixed lexicographic order on terms) term. For an associative and commutative operator f, you should add not only associativity and commutativity to the set of default rewrite rules, but also a derived rule, left-commutativity: f(x, f(y, z)) = f(y, f(x, z)). Please see Section 9.1.1 of the Isabelle/HOL tutorial for further details. Since ordered rewriting should prevent the simplifier from "getting stuck" on symmetries, loops are probably due to more complex interaction between different rewrite rules. Maybe try "Isabelle > Settings > Trace Simplifier" in ProofGeneral to see which rules are getting used. "apply (simp del: XXX)" and "apply (simp only: XXX)" (see Section 3.1.4 of the Isabelle/HOL tutorial) might also be useful to locate the problem. I hope this answers your question. Otherwise could you maybe supply a concrete example of a proof that hangs? Best, Tjark

**References**:**[isabelle] Proofs that hang***From:*Jesper Bengtson

- Previous by Date: [isabelle] Proofs that hang
- Next by Date: [isabelle] CALL FOR PAPERS: TPHOLs 2008--EMERGING TRENDS--
- Previous by Thread: [isabelle] Proofs that hang
- Next by Thread: [isabelle] CALL FOR PAPERS: TPHOLs 2008--EMERGING TRENDS--
- Cl-isabelle-users April 2008 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