src/Sequents/T.thy
changeset 51309 473303ef6e34
parent 42814 5af15f1e2ef6
child 54742 7a86358a3c0b
equal deleted inserted replaced
51308:51e158e988a5 51309:473303ef6e34
     5 
     5 
     6 theory T
     6 theory T
     7 imports Modal0
     7 imports Modal0
     8 begin
     8 begin
     9 
     9 
    10 axioms
    10 axiomatization where
    11 (* Definition of the star operation using a set of Horn clauses *)
    11 (* Definition of the star operation using a set of Horn clauses *)
    12 (* For system T:  gamma * == {P | []P : gamma}                  *)
    12 (* For system T:  gamma * == {P | []P : gamma}                  *)
    13 (*                delta * == {P | <>P : delta}                  *)
    13 (*                delta * == {P | <>P : delta}                  *)
    14 
    14 
    15   lstar0:         "|L>"
    15   lstar0:         "|L>" and
    16   lstar1:         "$G |L> $H ==> []P, $G |L> P, $H"
    16   lstar1:         "$G |L> $H ==> []P, $G |L> P, $H" and
    17   lstar2:         "$G |L> $H ==>   P, $G |L>    $H"
    17   lstar2:         "$G |L> $H ==>   P, $G |L>    $H" and
    18   rstar0:         "|R>"
    18   rstar0:         "|R>" and
    19   rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H"
    19   rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H" and
    20   rstar2:         "$G |R> $H ==>   P, $G |R>    $H"
    20   rstar2:         "$G |R> $H ==>   P, $G |R>    $H" and
    21 
    21 
    22 (* Rules for [] and <> *)
    22 (* Rules for [] and <> *)
    23 
    23 
    24   boxR:
    24   boxR:
    25    "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
    25    "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
    26                $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
    26                $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
    27   boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
    27   boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G" and
    28   diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
    28   diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G" and
    29   diaL:
    29   diaL:
    30    "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    30    "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    31                $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
    31                $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
    32 
    32 
    33 ML {*
    33 ML {*