[isabelle-dev] internal TYPE exception at lemma statement

[Makarius]

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