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:
> 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