*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Beta-contraction*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 5 Jul 2019 10:37:22 +0200*In-reply-to*: <1562254103.27549.105.camel@in.tum.de>*References*: <1562254103.27549.105.camel@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.13; rv:60.0) Gecko/20100101 Thunderbird/60.7.2

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?

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

**Attachment:
smime.p7s**

**References**:**[isabelle] Beta-contraction***From:*Peter Lammich

- Previous by Date: [isabelle] New in the AFP: Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
- Next by Date: [isabelle] Proving for Fun: Summer Edition
- Previous by Thread: [isabelle] Beta-contraction
- Next by Thread: [isabelle] New in the AFP: Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
- Cl-isabelle-users July 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list