Email Gateway (Aug 22 2022 at 20:11): Email Gateway (Aug 22 2022 at 20:11):From: Peter Lammich <lammich@in.tum.de>
Hi List,
I have
...
val ctxt = put_simpset HOL_ss ctxt addsimps inline_thms
in
Conv.fconv_rule ( Simplifier.rewrite ctxt ) thm
Unfortunately, the resulting theorem is not beta-contracted (it
contains (%x. ...) x ).
However, both inline_thms and thm contain no beta redexes.
Is it expected behaviour of the simplifier to introduce
new beta-redexes, or is this behaviour undesired, and worth
investigating?
In my application the beta-redexes cause problems in further
conversions, as some operations on Thm seem to silently remove them,
and Thm.equals (used in conversion) cannot match (aconv) the terms any
more.
Of cause, I can quick-fix this by introducing Thm.beta_conv, but I
always thought that expected behaviour of Isabelle functions is not to
produce beta-redexes ?
Thanks for any explanations,
Peter
Email Gateway (Aug 22 2022 at 20:12):From: Tobias Nipkow <nipkow@in.tum.de>
On 04/07/2019 17:28, Peter Lammich wrote:
Hi List,
I have
...
val ctxt = put_simpset HOL_ss ctxt addsimps inline_thms
in
Conv.fconv_rule ( Simplifier.rewrite ctxt ) thmUnfortunately, the resulting theorem is not beta-contracted (it
contains (%x. ...) x ).However, both inline_thms and thm contain no beta redexes.
Is it expected behaviour of the simplifier to introduce
new beta-redexes, or is this behaviour undesired, and worth
investigating?
I am aware that it can hapen although it is undesired. If you send me a minimal
example I can investigate when I find the time.
Tobias
In my application the beta-redexes cause problems in further
conversions, as some operations on Thm seem to silently remove them,
and Thm.equals (used in conversion) cannot match (aconv) the terms any
more.
Of cause, I can quick-fix this by introducing Thm.beta_conv, but I
always thought that expected behaviour of Isabelle functions is not to
produce beta-redexes ?Thanks for any explanations,
Peter
Last updated: Apr 23 2024 at 20:15 UTC