[isabelle] unfold_locales with names for subgoals
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and