OK, glad to hear [miz3 works]! By 2.20++ you mean that you're using one of the recent svn snapshots from Google Code, right?
John, I'm pretty sure I downloaded it from this link http://www.cl.cam.ac.uk/~jrh13/hol-light/ a snapshot from 10th January 2010 is available as a GZIPPED TAR FILE or as a zip file. That's the right version, as hol.ml reads hol_version = "2.20++";; 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. That would be excellent, John! I don't think in this case the additional load of having "TarskiModel" hypotheses on theorems is too bad anyway. No, I can live with my "TarskiModel" hypotheses. Thanks for reading my code carefully enough to spot that. 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. I would really like that advice. I want to submit my Hilbert geometry paper soon, and I want to cite some readable geometry code. By the simpler version, I assume you mean | I had one theorem [whose proof was a mile long] | | AXIOM_1 and ... AXIOM_1 implies lemma1, lemma2, ... lemma17 I can start out that way! Can you explain? I'm so ignorant I don't even know how to do that, but I bet it's easy, just new_definition... With either of these two solution, we're not using your original code showing that R^2 is a model of Tarski's axioms, and that's a priority. What I don't like about my Mizar code is 1) some clunky features of Mizar I bet Freek knows how to fix, and 2) The silly way I made my axioms into theorems which I could then cite. But I preferred the portability of this to the mile long 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. Would you really like to know how to prove that? I don't do it in my paper, but I've often thought I should. Hartshorne's whole book more of an extremely cool overview than a source of rigorous proofs, and this part is especially sketchy. Birkhoff's proof barely exists, and MacLane who cleaned up Birkhoff didn't fix that part? 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. I'll be happy to write miz3/HOL-Light code, if we can just fix some problems that annoyed me with Mizar (see below). But I'm not happy with Freek posting here about how he used dirty Ocaml hacks! What can we do to clean up the code? BTW you told me to write HOL-Light, and I'm be really happy to, and I must do this eventually, but right now I'm really confused by all the non-Mizar proof assistants, because: I say the first requirement for a good proof assistant is for humans to be able to code up nice readable axiomatic proofs. Right now this does not seem to be true for HOL-Light, Coq or Isabelle. But proof assistants can't do anything (I think) besides generate and check axiomatic proofs. And if we can't code up nice readable axiomatic proofs, then aren't the machines getting escaping our control? I assume everyone agrees with me, so maybe the problem was that no one had any nice readable axiomatic proofs they wanted to code up. The action seems to be in using powerful proof assistants to verify e.g. FoG or Tom's Hales's Kepler conjecture proof. These are worthy aims, and much more ambitious projects than mine. But mine is worth doing too, I claim, and probably not very hard. I'd write the readable axiomatic proofs code myself if I had a clue about how HOL-Light worked. But I'm stymied by the examples being so much more complicated than my Hilbert/Tarski geometry axioms examples. To take our copyright discussion public, I'm absolutely thrilled that HOL Light has a BSD license, as we see from http://code.google.com/p/hol-light/. I'm not sure why you think GPL is viral, but BSD is fine with me. What confused me was the copyright on your ml files, e.g. (* (c) Copyright, University of Cambridge 1998 *) (* (c) Copyright, John Harrison 1998-2007 *) -- Best, Bill ------------------------------------------------------------------------------ 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
