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

[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

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