Filter
Top Products
6.3. THEOREMS 61
implication p ==> q, dest conj breaks apart a conjunction p /\ q, and is_disj
tests if a term is a disjunction p \/ q.
6.3 Theorems
HOL theorems can be taken apart into a list of assumptions and a conclusion
using the function dest_thm :thm -> term list * term. The hypotheses and
conclusion can be grabbed separately using hyp and concl. However they can only
be created by using one of the primitive rules, making a term or type definition,
or finally asserting an axiom. The last of these is only done three times for the
basic mathematical axioms, and thereafter HOL users are discouraged from adding
new axioms, as this does not maintain the guarantee of consistency. The primitive
inference rules were listed earlier, and their CAML realizations are simply CAML
functions returning something of type thm. For example:
#BETA ‘(\p. ~p) p‘;;
it : thm = |- (\p. ~p) p = ~p
#INST [‘q:bool‘,‘p:bool‘] it;;
it : thm = |- (\p. ~p) q = ~q
#TRANS (ASSUME ‘p:bool = q‘) (ASSUME ‘q:bool = r‘);;
it : thm = p = q, q = r |- p = r
#dest_thm it;;
it : term list * term = [‘p = q‘; ‘q = r‘], ‘p = r‘
New definitions are made using the function new definition, which takes an
equational term ‘c = t’, where c is a variable. The system introduces a new con-
stant called c and returns the theorem |- c = t for the new constant. For example:
#new_definition ‘true = T‘;;
it : thm = |- true = T
Later on, more convenient derived definitional principles are built on top of this
— even new definition is bound to a more powerful derived function that can, for
example, accept function definitions in the form ‘f x1 ... xn = ...’.
The primitive function for performing type definitions is new_basic_type_definition.
The user gives the desired name for the new type and for the bijections that map
between the old and new types, and finally a theorem asserting that the chosen
subset of the existing type contains some object. For example, we can define a new
type single in bijection with the 1-element subset of bool containing just T. The
appropriate predicate is the function that asks of its argument x whether it is equal
to t, i.e. \x. x = T:
#let th1 = BETA_CONV ‘(\x. x = T) T‘;;
th1 : thm = |- (\x. x = T) T = T = T
#let th2 = EQ_MP (SYM th1) (REFL ‘T‘);;
th2 : thm = |- (\x. x = T) T
#new_basic_type_definition "single" ("mk_single","abs_single") th2;;
it : thm * thm =
|- mk_single (abs_single a) = a,
|- (\x. x = T) r = abs_single (mk_single r) = r
Two theorems are returned as an ML pair, which together imply that the chosen
bijections map 1-1 between the new type and the chosen subset of the old one.