author  haftmann 
Thu, 23 Nov 2017 17:03:27 +0000  
changeset 67087  733017b19de9 
parent 61386  0a29a984a91b 
permissions  rwrr 
35762  1 
(* Title: Sequents/S4.thy 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

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

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

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

5 

17481  6 
theory S4 
7 
imports Modal0 

8 
begin 

9 

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

11 
(* 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

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

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

14 

51309  15 
lstar0: "L>" and 
61385  16 
lstar1: "$G L> $H \<Longrightarrow> []P, $G L> []P, $H" and 
17 
lstar2: "$G L> $H \<Longrightarrow> P, $G L> $H" and 

51309  18 
rstar0: "R>" and 
61385  19 
rstar1: "$G R> $H \<Longrightarrow> <>P, $G R> <>P, $H" and 
20 
rstar2: "$G R> $H \<Longrightarrow> P, $G R> $H" and 

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

21 

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

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

23 

17481  24 
boxR: 
61385  25 
"\<lbrakk>$E L> $E'; $F R> $F'; $G R> $G'; 
61386  26 
$E' \<turnstile> $F', P, $G'\<rbrakk> \<Longrightarrow> $E \<turnstile> $F, []P, $G" and 
27 
boxL: "$E,P,$F,[]P \<turnstile> $G \<Longrightarrow> $E, []P, $F \<turnstile> $G" and 

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

28 

61386  29 
diaR: "$E \<turnstile> $F,P,$G,<>P \<Longrightarrow> $E \<turnstile> $F, <>P, $G" and 
17481  30 
diaL: 
61385  31 
"\<lbrakk>$E L> $E'; $F L> $F'; $G R> $G'; 
61386  32 
$E', P, $F' \<turnstile> $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F \<turnstile> $G" 
17481  33 

60770  34 
ML \<open> 
21426  35 
structure S4_Prover = Modal_ProverFun 
36 
( 

39159  37 
val rewrite_rls = @{thms rewrite_rls} 
38 
val safe_rls = @{thms safe_rls} 

39 
val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}] 

40 
val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] 

41 
val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, 

42 
@{thm rstar1}, @{thm rstar2}] 

21426  43 
) 
60770  44 
\<close> 
21426  45 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51309
diff
changeset

46 
method_setup S4_solve = 
60770  47 
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2))\<close> 
21426  48 

49 

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

51 

61386  52 
lemma "\<turnstile> []P \<longrightarrow> P" by S4_solve 
53 
lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S4_solve (* normality*) 

54 
lemma "\<turnstile> (P < Q) \<longrightarrow> []P \<longrightarrow> []Q" by S4_solve 

55 
lemma "\<turnstile> P \<longrightarrow> <>P" by S4_solve 

21426  56 

61386  57 
lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve 
58 
lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve 

59 
lemma "\<turnstile> [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >< Q)" by S4_solve 

60 
lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve 

61 
lemma "\<turnstile> []P \<longleftrightarrow> \<not> <>(\<not> P)" by S4_solve 

62 
lemma "\<turnstile> [](\<not> P) \<longleftrightarrow> \<not> <>P" by S4_solve 

63 
lemma "\<turnstile> \<not> []P \<longleftrightarrow> <>(\<not> P)" by S4_solve 

64 
lemma "\<turnstile> [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S4_solve 

65 
lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S4_solve 

21426  66 

61386  67 
lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve 
68 
lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve 

69 
lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve 

70 
lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve 

71 
lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve 

72 
lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S4_solve 

73 
lemma "\<turnstile> (P < Q) \<and> (Q < R) \<longrightarrow> (P < R)" by S4_solve 

74 
lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S4_solve 

21426  75 

76 

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

78 

61386  79 
lemma "\<turnstile> []A \<longrightarrow> A" by S4_solve (* refexivity *) 
80 
lemma "\<turnstile> []A \<longrightarrow> [][]A" by S4_solve (* transitivity *) 

81 
lemma "\<turnstile> []A \<longrightarrow> <>A" by S4_solve (* seriality *) 

82 
lemma "\<turnstile> <>[](<>A \<longrightarrow> []<>A)" by S4_solve 

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

84 
lemma "\<turnstile> []P \<longleftrightarrow> [][]P" by S4_solve 

85 
lemma "\<turnstile> <>P \<longleftrightarrow> <><>P" by S4_solve 

86 
lemma "\<turnstile> <>[]<>P \<longrightarrow> <>P" by S4_solve 

87 
lemma "\<turnstile> []<>P \<longleftrightarrow> []<>[]<>P" by S4_solve 

88 
lemma "\<turnstile> <>[]P \<longleftrightarrow> <>[]<>[]P" by S4_solve 

21426  89 

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

91 

61386  92 
lemma "\<turnstile> []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S4_solve 
93 
lemma "\<turnstile> ((P >< Q) < R) \<longrightarrow> ((P >< Q) < []R)" by S4_solve 

21426  94 

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

96 

61386  97 
lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve 
98 
lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve 

99 
lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve 

21426  100 

61386  101 
lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S4_solve 
102 
lemma "\<turnstile> []P \<longrightarrow> []<>P" by S4_solve 

103 
lemma "\<turnstile> <>[]P \<longrightarrow> <>P" by S4_solve 

21426  104 

61386  105 
lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve 
106 
lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve 

107 
lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve 

108 
lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve 

109 
lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve 

17481  110 

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

111 
end 