[isabelle] few questions about Isabelle/jEdit
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"
show ?thesis by auto
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
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
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"
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"
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"
have tf5 : "a*a + b*b + c*c - a*b - a*c - b*c >=0"
when Isabelle reads this the "by algebra" part in the proof of "tf3" is
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
indicating failure. why does the order matter ?
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