Hans de Nivelle wrote:
> 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) We have the following questions. (If the
> answers can be found somewhere in the literature, then I'm sorry for
> that)
> 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)
There are also MK_COMB, ABS, BETA, EQ_MP and DEDUCT_ANTISYM_RULE. See
the top of thm.ml in the HOL Light sources.
> 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?
Neither. There is a derived rule (EQT_INTRO) which turns any theorem
|- f
into
|- f = T
and it is also possible to prove the rewrite |- f = (f = T)
> 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. The , operator is itself defined in terms of the
representation of pairs as functions.
> 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.
> I suspect that the reason of the failure is the fact that
> ASSUME_TAC requires that Gamma1 is an exact subset of Gamma2,
> which is not the case due to hidden type variables.
This would be the cause of an invalid tactic error, yes.
> (In the example, I try to prove existence of a usual addition
> operator from the recursion definition of a type Nat that I
> defined by myself )
If you want to instantiate the recursion principle by hand, your
example was only really missing a call to INST_TYPE. For simple stuff
like this, you can do it all without having to invoke the goal
package.
In HOL4 syntax, the invocation required to get the theorem you were
after is
Hol_datatype `nat = Zero | Succ of nat`
(GEN ``x:nat`` o BETA_RULE o
SPECL [``x:nat``, ``\a:nat n. Succ n``] o
INST_TYPE [``:'a`` |-> ``:nat``])
(TypeBase.axiom_of ``:nat``)
where (TypeBase.axiom_of ``:nat``) gives you back the equivalent of
natrec in your example. (The other functions, GEN, BETA_RULE, SPECL
and INST_TYPE, are in HOL Light and HOL4 both.) In both systems you
can define recursive functions such as add in a more user-friendly
way. For example, in HOL4, you would write
Define`(add x 0 = x) /\ (add x (Succ n) = Succ (add x n))`
this automatically does the sort of instantiation I did by hand above.
Finally, to show type variables in HOL4, one can set the reference
variable show_types to true. I imagine there is something similar in
HOL Light.
Michael.
-------------------------------------------------------------------------
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
