src/Modal/s4.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 132 b5704e45d2d2
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	91/Modal/S4
     2     ID:         $Id$
     3     Author: 	Martin Coen
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 S4 = Modal0 +
     8 rules
     9 (* Definition of the star operation using a set of Horn clauses *)
    10 (* For system S4:  gamma * == {[]P | []P : gamma}               *)
    11 (*                 delta * == {<>P | <>P : delta}               *)
    12 
    13   lstar0         "|L>"
    14   lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
    15   lstar2         "$G |L> $H ==>   P, $G |L>      $H"
    16   rstar0         "|R>"
    17   rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    18   rstar2         "$G |R> $H ==>   P, $G |R>      $H"
    19 
    20 (* Rules for [] and <> *)
    21 
    22   boxR
    23    "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  \
    24 \           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    25   boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    26 
    27   diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    28   diaL
    29    "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  \
    30 \           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    31 end