Re: [isabelle] Reversing simp rules

On 30/04/2018 15:18, Dominique Unruh wrote:
I have an additional suggestion in this context: If "flip" (or whatever the
name will be) is implemented, perhaps the regular "add" could also check
whether the flipped rule already exists in the simpset, and, if so, print a
message informing the user that "flip" would be the right thing to do? That
will make it easier for people to find out about it, and probably also help
people tracking down accidental looping simpsets.

The implementation of this feature is a bit of work because for it to be useful one has to compare rules modulo renaming of free variables. Not sure if or when I'll get around to that.


Best wishes,

On 30 April 2018 at 15:36, Christian Sternagel <c.sternagel at>

Dear all,

just to make what Tobias already said more explicit: I also prefer

(auto reorient: A B C D)


(auto simp: A [symmetric] B [symmetric] C [symmetric] D [symmetric])

Alternatives for the name:

   simp\<^sup>- (*not actually supported as identifier*)



On 04/30/2018 10:11 AM, Tobias Nipkow wrote:
I have implemented a first version with modifier "reorient" and am
tempted to go with that because it saves you the [symmetric] (after all,
the whole thing is suppsed to be short, otherwise we wouldn't need it)
and does not change the behaviour of "add". The word "flip" is a nice
too (although a bit generic in the context of "auto").


On 29/04/2018 23:11, Bertram Felgenhauer via Cl-isabelle-users wrote:
Lawrence Paulson wrote:

[about having a modifier for flipping simp rules]

As it happens, we are investigating precisely this idea right now.

One question is whether to introduce a new modifier or instead just to
remove the “flipped” version (if present) whenever you insert a
simplification rule. Views would be welcome.

I like the idea of making the removal implicit. The main worry is
usually that such magic leads to confusion, but I honestly don't see
that happening in this particular case.

The main advantage I see is that no new vocabulary is required.



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

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