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; Mon, 18 Oct 1993 18:05:08 +0100
Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA19454;
          Mon, 18 Oct 93 10:51:56 -0600
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.4/16.2) id AA19450; Mon, 18 Oct 93 10:51:54 -0600
Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA23711; Mon, 18 Oct 93 09:51:45 -0700
Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk;
          Mon, 18 Oct 93 17:49:26 BST
From: David Shepherd <des@inmos.co.uk>
Message-Id: <2832.9310181648@frogland.inmos.co.uk>
Subject: Re: how to get FAUST?
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Mon, 18 Oct 1993 17:48:43 +0100 (BST)
In-Reply-To: <199310181521.AA24160@infix.cs.ruu.nl> from "Wishnu Prasetya" at Oct 18, 93 04:21:38 pm
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 2129

Wishnu Prasetya has said:
> (1) Can anyone tell me how to get a copy of FAUST?

I think its ftp-able from

	goethe.ira.uka.de

> (2) How fast FAUST can prove the following:
> 
>       "(?!x. x=f(g x)) = (?!y. y=g(f y))"

It can't prove that as
i) that looks like a HOL88 term ... I think FAUST is only in hol90
ii) in any case I don't think that FAUST will solve that goal. As an
experiment I tried it on it and after hol90 had increased heap
to 100Mb I interrupted it

BTW it took me just under 10 minutes to prove by hand

prove(--`(?!(x:'a). x=f(g x)) = (?!(y:'b). y=g(f y))`--,
	  CONV_TAC(ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV)
	  THEN EQ_TAC
	  THENL 
	  [
	    STRIP_TAC
	    THEN CONJ_TAC
	    THENL 
	    [
	      EXISTS_TAC(--`(g:'a->'b)x`--)
	      THEN ONCE_REWRITE_TAC[(SYM o ASSUME)(--`x = f ((g:'a->'b) x)`--)]
	      THEN REFL_TAC
	     ,
	      REPEAT STRIP_TAC
	      THEN EVERY_ASSUM(ASSUME_TAC o (fn th => AP_TERM(--`f:'b->'a`--) th handle _ => th))
	      THEN RES_TAC
	      THEN ASSUME_TAC((AP_TERM(--`g:'a->'b`--) o ASSUME)(--`(f:'b->'a) y = f y'`--))
	      THEN POP_ASSUM(ACCEPT_TAC
			     o REWRITE_RULE[(SYM o ASSUME)(--`y = (g:'a->'b) (f y)`--),
					    (SYM o ASSUME)(--`y' = (g:'a->'b) (f y')`--)])
	      ]
	    ,
	    STRIP_TAC
	    THEN CONJ_TAC
	    THENL 
	    [
	      EXISTS_TAC(--`(f:'b->'a)y`--)
	      THEN ONCE_REWRITE_TAC[(SYM o ASSUME)(--`y = g ((f:'b->'a) y)`--)]
	      THEN REFL_TAC
	     ,
	      REPEAT STRIP_TAC
	      THEN EVERY_ASSUM(ASSUME_TAC o (fn th => AP_TERM(--`g:'a->'b`--) th handle _ => th))
	      THEN RES_TAC
	      THEN ASSUME_TAC((AP_TERM(--`f:'b->'a`--) o ASSUME)(--`(g:'a->'b) x = g x'`--))
	      THEN POP_ASSUM(ACCEPT_TAC
			     o REWRITE_RULE[(SYM o ASSUME)(--`x = (f:'b->'a) (g x)`--),
					    (SYM o ASSUME)(--`x' = (f:'b->'a) (g x')`--)])
	      ]
	    ]);





--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
            inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
            Latest football score: Real Madrid:1, Surreal Madrid:lemon