*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 08 Jun 2015 19:26:58 +0200*In-reply-to*: <5575A9FF.3000108@in.tum.de>*References*: <5575A4DC.6070407@in.tum.de> <A7A26D57-0743-4A51-9943-BD251B37EEAA@inria.fr> <5575A9FF.3000108@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Tobias On 08/06/2015 16:43, Lars Noschinski wrote:

On 08.06.2015 16:34, Jasmin Blanchette wrote:The rule âXâ appears to violate the golden rule of thumb when using âsimpâ, i.e. that both the rhs and the preconditions should be simpler than the lhs (see Section 2.5.3 of Concrete Semantics). Surely, âf x ~= aâ is not simpler than âf xâ. That bad things happen then doesnât surprise me so muchâ Cheers, JasminIt is only simpler insofar as that it is literally part of the assumptions. I would not have been surprised if the simplifier had started looping -- after all, it is not really simpler. But refusal to rewrite does not yet fit into my mental model of the simplifier.

**Attachment:
smime.p7s**

**References**:**[isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"***From:*Lars Noschinski

**Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"***From:*Jasmin Blanchette

**Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"
- Next by Date: Re: [isabelle] Method combinator ; restricts to first subgoal
- Previous by Thread: Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"
- Next by Thread: [isabelle] interpretation and sublocale ignore order of parameters
- Cl-isabelle-users June 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