src/Sequents/S4.thy
changeset 17481 75166ebb619b
parent 2073 fb0655539d05
child 21426 87ac12bed1ab
     1.1 --- a/src/Sequents/S4.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/S4.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,31 +1,37 @@
     1.4 -(*  Title:      Modal/S4
     1.5 +(*  Title:      Modal/S4.thy
     1.6      ID:         $Id$
     1.7      Author:     Martin Coen
     1.8      Copyright   1991  University of Cambridge
     1.9  *)
    1.10  
    1.11 -S4 = Modal0 +
    1.12 -rules
    1.13 +theory S4
    1.14 +imports Modal0
    1.15 +begin
    1.16 +
    1.17 +axioms
    1.18  (* Definition of the star operation using a set of Horn clauses *)
    1.19  (* For system S4:  gamma * == {[]P | []P : gamma}               *)
    1.20  (*                 delta * == {<>P | <>P : delta}               *)
    1.21  
    1.22 -  lstar0         "|L>"
    1.23 -  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
    1.24 -  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
    1.25 -  rstar0         "|R>"
    1.26 -  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    1.27 -  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
    1.28 +  lstar0:         "|L>"
    1.29 +  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
    1.30 +  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
    1.31 +  rstar0:         "|R>"
    1.32 +  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    1.33 +  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
    1.34  
    1.35  (* Rules for [] and <> *)
    1.36  
    1.37 -  boxR
    1.38 -   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
    1.39 +  boxR:
    1.40 +   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
    1.41             $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    1.42 -  boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    1.43 +  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    1.44  
    1.45 -  diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    1.46 -  diaL
    1.47 -   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
    1.48 +  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    1.49 +  diaL:
    1.50 +   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    1.51             $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    1.52 +
    1.53 +ML {* use_legacy_bindings (the_context ()) *}
    1.54 +
    1.55  end