It also looks as if you could dispense with the T parameter, and just have
A1axiom (===) <=> !a b. a,b === b,a Thanks, Michael, it works!!! Whether or not I use first parse_as_infix("===",(12, "right"));; But I think that's only because === is already declared to be an infix. I don't know why you parenthesized ===, but it seems to be needed. I'll try to post working code soon. Can you explain why this works, when a and b don't have types? Or what it even means? To me, === is a 4-ary relation on set T. On to your other points: You could do it by replacing your concrete type point with a type variable. See type_of `MAP` for syntax. (In HOL4 and SML, you'd get (:'a->'b) -> 'a list -> 'b list, but I have this feeling that HOL Light does things a little differently.) Cool, I tried in HOL Light type_of `MAP`;; hol_type = `:(?134838->?134839)->(?134838)list->(?134839)list` I think that's a cryptic version of what you said, because the HOL html reference manual say map : ('a -> 'b) -> 'a list -> 'b list map f [x1;...;xn] returns [(f x1);...;(f xn)]. That's the map function I'm used to from Scheme. Strangely enough map has a different hol_type than MAP: type_of `map`;; val it : hol_type = `:?134840` I guess that's what polymorphism means: map works for any types a and b. I think I'm already using polymorphism in my Hilbert code, e.g.: let BiggerThanSingleton_THM = thm `; let p be A->bool; let x be A; assume x IN p [H1]; assume ~(p = {x}) [H2]; thus ? a . a IN p /\ ~(a = x) proof {x} SUBSET p by H1, SING_SUBSET; ~(p SUBSET {x}) by -, H2, SUBSET_ANTISYM; consider a such that a IN p /\ a NOTIN {x} [X1] by -, SUBSET, NOTIN; ~(a = x) by -, IN_SING, NOTIN; qed by -, X1`;; I don't know where I got the idea of using A as a type instead of 'a, or what 'a means, but to me, A stands for any type, and it works in my Hilbert code, A apparently being replaced by point. Here's another dumb question, for Freek maybe: It's been obvious to me for some time that much of sets.ml could be proved quite easily in miz3. But that's awkward if we can't load in such a file with miz3 stuff in it. Why doesn't use work for miz3 code, as in #use "hol.ml";; ? -- 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