Dear Lockwood
It was lovely to see your message.
I would be happy to look at your files, and, if they are in (or if we can
get them into) reasonable shape, to add them to HOL.
Can you put them online? Otherwise an attachment would be OK.
(Others on list interested in this feel free to help or take over.)
One comment, though, is that I suspect a lot of work on efficient
computation for explicit finite sets/lists has been put into computeLib.
Did you find that computeLib.EVAL_CONV was not appearing to do
logarithmic-time IN and linear-time UNION? (I'm not sure whether it's
supposed to currently.)
It may be worth seeing whether your improvements can be formulated as
theorems and conversions that can be added to the_compset.
Regarding your first and third questions:
As I understand, a library is an ML structure and there are no further
requirements, except perhaps consistency of interface and a theme (what the
library is for).
I just had a quick look for a theorem resembling "there's a total order on
every type" (by checking relationTheory and grepping the HOL sources for
"total") and didn't see anything.
But then I thought to look for "well-ordering" and variants thereof, and
found the result in examples/set-theory/hol_sets/wellorderScript.sml,
called "allsets_wellorderable".
Cheers,
Ramana
On Sat, Nov 10, 2012 at 11:40 PM, F.Lockwood Morris <[email protected]>wrote:
> For the past year I have been engaged in developing a collection of
> conversions, conversion-like functions, and supporting theories to enable
> the use of one form of well-balanced binary search tree in HOL, with the
> objective of bringing to computations with explicitly displayed finite
> sets and functions similar speeding-up to that which the `numeral'
> representation provides for numeric computations---for example,
> logarithmic time IN and linear-time UNION for finite sets (if element
> comparisons can be regarded as taking constant time)---but, sadly, with
> no hope of imitating the invisibility of numerals. I mean to
> submit a description of the package to next summer's Conference on
> Automated Deduction. My hope is that it may eventually become a useful
> addition to the HOL libraries.
>
> The rest of this message consists of three more or less specific questions
> and
> a more general plea for help.
>
> 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?
>
> 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, leaving to it the work of
> matching terms and types, but avoiding searching. As an easily
> grasped example of the style, here is an equivalent of the listLib's
> REVERSE_CONV:
>
> (* REVERSE_REV = |- !L. REVERSE L = REV L [] *)
>
> val [rev_nil, rev_rec] = CONJUNCTS REV_DEF;
>
> (* rev_nil = |- !acc. REV [ ] acc = acc
> rev_rec = |- !h t acc. REV (h::t) acc = REV t (h::acc) *)
>
> val REVERS_CONV =
> let fun rev_conv t = ((REWR_CONV rev_rec THENC rev_conv) ORELSEC
> REWR_CONV rev_nil) t
> in REWR_CONV REVERSE_REV THENC rev_conv end;
>
> (*- REVERS_CONV (Term`REVERSE [1; 2; 3; 4; 5]`);
> > val it = |- REVERSE [1; 2; 3; 4; 5] = [5; 4; 3; 2; 1] : thm *)
>
> 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.)
>
> 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.
>
>
> 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.
>
> I am not exactly in a hotbed of HOL activity here at Syracuse, and I fear
> that I am myself a good deal less UNIX-savvy than most hol-info
> correspondents seem to be. I get on all right with HOL and emacs,
> and I know to run Holmake and, when mysterious ailments appear,
> Holmake cleanAll, but that is about it. Please do not withhold remarks on
> grounds of obviousness.
>
> Thanks to all,
>
> Lockwood
>
> |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-
> |- |- |- |-
> Lockwood Morris [email protected] (315)443-3046 Rm. 4-125 CST
> EECS Syracuse University 111 College Place Syracuse NY 13244-4100
>
> ------------------------------------------------------------------------------
> 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
>
------------------------------------------------------------------------------
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
