On Mon, 4 Oct 2010, Alexander Krauss wrote:
To avoid that this issue, encountered by Lars, gets lost, I'll re-raise it
here:
The following lemma statement raises an obscure internal TYPE exception:
lemma
assumes "P foo" (is "P ?bar")
shows "Q ?bar"
I assume that is-bindings cannot be used in the same structured statement. I
also assume that this would be hard to support in general.
Yes, allowing to bind and reference within the same "expression" would
mean to have full Hindley-Milner let-polymorphism there. This was
dismissed as too complicated in the 2nd generation locale implementation
around 2001/2002, and in the current 3rd or 4th generation it is probably
not easier to achieve that. (Our type inference framework does not even
have a notion of truely local polymorphism.)
At some point, the error behaviour could be improved, though.
Technically it is a bit related to the surprise concerning ?thesis in
'interpretation' noticed by Brian Huffman recently: the simplistic
treatment of 'is' patterns in Isar proof commands is stretched a bit too
far by these more complex applications.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
