(* 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.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
