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, Dominique. On 30 April 2018 at 15:36, Christian Sternagel <c.sternagel at gmail.com> 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
Description: S/MIME Cryptographic Signature