Filter
Top Products
10.4. DEALING WITH ASSUMPTIONS 85
If one uses THEN to compress a proof into a single large tactic, then one might
as well dispense with the goal stack completely. One can simple get the theorem by
applying prove to the goal and the tactic, e.g.
let LTE_ADD2 = prove
(‘!m n p q. m < p /\ n <= q ==> m + n < p + q‘,
ONCE_REWRITE_TAC[ADD_SYM; CONJ_SYM] THEN
MATCH_ACCEPT_TAC LET_ADD2);;
10.4 Dealing with assumptions
Various tactics like DISCH TAC push parts of the goal onto the assumption list. You
can put any theorem there yourself using ASSUME TAC. The problem then arises of
identifying a particular assumption when it is needed. Often it is not necessary, but
when required there are several alternatives. One can design a tactic that will suc-
ceed only on the desired assumption, and use FIRST ASSUM. For example the tactic
SUBST1 TAC expects and equational theorem as an argument and substitutes in the
goal, so if there is only one equational assumption, FIRST ASSUM SUBST1 TAC will
use it. Alternatively, one can explicitly recreate the assumption as a theorem using
ASSUME. Finally, it is possible to label things when putting them on the assumptions
using LABEL TAC instead of ASSUME TAC. The appropriate assumption can then be
used with USE ASSUM.
10.5 Model elimination
Although proofs often need theory-specific reasoning tools, e.g. linear arithmetic,
quite a lot of small parts of proofs can be finished off by a prover for pure logic.
HOL Light provides a tactic MESON TAC that can dispose of a lot of simple first order
reasoning. It also has a limited ability to do higher order and equality reasoning.
This prover is based on the Prolog Technology Theorem Prover (Stickel 1988),
an implementation of model elimination (Loveland 1968). Such systems work by
reducing to clausal form and then further to a set of pseudo-Horn clauses that can
be used for Prolog-style backward search. The default search mode is one of our
own invention — see (Harrison 1996) for more details and a comparison with other
techniques. Here are a few examples of the HOL tactic in action:
#let LOS = prove
(‘(!x y z. P x y /\ P y z ==> P x z) /\
(!x y z. Q x y /\ Q y z ==> Q x z) /\
(!x y. P x y ==> P y x) /\
(!(x:A) y. P x y \/ Q x y)
==> (!x y. P x y) \/ (!x y. Q x y)‘,
MESON_TAC[]);;
LOS : thm =
|- (!x y z. P x y /\ P y z ==> P x z) /\
(!x y z. Q x y /\ Q y z ==> Q x z) /\
(!x y. P x y ==> P y x) /\
(!x y. P x y \/ Q x y)
==> (!x y. P x y) \/ (!x y. Q x y)
and
1
1
See message from Wishnu Prasetya to the info-hol mailing list on 18 October 1993, available
on the Web as http://lal.cs.byu.edu/lal/holdoc/info-hol/15xx/1515.html.