[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 23:58:37 CEST 2013
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"
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.
More information about the isabelle-dev