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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
