[isabelle-dev] NEWS: cases from goals
noschinl at in.tum.de
Tue Jun 30 19:34:46 CEST 2015
On 30.06.2015 17:42, Makarius wrote:
> 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.
I'd say this is a partial solution: When I have a situation where I need
?thesis1, ?thesis2, etc. then the goals are often very similar to solve
and my proof concludes with "... show ?thesis1 ?thesis ...".
I wonder though, why the goals method is better then the implicit goal1,
goal2, ... cases? Doesn't it lead to more instances of "proof
(initial_method, goals)" -- which I thought is a style you discouraged?
More information about the isabelle-dev