[isabelle-dev] NEWS: more informative errors in lazy enumerations

[Makarius]

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