*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] question about Simplifier.rewrite*From*: <Thomas.Sewell at data61.csiro.au>*Date*: Thu, 27 Oct 2016 02:19:45 +0000*Accept-language*: en-US, en-AU*In-reply-to*: <83e57e35-1e03-8693-976f-48be1e90a56e@aalto.fi>*References*: <83e57e35-1e03-8693-976f-48be1e90a56e@aalto.fi>*Thread-index*: AQHSL42S5r9wizTVjkG/I5l3YRcwqKC62aOA*Thread-topic*: [isabelle] question about Simplifier.rewrite*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

I haven't had a look at the attached file in detail, however, I'm pretty sure your confusion arises from congruence rules. There's a discussion of this here: - http://stackoverflow.com/questions/15627676/why-wont-isabelle-simplify-the-body-of-my-if-then-else-construct - https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-October/msg00069.html - https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-May/msg00046.html And probably in various other places. Short version: the default if_weak_cong congruence rule, declared by default with [cong], prevents the simplifier from looking inside the branches of if statements. My understanding is that this was originally done to allow some recursive unfolds to be safe with the simplifier, e.g. "fib x = (if x = 0 then 1 else fib (x - 1) + fib (x - 2))" Because the simplifier won't look inside the branches of the if-statement until it can decide whether x = 0, the above rewrite is safe. The datatype packages declares its equivalents of if_weak_cong as congruence rules themselves for the same reason. As I've said on this list before, I consider this a bit of a bug, but it's ancient in Isabelle, and probably too much work to change. Things you can do: - (simp cong: if_cong) - (simp cong del: if_weak_cong) - something else which controls simplifier application. Cheers, Thomas. On 27/10/16 00:30, Iulia Dragomir wrote: > Hello > > I have a problem with Simplifier.rewrite which simplifies the expression > (1::real) = (2::real) within some simple term, but not in a more complex > term. Since the complex term is quite involved, the actual questions are > in the attached file, which also contains the term. > > > Any help is greatly appreciated. > > Best regards, > Iulia Dragomir >

**References**:**[isabelle] question about Simplifier.rewrite***From:*Iulia Dragomir

- Previous by Date: Re: [isabelle] Isabelle2016-RC0: cvc4 crashing
- Next by Date: Re: [isabelle] pairs and friends
- Previous by Thread: Re: [isabelle] question about Simplifier.rewrite
- Next by Thread: [isabelle] CfP: MARS 2017 - Models for Formal Analysis of Real Systems
- Cl-isabelle-users October 2016 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