Re: [isabelle] Reversing simp rules



Dear all,

already (simp add: ac_simps) is a magic so I think more magic can be accepted.

Best regards,
Akihisa

On 2018/04/30 21: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







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