[isabelle] jEdit apparantly proves False



Hi all,

while giving a tutorial on Isabelle, I run into the following strange
effect, where jEdit seems to indicate that a lemma is proven. Actually,
the lemma just contains a diverging method invocation. See screenshot.

To reproduce this behaviour, just load the attached theory file, wait a
few seconds (the simp add: A A[symmetric] is marked purple now). Then
move the cursor after the lemma and type some newlines, save the file,
and you get (on my machine) the above effect. You can even use the lemma
to prove further non-theorems from it without any problems!

--
  Peter

p.s.
  As I can see from some homework submissions, some of our students seem
to run into this effect regularly when solving homeworks :(

pps:
 Thm.peek_status @{thm f} returns 
  val it = {failed = true, oracle = false, unfinished = false}:
   {failed: bool, oracle: bool, unfinished: bool}


Attachment: False.png
Description: PNG image

theory False
imports Main
begin

lemma f: False proof -
  {
    fix A B :: bool and f
    assume A: "A=B"
    have "f(A)" by (simp add: A A[symmetric])
  } note this[of True True Not]
  thus False by simp
qed

lemma "(1::nat) = 2" using f by simp

end



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.