Re: [isabelle] question about Simplifier.rewrite

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:

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.


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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.