[isabelle-dev] NEWS: 'consider' command and "cases" method

[Makarius]

* 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