Re: [isabelle] SELECT_GOAL and schematic variables



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
*** 'c
*** 'd

note that everything works fine without the [].

I've had a first round of studying 10-15 years of Isabelle source history yesterday.

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" by Larry.

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 investigation.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.