Thanks, Rob! Can you explain how HOL4 performs the quantification with GSPEC?
I would think that GSPEC would have to choose a fresh variable, and I've never
understood how that's to be done, because you have know that your new fresh
variable hasn't already been chosen. So I would think that the HOL Light
method of having the parser choose the fresh variable was defensible.
GSPEC : ('a -> 'b # bool) -> 'b -> bool with (essentially) the
following defining property:
GSPEC f v = ?x. f x = (v, T)
So it's GSPEC that chooses the fresh variable, because we need x to not be free
in v, right?
and then the parser translates {y + 6 | y < 0} into GSPEC(\y.(y + 6, y <
0)).
How does GSPEC know to use the same variable y?
In HOL Light there is a constant called GSPEC, but it is just the
identify function,
Thanks! I had wondered about the sets.ml definition:
let GSPEC = new_definition
`GSPEC (p:A->bool) = p`;;
the semantics of the set comprehension are given by something
called SETSPEC, which has to appear in a context where a variable
representing a candidate for membership of the set comprehension is
in scope.
Could you clarify? Here's the sets.ml definition, which I would like to
understand:
let SETSPEC = new_definition
`SETSPEC v P t <=> P /\ (v = t)`;;
As I posted before, SETSPEC is used by parser.ml to create set abstractions
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))
and I'd really like to understand this, as well as everything else in parser.ml.
Perhaps I can elaborate. My RichterHilbertAxiomGeometry/readable.ml does I
think a nice job of allowing readable HOL Light proofs, with a minimum of type
annotations, double-quotes and back-quotes. Basically it's a version of
Freek's miz3 that allows full use of tactics like REWRITE_TAC. I'm pretty
happy with it, but I wonder if I couldn't substitute some straightforward camlp
parsing for the exec I'm borrowing from update_database.ml. So my first task
is the understand parser.ml.
--
Best,
Bill
------------------------------------------------------------------------------
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
