On 7 Dec 2013, at 07:19, Bill Richter <rich...@math.northwestern.edu> 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info