# Theory S4

```(*  Title:      Sequents/S4.thy
Author:     Martin Coen
*)

theory S4
imports Modal0
begin

axiomatization where
(* Definition of the star operation using a set of Horn clauses *)
(* For system S4:  gamma * == {[]P | []P : gamma}               *)
(*                 delta * == {<>P | <>P : delta}               *)

lstar0:         "|L>" and
lstar1:         "\$G |L> \$H ⟹ []P, \$G |L> []P, \$H" and
lstar2:         "\$G |L> \$H ⟹   P, \$G |L>      \$H" and
rstar0:         "|R>" and
rstar1:         "\$G |R> \$H ⟹ <>P, \$G |R> <>P, \$H" and
rstar2:         "\$G |R> \$H ⟹   P, \$G |R>      \$H" and

(* Rules for [] and <> *)

boxR:
"⟦\$E |L> \$E';  \$F |R> \$F';  \$G |R> \$G';
\$E'         ⊢ \$F', P, \$G'⟧ ⟹ \$E          ⊢ \$F, []P, \$G" and
boxL:     "\$E,P,\$F,[]P ⊢         \$G    ⟹ \$E, []P, \$F ⊢          \$G" and

diaR:     "\$E          ⊢ \$F,P,\$G,<>P   ⟹ \$E          ⊢ \$F, <>P, \$G" and
diaL:
"⟦\$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';
\$E', P, \$F' ⊢         \$G'⟧ ⟹ \$E, <>P, \$F ⊢ \$G"

ML ‹
structure S4_Prover = Modal_ProverFun
(
val rewrite_rls = @{thms rewrite_rls}
val safe_rls = @{thms safe_rls}
val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}]
val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
@{thm rstar1}, @{thm rstar2}]
)
›

method_setup S4_solve =
‹Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2))›

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

lemma "⊢ []P ⟶ P" by S4_solve
lemma "⊢ [](P ⟶ Q) ⟶ ([]P ⟶ []Q)" by S4_solve   (* normality*)
lemma "⊢ (P --< Q) ⟶ []P ⟶ []Q" by S4_solve
lemma "⊢ P ⟶ <>P" by S4_solve

lemma "⊢  [](P ∧ Q) ⟷ []P ∧ []Q" by S4_solve
lemma "⊢  <>(P ∨ Q) ⟷ <>P ∨ <>Q" by S4_solve
lemma "⊢  [](P ⟷ Q) ⟷ (P >-< Q)" by S4_solve
lemma "⊢  <>(P ⟶ Q) ⟷ ([]P ⟶ <>Q)" by S4_solve
lemma "⊢        []P ⟷ ¬ <>(¬ P)" by S4_solve
lemma "⊢     [](¬ P) ⟷ ¬ <>P" by S4_solve
lemma "⊢       ¬ []P ⟷ <>(¬ P)" by S4_solve
lemma "⊢      [][]P ⟷ ¬ <><>(¬ P)" by S4_solve
lemma "⊢ ¬ <>(P ∨ Q) ⟷ ¬ <>P ∧ ¬ <>Q" by S4_solve

lemma "⊢ []P ∨ []Q ⟶ [](P ∨ Q)" by S4_solve
lemma "⊢ <>(P ∧ Q) ⟶ <>P ∧ <>Q" by S4_solve
lemma "⊢ [](P ∨ Q) ⟶ []P ∨ <>Q" by S4_solve
lemma "⊢ <>P ∧ []Q ⟶ <>(P ∧ Q)" by S4_solve
lemma "⊢ [](P ∨ Q) ⟶ <>P ∨ []Q" by S4_solve
lemma "⊢ <>(P ⟶ (Q ∧ R)) ⟶ ([]P ⟶ <>Q) ∧ ([]P ⟶ <>R)" by S4_solve
lemma "⊢ (P --< Q) ∧ (Q --< R) ⟶ (P --< R)" by S4_solve
lemma "⊢ []P ⟶ <>Q ⟶ <>(P ∧ Q)" by S4_solve

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

lemma "⊢ []A ⟶ A" by S4_solve             (* refexivity *)
lemma "⊢ []A ⟶ [][]A" by S4_solve         (* transitivity *)
lemma "⊢ []A ⟶ <>A" by S4_solve           (* seriality *)
lemma "⊢ <>[](<>A ⟶ []<>A)" by S4_solve
lemma "⊢ <>[](<>[]A ⟶ []A)" by S4_solve
lemma "⊢ []P ⟷ [][]P" by S4_solve
lemma "⊢ <>P ⟷ <><>P" by S4_solve
lemma "⊢ <>[]<>P ⟶ <>P" by S4_solve
lemma "⊢ []<>P ⟷ []<>[]<>P" by S4_solve
lemma "⊢ <>[]P ⟷ <>[]<>[]P" by S4_solve

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

lemma "⊢ []P ∨ []Q ⟷ []([]P ∨ []Q)" by S4_solve
lemma "⊢ ((P >-< Q) --< R) ⟶ ((P >-< Q) --< []R)" by S4_solve

(* These are from Hailpern, LNCS 129 *)

lemma "⊢ [](P ∧ Q) ⟷ []P ∧ []Q" by S4_solve
lemma "⊢ <>(P ∨ Q) ⟷ <>P ∨ <>Q" by S4_solve
lemma "⊢ <>(P ⟶ Q) ⟷ ([]P ⟶ <>Q)" by S4_solve

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

lemma "⊢ []P ∨ []Q ⟶ [](P ∨ Q)" by S4_solve
lemma "⊢ <>(P ∧ Q) ⟶ <>P ∧ <>Q" by S4_solve
lemma "⊢ [](P ∨ Q) ⟶ []P ∨ <>Q" by S4_solve
lemma "⊢ <>P ∧ []Q ⟶ <>(P ∧ Q)" by S4_solve
lemma "⊢ [](P ∨ Q) ⟶ <>P ∨ []Q" by S4_solve

end
```