1208963Srdivacky(* Title: HOL/HOLCF/IOA/TL.thy 2208963Srdivacky Author: Olaf M��ller 3208963Srdivacky*) 4208963Srdivacky 5208963Srdivackysection \<open>A General Temporal Logic\<close> 6210299Sed 7210299Sedtheory TL 8210299Sedimports Pred Sequence 9210299Sedbegin 10212904Sdim 11210299Seddefault_sort type 12210299Sed 13218893Sdimtype_synonym 'a temporal = "'a Seq predicate" 14210299Sed 15210299Seddefinition validT :: "'a Seq predicate \<Rightarrow> bool" ("\<^bold>\<TTurnstile> _" [9] 8) 16210299Sed where "(\<^bold>\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> P))" 17210299Sed 18210299Seddefinition unlift :: "'a lift \<Rightarrow> 'a" 19210299Sed where "unlift x = (case x of Def y \<Rightarrow> y)" 20218893Sdim 21210299Seddefinition Init :: "'a predicate \<Rightarrow> 'a temporal" ("\<langle>_\<rangle>" [0] 1000) 22210299Sed where "Init P s = P (unlift (HD \<cdot> s))" 23210299Sed \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close> 24210299Sed 25210299Seddefinition Next :: "'a temporal \<Rightarrow> 'a temporal" ("\<circle>(_)" [80] 80) 26210299Sed where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))" 27210299Sed 28210299Seddefinition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool" 29210299Sed where "suffix s2 s \<longleftrightarrow> (\<exists>s1. Finite s1 \<and> s = s1 @@ s2)" 30210299Sed 31210299Seddefinition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool" 32212904Sdim where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s" 33210299Sed 34210299Seddefinition Box :: "'a temporal \<Rightarrow> 'a temporal" ("\<box>(_)" [80] 80) 35208963Srdivacky where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)" 36208963Srdivacky 37208963Srdivackydefinition Diamond :: "'a temporal \<Rightarrow> 'a temporal" ("\<diamond>(_)" [80] 80) 38208963Srdivacky where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))" 39 40definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal" (infixr "\<leadsto>" 22) 41 where "(P \<leadsto> Q) = (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))" 42 43 44lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)" 45 by (auto simp add: Diamond_def NOT_def Box_def) 46 47lemma Boxnil: "nil \<Turnstile> \<box>P" 48 by (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc) 49 50lemma Diamondnil: "\<not> (nil \<Turnstile> \<diamond>P)" 51 using Boxnil by (simp add: Diamond_def satisfies_def NOT_def) 52 53lemma Diamond_def2: "(\<diamond>F) s \<longleftrightarrow> (\<exists>s2. tsuffix s2 s \<and> F s2)" 54 by (simp add: Diamond_def NOT_def Box_def) 55 56 57subsection \<open>TLA Axiomatization by Merz\<close> 58 59lemma suffix_refl: "suffix s s" 60 apply (simp add: suffix_def) 61 apply (rule_tac x = "nil" in exI) 62 apply auto 63 done 64 65lemma reflT: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)" 66 apply (simp add: satisfies_def IMPLIES_def Box_def) 67 apply (rule impI)+ 68 apply (erule_tac x = "s" in allE) 69 apply (simp add: tsuffix_def suffix_refl) 70 done 71 72lemma suffix_trans: "suffix y x \<Longrightarrow> suffix z y \<Longrightarrow> suffix z x" 73 apply (simp add: suffix_def) 74 apply auto 75 apply (rule_tac x = "s1 @@ s1a" in exI) 76 apply auto 77 apply (simp add: Conc_assoc) 78 done 79 80lemma transT: "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> \<box>\<box>F" 81 apply (simp add: satisfies_def IMPLIES_def Box_def tsuffix_def) 82 apply auto 83 apply (drule suffix_trans) 84 apply assumption 85 apply (erule_tac x = "s2a" in allE) 86 apply auto 87 done 88 89lemma normalT: "s \<Turnstile> \<box>(F \<^bold>\<longrightarrow> G) \<^bold>\<longrightarrow> \<box>F \<^bold>\<longrightarrow> \<box>G" 90 by (simp add: satisfies_def IMPLIES_def Box_def) 91 92 93subsection \<open>TLA Rules by Lamport\<close> 94 95lemma STL1a: "\<^bold>\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>P)" 96 by (simp add: validT_def satisfies_def Box_def tsuffix_def) 97 98lemma STL1b: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (Init P)" 99 by (simp add: valid_def validT_def satisfies_def Init_def) 100 101lemma STL1: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P))" 102 apply (rule STL1a) 103 apply (erule STL1b) 104 done 105 106(*Note that unlift and HD is not at all used!*) 107lemma STL4: "\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))" 108 by (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def) 109 110 111subsection \<open>LTL Axioms by Manna/Pnueli\<close> 112 113lemma tsuffix_TL [rule_format]: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> tsuffix s2 (TL \<cdot> s) \<longrightarrow> tsuffix s2 s" 114 apply (unfold tsuffix_def suffix_def) 115 apply auto 116 apply (Seq_case_simp s) 117 apply (rule_tac x = "a \<leadsto> s1" in exI) 118 apply auto 119 done 120 121lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] 122 123lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (\<circle>(\<box>F))))" 124 supply if_split [split del] 125 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def) 126 apply auto 127 text \<open>\<open>\<box>F \<^bold>\<longrightarrow> F\<close>\<close> 128 apply (erule_tac x = "s" in allE) 129 apply (simp add: tsuffix_def suffix_refl) 130 text \<open>\<open>\<box>F \<^bold>\<longrightarrow> \<circle>\<box>F\<close>\<close> 131 apply (simp split: if_split) 132 apply auto 133 apply (drule tsuffix_TL2) 134 apply assumption+ 135 apply auto 136 done 137 138lemma LTL2a: "s \<Turnstile> \<^bold>\<not> (\<circle>F) \<^bold>\<longrightarrow> (\<circle>(\<^bold>\<not> F))" 139 by (simp add: Next_def satisfies_def NOT_def IMPLIES_def) 140 141lemma LTL2b: "s \<Turnstile> (\<circle>(\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (\<circle>F))" 142 by (simp add: Next_def satisfies_def NOT_def IMPLIES_def) 143 144lemma LTL3: "ex \<Turnstile> (\<circle>(F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (\<circle>F) \<^bold>\<longrightarrow> (\<circle>G)" 145 by (simp add: Next_def satisfies_def NOT_def IMPLIES_def) 146 147lemma ModusPonens: "\<^bold>\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> Q" 148 by (simp add: validT_def satisfies_def IMPLIES_def) 149 150end 151