Re: [isabelle] few questions about Isabelle/jEdit
Le Sat, 19 Apr 2014 18:41:24 +0200, noam neer
<noamneer at gmail.com> a écrit:
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"
3. in the previous example, if I reverse the sides of the equality in
the "by algebra" part is colored red and the output buffer contains
indicating failure. why does the order matter ?
It's common the way you write a proposition has an effect on the way you
prove it. Humans see things which seems obvious to them (while sometimes
are wrong, and that's why there are machine‑checked proofs) which machines
so far can't easily see (while machines are a lot more exact than humans).
When it happens, you can help it.
When you feel something should be obvious according to a simple lemma, you
can search for it with the “Find” panel or test a more simpler proof to
see if Isabelle can solve it. If the “Find” panel is not visible, go to
“Plugins -> Isabelle -> Find Panel” and it will show‑up.
Here, may be you expected Isabelle to automatically swap the two sides of
the equality. If so, you wanted a the theorem like `A = B ==> B = A`. If
you type `_ = _ ==> _ = _` in the search bar of the Find panel and hit
enter, you will see the first result is `HOL.sym`, which may be what you
want for this case. You then explicitly tell Isabelle to use `HOL.sym` in
The Find panel is a lot useful if you have a guess of what you need.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and