Re: [isabelle] Rewriting modulo AC
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Rewriting modulo AC
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Mon, 7 Sep 2015 13:11:24 +0200
- In-reply-to: <CAJGV=ubgCbzWiFX3-JSTEsmdROUn4nan-8G1m-NbreRL-=kHJA@mail.gmail.com>
- References: <CAJGV=ubgCbzWiFX3-JSTEsmdROUn4nan-8G1m-NbreRL-=kHJA@mail.gmail.com>
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:38.0) Gecko/20100101 Thunderbird/38.2.0
I once implemented this http://www21.in.tum.de/~nipkow/pubs/scp89.html, but the
code was superseded and AC-rewriting was dropped. Still, you should be able to
recreate it or at least reuse the ideas.
For an overview of work in this area see http://arxiv.org/abs/1106.4448
On 27/08/2015 11:44, Aleks Kissinger wrote:
Does the Isabelle/HOL library have any built-in facilities for
simplification modulo associativity/commutativity rules? If not, is
there a fairly simple way to implement this in Isabelle/ML or Eisbach?
For example, I'm trying to implement something like "subst_ac" here:
class ac_thing = ab_semigroup_mult +
fixes a b c d e :: 'a
assumes foo: "a * b * c = d * e"
shows "x * y * c * a * z * b = x * y * z * d * e"
Bonus points if it backtracks well, i.e. doesn't produce tons of
Description: S/MIME Cryptographic Signature
This archive was generated by a fusion of
Pipermail (Mailman edition) and