Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 12 Jul 1995 22:12:08 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA082169476;
          Wed, 12 Jul 1995 11:17:56 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA082119447;
          Wed, 12 Jul 1995 11:17:27 -0600
Received: from ira.uka.de (actually i80s16) by irafs1 with SMTP (PP);
          Wed, 12 Jul 1995 19:18:13 +0200
X-Mailer: exmh version 1.5.3 12/28/94
To: Robert Eastham <reastham@valhalla.cs.wright.edu>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: Conditionals
In-Reply-To: Your message of "Wed, 12 Jul 1995 12:10:26 EDT." <199507121610.MAA21436@violin.cs.wright.edu>
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Wed, 12 Jul 1995 19:15:40 +0200
From: reetz <reetz@ira.uka.de>
Message-Id: <"irafs1.ira.687:12.07.95.17.18.16"@ira.uka.de>

> 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.
> 
> Bob Eastham
> reastham@valhalla.cs.wright.edu
> 

For proving with conditionals, you may like to the library "cond",
which comes with the contrib directory of HOL90.7 (or you may get
it via WWW by: http://goethe.ira.uka.de/hvg/software.html) and
just do

RULE_ASSUME_TAC cond.COND_bool_RULE;

There are a bunch of other ways. E.g. you may like to prove a theorem
val th = |- !P (A:'a).(P => F | A) = ~P /\ A
an then use

RULE_ASSUME_TAC (PURE_ONCE_REWRITE_RULE [th]);

Surely there may be even much more elegant ways...

Ralf.


(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  University of Karlsruhe                                        *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany              *)
(*                                                                 *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html       *)
(*  fax:    +49 721 370455                                         *)
(*  tel:    +49 721 6083771                                        *)
(*                                                                 *)
(*******************************************************************)