Thanks, Michael! I will treat the Logic Manual as a true description of the HOL in HOL Light, and I will try harder to read it. I have a lot of trouble with your 3 sentences:
Sets in HOL Light and HOL4 are predicates over their respective types. Types correspond to non-empty sets (as already discussed). So, because any predicate bounded above corresponds to a ZFC set, the sets in HOL do also correspond to ZFC sets. One question would be: how does HOL Light turn my code into ZFC FOL? That sounds like a tough question which I'm interested in, but it's not my real question. I need to talk about sets to my audience of mathematicians in my paper I'll submit soon to the Amer Math Monthly. I have 3900 lines of code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz and I want to tell them something about which sets I'm using. My first 4 lines of code are new_type("point",0);; new_type_abbrev("point_set",`:point->bool`);; new_constant("Between",`:point->point->point->bool`);; new_constant("Line",`:point_set->bool`);; I think that says I told HOL Light to define a set called point and two functions Between: point x point x point ---> {True, False} Line: P(point) ---> {True, False} These sets & functions will be specified more closely by my axioms. We then (in our heads) define a "point" to be an element of point, and a "line" to be a subset of point (i.e. element of P(point)) which Line sends to True. I think my first axiom let I1 = new_axiom `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;; says that given two elements of the set point, there is a unique line containing them. I often write let A B C be point; I think that means that A, B and C are variables referring to "points", and so (in our heads) we say that if Between A B C = True then the middle "point" is "between" the two outer "points". I have a definition let Interval_DEF = new_definition `! A B. open (A,B) = {X | Between A X B}`;; I think that says if A, B refer to two elements of a & a of the set point, then open (A,B) refers to the subset of point consisting of all "points" between a and a. Now is my interpretation of my own code correct? I'm happy to cite the Logic Manual in my paper, but need to give audience more to go on. Are there any examples in the Logic Manual that are as "concrete" as my description above? I'm not too worried right now about how HOL Light is able to prove my statements about such sets are actually true. I have technical questions about sets defined by {...}, whether they're abstractions or enumerations (thanks for the new terminology, Mark). My first theorem is let IN_Interval = prove (`! A B X. X IN open (A,B) <=> Between A X B`, REWRITE_TAC[IN_ELIM_THM; Interval_DEF]);; Here's the code in sets.ml for IN_ELIM_THM: let IN_ELIM_THM = prove (`(!P x. x IN GSPEC (\v. P (SETSPEC v)) <=> P (\p t. p /\ (x = t))) /\ (!p x. x IN GSPEC (\v. ?y. SETSPEC v (p y) y) <=> p x) /\ (!P x. GSPEC (\v. P (SETSPEC v)) x <=> P (\p t. p /\ (x = t))) /\ (!p x. GSPEC (\v. ?y. SETSPEC v (p y) y) x <=> p x) /\ (!p x. x IN (\y. p y) <=> p x)`, REPEAT STRIP_TAC THEN REWRITE_TAC[IN; GSPEC] THEN TRY(AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM]) THEN REWRITE_TAC[SETSPEC] THEN MESON_TAC[]);; Why do we have to work so hard to prove IN_Interval? I would have thought that the {...} definition in Interval_DEF just amounted to a lambda, so open (A,B) = {X | Between A X B} means that open (A,B) = \X. Between A X B With that lambda definition of open (A,B), my theorem IN_Interval looks really obvious, it just needs the first definition of sets.ml let IN = new_definition `!P:A->bool. !x. x IN P <=> P x`;; Are you & Mark saying that HOL Light has a more complicated definition of {X | Between A X B}, one that requires the serious technicality of IN_ELIM_THM? Can I just rewrite sets.ml myself with ordinary lambdas so that I don't need IN_ELIM_THM? I think my audience of mathematicians needs some explanation, and hoping you'll give me one. -- 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
