*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] few questions about Isabelle/jEdit*From*: noam neer <noamneer at gmail.com>*Date*: Sun, 20 Apr 2014 17:04:56 +0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <000CA2F1-5FE7-4D3B-BD3F-3485AF258100@cam.ac.uk>*References*: <CAGOKs0-ZoYyXJjm6xCGsarW+Avp86WUT+dfSKonUg+KCNoSWeg@mail.gmail.com> <000CA2F1-5FE7-4D3B-BD3F-3485AF258100@cam.ac.uk>

thanks. how do I run it as batch job on windows ? On Sun, Apr 20, 2014 at 2:20 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > Everything is processed in parallel under the assumption that everything > above has been processed okay. It is quite normal for processing to reach > the end of the file even though significant parts of proofs are continuing > to execute. You need to check that there is no red anywhere in the sidebar. > The definitive test is to run it as a batch job. > > --lcp > > > On 19 Apr 2014, at 17:41, noam neer <noamneer at gmail.com> wrote: > > > > 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. > -- 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:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] few questions about Isabelle/jEdit***From:*noam neer

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

- Previous by Date: Re: [isabelle] few questions about Isabelle/jEdit
- Next by Date: Re: [isabelle] few questions about Isabelle/jEdit
- Previous by Thread: Re: [isabelle] few questions about Isabelle/jEdit
- 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