Quelle TL.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/TL.thy
    Author:     Olaf Müller
*)

section \<open>A General Temporal Logic\<close>

theory TL
imports Pred Sequence
begin

default_sort type

type_synonym 'a temporal = "'a Seq predicate"

definition validT :: "'a Seq predicate \ bool" (\\<^bold>\ _\ [9] 8)
  where "(\<^bold>\ P) \ (\s. s \ UU \ s \ nil \ (s \ P))"

definition unlift :: "'a lift \ 'a"
  where "unlift x = (case x of Def y \ y)"

definition Init :: "'a predicate \ 'a temporal" (\\_\\ [0] 1000)
  where "Init P s = P (unlift (HD \ s))"
    \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>

definition Next :: "'a temporal \ 'a temporal" (\(\indent=1 notation=\prefix Next\\\_)\ [80] 80)
  where "(\P) s \ (if TL \ s = UU \ TL \ s = nil then P s else P (TL \ s))"

definition suffix :: "'a Seq \ 'a Seq \ bool"
  where "suffix s2 s \ (\s1. Finite s1 \ s = s1 @@ s2)"

definition tsuffix :: "'a Seq \ 'a Seq \ bool"
  where "tsuffix s2 s \ s2 \ nil \ s2 \ UU \ suffix s2 s"

definition Box :: "'a temporal \ 'a temporal" (\(\indent=1 notation=\prefix Box\\\_)\ [80] 80)
  where "(\P) s \ (\s2. tsuffix s2 s \ P s2)"

definition Diamond :: "'a temporal \ 'a temporal" (\(\indent=1 notation=\prefix Diamond\\\_)\ [80] 80)
  where "\P = (\<^bold>\ (\(\<^bold>\ P)))"

definition Leadsto :: "'a temporal \ 'a temporal \ 'a temporal" (infixr \\\ 22)
  where "(P \ Q) = (\(P \<^bold>\ (\Q)))"

lemma simple: "\\(\<^bold>\ P) = (\<^bold>\ \\P)"
  by (auto simp add: Diamond_def NOT_def Box_def)

lemma Boxnil: "nil \ \P"
  by (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)

lemma Diamondnil: "\ (nil \ \P)"
  using Boxnil by (simp add: Diamond_def satisfies_def NOT_def)

lemma Diamond_def2: "(\F) s \ (\s2. tsuffix s2 s \ F s2)"
  by (simp add: Diamond_def NOT_def Box_def)

subsection \<open>TLA Axiomatization by Merz\<close>

lemma suffix_refl: "suffix s s"
proof -
  have "Finite nil \ s = nil @@ s" by simp
  then show ?thesis unfolding suffix_def ..
qed

lemma suffix_trans:
  assumes "suffix y x"
    and "suffix z y"
  shows "suffix z x"
proof -
  from assms obtain s1 s2
    where "Finite s1 \ x = s1 @@ y"
      and "Finite s2 \ y = s2 @@ z"
    unfolding suffix_def by iprover
  then have "Finite (s1 @@ s2) \ x = (s1 @@ s2) @@ z"
    by (simp add: Conc_assoc)
  then show ?thesis unfolding suffix_def ..
qed

lemma reflT: "s \ UU \ s \ nil \ (s \ \F \<^bold>\ F)"
proof
  assume s: "s \ UU \ s \ nil"
  have "F s" if box_F: "\s2. tsuffix s2 s \ F s2"
  proof -
    from s and suffix_refl [of s] have "tsuffix s s"
      by (simp add: tsuffix_def)
    also from box_F have "?this \ F s" ..
    finally show ?thesis .
  qed
  then show "s \ \F \<^bold>\ F"
    by (simp add: satisfies_def IMPLIES_def Box_def)
qed

lemma transT: "s \ \F \<^bold>\ \\F"
proof -
  have "F s2" if *: "tsuffix s1 s" "tsuffix s2 s1"
    and **: "\s'. tsuffix s' s \ F s'"
    for s1 s2
  proof -
    from * have "tsuffix s2 s"
      by (auto simp: tsuffix_def elim: suffix_trans)
    also from ** have "?this \ F s2" ..
    finally show ?thesis .
  qed
  then show ?thesis
    by (simp add: satisfies_def IMPLIES_def Box_def)
qed

lemma normalT: "s \ \(F \<^bold>\ G) \<^bold>\ \F \<^bold>\ \G"
  by (simp add: satisfies_def IMPLIES_def Box_def)

subsection \<open>TLA Rules by Lamport\<close>

lemma STL1a: "\<^bold>\ P \ \<^bold>\ (\P)"
  by (simp add: validT_def satisfies_def Box_def tsuffix_def)

lemma STL1b: "\ P \ \<^bold>\ (Init P)"
  by (simp add: valid_def validT_def satisfies_def Init_def)

lemma STL1: assumes "\ P" shows "\<^bold>\ (\(Init P))"
proof -
  from assms have "\<^bold>\ (Init P)" by (rule STL1b)
  then show ?thesis by (rule STL1a)
qed

(*Note that unlift and HD is not at all used!*)
lemma STL4: "\ (P \<^bold>\ Q) \ \<^bold>\ (\(Init P) \<^bold>\ \(Init Q))"
  by (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)

subsection \<open>LTL Axioms by Manna/Pnueli\<close>

lemma tsuffix_TL [rule_format]: "s \ UU \ s \ nil \ tsuffix s2 (TL \ s) \ tsuffix s2 s"
  apply (unfold tsuffix_def suffix_def)
  apply auto
  apply (Seq_case_simp s)
  apply (rule_tac x = "a \ s1" in exI)
  apply auto
  done

lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]

lemma LTL1: "s \ UU \ s \ nil \ (s \ \F \<^bold>\ (F \<^bold>\ (\(\F))))"
  supply if_split [split del]
  apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
  apply auto
  text \<open>\<open>\<box>F \<^bold>\<longrightarrow> F\<close>\<close>
  apply (erule_tac x = "s" in allE)
  apply (simp add: tsuffix_def suffix_refl)
  text \<open>\<open>\<box>F \<^bold>\<longrightarrow> \<circle>\<box>F\<close>\<close>
  apply (simp split: if_split)
  apply auto
  apply (drule tsuffix_TL2)
  apply assumption+
  apply auto
  done

lemma LTL2a: "s \ \<^bold>\ (\F) \<^bold>\ (\(\<^bold>\ F))"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma LTL2b: "s \ (\(\<^bold>\ F)) \<^bold>\ (\<^bold>\ (\F))"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma LTL3: "ex \ (\(F \<^bold>\ G)) \<^bold>\ (\F) \<^bold>\ (\G)"
  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)

lemma ModusPonens: "\<^bold>\ (P \<^bold>\ Q) \ \<^bold>\ P \ \<^bold>\ Q"
  by (simp add: validT_def satisfies_def IMPLIES_def)

end

quality96%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.