Re: [isabelle] SELECT_GOAL and schematic variables
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] SELECT_GOAL and schematic variables
- From: Makarius <makarius at sketis.net>
- Date: Thu, 4 Apr 2013 12:58:18 +0200 (CEST)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <1363972783.11600.121.camel@lapbroy33>
- References: <1363883108.11600.102.camel@lapbroy33> <75F4C99D-8D66-4A5A-B2A3-124ED0867EF7@cam.ac.uk> <1363972783.11600.121.camel@lapbroy33>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Fri, 22 Mar 2013, Peter Lammich wrote:
Unfortunately, this problem does not only affect the (admittedly
low-level) SELECT_GOAL, but also high-level proof scripts, as the
following example demonstrates:
inductive P for x where I: "P x"
lemma J: "P (\<lambda>_. R)" by (rule I)
schematic_lemma "\<And>a b. P (?R a) \<or> P (?R)" "TERM ?R4"
apply (rule disjI2, rule J) 
*** exception TYPE raised (line 109 of "envir.ML"):
*** Variable "?R4" has two distinct types
note that everything works fine without the .
I've had a first round of studying 10-15 years of Isabelle source history
SELECT_GOAL and Subgoal.FOCUS represent different strands of tradition,
only the latter (much younger) uses high-end Isar infrastructure --
context import/export operations that vaguely resemble old "freeze_thaw"
SELECT_GOAL is also used for the "[...]" notation for Isar proof methods.
SELECT_GOAL was good old code by Larry in the nostalgic style of 1980-ies
Isabelle until 31-Aug-2001. Then Stefan Berghofer "Tidied function
SELECT_GOAL". I think before and after the behaviour wrt. newly invented
schematic was the same as it is still now. Much later I merely modified
its internal terminology and general setup to make it look more like
Subgoal.FOCUS, e.g. using certain "extract" and "retrofit" operations.
Beyond historical anecdotes, I have made one round of experiments to see
if SELECT_GOAL can be converged a bit more towards the way how the (very
sophisticated) Subgoal.FOCUS works, but it breaks various classic tactics.
Reasons still need to be explored, I can say more after the next round of
This archive was generated by a fusion of
Pipermail (Mailman edition) and