[isabelle] Type restrictions; document preparation [Re: Started auction theory toolbox; announcement, next steps, and questions]

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:

* defining restrictions of existing types
* tutorial.pdf vs. isar-ref.pdf

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?

Yes; see http://afp.sourceforge.net/updating.shtml

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

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 ;-)



Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)

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