Thanks for explaining GSPEC, SETSPEC & IN_ELIM_THM, Michael! I'm glad to know that HOL4 can replicate my 1-line proof with SRW_TAC [][EXTENSION], similarly "complicated underneath the hood." I'm confused by you paraphrasing Konrad as saying that your exercise was "annoying to prove." It would seem to me now that Konrad probably meant that there's a slick 1-line proof that would be, for newbies like me, "hard to understand".
Thanks for also explaining IN_ELIM_THM, John! Your 2nd fork is all I'm I'm worrying: the encoding of sets and the IN_ELIM_THM theorem that's used to unravel it seems complicated or unintuitive to explain to readers not versed in HOL? And it's not just me who's not versed in HOL. I'm hoping mathematicians and high school teachers are going to read my paper and code, so the less I befuddle them the better. It doesn't follow that my lambda rewrite is a good idea, and I'd like your guidance here. I didn't understand your SET_RULE rewrite, so I'll go read about SET_RULE. Let me back up a bit: Originally I had problems with set in miz3, but I think now that it was just my incompetence, and after I learned about IN_ELIM_THM, I could use {...} in my definitions of rays, angles etc. I just posted a problem with miz3 and {...}, but that seems pretty minor to me. So I'm no longer thinking that "compiler does a poor job on code." I still have set theory problems, but they don't seem to involve miz3. Ramana and Michael helped me to eliminate new_axiom and new_type from the beginning of my simpler Tarski axiomatic geometry code. But it got messy when I came to my defined infix predicate parse_as_infix("cong",(12, "right"));; let cong_DEF = new_definition `a,b,c cong x,y,z <=> a,b === x,y /\ a,c === x,z /\ b,c === y,z`;; and I never finished the rewrite. I was amazed to get even that far. Right now I'm worrying about a different problem, that I've never understood sets.ml, especially its use of IN_ELIM_THM to prove the IN_<operation> theorems. After Michael taught me that a {...} is equal, in a complicated way, to a lambda, I thought, why not just define INTER, DELETE, UNION etc as lambdas? Then the IN_<operation> theorems are easy to prove, and I wrote up miz3 proofs myself that I could easily understand. It would be easy to rewrite my 4000 lines of miz3 Hilbert code using lambda defs of INTER etc, and maybe that makes my code look simpler or more self-contained. I'm still not convinced it's a good idea. I think I'm missing a lot. What is the point of the {...} definition of INTER, other than to see the nice {...} notation? I love the {...} notation myself, but it's really equal to a lambda. So I wonder if the visual plus of some {...} in my code and in sets.ml offsets the fact that BETA_THM is so much simpler than IN_ELIM_THM. I can't judge. It ! was definitely a thrill for me to write readable understandable miz3 proofs of all the sets.ml results that I use. I can think of other miz3 problems that seem a lot more pressing that set notations, like being able to use #use "<miz3-file>.ml";; I'm guessing I'll have 5000 lines of code by the time I'm done, and what if somebody's machine can't store that much in the X-selection or whatever to paste it from one window to another? And if we could #use miz3 code, couldn't it be included in distributions with straight HOL Light code? We had a vigorous discussion about about how powerful miz3 could be, or wants to be. Here's what I learned, mostly from Michael. Mizar, as opposed to miz3, seems to have intentionally weakened itself (i.e. you have to write out very complete proofs), and that's a plus for using Mizar in classrooms to police the students' homework. I used to desire such weakness, but Michael convinced me that this is a bad idea (respect the students, don't shackle them!), and something that, at least in miz3, is just a matter of fiddling with the heuristics in a hit or miss way. Freek explained there was no evidence for any shackling of miz3, which can indeed give 1-line proofs of my first 24 theorems or so. But it's odd that miz3 isn't even more powerful. Freek pointed out that MESON has a built-in depth limit of 50 which GEN_MESON_TAC can remove. But you seem to argue in the reference manual that raising the depth limit isn't a good idea: However, the inconvenience of doing this is seldom repaid by a dramatic improvement in performance, since exploration is normally at least exponential with the size bound. Michael & I agreed we wanted miz3 to be more powerful, and you're the expert! Freek explained that all the calculation of "by" justifications is actually done in your code holby.ml. Here's a dumb question. I know MESON is an FOL prover that can't handle true HOL, and I think I have some true HOL code, owing to my sets.ml set theory. But I have no idea how much my sets slow MESON down. -- 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info