*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] few questions about Isabelle/jEdit*From*: noam neer <noamneer at gmail.com>*Date*: Sat, 19 Apr 2014 19:41:24 +0300

hi, I have a few newbie questions about Isabelle/jEdit. I'm using version 2013-2 on Windows 7. 1. when I put the following in my theory file - lemma NNF : "(1::real) < 0" proof - show ?thesis by auto qed the "by auto" part is colored in red, and when I move the cursor to the end of its line the output buffer shows some lines in red containing the message Failed to finish proof: ... however, the lemma itself seems to be considered proven. it can be printed with thm NNF and used in subsequent lemmas (such as proving "2<0"). why is this so? can I order Isabelle to stop at the first error and report? alternatively, is there a way to get a report from Isabelle about those proofs that failed, without having to scan the whole file myself for red spots? 2. here's an example of a more complex (and true) inequality with a proof - lemma mon_mix_1 : fixes a b c::real shows "a*a + b*b + c*c >= a*b + a*c + b*c" proof - have tf3 : "(a-b)*(a-b)/2 + (a-c)*(a-c)/2 + (b-c)*(b-c)/2 = a*a + b*b + c*c - a*b - a*c - b*c" by algebra have tf4 : "a*a + b*b + c*c - a*b - a*c - b*c = (a-b)*(a-b)/2 + (a-c)*(a-c)/2 + (b-c)*(b-c)/2" using tf3 by auto have tf5 : "a*a + b*b + c*c - a*b - a*c - b*c >=0" using tf4 by auto show ?thesis using tf5 by auto qed when Isabelle reads this the "by algebra" part in the proof of "tf3" is colored purple, but the output buffer seems to be OK, with no red or purple lines. what does this mean ? is there an error in the proof ? 3. in the previous example, if I reverse the sides of the equality in "tf3" the "by algebra" part is colored red and the output buffer contains some red lines indicating failure. why does the order matter ? thanks, Noam. -- I can't see very far, I must be standing on the shoulders of midgets.

**Follow-Ups**:**Re: [isabelle] few questions about Isabelle/jEdit***From:*Lawrence Paulson

**Re: [isabelle] few questions about Isabelle/jEdit***From:*Tobias Nipkow

**Re: [isabelle] few questions about Isabelle/jEdit***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Issue with `Simpl` user guide `Fac` example
- Next by Date: Re: [isabelle] few questions about Isabelle/jEdit
- Previous by Thread: Re: [isabelle] setup_lifting: »No relator for the type … found«
- Next by Thread: Re: [isabelle] few questions about Isabelle/jEdit
- Cl-isabelle-users April 2014 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