Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] rule_format and locales

Email Gateway (Aug 18 2022 at 09:35):

From: Peter Lammich <peter.lammich@uni-muenster.de>
I want to use a rule_format transformation for a lemma inside a locale,
but it does not work:

If I have, for example:
consts A :: 'a
B :: 'a

locale dummy
lemma (in dummy) X[rule_format]: "ALL x . A x --> B x" sorry

the lemma will be:

thm dummy.X
ALL x . A x --> B x [!]

but I expected something like
!! x . A x ==> B x
or
A ?x ==> B ?x
as I get when using rule_format outside a locale.

Can I use something similiar to rule_format that works inside a locale,
or do I have to transform the lemmas "by hand" ?

Greetings and thanks for any hints
Peter Lammich

Email Gateway (Aug 18 2022 at 09:35):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Peter Lammich wrote:

I want to use a rule_format transformation for a lemma inside a
locale, but it does not work:

If I have, for example:
consts A :: 'a
B :: 'a

locale dummy
lemma (in dummy) X[rule_format]: "ALL x . A x --> B x" sorry

the lemma will be:

thm dummy.X
ALL x . A x --> B x [!]

but I expected something like
!! x . A x ==> B x
or
A ?x ==> B ?x
as I get when using rule_format outside a locale.

If I declare
lemmas (in dummy) XX = X[rule_format]
XX has the expected format !

Can I use something similiar to rule_format that works inside a
locale, or do I have to transform the lemmas "by hand" ?

Greetings and thanks for any hints
Peter Lammich

Email Gateway (Aug 18 2022 at 09:36):

From: Clemens Ballarin <ballarin@in.tum.de>
Peter Lammich wrote:

I want to use a rule_format transformation for a lemma inside a locale
...

The attribute is only applied inside the locale, not to the exported
version (as dummy.X in your example).

It is not recommended to use attributes that undertake heavy theorem
transformations inside a locale---for example, simplified. These are
executed whenever a context is built from the locale and you will end
up with very slow code.

Clemens

Email Gateway (Aug 18 2022 at 09:36):

From: Makarius <makarius@sketis.net>
The easiest way is to avoid rule_format altogether, which is a legacy
feature anyway. If you state your problems with !!/==> or
fixes/assumes/shows in the first place, the outcome will be in canonical
rule format as expected. (Note that the induct method will do the right
thing on !!/==> goals).

Makarius

Last updated: Nov 21 2024 at 12:39 UTC