*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Things identified via `rewrites` not treated as identical*From*: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>*Date*: Sun, 28 Jul 2019 16:05:55 +0300*In-reply-to*: <ca0f9040-3613-ae5e-9980-c5d9a5d23f03@andreas-lochbihler.de>*References*: <b2be31f09caa353771fe2f01256690113966f565.camel@jeltsch.info> <ca0f9040-3613-ae5e-9980-c5d9a5d23f03@andreas-lochbihler.de>

Am Sonntag, den 28.07.2019, 14:24 +0200 schrieb Andreas Lochbihler: > Dear Wolfgang, > > The problem is that you have abbreviations on the left-hand sides of > your rewrites instead of definitions. Abbreviations are just for > pretty-printing; in the underlying term representation, abbreviations > are unfolded (and implicitly beta-reduced). If you change the > abbreviations into definitions, then the rewriting works as expected. > Let's look into what's happening: > > The term sub in zero_subtraction expands to λx y. (+) x (uminus y). > So the rewrite rule "zero_subtraction.neg zero sub = neg" becomes in > the interpretation > > λx. int.sub 0 x = uminus > > This has a lambda on the left, i.e., it is not a proper higher-order > rewrite rule. It will only kick in if there is a lambda abstraction > in the term. However, in the theorem neg_zero, the beta redex > "(λx. int.sub 0 x) 0" has already been reduced so int.sub 0 0. So > the rewrite rule will not trigger. If you turn the abbreviations into > definitions, there will be no trouble with implicit beta-reductions > and eta-expansions. > > Alternatively, you can add the eta-expanded version of the rewrite > rule: > > sublocale zero_subtraction zero sub > rewrites "zero_subtraction.neg zero sub = neg" > and "zero_subtraction.neg zero sub x = neg x" > > Then it works as expected. > > Hope this helps > Andreas Thanks for this detailed explanation. It seems that the thoughts I just sent as a response to mailing-list anonymous went in the right direction. 🙂 All the best, Wolfgang

**References**:**[isabelle] Things identified via `rewrites` not treated as identical***From:*Wolfgang Jeltsch

**Re: [isabelle] Things identified via `rewrites` not treated as identical***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Requirement 'fontconfig'
- Next by Date: Re: [isabelle] Meta: replying to the existing threads in "The Cl-isabelle-users Archives"
- Previous by Thread: Re: [isabelle] Things identified via `rewrites` not treated as identical
- Next by Thread: [isabelle] New AFP entry: Szpilrajn Extension Theorem
- 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