Email Gateway (Feb 03 2024 at 08:42): Email Gateway (Feb 03 2024 at 08:42):From: Alex Shkotin <alex.shkotin@gmail.com>
Hi All,
I have installed Isabelle and copy-paste theory from [1] like this [2].
How can I execute value commands from this theory and perform other
exercises from [1].
Thank you in advance,
Alex
[1] Tobias Nipkow, Programming and Proving in Isabelle/HOL, prog-prove.pdf
[2]
[image: image.png]
Email Gateway (Feb 03 2024 at 15:58):From: "John F. Hughes" <jfh@cs.brown.edu>
Try placing your cursor inside the theory. For instance, if I place my
cursor just at the end of the "value" line, I see this:
[image: image.png]
i.e., the value that I wanted to compute.
Moving up to the end of the previous line, I see this:
[image: image.png]
which is telling me that the recursive function "rev" has been successfully
defined, and that the recursion it defines actually is guaranteed to
terminate.
You might also want to remove a double-quote somewhere and see what
appears, or change "list" to "lst" somewhere, deliberately breaking the
'proof document', just to get a feel for which error messages can appear,
and how the 'constant update' thing feels.
When your cursor was just past the 'end' line, nothing new had been done or
produced, so there was no output showing.
You'd think that this sort of thing would be right there in a 'tutorial on
using Isabelle for the first time" somewhere on the project home page, but
it wasn't there when I started about 5 years ago. I began writing a
document about this for my class; it's for the 2018 or 2019 version, but it
may prove to be better than nothing.
Pro tip: if you had typed in your entire document (as I did) rather than
loading it from disk or copy-pasting from the text, you'd have seen lots of
responses as you were typing, and you'd have gotten a start on the whole "
when do I have to use double-quotes and how do I get to the point where
that seems natural?" thing. I strongly recommend typing in examples until
you're really confident that you've learned all that you can from doing so.
Email Gateway (Feb 03 2024 at 16:29):From: Alex Shkotin <alex.shkotin@gmail.com>
John and All, Thank you!
Is there a chance to get output to a file using maybe Isabelle command line
tool?
What is the usual way to perform all exercises from [1]?
Alex
сб, 3 февр. 2024 г. в 18:58, John F. Hughes <jfh@cs.brown.edu>:
Email Gateway (Feb 04 2024 at 14:01):From: Lawrence Paulson <lp15@cam.ac.uk>
Quite right. The first few times I tried out Isabelle/jEdit I was completely baffled. I would open a file and it would just sit there. Where was the theorem prover? I took a little while to see that it was there, had already processed the entire file like a flash, and would update itself immediately upon any change.
Larry
Email Gateway (Feb 04 2024 at 14:40):From: Makarius <makarius@sketis.net>
You won't need this to learn using Isabelle, nor to use it professionally.
Nonetheless, it is possible to do this, using the relatively recent "isabelle
build_log" command-line tool as follows (e.g. with Isabelle2023):
isabelle build HOL-Examples
isabelle build_log HOL-Examples
isabelle build_log -U HOL-Examples
isabelle build_log -U -H Warning HOL-Examples
See also "isabelle doc system" for more information.
Now you can forget that I've revealed that. It is just a diversion from
learning to use Isabelle professionally.
Makarius
Email Gateway (Feb 05 2024 at 07:46):From: Alex Shkotin <alex.shkotin@gmail.com>
Larry, Makarius and All,
For me exercises in [1] are examples of how to use theory. Now it looks
like to create a task theory, import theories involved and fulfill it with
exercises. I am ready to check Makarius' proposal.
The general question is: You have a lot of theories, how to use them to
work with particular structures?
My favorite working example is ugraphs :-)
Alex
[1] Tobias Nipkow, Programming and Proving in Isabelle/HOL, prog-prove.pdf
вс, 4 февр. 2024 г. в 17:00, Lawrence Paulson <lp15@cam.ac.uk>:
Last updated: Jan 04 2025 at 20:18 UTC