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 ) 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?
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.
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
Description: S/MIME Cryptographic Signature