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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
