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 