Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] addsimps with reorient?

Email Gateway (Aug 18 2022 at 11:47):

From: Holger Gast <gast@informatik.uni-tuebingen.de>
Dear all,

the Isabelle simplifier re-orients equalities
when extracting premises, such that, for instance,
equalities of the form x = t x, where x occurs on
the right hand side, become rewrite rules t x == x
to avoid looping.

Now I have a list of theorems thms
(they are actually premises extracted earlier)
which I would like to add as rewrite rules with

ss addsimps thms

Unfortunately, these re-write rules (as far as I see from
meta_simplifier.ML) do not get re-oriented, and the
theorems obtained with prems_of_ss are not re-oriented either.

Is there anything like

ss addsimps_safe thms

Thanks,

Holger

Email Gateway (Aug 18 2022 at 11:48):

From: Tobias Nipkow <nipkow@in.tum.de>
The reasoning was that if the user explicitly adds a certain equation,
the system should not interfere. But I agree that a "safe" variant would
be useful. I talked it over with Stefan who will make something like
that available.

Tobias

Holger Gast schrieb:

Last updated: May 03 2024 at 01:09 UTC