|
1 (* Title: HOLCF/IOA/meta_theory/TLS.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 header {* A General Temporal Logic *} |
|
6 |
|
7 theory TL |
|
8 imports Pred Sequence |
|
9 begin |
|
10 |
|
11 default_sort type |
|
12 |
|
13 types |
|
14 'a temporal = "'a Seq predicate" |
|
15 |
|
16 |
|
17 consts |
|
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 |
|
25 Init ::"'a predicate => 'a temporal" ("<_>" [0] 1000) |
|
26 |
|
27 Box ::"'a temporal => 'a temporal" ("[] (_)" [80] 80) |
|
28 Diamond ::"'a temporal => 'a temporal" ("<> (_)" [80] 80) |
|
29 Next ::"'a temporal => 'a temporal" |
|
30 Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22) |
|
31 |
|
32 notation (xsymbols) |
|
33 Box ("\<box> (_)" [80] 80) and |
|
34 Diamond ("\<diamond> (_)" [80] 80) and |
|
35 Leadsto (infixr "\<leadsto>" 22) |
|
36 |
|
37 defs |
|
38 |
|
39 unlift_def: |
|
40 "unlift x == (case x of Def y => y)" |
|
41 |
|
42 (* this means that for nil and UU the effect is unpredictable *) |
|
43 Init_def: |
|
44 "Init P s == (P (unlift (HD$s)))" |
|
45 |
|
46 suffix_def: |
|
47 "suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)" |
|
48 |
|
49 tsuffix_def: |
|
50 "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s" |
|
51 |
|
52 Box_def: |
|
53 "([] P) s == ! s2. tsuffix s2 s --> P s2" |
|
54 |
|
55 Next_def: |
|
56 "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)" |
|
57 |
|
58 Diamond_def: |
|
59 "<> P == .~ ([] (.~ P))" |
|
60 |
|
61 Leadsto_def: |
|
62 "P ~> Q == ([] (P .--> (<> Q)))" |
|
63 |
|
64 validT_def: |
|
65 "validT P == ! s. s~=UU & s~=nil --> (s |= P)" |
|
66 |
|
67 |
|
68 lemma simple: "[] <> (.~ P) = (.~ <> [] P)" |
|
69 apply (rule ext) |
|
70 apply (simp add: Diamond_def NOT_def Box_def) |
|
71 done |
|
72 |
|
73 lemma Boxnil: "nil |= [] P" |
|
74 apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc) |
|
75 done |
|
76 |
|
77 lemma Diamondnil: "~(nil |= <> P)" |
|
78 apply (simp add: Diamond_def satisfies_def NOT_def) |
|
79 apply (cut_tac Boxnil) |
|
80 apply (simp add: satisfies_def) |
|
81 done |
|
82 |
|
83 lemma Diamond_def2: "(<> F) s = (? s2. tsuffix s2 s & F s2)" |
|
84 apply (simp add: Diamond_def NOT_def Box_def) |
|
85 done |
|
86 |
|
87 |
|
88 |
|
89 subsection "TLA Axiomatization by Merz" |
|
90 |
|
91 lemma suffix_refl: "suffix s s" |
|
92 apply (simp add: suffix_def) |
|
93 apply (rule_tac x = "nil" in exI) |
|
94 apply auto |
|
95 done |
|
96 |
|
97 lemma reflT: "s~=UU & s~=nil --> (s |= [] F .--> F)" |
|
98 apply (simp add: satisfies_def IMPLIES_def Box_def) |
|
99 apply (rule impI)+ |
|
100 apply (erule_tac x = "s" in allE) |
|
101 apply (simp add: tsuffix_def suffix_refl) |
|
102 done |
|
103 |
|
104 |
|
105 lemma suffix_trans: "[| suffix y x ; suffix z y |] ==> suffix z x" |
|
106 apply (simp add: suffix_def) |
|
107 apply auto |
|
108 apply (rule_tac x = "s1 @@ s1a" in exI) |
|
109 apply auto |
|
110 apply (simp (no_asm) add: Conc_assoc) |
|
111 done |
|
112 |
|
113 lemma transT: "s |= [] F .--> [] [] F" |
|
114 apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def) |
|
115 apply auto |
|
116 apply (drule suffix_trans) |
|
117 apply assumption |
|
118 apply (erule_tac x = "s2a" in allE) |
|
119 apply auto |
|
120 done |
|
121 |
|
122 |
|
123 lemma normalT: "s |= [] (F .--> G) .--> [] F .--> [] G" |
|
124 apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def) |
|
125 done |
|
126 |
|
127 |
|
128 subsection "TLA Rules by Lamport" |
|
129 |
|
130 lemma STL1a: "validT P ==> validT ([] P)" |
|
131 apply (simp add: validT_def satisfies_def Box_def tsuffix_def) |
|
132 done |
|
133 |
|
134 lemma STL1b: "valid P ==> validT (Init P)" |
|
135 apply (simp add: valid_def validT_def satisfies_def Init_def) |
|
136 done |
|
137 |
|
138 lemma STL1: "valid P ==> validT ([] (Init P))" |
|
139 apply (rule STL1a) |
|
140 apply (erule STL1b) |
|
141 done |
|
142 |
|
143 (* Note that unlift and HD is not at all used !!! *) |
|
144 lemma STL4: "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))" |
|
145 apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def) |
|
146 done |
|
147 |
|
148 |
|
149 subsection "LTL Axioms by Manna/Pnueli" |
|
150 |
|
151 lemma tsuffix_TL [rule_format (no_asm)]: |
|
152 "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s" |
|
153 apply (unfold tsuffix_def suffix_def) |
|
154 apply auto |
|
155 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
|
156 apply (rule_tac x = "a>>s1" in exI) |
|
157 apply auto |
|
158 done |
|
159 |
|
160 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |
|
161 |
|
162 declare split_if [split del] |
|
163 lemma LTL1: |
|
164 "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))" |
|
165 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def) |
|
166 apply auto |
|
167 (* []F .--> F *) |
|
168 apply (erule_tac x = "s" in allE) |
|
169 apply (simp add: tsuffix_def suffix_refl) |
|
170 (* []F .--> Next [] F *) |
|
171 apply (simp split add: split_if) |
|
172 apply auto |
|
173 apply (drule tsuffix_TL2) |
|
174 apply assumption+ |
|
175 apply auto |
|
176 done |
|
177 declare split_if [split] |
|
178 |
|
179 |
|
180 lemma LTL2a: |
|
181 "s |= .~ (Next F) .--> (Next (.~ F))" |
|
182 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) |
|
183 apply simp |
|
184 done |
|
185 |
|
186 lemma LTL2b: |
|
187 "s |= (Next (.~ F)) .--> (.~ (Next F))" |
|
188 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) |
|
189 apply simp |
|
190 done |
|
191 |
|
192 lemma LTL3: |
|
193 "ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)" |
|
194 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) |
|
195 apply simp |
|
196 done |
|
197 |
|
198 |
|
199 lemma ModusPonens: "[| validT (P .--> Q); validT P |] ==> validT Q" |
|
200 apply (simp add: validT_def satisfies_def IMPLIES_def) |
|
201 done |
|
202 |
|
203 end |