Re: [isabelle] Rewriting modulo AC

I once implemented this, 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


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)

Bonus points if it backtracks well, i.e. doesn't produce tons of
redundant matches.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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