*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Mon, 8 Jun 2015 16:34:27 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5575A4DC.6070407@in.tum.de>*References*: <5575A4DC.6070407@in.tum.de>

Hi Lars, > assume X: "âx :: 'a. f x â a â f x = xâ > Here, "simp add: X" fails, even though all its premises can be solved by > "assumption" -- or, as the second line shows, by "simp". Has anyone got > an idea why this is the case? 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, Jasmin

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

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

- Previous by Date: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"
- Next by Date: Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"
- Previous by Thread: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"
- Next by Thread: Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"
- 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