src/Modal/t.thy
 changeset 0 a5a9c433f639
equal inserted replaced
-1:000000000000 0:a5a9c433f639

1 (*  Title: 	91/Modal/T

2     ID:         \$Id\$

3     Author: 	Martin Coen

4     Copyright   1991  University of Cambridge

5 *)

6

7 T = Modal0 +

8 rules

9 (* Definition of the star operation using a set of Horn clauses *)

10 (* For system T:  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  |-         \$G    ==> \$E, []P, \$F |-          \$G"

26   diaR     "\$E         |- \$F, P,  \$G    ==> \$E          |- \$F, <>P, \$G"

27   diaL

28    "[| \$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';  \

29 \               \$E', P, \$F'|-         \$G'|] ==> \$E, <>P, \$F |-          \$G"

30 end