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.

Thank you

Please accept my apologies for posting anonymously. This is done to
protect my privacy. I can make my identity and my real contact details
available upon request in private communication under the condition
that they are not to be mentioned on the mailing list.

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