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