src/Sequents/T.thy
changeset 17481 75166ebb619b
parent 2073 fb0655539d05
child 21426 87ac12bed1ab
     1.1 --- a/src/Sequents/T.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/T.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,30 +1,36 @@
     1.4 -(*  Title:      Modal/T
     1.5 +(*  Title:      Modal/T.thy
     1.6      ID:         $Id$
     1.7      Author:     Martin Coen
     1.8      Copyright   1991  University of Cambridge
     1.9  *)
    1.10  
    1.11 -T = Modal0 +
    1.12 -rules
    1.13 +theory T
    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 T:  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  |-         $G    ==> $E, []P, $F |-          $G"
    1.43 -  diaR     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
    1.44 -  diaL
    1.45 -   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
    1.46 +  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
    1.47 +  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
    1.48 +  diaL:
    1.49 +   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    1.50                 $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
    1.51 +
    1.52 +ML {* use_legacy_bindings (the_context ()) *}
    1.53 +
    1.54  end