# [isabelle] few questions about Isabelle/jEdit

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.