On Thu, 18 Oct 2012, Andreas Lochbihler wrote:
Does anybody remember a use of the 'apply_end' command?
Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although they
could be fused into the qed. However, I regularly use apply_end when I
develop the method call for qed to finish off all the remaining cases after
having dealt with the interesting ones.
This is more or less the classic use of it. In the rather massive proof
here, the two apply_end steps are indeed easily fused into one qed.
http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/6881d417d5d5 -- actually I
was merely experimented here, and pushed the first half by accident, in
the present confusion of the AFP state.
It usually saves me reprocessing the first 42 goals when goal 43 needs
another intro/simp/elim rule - and I can interactively explore goal 43
immediately. Before I knew about apply_end, I used "case goal_43 thus
?case", but proof methods behave differently there, because the
variables are fixed in the context (e.g., tuples are not split
automatically).
The question on this thread is if the traditional techniques are still
relevant. The exploration of a tiny 'qed' script would just be done as
'qed' attempts, without breaking it up into seperate 'apply_end' steps.
There is a potential cost for that, since the qed is just one step that
needs to be repeated. In the massive example proof it is still below a
few seconds, or less.
There many more possibilties for the initial refinedment stage before
'proof', with 'apply', 'defer', 'prefer', and potentially proof methods
restricted to intervals via the [...] postfix notation.
Going back over 42 goals is still an issue right now when using Proof
General, with its built-in sequentialism. But that will hopefully be
forgotton soon, after more people have retrained their fingers.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
