[isabelle-dev] SELECT_GOAL

[Makarius]

This is a continuation of the following threads from some weeks ago:

   [isabelle] SELECT_GOAL and schematic variables
   [isabelle-dev] auto raises a TYPE exception


The notable change is here:

changeset:   52454:210bca64b894
user:        wenzelm
date:        Wed Jun 26 21:48:23 2013 +0200
files:       src/Pure/Isar/proof.ML src/Pure/goal.ML 
src/Pure/simplifier.ML src/ZF/Constructible/Relative.thy
description:
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac;
adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);


So SELECT_GOAL no longer detaches a separate goal state, and thus retains 
the cumulative information about schematic variables (maxidx required for 
incrementing etc.). The other subgoals are merely pushed behind some 
Goal.protect barrier.  This principle was introduced around 1998/1999 for 
Isar proofs, but has become a standard approach to goal state structure in 
recent years.  It is also explained in the "implementation" manual.


One would expect that such well-understood and documented technology would 
work out on the spot, but I've spent quite a long time guessing at 
failures in boundary cases, potentially due to proof tools that do not 
conform 100% to the way tactics are supposed to work (e.g. not peeking at 
the main conclusion).

In particular, there were problems of unknown origin in the Simplifier, 
until that was done with the even less intrusive PREFER_GOAL tactical 
(which is also new here).


Further examples how to manage goal structure in a light-weight and 
minimal invasive way can be seen here for PARALLEL_GOALS: ef4c16887f83.


 	Makarius