Email Gateway (Aug 19 2022 at 09:06): Email Gateway (Aug 19 2022 at 09:06):From: Makarius <makarius@sketis.net>
Depends what you mean by "modern" and "editor".
jEdit is a very capable "programmer's editor" is it advertizes itself, but
not a word processor. Program text is hardly ever soft-wrapped, so
relatively little has been invested in this area. It you take Isar
sources, things like {* ... *} are a separate token anyway, like " ... ".
Would you expect from a source-code editor to wrap lines within string
literals?
Nonetheless, I can myself imagine Isabelle/jEdit doing something for
text {* ... *} blocks within Isar source, but that has to be specific to
the language, meaning I have to sit down and provide that functionality.
(As I did already for many other things.)
Makarius
Email Gateway (Aug 19 2022 at 09:12):From: Tobias Nipkow <nipkow@in.tum.de>
If you want to restrict to a subset of a type wityhout creating a completely new
type, you must do that on the formula level with explicit assumptions in your
propositions.
Tobias
Email Gateway (Aug 19 2022 at 09:13):From: Tobias Nipkow <nipkow@in.tum.de>
Great stuff, look forward to more of this.
A small random point: the definition
definition in_range ::
"nat \<Rightarrow> nat \<Rightarrow> bool" where
"in_range n i \<equiv> 1 \<le> i \<and> i \<le> n"
excludes 0. Unless you have some very good reason for starting at 1, I would
start at 0, which typically makes things smoother. For a start, you can just
write "i<n" instead of "in_range n i".
Tobias
Email Gateway (Aug 19 2022 at 09:16):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
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
- 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?
Perhaps there's also other documentation in another file; if so, I hope
someone else knows where and points you to it.
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:
http://wp.me/p2IaW7-W (I'm not trained in economics, so please be
gentle, but please do comment on my musings if you think I'm in error,
or if you have anything else to say about them.) Consequently, I
decided to have a look at your Vickrey theory. 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). Unfortunately, it didn't work at first, for a couple of
reasons.
First, Vickrey.thy didn't end with "end", which was easy to fix.
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. I've made almost no
effort to make it look as you intended --- only to make it compile.
Tim
<><
Vickrey.thy
signature.asc
Email Gateway (Aug 19 2022 at 09:19):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
I've had a look at your work, and found it interesting.
One thing that I noticed was that you defined what it means to be a
second_price_auction, and you proved various things about functions that
satisfy this definition, but you never showed that the definition was
satisfiable.
This isn't an inconsequential detail; at first, I thought you'd got the
definition wrong, and that "second_price_auction n x p" implied n < 2.
When I tried to prove it, I finally noticed that your allocation and
payment functions depend on the set of bids. But it is easy to write
definitions that aren't satisfiable, or that imply trivialities.
So I decided to prove that your second_price_auction was satisfiable for
n > 0. See attached for the proof.
Also, you made a comment about removing an element from a set. Given a
set A, the set of all the elements of A except x can be written as
"A - {x}"
I have a feeling that there was something else I was going to comment
on, but I should go and have lunch, and write again if I remember it.
Tim
<><
Vickrey_Extras.thy
signature.asc
Email Gateway (Aug 19 2022 at 09:24):From: Makarius <makarius@sketis.net>
On Wed, 31 Oct 2012, Christoph LANGE wrote:
QUESTIONS FOR ISABELLE COMMUNITY
We would like to contribute our formalisation to the AFP, but are unsure
about the procedure: once accepted and published, can we submit updates?
We could imagine submitting this formalisation soon (as it is
self-contained and covers a relevant field), but still we are planning
to evolve and improve it.
I am not an editor of AFP, but it is generally a good idea to refine and
consilidate some development several times, before entering the submission
process.
If you need a hosting platform for the development process, I can
recommend https://bitbucket.org/ (with Mercurial).
As this was our first major Isabelle formalisation, we may have got a
lot of things wrong. We would be grateful if any of you were able to
look into the source and tell us of any "anti-patterns" we shouldn't
use. I will also follow up on this mail with a number of mails asking
specific questions on how certain things in Isabelle work, and with some
jEdit bug reports.
Looking only briefly over your Vickrey.thy, it already looks quite good as
a start. There are many fine points to be considered; we should go
through it gradually and without attacking everything at the same time.
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. (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.)
When doing functional programming properly, you also don't write funny
tuple arguments all the time, just to please ousiders, you use currying.
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.
jEdit is not very good at soft line-breaks, 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.)
Makarius
Email Gateway (Aug 19 2022 at 09:25):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
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
Last updated: Apr 25 2024 at 04:18 UTC