*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] few questions about Isabelle/jEdit*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 20 Apr 2014 13:57:46 +0200*In-reply-to*: <CAGOKs0-ZoYyXJjm6xCGsarW+Avp86WUT+dfSKonUg+KCNoSWeg@mail.gmail.com>*References*: <CAGOKs0-ZoYyXJjm6xCGsarW+Avp86WUT+dfSKonUg+KCNoSWeg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

The color purple means that the proof method is still executing. If this is still the case after 5 or so seconds, there is a good chance it will never finish. All proof methods are sensitive to exactly how a you state a goal. Some more so than others. What "algebra" can and cannot do is not so clear. For proofs about real (in)equalities you could try (simp add: field_simps). It proves your tf3. Tobias On 19/04/2014 18:41, noam neer 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. > >

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

- 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