[isabelle-dev] Fwd: A possible bug with Isabelle 2013

[Tobias Nipkow]

Am 26/02/2013 17:17, schrieb Lawrence Paulson:
> A student has forwarded this problem to me. It seems weird and unbelievable. What have I overlooked?
> 
> I tidied it up slightly (see below) but I get the same error message.
> 
> lemma "True"
> proof -
>   have     "True = (∃x. (λy. True) x)" by simp
>   also have "... = (∃x. (λy. True) x)"
> oops

The two y's are given separate types. In fact, Isabelle introduces ??'a itself
in the process.

Tobias

> Larry
> 
> Begin forwarded message:
> 
>> From: "W. Li" <wl302 at cam.ac.uk>
>> Subject: A possible bug with Isabelle 2013
>> Date: 26 February 2013 15:56:58 GMT
>> To: "L. Paulson" <lp15 at cam.ac.uk>
>>
>> lemma "True"
>> proof -
>> have "True=(∃x. (λ_.True) x)" by simp
>> also have "...=(∃x. (λ_.True) x)"
>> oops
>>
>> Here is the error message:
>>
>> Type unification failed: Clash of types "bool" and "_ ⇒ _"
>>
>> Type error in application: incompatible operand type
>>
>> Operator:  op = … :: (??'a itself ⇒ bool) ⇒ bool
>> Operand:   ∃x. True :: bool
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>