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
next
case prems: 2
then show ?case using prems sorry
qed
* 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
cases.
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
