[isabelle-dev] NEWS: more informative errors in lazy enumerations
makarius at sketis.net
Fri Oct 19 17:16:06 CEST 2012
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
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.
More information about the isabelle-dev