1 (* Title: Modal/T |
1 (* Title: Modal/T.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 T = Modal0 + |
7 theory T |
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 T: gamma * == {P | []P : gamma} *) |
13 (* For system T: 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 |- $G ==> $E, []P, $F |- $G" |
28 boxL: "$E, P, $F |- $G ==> $E, []P, $F |- $G" |
26 diaR "$E |- $F, P, $G ==> $E |- $F, <>P, $G" |
29 diaR: "$E |- $F, P, $G ==> $E |- $F, <>P, $G" |
27 diaL |
30 diaL: |
28 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; |
31 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; |
29 $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G" |
32 $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G" |
|
33 |
|
34 ML {* use_legacy_bindings (the_context ()) *} |
|
35 |
30 end |
36 end |