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:".

Tobias

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)

over

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

Alternatives for the name:

   reorient
   flip
   swap
   sym
   pmis
   simp\<^sup>- (*not actually supported as identifier*)

cheers

chris

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").

Tobias

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.

Cheers,

Bertram




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



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