* New command 'consider' states rules for generalized elimination and
case splitting. This is like a toplevel statement "theorem obtains" used
within a proof body; or like a multi-branch 'obtain' without activation
of the local context elements yet.
* Proof method "cases" allows to specify the rule as first entry of
chained facts. This is particularly useful with 'consider':
consider (a) A | (b) B | (c) C <proof>
then have something
proof cases
case a
then show ?thesis <proof>
next
case b
then show ?thesis <proof>
next
case c
then show ?thesis <proof>
qed
This refers e.g. to Isabelle/051b200f7578. Some examples are in
~~/src/HOL/Isar_Examples/Structured_Statements.thy
It may be seen as an answer to the open problem of section 5.5.3
"Generalized case-splitting" from my Ph.D. thesis. There is no need to
support non-linear proof processing in the Isar/VM: 'consider' merely
states and proves the rule, and the "cases" method does the splitting in a
normal backwards proof (with case names).
This means that awkward use of raw proof blocks with "big-bang
integration" by blast is no longer required. General case-splitting can
now be written explicitly and robustly.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
