On 5/08/12 8:49 PM, Bill Richter wrote:
> parse_as_infix("cong",(12, "right"));;
> let cong_DEF = new_definition `a,b,c cong x,y,z <=> a,b === x,y /\
> a,c === x,z /\ b,c === y,z`;;
> My problem, I think, is that cong is now a function of ===, which is
> now a variable being passed around. Here's my miz3 code below, which
> I really enjoyed writing, as it took quite a bit of fiddling to get
> right.
Yes, cong needs to take === as a parameter, which probably then means
that you can't have cong as an infix.
You'd have to define
cong R (a,b,c) (x,y,z) <=>
R (a,b) (x,y) /\ R (a,c) (x,z) /\ R (b,c) (y,z)
(where I've replaced === with R just to make everything clearly a variable)
I know how I'd hack the now-parameterised cong into behaving like an
infix thing in HOL4, but I'm not sure how to do it in HOL Light. You're
definitely butting up against the limits of what is friendly. (Of
course, you'd like to either have a particular === as an understood
parameter, or to be able to write
(a,b,c) cong_{===} (x,y,z)
or both.
> I'm a bit puzzled here because in the statement of A4, I wrote let
> === be 'a#'a->'a#'a->bool; let Between be 'a#'a#'a->bool; To me, that
> means that all 7 arguments of === and Between have the same type, the
> unspecified type 'a, but you can't see that in val A4 above. I had
> the impression that HOL Light printed out less information in the
> theorem statements than I'd put in because of its clever
> type-inference scheme, but this looks like taking it too far. Maybe
> I don't know what 'a means.
In SML and HOL4, 'a is a type variable, not an actual type. However,
having seen your other scripts, I'm reminded that convention (at least)
allows HOL Light to use capital letters as type variables. Thus you
earlier wrote
let v be A ..
That capital A is the HOL Light idiom for writing 'a, so you should
stick with it and write
let Between be A#A#A->bool ...
and avoid the 'a.
I'm sorry
type_of `MAP`
was so unilluminating. Note that you also earlier confused "map", an
OCaml function and `MAP`, the logical constant within HOL. When you
wrote `map` into the HOL Light interactive loop, it parsed it as a
polymorphic variable because there is no such constant in HOL Light.
(HOL4 shares the common ancestry here; we also have MAP in the logic and
map in the ML system.)
Best,
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
