Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] unfold_locales with names for subgoals

Email Gateway (Aug 18 2022 at 12:14):

From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi,

when I interpret a locale with some parameters and multiple assumptions,
applying the unfold_locales method yields all the goals that have to
be shown. With many fixes, assumptions and complex conclusions, I would
be happy to have such convenient shortcuts like "case (... ...)" and
?case for inductions with induct, with the names e.g. being taken from
the assumptions' names in the locale definition, but according to the
print_cases command, unfold_locales does not provide these by default.
Does unfold_locales offer such a feature?

Meanwhile, I help myself with

proof(induct rule: <locale_name>.intro[case_names ...])

but this is not optimal since

1. it does not support hierarchical interpretations
2. there is nothing like induction going on here, so induct is a bad name.
3. the case names get messed up if the order of the assumptions is
   changed in the locale.

Does anyone have any better ideas?

Andreas

Email Gateway (Aug 18 2022 at 12:14):

From: Makarius <makarius@sketis.net>
On Thu, 24 Jul 2008, Andreas Lochbihler wrote:

applying the unfold_locales method yields all the goals that have to be
shown. With many fixes, assumptions and complex conclusions, I would be
happy to have such convenient shortcuts like "case (... ...)" and ?case
for inductions with induct, with the names e.g. being taken from the
assumptions' names in the locale definition, but according to the
print_cases command, unfold_locales does not provide these by default.
Does unfold_locales offer such a feature?

No, even though this omission has been known for a long time already.

Meanwhile, I help myself with

proof(induct rule: <locale_name>.intro[case_names ...])

but this is not optimal since

2. there is nothing like induction going on here, so induct is a bad
   name.

The usual to applies arbitrary rules with cases emitted into the proof
context is via the "cases" method.

Makarius

Last updated: May 03 2024 at 12:27 UTC