*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] jEdit apparantly proves False*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 19 Nov 2013 13:40:29 +0100

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**

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

**Follow-Ups**:**Re: [isabelle] jEdit apparantly proves False***From:*Peter Lammich

**Re: [isabelle] jEdit apparantly proves False***From:*bnord

**Re: [isabelle] jEdit apparantly proves False***From:*Manuel Eberl

**Re: [isabelle] jEdit apparantly proves False***From:*Christoph Feller

- Previous by Date: Re: [isabelle] Quotient package and the type real
- Next by Date: [isabelle] partial_function shifts variable names in raw_induct
- Previous by Thread: [isabelle] two new AFP entries
- Next by Thread: Re: [isabelle] jEdit apparantly proves False
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list