Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Modal/ex/Tthms.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
Initial revision

(*  Title: 	91/Modal/ex/Tthms
    ID:         $Id$
    Author: 	Martin Coen
    Copyright   1991  University of Cambridge
*)

(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)

try "|- []P --> P";
try "|- [](P-->Q) --> ([]P-->[]Q)";    (* normality*)
try "|- (P--<Q) --> []P --> []Q";
try "|- P --> <>P";

try "|-  [](P & Q) <-> []P & []Q";
try "|-  <>(P | Q) <-> <>P | <>Q";
try "|-  [](P<->Q) <-> (P>-<Q)";
try "|-  <>(P-->Q) <-> ([]P--><>Q)";
try "|-        []P <-> ~<>(~P)";
try "|-     [](~P) <-> ~<>P";
try "|-       ~[]P <-> <>(~P)";
try "|-      [][]P <-> ~<><>(~P)";
try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";

try "|- []P | []Q --> [](P | Q)";
try "|- <>(P & Q) --> <>P & <>Q";
try "|- [](P | Q) --> []P | <>Q";
try "|- <>P & []Q --> <>(P & Q)";
try "|- [](P | Q) --> <>P | []Q";
try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
try "|- (P--<Q) & (Q--<R) --> (P--<R)";
try "|- []P --> <>Q --> <>(P & Q)";
isabelle