Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Tue, 10 Mar 92 11:07:52 +0100
From: vdvoort@nl.utwente.cs (Mark van de Voort)
Message-Id: <9203101007.AA05437@perseus.cs.utwente.nl>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: Theorem continuation functions
In-Reply-To: Mail from 'info-hol-request@ted.cs.uidaho.edu' dated: Mon, 09 Mar 92 23:13:04 PST

Ching Tsun writes

|> I like to use theorem continuation functions to "capture" assumptions.
|> For instance, suppose I want to prove "A ==> B" for some terms A and B.
|> Instead of using DISCH_TAC to add A to the set of assumptions and then
|> worrying about how to get to A again, I would write something like:

|> (*)     DISCH_THEN (\asm. rest_of_the_proof)

|>Is there a better way?


I use a similar technique but instead of relying on the
theorem continuation to provide the theorem I explicitly
give it.

So my code would be:

  let asm = (ASSUME ....)
  in
  DISCH_TAC THEN rest_of_the_proof

During testing I use cut and paste to turn all the so introduced
locals into globals.
This way I can test small pieces of code without having to rerun
the whole proof.

I hope this is useful  to you,

Mark.