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



Dear All,

I apologise for posting the same message twice. The mistake is related
to making the first attempt to use a different email client that would
enable the modification of the email headers (related to my previous
post https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-July/msg00110.html).
I will make every attempt to ensure that this does not happen again.

Thank you

On Sun, Jul 28, 2019 at 6:56 PM mailing-list anonymous
<mailing.list.anonymous at gmail.com> wrote:
>
> 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.



-- 
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.