Re: [isabelle] few questions about Isabelle/jEdit



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.




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