[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.