Re: [isabelle] Things identified via `rewrites` not treated as identical
Dear Wolfgang Jeltsch,
> Apparently, the problem has more to do with rewriting in general than
> with rewriting introduced by `rewrites` clauses. I understand that
> defining `(⊖)` as an abbreviation via `x ⊖ y ≡ x ⊕ ((⊖) y)` doesn’t play
> well with using a partial application of it in the rewrite rule `(⊖) 𝟬
> = neg`. While `(⊖) 𝟬` looks like an innocent partial application, it i
> s in fact `λy. 𝟬 ⊕ ((⊖) y)`, and thus the rewrite rule doesn’t match i
> n places where `(⊖)` is fully applied, because full applications of
> abbreviations don’t use `λ`.
Thank you for your reply. Indeed, my initial intention was to write a reply with the fully expanded abbreviations (initially, in writing the reply I analysed the structure of the terms in ML and used Conv.rewrs_conv instead of the attribute ‘unfolded'). However, I thought that the structure of the terms would be apparent anyway, because there was only one abbreviation left to expand.
Unfortunately, I have not studied, specifically, the HRS algorithms (apparently) used for rewriting in lambda calculus/Isabelle. Therefore, I did not wish to speculate any further as to why `λy. 𝟬 ⊕ ((⊖) y)` is not suitable as the lhs of a rule. In any case, the answer by Andreas Lochbihler provides a more complete explanation.
This archive was generated by a fusion of
Pipermail (Mailman edition) and