Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Rewriting modulo AC

Email Gateway (Aug 22 2022 at 11:00):

From: Aleks Kissinger <aleks0@gmail.com>
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.

Email Gateway (Aug 22 2022 at 11:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Alex,

try

apply (simp add: ac_simps)

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 11:00):

From: Aleks Kissinger <aleks0@gmail.com>
I'm sure simp/metis/auto can all handle this simple example with a bit
of fiddling, although this is already too hard for just "apply(simp
add:ac_simps)".

What I'm looking for is a method for single-step substitution modulo
AC which always succeeds when there is a match.

Email Gateway (Aug 22 2022 at 11:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

What I'm looking for is a method for single-step substitution modulo
AC which always succeeds when there is a match.

Maybe rewrite or subst is the solution.

Florian

On 27 August 2015 at 11:55, Florian Haftmann
<florian.haftmann@informatik.tu-muenchen.de> wrote:

Hi Alex,

try

apply (simp add: ac_simps)

Cheers,
Florian

Am 27.08.2015 um 11:44 schrieb Aleks Kissinger:

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.

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

signature.asc

Email Gateway (Aug 22 2022 at 11:24):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Tobias
smime.p7s

Last updated: Apr 30 2024 at 12:28 UTC