Thanks, Michael, you're right, I don't want every lambda to be displayed as
{...}. But the main thing I learned from you is that there's no reason for me
to not rewrite the parts of sets.ml that I use (IN_SING etc) to use lambda
rather {...}, as the lambdas are actually equal to {...} defs. It looks nicer
to have the curly braces, but that's just looks, and for my readers, it will be
in just a few lines anyway. I'll try to work this rewrite-sets.ml exercise.
I came close enough to solving your {...} = lambda exercise, and I think it's
a miz3 problem that I didn't completely solve it. IN_INTER (which I used
successfully) and IN_ELIM_THM (which was partly successful) both use the HOL
Light functions GSPEC and SET_SPEC you suggested I use. I don't understand
them, but their definitions are simple:
let GSPEC = new_definition
`GSPEC (p:A->bool) = p`;;
let SETSPEC = new_definition
`SETSPEC v P t <=> P /\ (v = t)`;;
There's no reason for me to use these defs explicitly rather than IN_ELIM_THM,
which uses them, but this definition bewilders me:
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[]);;
I'd rather use BETA_THM instead, and I can do this by using lambda defs of
INTER, UNION etc instead of the {...} defs in sets.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
