Hi Bill, | John, I was wrong, and all the mizar modes work fine with ocaml-3.09.3 | and hol_version 2.20++. I can successfully paste in these 5 commands: | | hol_light> ocaml | #use "hol.ml";; | #load "unix.cma";; | #use "miz3/miz3.ml";; | #use "JohnTarskiGeometry.ml";;
OK, glad to hear it! By 2.20++ you mean that you're using one of the recent svn snapshots from Google Code, right? | It didn't work to substitute your Mizar mode Examples/mizar.ml. Your | Tarski code chugged away but hung for hours. Mizarlight/make.ml also | didn't work, failing to prove your EquivReflexive, with error message | Unbound value thm. | So Freek's miz3 was the big winner! Yes, I think miz3 is definitely the best of the bunch. I've been quite pleasantly surprised how usable it is, and how like Mizar the experience of writing proofs in it becomes. My old Mizar mode is probably mainly of historical interest, as an existence proof that one could support such proof styles in the LCF world. | Thanks for your new miz3 code, which is quite readable, and runs fine, | together with your (not so readable) earlier code, which amounts to | | 1) Proving Tarski's axioms as theorems in the coordinate plane R^2 | 2) using these axiom-theorems to prove Tarski's theorems. | | We're not actually deducing consequences of Tarski's axioms here. | We're proving theorems in R^2, where all of Tarski's theorems (or | Hilbert's) are clearly true. That's not what want. For one thing, we | miss out on applying Tarski's axioms to hyperbolic geometry, as Tim | did on the Isabelle list (I can't read his code). Sure, I said as much earlier in this thread. However, although we are "in fact" proving things in R^2, we are throwing away the derivation of the axioms and reasoning purely axiomatically, so it doesn't mean much from the practical point of view of what the proofs look like. If you decide to set things up a bit differently, the cores of the proofs would be the same or similar with just a bit of extra cruft, and I thought it was nice to have the most transparent versions as your introduction to HOL Light. | You and Freek didn't define the Mizar datatype `struct', which is what | I use: A Plane is a struct, a set with a 4-ary Betweenness relation | and 3-ary Equidistant relation. It's perfectly possible to set things up this way, effectively giving each theorem the additional hypothesis. I think that then the proofs would look even more like your Mizar originals with the "TarskiModel" hypothesis and the corresponding first step of each proof. | BTW Hilbert and Birkhoff both prove that with enough axioms including | the parallel postulate, there's a unique model R^2, so there's nothing | unrigorous about working in coordinates, at least if you understand | this result, which Hartshorne does a pretty good job explaining. Yes, it would be very interesting to prove that. | I don't know what the plan to do this in miz3 is, though. Do we still | use newdefinition to define the axioms? Can we stack the axioms and | definitions together into something like a Isabelle locale and invoke | it when we want to prove theorems? BTW my first Mizar success was | really ugly: I had one theorem | | AXIOM_1 and ... AXIOM_1 implies lemma1, lemma2, ... lemma17 | | and the proof was a mile long. I finally stumbled on my also | inelegant solution of making each axioms into a theorem. I don't think it's all that inelegant, really. You can do exactly the same in HOL Light, but there isn't something like the locale mechanism to hide it from the user. I don't think in this case the additional load of having "TarskiModel" hypotheses on theorems is too bad anyway. I can give you more detailed guidance on how to set this up if you like, but it might be fine to stick to the simpler version for a bit. John. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
