Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 18 May 1993 08:45:28 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26730;
          Tue, 18 May 93 00:28:11 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de 
          by ted.cs.uidaho.edu (16.6/1.34) id AA26725;
          Tue, 18 May 93 00:27:57 -0700
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57710>;
          Tue, 18 May 1993 09:27:47 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8081>;
          Tue, 18 May 1993 09:27:24 +0200
From: Tobias.Nipkow@Informatik.TU-Muenchen.De
To: info-hol@ted.cs.uidaho.edu
Cc: Larry.Paulson@cl.cam.ac.uk
Subject: Higher-Order Reasoning
Message-Id: <93May18.092724met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 18 May 1993 09:27:10 +0200

schneide <schneide@ira.uka.de> asks:

> Has anybody similar tactics or conversions?

Isabelle comes with a standard package of tactics for proofs in classical
logics. This package is also used in Isabelle's HOL. Its workhorse is called
'fast_tac'. HOL_cs is a collection of simple lemmas about HOL connectives. It
has not been adapted to this example!

goal HOL.thy "lives(agatha) & lives(butler) & lives(charles) & \
\  (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) & \
\  (!x y. killed(x,y) --> hates(x,y) & ~(richer(x,y))) & \
\  (!x. hates(agatha,x) --> ~(hates(charles,x))) & \
\  (hates(agatha,agatha) & hates(agatha,charles)) & \
\  (!x. lives(x) & ~(richer(x,agatha)) --> hates(butler,x)) & \
\  (!x. hates(agatha,x) --> hates(butler,x)) & \
\  (!x. ~(hates(x,agatha)) | ~(hates(x,butler)) | ~(hates(x,charles))) --> \
\   killed(agatha,agatha)";

by(fast_tac HOL_cs 1);

Level 1
lives(agatha) &
lives(butler) &
lives(charles) &
(killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &
(! x y. killed(x,y) --> hates(x,y) & ~ richer(x,y)) &
(! x. hates(agatha,x) --> ~ hates(charles,x)) &
(hates(agatha,agatha) & hates(agatha,charles)) &
(! x. lives(x) & ~ richer(x,agatha) --> hates(butler,x)) &
(! x. hates(agatha,x) --> hates(butler,x)) &
(! x. ~ hates(x,agatha) | ~ hates(x,butler) | ~ hates(x,charles)) -->
killed(agatha,agatha)
No subgoals!
val it = () : unit   
Timing  compile-0.0s (0.0s+0.0s+0.0s+0.0s+0.0s) run-46.0s

However, we can do a bit better than this and let fast_tac find out who
killed agatha. The token "?k" is the logical variable (in Prolog parlance)
representing the killer:

goal HOL.thy "lives(agatha) & lives(butler) & lives(charles) & \
\  (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) & \
\  (!x y. killed(x,y) --> hates(x,y) & ~(richer(x,y))) & \
\  (!x. hates(agatha,x) --> ~(hates(charles,x))) & \
\  (hates(agatha,agatha) & hates(agatha,charles)) & \
\  (!x. lives(x) & ~(richer(x,agatha)) --> hates(butler,x)) & \
\  (!x. hates(agatha,x) --> hates(butler,x)) & \
\  (!x. ~(hates(x,agatha)) | ~(hates(x,butler)) | ~(hates(x,charles))) --> \
\   killed(?k,agatha)";

by(fast_tac HOL_cs 1);

Level 1
lives(agatha) &
lives(butler) &
lives(charles) &
(killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &
(! x y. killed(x,y) --> hates(x,y) & ~ richer(x,y)) &
(! x. hates(agatha,x) --> ~ hates(charles,x)) &
(hates(agatha,agatha) & hates(agatha,charles)) &
(! x. lives(x) & ~ richer(x,agatha) --> hates(butler,x)) &
(! x. hates(agatha,x) --> hates(butler,x)) &
(! x. ~ hates(x,agatha) | ~ hates(x,butler) | ~ hates(x,charles)) -->
killed(agatha,agatha)
No subgoals!
val it = () : unit   
Timing  compile-0.1s (0.1s+0.0s+0.0s+0.0s+0.0s) run-45.2s

All credits due to Larry Paulson who wrote fast_tac.
All timings on an ELC.

Tobias