On Wed, 25 Aug 2010, Andreas Schropp wrote:

What does this say about our equality-elimination criterion, which wants to check if there are any assumptions involving a Free?

It does not want to check that, and the version by Thomas does not do it.
In fact his approach looks like going in the right direction.

Going back tp that, it has already been mentioned that goal parameters (bounds) can somehow be treated as private to the proof state, while frees can reach back into the context arbitraily. In fact, a Free is just like a local Const in most situations, i.e. Free/Const are only different in their scopes.

Is there any chance to get a practically useful version of hypsubst that does not distinguish local constants (Free) from constants of the background theory (Const)?


        Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to