Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <00832-0@swan.cl.cam.ac.uk>; Wed, 5 Aug 1992 08:19:42 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17524;
          Wed, 5 Aug 92 00:04:18 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA17519;
          Wed, 5 Aug 92 00:04:10 -0700
Message-Id: <9208050704.AA17519@ted.cs.uidaho.edu>
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <10411-0@iraun1.ira.uka.de>; Wed, 5 Aug 1992 09:02:48 +0200
To: wishnu@nl.ruu.cs
Subject: Reply to How to prove this shortly?
Cc: info-hol@edu.uidaho.cs.ted
Date: Wed, 5 Aug 92 9:01:18 MET DST
From: kumar@de.uka.ira

Hi!
I just saw your mail regarding a short proof of 

	"!P:*->bool. !Q R (St:(*->bool)->(*->bool)).
    	(!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)"

I called FAUST and here are the results:

***************************************************************************************
          _  _    __    _      __    __
   |___   |__|   |  |   |     |__|  |__|
   |      |  |   |__|   |__   |__|  |__|
   
          Version 2.0, built on 14/10/91



File hol-init loaded
() : void

#let g = ([],"!P:*->bool. !Q R (St:(*->bool)->(*->bool)).
    (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)"#);;
g = 
([],
 "!P Q R St.
   (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)")
: (* list # term)

#loadf `publicprover`;;
...........................................() : void

#loadf `fwd_prover`;;
....................................() : void

#set_goal g;;
"!P Q R St.
  (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)"

() : void

#timer true;;
false : bool
Run time: 0.0s

#e (DEPTH_FAUST_TAC);;
OK..
goal proved
|- !P Q R St.
    (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)

Previous subproof:
goal proved
() : void
Run time: 0.4s
Intermediate theorems generated: 2

#set_goal g;;
"!P Q R St.
  (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)"

() : void
Run time: 0.1s

#e (FAUST_TAC);;
OK..
goal proved
|- !P Q R St.
    (!x. P x ==> Q x) /\ (!s. Q s ==> St R s) ==> (!s. P s ==> St R s)

Previous subproof:
goal proved
() : void
Run time: 1.2s
Intermediate theorems generated: 542

********************************************************************************

So it is not only in Isabelle that one can use a single tactic but also in HOL.
The application of DEPTH_FAUST_TAC uses "mk_thm" and the FAUST_TAC
generates a HOL proof.

It is worthwhile to try out FAUST once in a while especially when the
goals are small!


*******************************************************************************
Ramayya Kumar				          | email: kumar@ira.uka.de 
Institut fuer Rechnerentwurf und Fehlertoleranz,  | Tel.: +49 (721) 608 4354
Fakultaet fuer Informatik, Universitaet Karlsruhe,| Fax: +49 (721) 370455
P.O. Box 6980, W-7500 Karlsruhe 1, 		  |
Germany					          |