Email Gateway (Aug 19 2022 at 14:22): Email Gateway (Aug 19 2022 at 14:22):From: noam neer <noamneer@gmail.com>
hi,
I have a few newbie questions about Isabelle/jEdit.
I'm using version 2013-2 on Windows 7.
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?
here's an example of a more complex (and true) inequality with a proof -
lemma mon_mix_1 :
fixes a b c::real
shows "aa + bb + cc >= ab + ac + bc"
proof -
have tf3 :
"(a-b)(a-b)/2 + (a-c)(a-c)/2 + (b-c)*(b-c)/2
=
aa + bb + cc - ab - ac - bc"
by algebra
have tf4 :
"aa + bb + cc - ab - ac - bc
=
(a-b)(a-b)/2 + (a-c)(a-c)/2 + (b-c)*(b-c)/2"
using tf3
by auto
have tf5 : "aa + bb + cc - ab - ac - bc >=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 ?
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.
Email Gateway (Aug 19 2022 at 14:22):From: Lawrence Paulson <lp15@cam.ac.uk>
Everything is processed in parallel under the assumption that everything above has been processed okay. It is quite normal for processing to reach the end of the file even though significant parts of proofs are continuing to execute. You need to check that there is no red anywhere in the sidebar. The definitive test is to run it as a batch job.
--lcp
Email Gateway (Aug 19 2022 at 14:22):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 19 2022 at 14:22):From: noam neer <noamneer@gmail.com>
thanks.
how do I run it as batch job on windows ?
Email Gateway (Aug 19 2022 at 14:22):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
The batch mode is when Isabelle is not running in interactive mode.
Similarly, you check a theory when you build a heap image or build the
documentation for it. If ever there is an error in a theory, the whole
process will fail. Most people want to at least produce a PDF file for
their theories, so the theory is always checked this way.
To understand all of this, you may have a look at “The Isabelle System
Manual” which is the file doc/system.pdf.
Email Gateway (Aug 19 2022 at 14:23):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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 proof.
The Find panel is a lot useful if you have a guess of what you need.
Email Gateway (Aug 19 2022 at 14:24):From: Makarius <makarius@sketis.net>
The Isabelle manuals are also accessible in the Documentation panel, which
is open by default in Isabelle/jEdit.
Anyway, the question above might be more basic: How to run batch tools at
all. For Isabelle on Windows there is Cygwin-Terminal in the top-level
directory, see also http://isabelle.in.tum.de/installation.html
Makarius
Last updated: Apr 19 2024 at 01:05 UTC