[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Tobias Nipkow wrote:

>> What is a bit unstisfactory here is that it merely avoids certain 
>> crashes of SELECT_GOAL (and maybe other crashes), but the example from 
>> this thread would still not quite work, since the unification problem 
>> is presumably too difficult.
>
> i thought the only limitation of the unification code is that it does 
> not instantiate type vars to function types (to avoid another dimension 
> of search). if that is happening here, so be it.

I did not inspect the concrete failure here yet, but in general there is 
always the inherent complexity of HO-unification: if the two goal states 
happen to be schematic in an overly ambitious manner, then "retrofit" 
breaks down.

We used to have the same for what is now called 'schematic_theorem': at 
the end of the proof the check that the result fits to the original goal 
statement could fail for technical reasons.  There are ways to address 
that, but it is not done for SELECT_GOAL (and SUBPROOF) to keep things 
reasonably simple and light-weight.


 	Makarius