author  wenzelm 
Wed, 29 Nov 2006 15:44:57 +0100  
changeset 21590  ef7278f553eb 
parent 21426  87ac12bed1ab 
child 30510  4120fc59dd85 
permissions  rwrr 
17481  1 
(* Title: Modal/S4.thy 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

2 
ID: $Id$ 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

3 
Author: Martin Coen 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

4 
Copyright 1991 University of Cambridge 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

5 
*) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

6 

17481  7 
theory S4 
8 
imports Modal0 

9 
begin 

10 

11 
axioms 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

12 
(* Definition of the star operation using a set of Horn clauses *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

13 
(* For system S4: gamma * == {[]P  []P : gamma} *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

14 
(* delta * == {<>P  <>P : delta} *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

15 

17481  16 
lstar0: "L>" 
17 
lstar1: "$G L> $H ==> []P, $G L> []P, $H" 

18 
lstar2: "$G L> $H ==> P, $G L> $H" 

19 
rstar0: "R>" 

20 
rstar1: "$G R> $H ==> <>P, $G R> <>P, $H" 

21 
rstar2: "$G R> $H ==> P, $G R> $H" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

22 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

23 
(* Rules for [] and <> *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

24 

17481  25 
boxR: 
26 
"[ $E L> $E'; $F R> $F'; $G R> $G'; 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

27 
$E'  $F', P, $G'] ==> $E  $F, []P, $G" 
17481  28 
boxL: "$E,P,$F,[]P  $G ==> $E, []P, $F  $G" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

29 

17481  30 
diaR: "$E  $F,P,$G,<>P ==> $E  $F, <>P, $G" 
31 
diaL: 

32 
"[ $E L> $E'; $F L> $F'; $G R> $G'; 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

33 
$E', P, $F'  $G'] ==> $E, <>P, $F  $G" 
17481  34 

21426  35 
ML {* 
36 
structure S4_Prover = Modal_ProverFun 

37 
( 

38 
val rewrite_rls = thms "rewrite_rls" 

39 
val safe_rls = thms "safe_rls" 

40 
val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"] 

41 
val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] 

42 
val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", 

43 
thm "rstar1", thm "rstar2"] 

44 
) 

45 
*} 

46 

47 
method_setup S4_solve = 

21590  48 
{* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver" 
21426  49 

50 

51 
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) 

52 

53 
lemma " []P > P" by S4_solve 

54 
lemma " [](P>Q) > ([]P>[]Q)" by S4_solve (* normality*) 

55 
lemma " (P<Q) > []P > []Q" by S4_solve 

56 
lemma " P > <>P" by S4_solve 

57 

58 
lemma " [](P & Q) <> []P & []Q" by S4_solve 

59 
lemma " <>(P  Q) <> <>P  <>Q" by S4_solve 

60 
lemma " [](P<>Q) <> (P><Q)" by S4_solve 

61 
lemma " <>(P>Q) <> ([]P><>Q)" by S4_solve 

62 
lemma " []P <> ~<>(~P)" by S4_solve 

63 
lemma " [](~P) <> ~<>P" by S4_solve 

64 
lemma " ~[]P <> <>(~P)" by S4_solve 

65 
lemma " [][]P <> ~<><>(~P)" by S4_solve 

66 
lemma " ~<>(P  Q) <> ~<>P & ~<>Q" by S4_solve 

67 

68 
lemma " []P  []Q > [](P  Q)" by S4_solve 

69 
lemma " <>(P & Q) > <>P & <>Q" by S4_solve 

70 
lemma " [](P  Q) > []P  <>Q" by S4_solve 

71 
lemma " <>P & []Q > <>(P & Q)" by S4_solve 

72 
lemma " [](P  Q) > <>P  []Q" by S4_solve 

73 
lemma " <>(P>(Q & R)) > ([]P > <>Q) & ([]P><>R)" by S4_solve 

74 
lemma " (P<Q) & (Q<R) > (P<R)" by S4_solve 

75 
lemma " []P > <>Q > <>(P & Q)" by S4_solve 

76 

77 

78 
(* Theorems of system S4 from Hughes and Cresswell, p.46 *) 

79 

80 
lemma " []A > A" by S4_solve (* refexivity *) 

81 
lemma " []A > [][]A" by S4_solve (* transitivity *) 

82 
lemma " []A > <>A" by S4_solve (* seriality *) 

83 
lemma " <>[](<>A > []<>A)" by S4_solve 

84 
lemma " <>[](<>[]A > []A)" by S4_solve 

85 
lemma " []P <> [][]P" by S4_solve 

86 
lemma " <>P <> <><>P" by S4_solve 

87 
lemma " <>[]<>P > <>P" by S4_solve 

88 
lemma " []<>P <> []<>[]<>P" by S4_solve 

89 
lemma " <>[]P <> <>[]<>[]P" by S4_solve 

90 

91 
(* Theorems for system S4 from Hughes and Cresswell, p.60 *) 

92 

93 
lemma " []P  []Q <> []([]P  []Q)" by S4_solve 

94 
lemma " ((P><Q) < R) > ((P><Q) < []R)" by S4_solve 

95 

96 
(* These are from Hailpern, LNCS 129 *) 

97 

98 
lemma " [](P & Q) <> []P & []Q" by S4_solve 

99 
lemma " <>(P  Q) <> <>P  <>Q" by S4_solve 

100 
lemma " <>(P > Q) <> ([]P > <>Q)" by S4_solve 

101 

102 
lemma " [](P > Q) > (<>P > <>Q)" by S4_solve 

103 
lemma " []P > []<>P" by S4_solve 

104 
lemma " <>[]P > <>P" by S4_solve 

105 

106 
lemma " []P  []Q > [](P  Q)" by S4_solve 

107 
lemma " <>(P & Q) > <>P & <>Q" by S4_solve 

108 
lemma " [](P  Q) > []P  <>Q" by S4_solve 

109 
lemma " <>P & []Q > <>(P & Q)" by S4_solve 

110 
lemma " [](P  Q) > <>P  []Q" by S4_solve 

17481  111 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

112 
end 