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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
