Re: [isabelle] SELECT_GOAL and schematic variables



On Fri, 22 Mar 2013, Lawrence Paulson wrote:

I'm afraid that I really can't answer this question without a time machine.

In principle the time machine is Mercurial, but it also takes time to study our immense history that has accumulated since changeset 0 from Sep-16 12:20:38 1993 (and more years of unwritten history before that).


The usual method of getting around such problems was to freeze variables prior to applying the tactic, thawing them afterwards. That was a hack, but it generally worked. My impression is that Makarius has replaced such trickery by more robust methods, but it's possible that quite a lot about old code is still there and running. I'm not sure about the current best practice for dealing with this sort of situation.

The ancient freeze_thaw and freeze_thaw_robust (which were actually both fragile) have evolved over a long way to become the current FOCUS combinators, which are also mentioned in the "implementation" manual.

This Isar technology for structured tactic programming is useful in many situations, but it does not really cover the schematic goal approach that Peter appears to use a lot. In fact, the continued retreat of genuine logic-programming with schematic variables in Isabelle tactics over the years had paved the way for these more recent high-level tacticals.

Readers of the old "intro" manual by Larry might remember the final Prolog example. Such techniques are now extremely rare, so it is no surprise that certain tools choke.

(I will have a close look later at what is actually happening here, when I have catched up with various other open threads.)


	Makarius




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