Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: marco@mirtillo.usr.dsi.unimi.it (Marco Benini)
Message-Id: <9507180210.AA00696@ mirtillo.usr.dsi.unimi.it >
Subject: easy HOL?
To: info-hol@leopard.cs.byu.edu
Date: Mon, 17 Jul 1995 19:10:39 -0700 (PDT)
Content-Type: text
Content-Length: 2380

While I.m not a master in the use of HOL, one of the most
difficult things I found when I was learning how to develop
a proof was assumptions management.

Theorem continuations, I think, are far too difficult to
understand  when you are a beginner.

So I developed a couple of tactics which are easier to use,
although they are very inefficent, and inelegant. The key
idea is that who uses HOL knows natural deduction.

A natural way to develop a proof using natural deduction is
to reason backward, i.e. try to reduce the goal formula to
assumptions, or to reason backward, deducing something
useful from assumptions.

The first case is easy implemented in HOL by means of tactics,
while the second one is difficult, because we have no instruments
to manipulate directly assumpitions.

We have the RULE_ASSUM_TAC which applies a gicen inference
rule to all assumptions, but sometimes, a novice want to
apply an inference rule to only one assumption.

The way to do this is easy: undischarge every assumption you don't
need, and then apply the RULE_ASSUM_TAC properly, then, when
you get the result, do a REPEAT STRIP_TAC to discharge what you
can (usually the previously undischarged assumptions).

The tactics to do this in a more user friendly way are:

let assum n = (el n (fst(top_goal ())));;

let UNDISCH_BUT_TAC n = letref x = length (fst(top_goal ()))
                        and t = ALL_TAC
                        in while x > 0 do
                             t, x := (x = n => t THEN ALL_TAC |
                                               t THEN (UNDISCH_TAC (assum x))),
                                     x - 1
                        ; t;;

let UNDISCH_N_TAC n = UNDISCH_TAC (assum n);;

I know, these things are trivial, and the result is very
inelegant, but for a novice user these can be very useful
to carry out his first proofs.

I hope this small contrib helps someone.

	Marco

-----------------------------------------------------------
Marco Benini			marco@mora.usr.dsi.unimi.it
   Departement of Computer Science - University of Milan
           Computational Architectures Laboratory
tel. 0039-02-55006344		      fax. 0039-02-55006348
-----------------------------------------------------------

"But did thee feel the earth move?"
For Whom the Bell Tolls (1940), ch.13, ERNEST HEMINGWAY

GCS/M d-- -p+ c++ l+ u+ e--- m++ s/- !n h* f+ g+ w+ t r+ y+