The constant = is not defined in HOL Light, but simply declared (as Mark
said). In fact, equality is even more basic than that: it's a built in
term. You can see, for example, the "safe_mk_eq" function in fusion.ml, and
also the "the_term_constants" reference (which starts with "=" built in).
I feel like I must add my bit to this interesting discussion: I've recently
extended a formalisation due to John Harrison of (simplified) HOL in HOL
(which you can find in the Model/ subdirectory of HOL Light) with support
for defined types and constants and new axioms etc. (which brings it up to
"full" HOL), with much help from Rob Arthan. It may be elucidating to read
through some of this formalisation. You can find it here:
https://github.com/xrchz/vml/tree/c3fd5a3c2f797444d242299155290964c3cc793e/hol-light/stateful
By the way, I also second Mark's advice to read the HOL Zero source code,
which is very well commented.
On Fri, Mar 21, 2014 at 4:28 PM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> Thanks for correcting me, Mark! I'll look at your HOL Zero source code,
> especially corethy.ml. I see my error now. From bool.ml:
>
> let T_DEF = new_basic_definition
> `T = ((\p:bool. p) = (\p:bool. p))`;;
>
> The first = is an Ocaml =, but the 2nd =, the one we care about, is the
> primitive HOL Light constant =.
>
> The above is defining the constant 'T'. The constant '=' does not
> have a definition in HOL Light, or in any of the HOL
> axiomatisations. We have to start somewhere with entities that
> don't have definitions but are just declared. In HOL Light's
> axiomatisation, the only such entities are the 'bool' and 'fun'
> type constants and the '=' constant (the other axiomatisations also
> have the '==>' and '?' constants). In the logic, the meaning of
> such entities is not captured in definitions, but instead "drops
> out" from the aggregation of the axioms and primitive inference
> rules.
>
> Thanks, that's a good explaination. BTW where is the constant = defined
> in HOL Light? I see now that the line in bool.ml
> override_interface ("<=>",`(=):bool->bool->bool`);;
> just means that <=> is being defined as a synonym for = in this special
> case. In general = has type A->A-bool.
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> Learn Graph Databases - Download FREE O'Reilly Book
> "Graph Databases" is the definitive new guide to graph databases and their
> applications. Written by three acclaimed leaders in the field,
> this first edition is now available. Download your free book today!
> http://p.sf.net/sfu/13534_NeoTech
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
