Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199507131224.AA132248278@bobcat.cs.byu.edu>
To: info-hol@cs.byu.edu
Subject: Holger Busch: Re: Conditionals
Date: Thu, 13 Jul 1995 06:24:38 -0600
From: Phil Windley <windley@cs.byu.edu>


Bob Eastham asked:
> How do I handle proofs which contain conditionals? For example, I am left
> with a subgoal:
>
> !t. out(SUC t) = inp t /\ inp(SUC t)
> --------------------------------------
> !t. out t = ((t=0) => F | (inp (t-SUC 0))) /\ inp t

> How do I finish this proof? A rewrite with the assumptions does not finish
> this.

Phil Windley answered:
>> This points out a larger question for the HOL community.  I suspect
>> that PVS would solve this straight up.  It certainly solved the last little
>> exercise we went through a few days ago straight away.  These sorts of
>> niggling little proofs are just too hard in HOL.

..
>> HOL {and LAMBDA} is just to hard for the non-expert to use and its time
>> we did something about it.

That's what led me to develop Rispe (reduced instruction set proof
environment) in LAMBDA. It is not only intended for the non-expert, but
also for the lazy expert who does not want to waste time on such basic
problems, which Rispe solves fully automatically. At the same time all
libraries of tactics, rules and LAMBDA proof functions are still
accessible. To me there does not appear to be a contradiction between
offering powerful and easy-to-use "catch all tactics" and keeping the 
architecture of HOL or LAMBDA open.

Regards,

   Holger