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

34 

35 ML {* use_legacy_bindings (the_context ()) *} 

36 
31 end 
37 end 