Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: S4.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      Sequents/S4.thy
    Author:     Martin Coen
    Copyright   1991  University of Cambridge
*)

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' \<turnstile>         $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F \<turnstile> $G"

ML \<open>
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}]
)
\<close>

method_setup S4_solve =
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2))\<close>

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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.