On 11/11/12 10:40, F.Lockwood Morris wrote: > First, I don't understand at all how libraries work, and have come > across nothing in the HOL documentation about them beyond a caution > to the effect that the addition of new ones to the system requires > central approval. Can anyone point me to relevant information on the > design of, and requirements for, HOL libraries?
That language sounds a deal more forbidding than I’d like. Can you point me to it so it can be fixed/removed? In any case, I’d be quite happy to take delivery of source code in whatever form you like. > Second, efficiency of derivation is of course a concern for the > conversions I have been writing, but so also to some extent is > readability. I have been modeling my style on Paulson's "A > higher-order implementation of rewriting", taking REWR_CONV (which > he in that paper called "REWRITE_CONV") as the workhorse [...] > Is this a reasonably efficient way to go, at least for a first > version? (Source for conversions I see in various libraries seems to > feature a lot more of INST_TYPE and SUBST in ways that I find > difficult to understand.) I think use of REWR_CONV is absolutely fine. > Third, I have been led to define a polymorphic type 'a toto of total > orders on type 'a, and this has of course entailed showing that at > least one such exists. It was a most educational experience for me > to translate the chapter of Halmos's Naive Set Theory in which he > proves the well-ordering theorem into HOL in order to make this > existence proof, but the result was a large file which I would be > very happy to suppress if, as I suppose very likely, there is > already a proof somewhere in the HOL system. As Ramana said, I recently proved this (every set can be well-ordered) as part of my development of the ordinal numbers. I needed Scott Owens’ earlier proof of Zorn’s Lemma. My proof is in examples/set-theory/hol_sets, in Kananaskis-8 onwards. Let me know if you’d like any help in linking your theories to those of mine that you need. > My general plea is for comments and advice from anyone who has them > to offer. I would be happy to send my files in their current state, > with some rough descriptive notes, to anyone (ideally, someone who > is desperate to get some set operatons or list searches inside a HOL > proof to run faster) who would care to look at them and give helpful > criticism. The only roughly related work I’m aware of is the mechanisation of Patricia trees, in src/patricia. I don’t think this work has been written up. Ramana earlier mentioned EVAL, also known as CBV_CONV. This aims to allow efficient rewriting for sets of equations that look like functional programs. I imagine your HOL definitions look quite functional so it might be interesting to compare the behaviour of the hand-crafted code and EVAL when primed with them. Best, Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_nov
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
