Hi Bill
These are nice explanations, but here are a few comments and
corrections:
> ***** 1) the definitions of type bool and the constant =
*****
> ....
You're still using the terminology "definition" for 'bool'
and '=', whereas they are only *declared* in each of the HOL systems'
axiomatisations, and not *defined*. Declare is when you just introduce
an entity to the theory, define is when you declare something and
constrain it (beyond type constraints). The HOL Light command
'new_constant' declares a new constant, whereas 'new_definition' defines
a new constant.
> ***** 2) sequents, new_basic_definition and the HOL
Light inference rules
> ....
> Similar code is found in the 150 line
segment of the file thm.ml
> module Hol : Hol_thm_primitives = struct
>
[...]
> end;;
> but I won't discuss this. My guess is that the fusion.ml
definitions are
> used first for some basic theorem and then the thm.ml
definitions are used
> for more sophisticated or faster handling of
theorems.
Actually fusion.ml replaces type.ml, term.ml and thm.ml, but
these unused source code files are still hanging around in the HOL Light
source directory.
> So a theorem is of the form Sequent ([a1;...;an],
t), which we will write as
>
> {a1,...,an} |- t
>
> It will turn out
that t will always have HOL type bool.
And a1,..,an will also always
have HOL type bool.
> Sequent is an Ocaml constructor defined in the
module Hol. Thus we have no
> way to produce theorems except by
sequent-producing functions defined in
> Hol ...
The crucial point is
that OCaml type 'thm' is an abstract datatype, and so its only
constructors are those supplied in the module interface (which are the
sequent-producing functions defined in Hol).
> ...
> including
new_basic_definition,
> ...
>
> Another way to produce sequents is
with the Hol module function
> new_basic_type_definition.
>
> The only
other way to produce sequents is with 10 Hol module functions which
>
produce theorems from earlier theorems:
Actually, there is also
'new_axiom'.
> ...
> The term T is are defined to have type bool by
>
> let T_DEF = new_basic_definition
> `T = ((p:bool. p) = (p:bool.
p))`;;
>
> Note a subtlety about = here which I messed up in a previous
post. The
> first = is the Ocaml =, meaning that T_DEF is bound in Ocaml
to the value of
> the new_basic_definition expression. Each of the other
two =s is the
> constants = of type A->A->bool. Therefore the RHS
(p:bool. p) = (p:bool.
> p) has type bool, and therefore T has type
bool.
To use the correction terminology, we say "are instances of the
constant '=', which has generic type `:A->A->bool` ".
> I think the
parser treats prefixes in a special way, but I'm not sure what
> it
is.
Prefix operators bind differently from nonfix operators, and less
tightly, so that `~ ~ p` is the double negation of `p`, and `~ P x` is
the negation of `P x`. If '~' were nonfix, you'd need to supply extra
parentheses in these expressions.
Best,
Mark. ------------------------------------------------------------------------------
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
