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



Hi Makarius, hi all,

@All: Let me slowly resume the discussion of your feedback about our formalisation. The earlier feedback sent by others (thanks once more!) is not forgotten, I will get back to this next week, but the points in this mail are good for me to start with, as they don't require me to learn a lot of new things.

2012-11-16 22:49 Makarius:
Since Christoph is also a CICM person, I would like to point out the MKM
2008 paper by myself and Stefan Berghofer on "Logic-free reasoning in
Isabelle/Isar".  It shows how to deflate your theories by a significant
factor, by removing unnecessary fluff.

Thanks for the pointer!

(Informal people sometimes think
they are doing formal logic when writing a lot of logical connectives
around there meterial, but this is not the real point of it.)

Well, I actually didn't try to be as "formal" as possible, but I did not yet know how to do it right. In several lemmas I started with a simpler statement, e.g. just the right side of an implication, and put the left side into "assumes" declarations, but then I wasn't able to reuse these assumptions in the proof as expected. In the cumbersome way I ended up doing it I got the work done at least – but of course I'll be excited to learn about the nicer way of doing it, and how to avoid such pitfalls as I mentioned.

Can you write your sources with 80 char per line, or 100 maximum?  These
exceedingly long lines are hard to read.  The physicial parameters of
cinema displays have changed a lot recently, but not the parameters of
the human brain.

OK, I will try; it should be possible to introduce line breaks where it semantically makes sense.

But actually I'd like to blame half of the problem on this:

jEdit is not very good at soft line-breaks,

Not having much previous jEdit experience I simply had hoped that a modern editor would be good at that (even recent versions of dinosaurs such as Emacs are), and somehow denied that it didn't work so well after all.

End of rant; I don't want to start an editor war here.

and it is better to layout
your formal sources explicitly yourself.  (The jEdit indentation
facilities still need to be activated for Isar sources, like I did many
years ago for Proof General / Emacs.)

Let me report a problem related to that: I tried at least to enable auto-indentation, so that any new line would be indented as much as the previous line. But with that I found that Isabelle didn't pick up the changes I made. (This is roughly what I remember from trying it a few weeks ago; if you'd like me to do some experiments and give a more detailed report, I'm happy to do so.)

Cheers,

Christoph

--
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)
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/





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