Tony Johnson wrote:
> I'm trying to make a Cartesian product like this
> (--`X x Y = {(x,y) | x IN X /\ y IN Y}`--);
> How would I make this work?
(This is a HOL4 answer.)
This constant is already defined in pred_setTheory as CROSS. It's an
infix, so the theorem looks like
|- !P Q. P CROSS Q = {p | FST p IN P /\ SND p IN Q}
(See
http://hol.sourceforge.net/kananaskis-4-helpdocs/help/src/htmlsigs/pred_setTheory.html#CROSS_DEF-val)
If you wanted to see CROSS as "x", you could
set_fixity "x" (Infixl 500);
overload_on ("x", ``(CROSS)``);
You would then see the derived theorem IN_CROSS as
|- !P Q $x. $x IN P x Q = FST $x IN P /\ SND $x IN Q : thm
This demonstrates the problem with attempting to have x as a constant;
it's used all over the place as a variable. The pretty-printer uses
the $ to "escape" it when it doesn't appear as a constant, but you
would still have trouble using even $x as a variable when handing
things to the parser:
- ``$x + 3``
Type inference failure: unable to infer a type for the application of
$+ :num -> num -> num
at line 7, character 3
to
($x :('a -> bool) -> ('b -> bool) -> 'a # 'b -> bool) :('a -> bool)
-> ('b -> bool) -> 'a # 'b -> bool
You can manage it if the occurrence is bound:
- ``\$x. $x + 3``;
> val it = ``\$x. $x + 3`` : term
- type_of it;
> val it = ``:num -> num`` : hol_type
but it still all looks pretty disgusting.
This sort of problem would prevent your attempted definition, which
has x on the left and the right hand side.
Overloading "*" to ``(CROSS)`` works a lot better.
That is,
overload_on ("*", ``(CROSS)``)
(I'm using the (constant) syntax rather than $constant syntax, but
both work.)
Michael.
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
