[isabelle-dev] NEWS: cases from goals

Makarius makarius at sketis.net
Tue Jun 30 17:42:10 CEST 2015

Here is an updated NEWS entry from Isabelle/0eb41780449b -- no changes, 
just more explanations:

* Proof method "goals" turns the current subgoals into cases within the
context; the conclusion is bound to variable ?case in each case.
For example:

lemma "⋀x. A x ⟹ B x ⟹ C x"
   and "⋀y z. U y ⟹ V u ⟹ W y z"
proof goals
   case prems: 1
   then show ?case using prems sorry
   case prems: 2
   then show ?case using prems sorry

* The undocumented feature of implicit cases goal1, goal2, goal3, etc.
is marked as legacy, and will be removed eventually. The proof method
"goals" achieves a similar effect within regular Isar; often it can be
done more adequately by other means (e.g. 'consider').

Above I am using a new idiom, to name "prems" uniformly in each case. 
This helps to avoid specific names like "1", "2" etc. intrude the proof 
body.  Thus cases may be re-arranged later, without changing all the proof 

Moreover note, that the above example provides a solution to the 
occasional problem of ?thesis1, ?thesis2, etc. -- which are not provided 
by the system.  It just becomes ?case in each case.


More information about the isabelle-dev mailing list