Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, rahard@ee.umanitoba.ca
In-Reply-To: <9507081603.AA03789@wine> (rahard@ee.umanitoba.ca)
Subject: Re: [Q] manipulating assumptions
Message-Id: <95Jul9.215733met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Sun, 9 Jul 1995 21:57:33 +0200


> Question from a newbie: How do I manipulate assumptions? ... I was
> trying to prove: 

>  "!inp out.
>    (?p1 p2.
>      (p1 = T) /\
>      (~inp ==> (p1 = out)) /\
>      (inp ==> (p2 = out)) /\
>      (p2 = F)) ==>
>    (out = ~inp)"

Often the key to using assumptions is to never let them be assumptions,
since then one loses fine-grain control. The answer lies in a special
class of tactics called `theorem continuations'. These perform an
operation on the current goal and pass the result of that to another
function (often a tactic). In Budi's example, one would first do a
"REPEAT GEN_TAC" to get rid of the universals, leaving the goal

  (?p1 p2.
    (p1 = T) /\ (~inp ==> (p1 = out)) /\ (inp ==> (p2 = out)) /\ (p2 = F)) ==>
  (out = ~inp)

This is an implication with the antecedent being twice existentially
quantified. The following tactic reduces the problem to a tautology:

    DISCH_THEN (CHOOSE_THEN (CHOOSE_THEN MP_TAC))

This code admits a left-to-right reading: "grab the antecedent of the
goal, then give hypothetical witnesses for its two existentially
quantified variables, then bring the result back as the new
antecedent". The result is

    (p1 = T) /\ (~inp ==> (p1 = out)) /\ (inp ==> (p2 = out)) /\ (p2 = F) ==>
    (out = ~inp)

As I said, this is a tautology, but to continue in the same fine-grained
vein, we could get eliminate "p1" and "p2" with the following

    DISCH_THEN (fn th => let val [a,b,c,d] = CONJUNCTS th 
                         in MP_TAC(REWRITE_RULE[a,d] (CONJ b c)) end)

In effect, the assumption list is being explicitly maintained, with
forward inference operations on the assumptions being "bracketed" by
DISCH_THEN and MP_TAC. I don't recommend this style (which originated
with John Harrison) in all cases, but it can be quite useful in tight
spots.

There's a leisurely discussion of related approaches in Chapter 24 of
the HOL book.


Konrad.