src/Sequents/S4.thy
changeset 17481 75166ebb619b
parent 2073 fb0655539d05
child 21426 87ac12bed1ab
equal deleted inserted replaced
17480:fd19f77dcf60 17481:75166ebb619b
     1 (*  Title:      Modal/S4
     1 (*  Title:      Modal/S4.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Martin Coen
     3     Author:     Martin Coen
     4     Copyright   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 S4 = Modal0 +
     7 theory S4
     8 rules
     8 imports Modal0
       
     9 begin
       
    10 
       
    11 axioms
     9 (* Definition of the star operation using a set of Horn clauses *)
    12 (* Definition of the star operation using a set of Horn clauses *)
    10 (* For system S4:  gamma * == {[]P | []P : gamma}               *)
    13 (* For system S4:  gamma * == {[]P | []P : gamma}               *)
    11 (*                 delta * == {<>P | <>P : delta}               *)
    14 (*                 delta * == {<>P | <>P : delta}               *)
    12 
    15 
    13   lstar0         "|L>"
    16   lstar0:         "|L>"
    14   lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
    17   lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
    15   lstar2         "$G |L> $H ==>   P, $G |L>      $H"
    18   lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
    16   rstar0         "|R>"
    19   rstar0:         "|R>"
    17   rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    20   rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    18   rstar2         "$G |R> $H ==>   P, $G |R>      $H"
    21   rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
    19 
    22 
    20 (* Rules for [] and <> *)
    23 (* Rules for [] and <> *)
    21 
    24 
    22   boxR
    25   boxR:
    23    "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
    26    "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
    24            $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    27            $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    25   boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    28   boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    26 
    29 
    27   diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    30   diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    28   diaL
    31   diaL:
    29    "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
    32    "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    30            $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    33            $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
       
    34 
       
    35 ML {* use_legacy_bindings (the_context ()) *}
       
    36 
    31 end
    37 end