Re: [isabelle] Reversing simp rules

In Isabelle/223172b97d0b I went for Christian's suggestion and renamed "reorient" to "flip":

* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
  of theorems. Each of these theorems is removed from the simpset
  (without warning if it is not there) and the symmetric version of the theorem
  (i.e. lhs and rhs exchanged) is added to the simpset.
  For 'auto' and friends the modifier is "simp flip:".


On 30/04/2018 14:36, Christian Sternagel wrote:
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.