*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

For an overview of work in this area see http://arxiv.org/abs/1106.4448 Tobias 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" theorem test: shows "x * y * c * a * z * b = x * y * z * d * e" apply(subst_ac foo) apply(rule refl) done Bonus points if it backtracks well, i.e. doesn't produce tons of redundant matches.

**Attachment:
smime.p7s**

- Previous by Date: Re: [isabelle] Expansion of let-bindings in proofs
- Next by Date: Re: [isabelle] "Undeclared hyps" in BNF_FP_Def_Sugar
- Previous by Thread: Re: [isabelle] Expansion of let-bindings in proofs
- Next by Thread: Re: [isabelle] "Undeclared hyps" in BNF_FP_Def_Sugar
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list