Re: [isabelle] few questions about Isabelle/jEdit



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.



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