Rob, I think the answer to your interesting question involves more complicated
set abstractions like {y + 6 | y < 0}. I think here we see the merit of the
HOL Light invisible variables, as this simple proof shows:
g `EMPTY = {y + 6 | y < 0}`;;
e(REWRITE_TAC[SETSPEC; GSPEC]);;
e(REWRITE_TAC[LT; EMPTY]);;
`{} = (\GEN%PVAR%459. ?y. y < 0 /\ GEN%PVAR%459 = y + 6)`
# val it : goalstack = No subgoals
Let's replace the computer-generated invisible variable GEN%PVAR%451 with a for
clarity:
`{} = (\a. ?y. y < 0 /\ a = y + 6)`
I think that's correct, because I think the meaning of
{y + 6 | y < 0}
is
{a | ?y. y < 0 /\ a = y + 6}
so HOL Light should generate an invisible variable automatically for {y + 6 | y
< 0}.
BTW Michael Norish's response a year ago is quite relevant:
http://article.gmane.org/gmane.comp.mathematics.hol/2118
Sorry it took me so long to respond, and I still don't understand parser.ml
well enough, but I bet Michael does.
RDA> This is idle curiosity on my part about HOL Light: why are the
RDA> constants that support set comprehensions defined in such a way
RDA> that the parser has to generate an invisible bound variable?
RDA> This results in surprising behaviour like:
RDA> # `{x | x > 9}` = `{x | x > 9}`;;
RDA> val it : bool = false
First, the constants SETSPEC and GSPEC are defined in sets.ml in a way that
involves no invisible bound variables:
let GSPEC = new_definition
`GSPEC (p:A->bool) = p`;;
let SETSPEC = new_definition
`SETSPEC v P t <=> P /\ (v = t)`;;
I bet Michael understands these definitions. So the invisible bound variables
that you and Michael's post refer to must come from the HOL Light parser making
sense of the curly braces, and I think that involves these lines of parser.ml:
|| a (Resword "{") ++
let pgenvar =
let gcounter = ref 0 in
fun () -> let count = !gcounter in
(gcounter := count + 1;
Varp("GEN%PVAR%"^(string_of_int count),dpty)) in
let pmk_setcompr (fabs,bvs,babs) =
let v = pgenvar() in
let bod = itlist (curry pmk_exists) bvs
(Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in
Combp(Varp("GSPEC",dpty),Absp(v,bod)) in
So HOL Light must use parser.ml to turn a set abstraction
{ ... | ... }
into a combination involving GSPEC, SETSPEC and your invisible variables.
Here's evidence:
g `EMPTY = {y | y < 0}`;;
e(REWRITE_TAC[SETSPEC; GSPEC]);;
`{} = (\GEN%PVAR%450. ?y. y < 0 /\ GEN%PVAR%450 = y)`
Let's rewrite the lambda abstraction for clarity as, changing GEN%PVAR%450 to a:
(\a. ?y. y < 0 /\ a = y)
Maybe your point is that HOL Light should instead use this simpler lambda
abstraction
(\y. y < 0)
There you'd be making a really good point, but with more complicated set
abstraction above, I think we see the value of invisible variables.
BTW note that my simple proof above did not use IN_ELIM_THM, and I got away
with that because IN_ELIM_THM has a large intersection with
REWRITE_TAC[SETSPEC; GSPEC].
--
Best,
Bill
------------------------------------------------------------------------------
Sponsored by Intel(R) XDK
Develop, test and display web and hybrid apps with a single code base.
Download it for free now!
http://pubads.g.doubleclick.net/gampad/clk?id=111408631&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
