Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <24946-0@swan.cl.cam.ac.uk>; Mon, 27 Jul 1992 16:37:45 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19008; Mon, 27 Jul 92 08:26:32 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA19003; Mon, 27 Jul 92 08:26:26 -0700 Received: from dunlin.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <23728-0@swan.cl.cam.ac.uk>; Mon, 27 Jul 1992 15:53:52 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Re: How to prove this shortly? Date: Mon, 27 Jul 92 15:53:47 +0100 From: Lawrence Paulson Message-Id: <"swan.cl.ca.730:27.06.92.14.53.54"@cl.cam.ac.uk> I prefer the following one-step proof. Of course, you have to use Isabelle :-) > goal HOL_Rule.thy "! P Q R St. (! x. P(x) --> Q(x)) & (! s. Q(s) --> St(R,s)) --> \ \ (! s. P(s) --> St(R,s))"; Level 0 ! P Q R St. (! x. P(x) --> Q(x)) & (! s. Q(s) --> St(R,s)) --> (! s. P(s) --> St(R,s)) 1. ! P Q R St. (! x. P(x) --> Q(x)) & (! s. Q(s) --> St(R,s)) --> (! s. P(s) --> St(R,s)) > by (fast_tac HOL_cs 1); Level 1 ! P Q R St. (! x. P(x) --> Q(x)) & (! s. Q(s) --> St(R,s)) --> (! s. P(s) --> St(R,s)) No subgoals! Process time (incl GC): 0.7 secs Larry Paulson