On 7 Dec 2013, at 07:19, Bill Richter <[email protected]> wrote:
> 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:
>
> …
> 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}.
>
>
Sure, but my surprise is tthat the quantification isn't hidden inside a
definition like it is in HOL4.
HOL4 defines a constant GSPEC : ('a -> 'b # bool) -> 'b -> bool with
(essentially) the following defining
property:
GSPEC f v = ?x. f x = (v, T)
and then the parser translates {y + 6 | y < 0} into GSPEC(\y.(y + 6, y < 0)).
In HOL Light there is a
constant called GSPEC, but it is just the identify function, 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.
This seems
inside out to me.
Regards,
Rob.
\
> 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
>
------------------------------------------------------------------------------
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
