Re: [isabelle] Things identified via `rewrites` not treated as identical



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.