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

Makarius makarius at sketis.net
Mon Jun 15 00:11:06 CEST 2015

* 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>
     case b
     then show ?thesis <proof>
     case c
     then show ?thesis <proof>

This refers e.g. to Isabelle/051b200f7578. Some examples are in 

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.


More information about the isabelle-dev mailing list