[isabelle-dev] Interrupt exception

[Lucas Dixon]

Makarius wrote:
> On Wed, 15 Jul 2009, Lucas Dixon wrote:
> 
>>>>   apply (unfold Product_Type.pair_collapse[symmetric, of "al"])
>>>
>>> The equation Product_Type.pair_collapse[symmetric, of "al"] can be
>>> unfolded forever, so the method invocation does not terminate, leading
>>> to an unspecified behaviour of the system!
>>
>> The point was just that unfold should probably be giving an error 
>> message of some more readable sort.
> 
> The interrupt exception is probably produced by the Poly/ML runtime 
> system when it runs out of resources.  The behaviour might have changed 
> a bit in recent internal versions.  Which one did you use?

Yes, I'm sure you are right; I'm using Isabelle (1d4d0b305f16: date: 
     Fri Jul 10 09:24:50 2009 +0200), and PolyML (svn 801, 2009-07-12)

The problem came up when I was writing a tactic and I wanted to unfold 
all occurences within a goal but not do this recursively - I wanted any 
introduced occurrences to be untouched. I was simulating this within a 
tactic script as an experiment. But perhaps the idea of unfold all 
current occurrences (modulo critical pairs) would be a sensible 
semantics for unfold? It seems like a sensible semantics for something, 
call it unfold or something else :)

best,
lucas

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.