Re: [isabelle] few questions about Isabelle/jEdit



The color purple means that the proof method is still executing. If this is
still the case after 5 or so seconds, there is a good chance it will never finish.

All proof methods are sensitive to exactly how a you state a goal. Some more so
than others. What "algebra" can and cannot do is not so clear.

For proofs about real (in)equalities you could try (simp add: field_simps). It
proves your tf3.

Tobias

On 19/04/2014 18:41, noam neer 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.
> 
> 




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