Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 26 Sep 1995 12:15:14 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA013222339; Tue, 26 Sep 1995 04:45:39 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from bunsen.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA013192338; Tue, 26 Sep 1995 04:45:38 -0600 Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) by bunsen.cs.byu.edu (8.6.9/8.6.9) with ESMTP id EAA17933 for ; Tue, 26 Sep 1995 04:44:21 -0600 Received: from albatross.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 26 Sep 1995 11:44:21 +0100 X-Mailer: exmh version 1.6.1 5/23/95 To: John Harrison IB Cc: info-hol@cs.byu.edu, isabelle-users@cl.cam.ac.uk Subject: Re: At a Los for something to do? (II) X-Uri: X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. In-Reply-To: Your message of Mon, 25 Sep 1995 19:21:18 +0200. <199509251721.TAA13911@aton.abo.fi> Content-Transfer-Encoding: quoted-printable Date: Tue, 26 Sep 1995 11:44:15 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:144290:950926104427"@cl.cam.ac.uk> > val LOS =3D prove > (%`(!x y z. P x y /\ P y z =3D=3D> P x z) /\ > (!x y z. Q x y /\ Q y z =3D=3D> Q x z) /\ > (!x y. P x y =3D=3D> P y x) /\ > (!(x:'a) y. P x y \/ Q x y) > =3D=3D> (!x y. P x y) \/ (!x y. Q x y)`, > REWRITE_TAC[TAUT (%`(a =3D=3D> b) =3D ~a \/ b`)] THEN > CONV_TAC (REDEPTH_CONV (NOT_FORALL_CONV ORELSEC > NOT_EXISTS_CONV ORELSEC > GEN_REWRITE_CONV I empty_rewrites [DE_MORGAN_THM= ])) THEN > CONV_TAC (REDEPTH_CONV (RIGHT_OR_FORALL_CONV ORELSEC > LEFT_OR_FORALL_CONV)) THEN > CONV_TAC (REDEPTH_CONV (OR_EXISTS_CONV ORELSEC > REWR_CONV DISJ_ASSOC)) THEN > CONV_TAC (REDEPTH_CONV LEFT_OR_EXISTS_CONV) THEN > BERNAYS_SCHOENFINKEL_TAC THEN > CONV_TAC(EQT_INTRO o BDD_TAUT));; Why not prove it the easy way, using Isabelle/HOL? > by (safe_meson_tac 1); Level 1 (! x y z. P x y & P y z --> P x z) & (! x y z. Q x y & Q y z --> Q x z) & (! x y. P x y --> P y x) & (! x y. P x y | Q x y) --> (! x y. P x y) | (! x y. Q x y) No subgoals! Process time (incl GC): 4.3 secs Here is one in a similar vein: > by (safe_meson_tac 1); > Level 1 (! x y z. P x y --> P y z --> P x z) --> (! x y z. Q x y --> Q y z --> Q x z) --> (! x y. Q x y --> Q y x) --> (! x y. P x y | Q x y) --> (! x y. P x y) | (! x y. Q x y) No subgoals! Process time (incl GC): 3.8 secs safe_meson_tac works by the so-called MESON proof procedure, which is a = sequent formulation of Model Elimination. Larry =