[isabelle] unfold_locales with names for subgoals



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





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