Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: TL.thy Sprache: Isabelle

Original von: 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" ("\(_)" [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" ("\(_)" [80] 80)
  where "(\P) s \ (\s2. tsuffix s2 s \ P s2)"

definition Diamond :: "'a temporal \ 'a temporal" ("\(_)" [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"
  apply (simp add: suffix_def)
  apply (rule_tac x = "nil" in exI)
  apply auto
  done

lemma reflT: "s \ UU \ s \ nil \ (s \ \F \<^bold>\ F)"
  apply (simp add: satisfies_def IMPLIES_def Box_def)
  apply (rule impI)+
  apply (erule_tac x = "s" in allE)
  apply (simp add: tsuffix_def suffix_refl)
  done

lemma suffix_trans: "suffix y x \ suffix z y \ suffix z x"
  apply (simp add: suffix_def)
  apply auto
  apply (rule_tac x = "s1 @@ s1a" in exI)
  apply auto
  apply (simp add: Conc_assoc)
  done

lemma transT: "s \ \F \<^bold>\ \\F"
  apply (simp add: satisfies_def IMPLIES_def Box_def tsuffix_def)
  apply auto
  apply (drule suffix_trans)
  apply assumption
  apply (erule_tac x = "s2a" in allE)
  apply auto
  done

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: "\ P \ \<^bold>\ (\(Init P))"
  apply (rule STL1a)
  apply (erule STL1b)
  done

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

¤ Dauer der Verarbeitung: 0.15 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.