[isabelle-dev] NEWS: cases from goals

[Makarius]

On Tue, 30 Jun 2015, Lars Noschinski wrote:

>> 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 ...".

These are just implicit "auto" bindings.  In specific situations it is 
always possible to use explicit "is" patterns.


> 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?

The whole use of goal cases is not really best-style Isar.  The new proof 
method is just a way to re-integrate things that have accumulated over the 
years, such they fit formally better into the framework.

The main advantages I see at the moment:

   * "Explicit is better than implicit", i.e. the "goals" method says that
     goal cases should be produced (maybe it should be actually called
     "goal_cases"!?).  The default case names are shorter: 1, 2, 3 instead
     of goal1, goal2, goal3.  It is also possible to specify case names in
     the method invocation.

   * Cases don't expose hidden goal parameters by default, according to the
     way how cases methods work.  This means the case invocation needs to
     provide parameter names as desired.

There are presently two main applications where goal cases are really 
needed in regular Isar proofs: intro_classes and intro_locales.  Since 
these proof methods are a bit too complex to provide properly named cases 
(although it is possible in theory), post-hoc addition of "goals" is the 
way to do it.  For example:

   instance
   proof (standard, goals)
     case 1
     then show ?case sorry
   next
     case 2
     then show ?case sorry
   next
     case 3
     then show ?case sorry
   qed


Now we are also back to the motivating situation to rename "default" into 
"standard".  Note that the "default" method was originally not meant to be 
written explicitly in the text at all.

If there are significantly better ideas for the above, I am intersted to 
hear them.


 	Makarius