Thanks, Mark! My draft can use a lot of help from experts like you. I think I
decided that what I'm attempting is to describe, in the usual language of
mathematicians, the set of HOL Light sequents.
But I'm not sure your declare/define terminology is standard. The string
"declar" does not occur in the HOL4 manual LOGIC, and only occurs on p 102 in
the HOL Light tutorial in section 15.2 Recursive types.
The HOL Light command 'new_constant' declares a new constant,
whereas 'new_definition' defines a new constant.
The HOL Light on-line help says you're 3/4 right:
new_constant : string * hol_type -> unit
Declares a new constant.
new_definition : term -> thm
Declare a new constant and a definitional axiom.
I'm not saying you're wrong. Can you take it up with John and Konrad?
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.
Excellent!!! I see you're correct, because hol.ml never loads these files!
Nothing wrong with keeping old code around, might be some good ideas in there,
design choices that were made differently but the old ideas maybe still have
merit...
And [the assumptions] a1,..,an will also always have HOL type bool.
Correct! I'm having some trouble with the idea that with a sequent
A |- t
that A is a set of terms of type bool, rather than a list. Mathematically that
makes the most sense, and we're taking unions and differences...
[the] 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).
Thanks. That's what I was trying to get at, but my ignorance of modules
befuddled me. What's a good way for me to learn enough about Ocaml modules to
understand fusion.ml? I tried reading the Ocaml reference manual and got
stuck. I do see something like what you write in the code:
module type Hol_kernel =
[...]
type thm
module Hol : Hol_kernel = struct
[...]
type thm = Sequent of (term list * term)
Actually, there is also 'new_axiom'.
Thanks for the correction, and you're right:
let new_axiom tm =
if Pervasives.compare (type_of tm) bool_ty = 0 then
let th = Sequent([],tm) in
(the_axioms := th::(!the_axioms); th)
else failwith "new_axiom: Not a proposition"
But I wasn't going for completeness there, although I should have. I was
trying to understand why both =s here are HOL Light constants:
let T_DEF = new_basic_definition
`T = ((\p:bool. p) = (\p:bool. p))`;;
It was dumb of me, but I've always misread definitions like this as more like
let T = `((\p:bool. p) = (\p:bool. p))`;;
so the first = would be an Ocaml =. But the bool.ml code for TRUTH made it
clear to me that both =s are occurrences of the HOL Light constant =. So I was
doing through fusion.ml to see where I'd gone wrong.
To use the correction terminology, we say "are instances of the
constant '=', which has generic type `:A->A->bool` ".
That sounds better than my "the other two =s". I'm not sure that instance is
the right terminology, though.
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.
Excellent! And where is this explained, or how binders and infixes work? I
mean, I can see prefix, binders and infix stuff in parser.ml, but I can't
actually understand it.
--
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
