42151

1 
(* Title: HOL/HOLCF/IOA/meta_theory/TL.thy

40945

2 
Author: Olaf MÃ¼ller

17233

3 
*)

4559

4 

62002

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

4559

6 

17233

7 
theory TL


8 
imports Pred Sequence


9 
begin


10 

36452

11 
default_sort type

4559

12 

41476

13 
type_synonym

17233

14 
'a temporal = "'a Seq predicate"

4559

15 


16 

17233

17 
consts

4559

18 
suffix :: "'a Seq => 'a Seq => bool"


19 
tsuffix :: "'a Seq => 'a Seq => bool"


20 


21 
validT :: "'a Seq predicate => bool"


22 


23 
unlift :: "'a lift => 'a"


24 

62004

25 
Init :: "'a predicate => 'a temporal" ("\<langle>_\<rangle>" [0] 1000)

4559

26 

62000

27 
Box :: "'a temporal => 'a temporal" ("\<box>(_)" [80] 80)


28 
Diamond :: "'a temporal => 'a temporal" ("\<diamond>(_)" [80] 80)

61999

29 
Next :: "'a temporal => 'a temporal"


30 
Leadsto :: "'a temporal => 'a temporal => 'a temporal" (infixr "\<leadsto>" 22)

17233

31 

4559

32 
defs


33 

17233

34 
unlift_def:

28524

35 
"unlift x == (case x of Def y => y)"

4559

36 


37 
(* this means that for nil and UU the effect is unpredictable *)

17233

38 
Init_def:


39 
"Init P s == (P (unlift (HD$s)))"

4559

40 

17233

41 
suffix_def:


42 
"suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)"

4559

43 

17233

44 
tsuffix_def:

4559

45 
"tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"


46 

17233

47 
Box_def:

61999

48 
"(\<box>P) s == ! s2. tsuffix s2 s > P s2"

4559

49 

17233

50 
Next_def:

10835

51 
"(Next P) s == if (TL$s=UU  TL$s=nil) then (P s) else P (TL$s)"

4559

52 

17233

53 
Diamond_def:

62000

54 
"\<diamond>P == \<^bold>\<not> (\<box>(\<^bold>\<not> P))"

4559

55 

17233

56 
Leadsto_def:

62000

57 
"P \<leadsto> Q == (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))"

4559

58 

17233

59 
validT_def:

62000

60 
"validT P == ! s. s~=UU & s~=nil > (s \<Turnstile> P)"

4559

61 

19741

62 

62000

63 
lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)"

19741

64 
apply (rule ext)


65 
apply (simp add: Diamond_def NOT_def Box_def)


66 
done


67 

62000

68 
lemma Boxnil: "nil \<Turnstile> \<box>P"

19741

69 
apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)


70 
done


71 

62000

72 
lemma Diamondnil: "~(nil \<Turnstile> \<diamond>P)"

19741

73 
apply (simp add: Diamond_def satisfies_def NOT_def)


74 
apply (cut_tac Boxnil)


75 
apply (simp add: satisfies_def)


76 
done


77 

61999

78 
lemma Diamond_def2: "(\<diamond>F) s = (? s2. tsuffix s2 s & F s2)"

19741

79 
apply (simp add: Diamond_def NOT_def Box_def)


80 
done


81 


82 


83 


84 
subsection "TLA Axiomatization by Merz"


85 


86 
lemma suffix_refl: "suffix s s"


87 
apply (simp add: suffix_def)


88 
apply (rule_tac x = "nil" in exI)


89 
apply auto


90 
done


91 

62000

92 
lemma reflT: "s~=UU & s~=nil > (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)"

19741

93 
apply (simp add: satisfies_def IMPLIES_def Box_def)


94 
apply (rule impI)+


95 
apply (erule_tac x = "s" in allE)


96 
apply (simp add: tsuffix_def suffix_refl)


97 
done


98 


99 


100 
lemma suffix_trans: "[ suffix y x ; suffix z y ] ==> suffix z x"


101 
apply (simp add: suffix_def)


102 
apply auto


103 
apply (rule_tac x = "s1 @@ s1a" in exI)


104 
apply auto


105 
apply (simp (no_asm) add: Conc_assoc)


106 
done


107 

62000

108 
lemma transT: "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> \<box>\<box>F"

19741

109 
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def)


110 
apply auto


111 
apply (drule suffix_trans)


112 
apply assumption


113 
apply (erule_tac x = "s2a" in allE)


114 
apply auto


115 
done


116 


117 

62000

118 
lemma normalT: "s \<Turnstile> \<box>(F \<^bold>\<longrightarrow> G) \<^bold>\<longrightarrow> \<box>F \<^bold>\<longrightarrow> \<box>G"

19741

119 
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def)


120 
done


121 


122 


123 
subsection "TLA Rules by Lamport"


124 

61999

125 
lemma STL1a: "validT P ==> validT (\<box>P)"

19741

126 
apply (simp add: validT_def satisfies_def Box_def tsuffix_def)


127 
done


128 


129 
lemma STL1b: "valid P ==> validT (Init P)"


130 
apply (simp add: valid_def validT_def satisfies_def Init_def)


131 
done


132 

61999

133 
lemma STL1: "valid P ==> validT (\<box>(Init P))"

19741

134 
apply (rule STL1a)


135 
apply (erule STL1b)


136 
done


137 


138 
(* Note that unlift and HD is not at all used !!! *)

62000

139 
lemma STL4: "valid (P \<^bold>\<longrightarrow> Q) ==> validT (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"

19741

140 
apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)


141 
done


142 


143 


144 
subsection "LTL Axioms by Manna/Pnueli"


145 


146 
lemma tsuffix_TL [rule_format (no_asm)]:


147 
"s~=UU & s~=nil > tsuffix s2 (TL$s) > tsuffix s2 s"


148 
apply (unfold tsuffix_def suffix_def)


149 
apply auto

62002

150 
apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)

62001

151 
apply (rule_tac x = "a\<leadsto>s1" in exI)

19741

152 
apply auto


153 
done


154 


155 
lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]


156 


157 
declare split_if [split del]


158 
lemma LTL1:

62000

159 
"s~=UU & s~=nil > (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"

19741

160 
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)


161 
apply auto

62000

162 
(* \<box>F \<^bold>\<longrightarrow> F *)

19741

163 
apply (erule_tac x = "s" in allE)


164 
apply (simp add: tsuffix_def suffix_refl)

62000

165 
(* \<box>F \<^bold>\<longrightarrow> Next \<box>F *)

19741

166 
apply (simp split add: split_if)


167 
apply auto


168 
apply (drule tsuffix_TL2)


169 
apply assumption+


170 
apply auto


171 
done


172 
declare split_if [split]


173 


174 


175 
lemma LTL2a:

62000

176 
"s \<Turnstile> \<^bold>\<not> (Next F) \<^bold>\<longrightarrow> (Next (\<^bold>\<not> F))"

19741

177 
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)


178 
apply simp


179 
done


180 


181 
lemma LTL2b:

62000

182 
"s \<Turnstile> (Next (\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (Next F))"

19741

183 
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)


184 
apply simp


185 
done


186 


187 
lemma LTL3:

62000

188 
"ex \<Turnstile> (Next (F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (Next F) \<^bold>\<longrightarrow> (Next G)"

19741

189 
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)


190 
apply simp


191 
done


192 


193 

62000

194 
lemma ModusPonens: "[ validT (P \<^bold>\<longrightarrow> Q); validT P ] ==> validT Q"

19741

195 
apply (simp add: validT_def satisfies_def IMPLIES_def)


196 
done

17233

197 


198 
end
