Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Rewriting with Quasi-AC operators?

Email Gateway (Jun 23 2026 at 06:26):

From: Gidon Ernst <gidon.ernst@lmu.de>

Dear all,

Sec 9.3.3 of the Isabelle/Isar reference manual explains how rewriting
modulo permutative operators.

I was wondering whether the following example can be made to work? The
actual use-case is somewhat more complex but this MWE demonstrates the
main requirement I have.

It seems the simplifier does not recognize the combination of map and
zip as permutative and therefore loops.

Best,
Gidon

fun comm where "comm f (x,y) = f (y,x)"
fun assoc where "assoc f (x,y,z) = f ((x,y),z)"
fun lcomm where "lcomm f (x,y,z) = f ((y,x),z)"

lemma map_comm:
"map f (zip xs ys) = map (comm f) (zip ys xs)"
sorry

lemma map_assoc:
"map f (zip (zip xs ys) zs) = map (assoc f) (zip xs (zip ys zs))"
sorry

lemma map_lcomm:
"map f (zip (zip xs ys) zs) = map (lcomm f) (zip ys (zip xs zs))"
sorry

lemmas map_ac = map_comm map_assoc map_lcomm

lemma test:
"map f (zip xs ys) = foo"
apply (simp add: map_ac) (* loops *)

Email Gateway (Jun 24 2026 at 12:43):

From: Tobias Nipkow <nipkow@in.tum.de>

Dear Gideon,

A rule is permutative if, roughly speaking, the left and the right hand side
have the same skeleton, ignoring variables. Commutativity and left commutativity
have that property, but none of your map_comm map_assoc map_lcomm do.

Best
Tobias

On 23/06/2026 08:26, Gidon Ernst wrote:

Dear all,

Sec 9.3.3 of the Isabelle/Isar reference manual explains how rewriting modulo
permutative operators.

I was wondering whether the following example can be made to work? The actual
use-case is somewhat more complex but this MWE demonstrates the main requirement
I have.

It seems the simplifier does not recognize the combination of map and zip as
permutative and therefore loops.

Best,
 Gidon

fun comm  where "comm f (x,y) = f (y,x)"
fun assoc where "assoc f (x,y,z) = f ((x,y),z)"
fun lcomm where "lcomm f (x,y,z) = f ((y,x),z)"

lemma map_comm:
  "map f (zip xs ys) = map (comm f) (zip ys xs)"
  sorry

lemma map_assoc:
  "map f (zip (zip xs ys) zs) = map (assoc f) (zip xs (zip ys zs))"
  sorry

lemma map_lcomm:
  "map f (zip (zip xs ys) zs) = map (lcomm f) (zip ys (zip xs zs))"
  sorry

lemmas map_ac = map_comm map_assoc map_lcomm

lemma test:
  "map f (zip xs ys) = foo"
  apply (simp add: map_ac) (* loops *)

smime.p7s

Last updated: Jul 02 2026 at 07:34 UTC