Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Mon, 6 Jun 94 18:10:15 +0200
From: Holger.Busch@zfe.siemens.de (Holger Busch)
Message-Id: <9406061610.AA26680@koetsier.zfe.siemens.de>
To: hol2000@leopard.cs.byu.edu
Subject: Re: An Alternate Subgoal Package

Mark Aagaard writes:

> I think, but I may be wrong about this, that Lambda begins a
> proof for hardware verification with (Spec |- Spec), which
> the user refines to (Imp |- Spec).  This seems to be similar
> to the style that Jim proposes.  
 
Yes, you typically start with such a trivial rule in LAMBDA,
which is gradually transformed into a theorem by applying 
rules or tactics

|- goal  (1)    |- subgoal1 ,  |- subgoal2  (2)
-------  ~~>    --------------------------  ~~> 
|- goal         |- goal

hyp1 |- subgoal1,  |- subgoal21,  |- subgoal22  (3)
----------------------------------------------  ~~> 
hyp1 |- goal

|- subgoal22  (4)
------------  ~~>  ------------
hyp1 |- goal       hyp1 |- goal

All intermediate rules are accessible by means of goal stack 
functions. Transformation (2) illustrates that hypotheses may be 
introduced on the fly. Transformation (3) illustrates that you
can simultaneously operate on parallel subgoals in one step.
Instantiations of variables occurring in several subgoals are 
propagated consistently.

Often you are not just interested in deriving a theorem,i.e., proving a 
goal, but in deriving a generic rule scheme with premises. Such a rule can be
used for transforming similar goals in just one step into a couple of
subgoals (which correspond to the unified premises of the applied rule)
instead of applying a tactic which internally applies several basic
proof steps.  

Of course you are not restricted to starting with a trivial rule, but
can push any rule of your database onto the goal stack and manipulate
it further.

   Holger Busch.