Hi Hans,
| my name is Hans de Nivelle, I am organizing a seminar on formal
| verification. We are currently trying to understand the HOL-system.
| (Hol-light, version 2.20)
Good luck with that! Understanding a big theorem prover is quite an
undertaking, though I like to think that HOL Light is as easy as it
currently gets.
| We have the following questions. (If the answers can be found somewhere in
| the literature, then I'm sorry for that)
No problem. I think many of the things you ask are not very clearly
documented. Or at least, you have to know exactly where to look. The
best way is sometimes just to skim through the code in the build
order (see "hol.ml"), just to get a feel for how the system constructs
things from first principles.
| 1. What are the 10 primitive inference rules?
| We now have collected INST, INST_TYPE, ASSUME t, TRANS, REFL t,
| but there must be 5 more.
| (There must be also one that lambda-abstracts equations)
Indeed, the one that lambda-abstracts equations is called ABS. You
can find the complete list in the file "thm.ml" (in version 2.20)
together with their definitions:
val REFL : term -> thm
val TRANS : thm -> thm -> thm
val MK_COMB : thm * thm -> thm
val ABS : term -> thm -> thm
val BETA : term -> thm
val ASSUME : term -> thm
val EQ_MP : thm -> thm -> thm
val DEDUCT_ANTISYM_RULE : thm -> thm -> thm
val INST_TYPE : (hol_type * hol_type) list -> thm -> thm
val INST : (term * term) list -> thm -> thm
The reference manual and help system will tell you more about each one
once you know the name.
| 2. In which way is an arbitrary formula f related to the equation
| f <=> T.
| Is f an abbreviation for f <=> T, or is f <=> T an axiom?
No, "f" isn't an abbreviation for "f <=> T", although I did once think
of setting things up this way, so that everything would be an
equation. They are really distinct formulas, but their equivalence is
deducible just from the definition of "T". Like all the other logical
connectives, "T" is a defined construct; the definition is in the file
"bool.ml":
let T_DEF = new_basic_definition
`T = ((\p:bool. p) = (\p:bool. p))`;;
Via a somewhat contorted but not very long sequence of primtive rules,
you can deduce the equivalence of f <=> T and f. In fact, the rules
EQT_ELIM and EQT_INTRO directly below the definition in "bool.ml" swap
a theorem's conclusion from one form to the other.
| 3. Concerning pairs and ordinary application terms.
| Is one defined in terms of the other?
|
| Are pairs (t1,t2) defined as (( , t1 ) t2 ) or are they primitive?
The former. Pairs are defined exactly as you indicated; "," is just
another infix operator (defined in "pair.ml"). This is even hinted at
in the concrete syntax, where the parentheses round a pair are
optional (as indeed they are in OCaml).
| 4. ASSUME_TAC seems to dislike hidden type variables.
| In the following example, I try to apply ASSUME_TAC Gamma1 |- t on a goal
| Gamma2 |- u, and want to obtain Gamma2, t |- u.
Before I dive into the details of your question, I'll try to just make
the definition you want in a different way; see below. But indeed,
there are sometimes subtleties with type variables in goals.
| let natind, natrec = define_type "nat = Zero | Succ nat " ;;
| (* Inductive type nat. *)
Given this definition you can make the definition you want more
directly with exactly the clauses you seek thanks to "define":
let plusdef = define
`plus x Zero = x /\
!n. plus x (Succ n) = Succ(plus x n)`;;
You can also derive the existence theorem as follows:
(GEN `x:nat` o prove_general_recursive_function_exists)
`?a .
( ( a Zero ) = x /\
( ! (n:nat). a ( Succ n ) = ( Succ ( a n ) ) ) ) ` ;;
Of course, you may already know this and be more interested in the
subtleties of types than the actual definition --- let me know if
so and I can go into detail on your earlier query.
I should also add that these one-line proofs depend on some
infrastructure like "define" that is developed quite late. In the
actual build of the system, the natural numbers are defined and the
recursive definitions made in a somewhat more low-level way rather as
you are doing in your question (see the files "num.ml" and
"arith.ml").
John.
-------------------------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems? Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
