Email Gateway (Aug 22 2022 at 14:12): Email Gateway (Aug 22 2022 at 14:12):From: Thomas.Sewell@data61.csiro.au
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:
-
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.
Email Gateway (Aug 22 2022 at 14:23):From: Iulia Dragomir <iulia.dragomir@aalto.fi>
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
Test.thy
Email Gateway (Aug 22 2022 at 14:24):From: Peter Lammich <lammich@in.tum.de>
Hi,
try invoking the simplifier with (simp cong: if_cong)
By default, the simplifier uses thm weak_if_cong as congruence rule for
if, which prevents it from simplifying inside if expressions.
Last updated: Apr 16 2024 at 12:28 UTC