Hello,
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)
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?
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?
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.
So my question is:
- How can I get to see the type variables of Gamma1?
- How can I instantiate them?
(preferably without mentioning their names, because their
names are somewhat random)
- Is there maybe some other variant of ASSUME_TAC that attempts to
match the type variables?
(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 )
Thanks,
Hans.
Example:
----------------------------------------------------
let natind, natrec = define_type "nat = Zero | Succ nat " ;;
(* Inductive type nat. *)
let plusdef = define ` plus =
\ (x:nat). ( @ ( a:nat -> nat ) . ( a Zero ) = x /\
! (n:nat). ( a ( Succ n )) = ( Succ ( a n )) ) ` ;;
(* definition of plus *)
g ` ! (x:nat) . ?a .
( ( a Zero ) = x /\
( ! (n:nat). a ( Succ n ) = ( Succ ( a n ) ) ) ) ` ;;
e ( X_GEN_TAC `x:nat` ) ;;
e ( ASSUME_TAC natrec ) ;;
let instantiation = ( BETA_RULE
( ISPECL [ `x:nat` ; ` \a:nat b:nat. ( Succ b ) ` ]
( ASSUME `!f0 f1. ?fn. fn Zero = f0 /\ (!a. fn (Succ a) = f1 a (fn a))` )
));;
e( ASSUME_TAC instantiation ) ;;
(* This application fails with Failure "VALID: Invalid tactic"
-------------------------------------------------------------------------
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
