Email Gateway (Aug 19 2022 at 09:09): Email Gateway (Aug 19 2022 at 09:09):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
Hi Tim,
thanks for your reply! Colin has already covered your feedback on
auction theory; he is our expert for economics. Let me reply on the
Isabelle-specific things, with some more questions to everyone, covering:
2012-11-01 02:07 Tim (McKenzie) Makarios:
We would like to contribute our formalisation to the AFP, but are unsure about the procedure: once accepted and published, can we submit updates?
Thanks, and sorry; I should have noticed that on the AFP homepage. I
think that after another revision (according to the other feedback
collected here, plus some other things we wanted to do anyway), we will
submit.
- It would be nice to be able to introduce proper types (not just type_synonyms) for things such as non-negative real vectors.
Have you seen section 8.5.2 of tutorial.pdf in Isabelle's doc folder?
I have, but wasn't sure whether/how it applies to what we are doing.
IIUC this is about defining completely new types from scratch, whereas
we are rather interested in restricting existing types.
Plus, a question to everyone reading this: I haven't worked with the
Tutorial too much, but mainly consulted the Isar Reference. The
Tutorial does proofs in the "apply(rule)" style, which we don't consider
helpful for our target audience; we prefer textbook style. Of course,
I'm sure, for "apply(rule)" proof there is a straightforward translation
to Isar, but for me, being a relative beginner, this is not yet _so_
straightforward.
I'm quite interested in what you're doing; after working with Isabelle
for my Master's project, I'm now musing about auction theory: …
Interesting! (I just can't add anything to Colin's comment.)
In preparation for this,
I tried running Isabelle's document preparation system on Vickrey.thy
(see chapter 4 of isar-ref.pdf, and possibly other parts of Isabelle's
documentation).
So far we haven't bothered to generate a document from our
formalisation, but I agree that we should soon do. I see that chapter
4.2 of the Tutorial also documents this. So I should learn how to do it.
Second, your "text {* ... *}" portions don't always contain valid LaTeX.
I made minimal changes to get your document to compile, but I haven't
had time to read it yet. I've attached my edited version of your
Vickrey.thy, so you can see what changes I've made.
Thanks for these!
I've made almost no
effort to make it look as you intended
Well, as I said, I have not yet _intended_ anything ;-)
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 09:11):From: Tobias Nipkow <nipkow@in.tum.de>
If you look at the documentation page
http://isabelle.in.tum.de/documentation.html you will find that the first
document is the relatively new Programming and Proving in Isabelle/HOL, which
does cover structured proofs (which is why I wrote it). The Tutorial is now only
second choice because of the foucus on "apply".
Tobias
Email Gateway (Aug 19 2022 at 09:22):From: Makarius <makarius@sketis.net>
In addition, see
* http://isabelle.in.tum.de/dist/Isabelle2012/doc/system.pdf
Chapter 3: Presenting theories
* http://isabelle.in.tum.de/dist/Isabelle2012/doc/isar-ref.pdf
Chapter 4: Document preparation
Makarius
Last updated: Apr 26 2024 at 08:19 UTC