author | paulson |
Fri, 18 Feb 2000 15:35:29 +0100 | |
changeset 8255 | 38f96394c099 |
parent 6255 | db63752140c7 |
child 9168 | 77658111e122 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: TLA/TLA.ML |
|
3 |
Author: Stephan Merz |
|
6255 | 4 |
Copyright: 1998 University of Munich |
3807 | 5 |
|
6 |
Lemmas and tactics for temporal reasoning. |
|
7 |
*) |
|
8 |
||
6255 | 9 |
(* Specialize intensional introduction/elimination rules for temporal formulas *) |
3807 | 10 |
|
6255 | 11 |
qed_goal "tempI" TLA.thy "(!!sigma. sigma |= (F::temporal)) ==> |- F" |
3807 | 12 |
(fn [prem] => [ REPEAT (resolve_tac [prem,intI] 1) ]); |
13 |
||
6255 | 14 |
qed_goal "tempD" TLA.thy "|- (F::temporal) ==> sigma |= F" |
15 |
(fn [prem] => [ rtac (prem RS intD) 1 ]); |
|
3807 | 16 |
|
17 |
||
6255 | 18 |
(* ======== Functions to "unlift" temporal theorems ====== *) |
3807 | 19 |
|
6255 | 20 |
(* The following functions are specialized versions of the corresponding |
21 |
functions defined in Intensional.ML in that they introduce a |
|
22 |
"world" parameter of type "behavior". |
|
3807 | 23 |
*) |
6255 | 24 |
fun temp_unlift th = |
25 |
(rewrite_rule action_rews (th RS tempD)) |
|
26 |
handle _ => action_unlift th; |
|
3807 | 27 |
|
6255 | 28 |
(* Turn |- F = G into meta-level rewrite rule F == G *) |
29 |
val temp_rewrite = int_rewrite; |
|
3807 | 30 |
|
6255 | 31 |
fun temp_use th = |
32 |
case (concl_of th) of |
|
33 |
Const _ $ (Const ("Intensional.Valid", _) $ _) => |
|
34 |
((flatten (temp_unlift th)) handle _ => th) |
|
35 |
| _ => th; |
|
3807 | 36 |
|
37 |
(* Update classical reasoner---will be updated once more below! *) |
|
38 |
||
39 |
AddSIs [tempI]; |
|
40 |
AddDs [tempD]; |
|
41 |
||
6255 | 42 |
val temp_css = (claset(), simpset()); |
4651 | 43 |
val temp_cs = op addss temp_css; |
3807 | 44 |
|
6255 | 45 |
(* Modify the functions that add rules to simpsets, classical sets, |
46 |
and clasimpsets in order to accept "lifted" theorems |
|
47 |
*) |
|
3807 | 48 |
|
6255 | 49 |
local |
50 |
fun try_rewrite th = |
|
51 |
(temp_rewrite th) handle _ => temp_use th |
|
52 |
in |
|
53 |
val op addsimps = fn (ss, ts) => ss addsimps (map try_rewrite ts) |
|
54 |
val op addsimps2 = fn (css, ts) => css addsimps2 (map try_rewrite ts) |
|
55 |
end; |
|
3807 | 56 |
|
6255 | 57 |
val op addSIs = fn (cs, ts) => cs addSIs (map temp_use ts); |
58 |
val op addSEs = fn (cs, ts) => cs addSEs (map temp_use ts); |
|
59 |
val op addSDs = fn (cs, ts) => cs addSDs (map temp_use ts); |
|
60 |
val op addIs = fn (cs, ts) => cs addIs (map temp_use ts); |
|
61 |
val op addEs = fn (cs, ts) => cs addEs (map temp_use ts); |
|
62 |
val op addDs = fn (cs, ts) => cs addDs (map temp_use ts); |
|
3807 | 63 |
|
6255 | 64 |
val op addSIs2 = fn (css, ts) => css addSIs2 (map temp_use ts); |
65 |
val op addSEs2 = fn (css, ts) => css addSEs2 (map temp_use ts); |
|
66 |
val op addSDs2 = fn (css, ts) => css addSDs2 (map temp_use ts); |
|
67 |
val op addIs2 = fn (css, ts) => css addIs2 (map temp_use ts); |
|
68 |
val op addEs2 = fn (css, ts) => css addEs2 (map temp_use ts); |
|
69 |
val op addDs2 = fn (css, ts) => css addDs2 (map temp_use ts); |
|
3807 | 70 |
|
71 |
||
72 |
(* ------------------------------------------------------------------------- *) |
|
73 |
(*** "Simple temporal logic": only [] and <> ***) |
|
74 |
(* ------------------------------------------------------------------------- *) |
|
75 |
section "Simple temporal logic"; |
|
76 |
||
6255 | 77 |
(* []~F == []~Init F *) |
78 |
bind_thm("boxNotInit", rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] boxInit)); |
|
79 |
||
80 |
qed_goalw "dmdInit" TLA.thy [dmd_def] "TEMP <>F == TEMP <> Init F" |
|
81 |
(fn _ => [rewtac (read_instantiate [("F", "LIFT ~F")] boxInit), |
|
82 |
simp_tac (simpset() addsimps Init_simps) 1]); |
|
83 |
||
84 |
bind_thm("dmdNotInit", rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] dmdInit)); |
|
85 |
||
86 |
(* boxInit and dmdInit cannot be used as rewrites, because they loop. |
|
87 |
Non-looping instances for state predicates and actions are occasionally useful. |
|
88 |
*) |
|
89 |
bind_thm("boxInit_stp", read_instantiate [("'a","state")] boxInit); |
|
90 |
bind_thm("boxInit_act", read_instantiate [("'a","state * state")] boxInit); |
|
91 |
bind_thm("dmdInit_stp", read_instantiate [("'a","state")] dmdInit); |
|
92 |
bind_thm("dmdInit_act", read_instantiate [("'a","state * state")] dmdInit); |
|
93 |
||
94 |
(* The symmetric equations can be used to get rid of Init *) |
|
95 |
bind_thm("boxInitD", symmetric boxInit); |
|
96 |
bind_thm("dmdInitD", symmetric dmdInit); |
|
97 |
bind_thm("boxNotInitD", symmetric boxNotInit); |
|
98 |
bind_thm("dmdNotInitD", symmetric dmdNotInit); |
|
99 |
||
100 |
val Init_simps = Init_simps @ [boxInitD, dmdInitD, boxNotInitD, dmdNotInitD]; |
|
101 |
||
3807 | 102 |
(* ------------------------ STL2 ------------------------------------------- *) |
103 |
bind_thm("STL2", reflT); |
|
104 |
||
6255 | 105 |
(* The "polymorphic" (generic) variant *) |
106 |
qed_goal "STL2_gen" TLA.thy "|- []F --> Init F" |
|
107 |
(fn _ => [rewtac (read_instantiate [("F", "F")] boxInit), |
|
108 |
rtac STL2 1]); |
|
109 |
||
110 |
(* see also STL2_pr below: "|- []P --> Init P & Init (P`)" *) |
|
111 |
||
3807 | 112 |
|
113 |
(* Dual versions for <> *) |
|
6255 | 114 |
qed_goalw "InitDmd" TLA.thy [dmd_def] "|- F --> <> F" |
115 |
(fn _ => [ auto_tac (temp_css addSDs2 [STL2]) ]); |
|
3807 | 116 |
|
6255 | 117 |
qed_goal "InitDmd_gen" TLA.thy "|- Init F --> <>F" |
118 |
(fn _ => [Clarsimp_tac 1, |
|
119 |
dtac (temp_use InitDmd) 1, |
|
120 |
asm_full_simp_tac (simpset() addsimps [dmdInitD]) 1]); |
|
3807 | 121 |
|
122 |
||
123 |
(* ------------------------ STL3 ------------------------------------------- *) |
|
6255 | 124 |
qed_goal "STL3" TLA.thy "|- ([][]F) = ([]F)" |
125 |
(K [force_tac (temp_css addEs2 [transT,STL2]) 1]); |
|
3807 | 126 |
|
127 |
(* corresponding elimination rule introduces double boxes: |
|
128 |
[| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W |
|
129 |
*) |
|
130 |
bind_thm("dup_boxE", make_elim((temp_unlift STL3) RS iffD2)); |
|
131 |
bind_thm("dup_boxD", (temp_unlift STL3) RS iffD1); |
|
132 |
||
133 |
(* dual versions for <> *) |
|
6255 | 134 |
qed_goalw "DmdDmd" TLA.thy [dmd_def] "|- (<><>F) = (<>F)" |
3807 | 135 |
(fn _ => [ auto_tac (temp_css addsimps2 [STL3]) ]); |
136 |
bind_thm("dup_dmdE", make_elim((temp_unlift DmdDmd) RS iffD2)); |
|
137 |
bind_thm("dup_dmdD", (temp_unlift DmdDmd) RS iffD1); |
|
138 |
||
139 |
||
140 |
(* ------------------------ STL4 ------------------------------------------- *) |
|
6255 | 141 |
qed_goal "STL4" TLA.thy "|- F --> G ==> |- []F --> []G" |
142 |
(fn [prem] => [Clarsimp_tac 1, |
|
143 |
rtac (temp_use normalT) 1, |
|
144 |
rtac (temp_use (prem RS necT)) 1, |
|
145 |
atac 1 |
|
3807 | 146 |
]); |
147 |
||
6255 | 148 |
(* Unlifted version as an elimination rule *) |
3807 | 149 |
qed_goal "STL4E" TLA.thy |
6255 | 150 |
"[| sigma |= []F; |- F --> G |] ==> sigma |= []G" |
151 |
(fn prems => [ REPEAT (resolve_tac (prems @ [temp_use STL4]) 1) ]); |
|
152 |
||
153 |
qed_goal "STL4_gen" TLA.thy "|- Init F --> Init G ==> |- []F --> []G" |
|
154 |
(fn [prem] => [rtac (rewrite_rule [boxInitD] (prem RS STL4)) 1]); |
|
155 |
||
156 |
qed_goal "STL4E_gen" TLA.thy |
|
157 |
"[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G" |
|
158 |
(fn prems => [ REPEAT (resolve_tac (prems @ [temp_use STL4_gen]) 1) ]); |
|
3807 | 159 |
|
160 |
(* see also STL4Edup below, which allows an auxiliary boxed formula: |
|
161 |
[]A /\ F => G |
|
162 |
----------------- |
|
163 |
[]A /\ []F => []G |
|
164 |
*) |
|
165 |
||
166 |
(* The dual versions for <> *) |
|
167 |
qed_goalw "DmdImpl" TLA.thy [dmd_def] |
|
6255 | 168 |
"|- F --> G ==> |- <>F --> <>G" |
169 |
(fn [prem] => [fast_tac (temp_cs addSIs [prem] addSEs [STL4E]) 1]); |
|
3807 | 170 |
|
171 |
qed_goal "DmdImplE" TLA.thy |
|
6255 | 172 |
"[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G" |
173 |
(fn prems => [ REPEAT (resolve_tac (prems @ [temp_use DmdImpl]) 1) ]); |
|
3807 | 174 |
|
175 |
||
176 |
(* ------------------------ STL5 ------------------------------------------- *) |
|
6255 | 177 |
qed_goal "STL5" TLA.thy "|- ([]F & []G) = ([](F & G))" |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
178 |
(fn _ => [Auto_tac, |
6255 | 179 |
subgoal_tac "sigma |= [](G --> (F & G))" 1, |
180 |
etac (temp_use normalT) 1, atac 1, |
|
3807 | 181 |
ALLGOALS (fast_tac (temp_cs addSEs [STL4E])) |
182 |
]); |
|
183 |
(* rewrite rule to split conjunctions under boxes *) |
|
184 |
bind_thm("split_box_conj", (temp_unlift STL5) RS sym); |
|
185 |
||
186 |
(* the corresponding elimination rule allows to combine boxes in the hypotheses |
|
187 |
(NB: F and G must have the same type, i.e., both actions or temporals.) |
|
6255 | 188 |
Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop! |
3807 | 189 |
*) |
190 |
qed_goal "box_conjE" TLA.thy |
|
6255 | 191 |
"[| sigma |= []F; sigma |= []G; sigma |= [](F&G) ==> PROP R |] ==> PROP R" |
3807 | 192 |
(fn prems => [ REPEAT (resolve_tac |
193 |
(prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]); |
|
194 |
||
6255 | 195 |
(* Instances of box_conjE for state predicates, actions, and temporals |
196 |
in case the general rule is "too polymorphic". |
|
197 |
*) |
|
198 |
bind_thm("box_conjE_temp", read_instantiate [("'a","behavior")] box_conjE); |
|
199 |
bind_thm("box_conjE_stp", read_instantiate [("'a","state")] box_conjE); |
|
200 |
bind_thm("box_conjE_act", read_instantiate [("'a","state * state")] box_conjE); |
|
201 |
||
3807 | 202 |
(* Define a tactic that tries to merge all boxes in an antecedent. The definition is |
6255 | 203 |
a bit kludgy in order to simulate "double elim-resolution". |
3807 | 204 |
*) |
6255 | 205 |
|
206 |
Goal "[| sigma |= []F; PROP W |] ==> PROP W"; |
|
207 |
by (atac 1); |
|
208 |
val box_thin = result(); |
|
3807 | 209 |
|
210 |
fun merge_box_tac i = |
|
211 |
REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i]); |
|
212 |
||
213 |
fun merge_temp_box_tac i = |
|
6255 | 214 |
REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i, |
215 |
eres_inst_tac [("'a","behavior")] box_thin i]); |
|
3807 | 216 |
|
6255 | 217 |
fun merge_stp_box_tac i = |
218 |
REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i, |
|
219 |
eres_inst_tac [("'a","state")] box_thin i]); |
|
220 |
||
3807 | 221 |
fun merge_act_box_tac i = |
6255 | 222 |
REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i, |
223 |
eres_inst_tac [("'a","state * state")] box_thin i]); |
|
224 |
||
3807 | 225 |
|
226 |
(* rewrite rule to push universal quantification through box: |
|
6255 | 227 |
(sigma |= [](! x. F x)) = (! x. (sigma |= []F x)) |
3807 | 228 |
*) |
229 |
bind_thm("all_box", standard((temp_unlift allT) RS sym)); |
|
230 |
||
231 |
||
6255 | 232 |
qed_goal "DmdOr" TLA.thy "|- (<>(F | G)) = (<>F | <>G)" |
3807 | 233 |
(fn _ => [auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]), |
234 |
TRYALL (EVERY' [etac swap, |
|
235 |
merge_box_tac, |
|
236 |
fast_tac (temp_cs addSEs [STL4E])]) |
|
237 |
]); |
|
238 |
||
6255 | 239 |
qed_goal "exT" TLA.thy "|- (? x. <>(F x)) = (<>(? x. F x))" |
240 |
(fn _ => [ auto_tac (temp_css addsimps2 [dmd_def,Not_Rex,all_box]) ]); |
|
3807 | 241 |
|
242 |
bind_thm("ex_dmd", standard((temp_unlift exT) RS sym)); |
|
243 |
||
244 |
||
245 |
qed_goal "STL4Edup" TLA.thy |
|
6255 | 246 |
"!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G" |
3807 | 247 |
(fn _ => [etac dup_boxE 1, |
248 |
merge_box_tac 1, |
|
249 |
etac STL4E 1, |
|
250 |
atac 1 |
|
251 |
]); |
|
252 |
||
253 |
qed_goalw "DmdImpl2" TLA.thy [dmd_def] |
|
6255 | 254 |
"!!sigma. [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G" |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
255 |
(fn _ => [Auto_tac, |
3807 | 256 |
etac notE 1, |
257 |
merge_box_tac 1, |
|
258 |
fast_tac (temp_cs addSEs [STL4E]) 1 |
|
259 |
]); |
|
260 |
||
261 |
qed_goal "InfImpl" TLA.thy |
|
6255 | 262 |
"[| sigma |= []<>F; sigma |= []G; |- F & G --> H |] ==> sigma |= []<>H" |
3807 | 263 |
(fn [prem1,prem2,prem3] |
264 |
=> [cut_facts_tac [prem1,prem2] 1, |
|
265 |
eres_inst_tac [("F","G")] dup_boxE 1, |
|
266 |
merge_box_tac 1, |
|
6255 | 267 |
fast_tac (temp_cs addSEs [STL4E,DmdImpl2] addSIs [prem3]) 1 |
3807 | 268 |
]); |
269 |
||
270 |
(* ------------------------ STL6 ------------------------------------------- *) |
|
271 |
(* Used in the proof of STL6, but useful in itself. *) |
|
6255 | 272 |
qed_goalw "BoxDmd" TLA.thy [dmd_def] "|- []F & <>G --> <>([]F & G)" |
273 |
(fn _ => [ Clarsimp_tac 1, |
|
3807 | 274 |
etac dup_boxE 1, |
275 |
merge_box_tac 1, |
|
276 |
etac swap 1, |
|
277 |
fast_tac (temp_cs addSEs [STL4E]) 1 ]); |
|
278 |
||
279 |
(* weaker than BoxDmd, but more polymorphic (and often just right) *) |
|
6255 | 280 |
qed_goalw "BoxDmd_simple" TLA.thy [dmd_def] "|- []F & <>G --> <>(F & G)" |
281 |
(fn _ => [ Clarsimp_tac 1, |
|
282 |
merge_box_tac 1, |
|
283 |
fast_tac (temp_cs addSEs [notE,STL4E]) 1 |
|
284 |
]); |
|
285 |
||
286 |
qed_goalw "BoxDmd2_simple" TLA.thy [dmd_def] "|- []F & <>G --> <>(G & F)" |
|
287 |
(fn _ => [ Clarsimp_tac 1, |
|
3807 | 288 |
merge_box_tac 1, |
289 |
fast_tac (temp_cs addSEs [notE,STL4E]) 1 |
|
290 |
]); |
|
291 |
||
6255 | 292 |
qed_goal "DmdImpldup" TLA.thy |
293 |
"[| sigma |= []A; sigma |= <>F; |- []A & F --> G |] ==> sigma |= <>G" |
|
294 |
(fn [p1,p2,p3] => [rtac ((p2 RS (p1 RS (temp_use BoxDmd))) RS DmdImplE) 1, |
|
295 |
rtac p3 1]); |
|
296 |
||
297 |
qed_goal "STL6" TLA.thy "|- <>[]F & <>[]G --> <>[](F & G)" |
|
3807 | 298 |
(fn _ => [auto_tac (temp_css addsimps2 [symmetric (temp_rewrite STL5)]), |
6255 | 299 |
dtac (temp_use linT) 1, atac 1, etac thin_rl 1, |
3807 | 300 |
rtac ((temp_unlift DmdDmd) RS iffD1) 1, |
301 |
etac disjE 1, |
|
6255 | 302 |
etac DmdImplE 1, rtac BoxDmd 1, |
303 |
(* the second subgoal needs commutativity of &, which complicates the proof *) |
|
3807 | 304 |
etac DmdImplE 1, |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
305 |
Auto_tac, |
6255 | 306 |
dtac (temp_use BoxDmd) 1, atac 1, etac thin_rl 1, |
3807 | 307 |
fast_tac (temp_cs addSEs [DmdImplE]) 1 |
308 |
]); |
|
309 |
||
310 |
||
311 |
(* ------------------------ True / False ----------------------------------------- *) |
|
312 |
section "Simplification of constants"; |
|
313 |
||
6255 | 314 |
qed_goal "BoxConst" TLA.thy "|- ([]#P) = #P" |
315 |
(fn _ => [rtac tempI 1, |
|
316 |
case_tac "P" 1, |
|
317 |
auto_tac (temp_css addSIs2 [necT] addDs2 [STL2_gen] |
|
318 |
addsimps2 Init_simps) |
|
319 |
]); |
|
3807 | 320 |
|
6255 | 321 |
qed_goalw "DmdConst" TLA.thy [dmd_def] "|- (<>#P) = #P" |
322 |
(fn _ => [case_tac "P" 1, |
|
323 |
ALLGOALS (asm_full_simp_tac (simpset() addsimps [BoxConst])) |
|
324 |
]); |
|
3807 | 325 |
|
6255 | 326 |
val temp_simps = map temp_rewrite [BoxConst, DmdConst]; |
3807 | 327 |
|
328 |
(* Make these rewrites active by default *) |
|
329 |
Addsimps temp_simps; |
|
330 |
val temp_css = temp_css addsimps2 temp_simps; |
|
4651 | 331 |
val temp_cs = op addss temp_css; |
3807 | 332 |
|
333 |
||
334 |
(* ------------------------ Further rewrites ----------------------------------------- *) |
|
335 |
section "Further rewrites"; |
|
336 |
||
6255 | 337 |
qed_goalw "NotBox" TLA.thy [dmd_def] "|- (~[]F) = (<>~F)" |
338 |
(fn _ => [ Simp_tac 1 ]); |
|
3807 | 339 |
|
6255 | 340 |
qed_goalw "NotDmd" TLA.thy [dmd_def] "|- (~<>F) = ([]~F)" |
341 |
(fn _ => [ Simp_tac 1 ]); |
|
3807 | 342 |
|
343 |
(* These are not by default included in temp_css, because they could be harmful, |
|
6255 | 344 |
e.g. []F & ~[]F becomes []F & <>~F !! *) |
3807 | 345 |
val more_temp_simps = (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd]) |
346 |
@ (map (fn th => (temp_unlift th) RS eq_reflection) |
|
347 |
[NotBox, NotDmd]); |
|
348 |
||
6255 | 349 |
qed_goal "BoxDmdBox" TLA.thy "|- ([]<>[]F) = (<>[]F)" |
350 |
(fn _ => [ auto_tac (temp_css addSDs2 [STL2]), |
|
3807 | 351 |
rtac ccontr 1, |
6255 | 352 |
subgoal_tac "sigma |= <>[][]F & <>[]~[]F" 1, |
3807 | 353 |
etac thin_rl 1, |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
354 |
Auto_tac, |
6255 | 355 |
dtac (temp_use STL6) 1, atac 1, |
3807 | 356 |
Asm_full_simp_tac 1, |
4089 | 357 |
ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps)) |
3807 | 358 |
]); |
359 |
||
6255 | 360 |
qed_goalw "DmdBoxDmd" TLA.thy [dmd_def] "|- (<>[]<>F) = ([]<>F)" |
361 |
(fn _ => [ auto_tac (temp_css addsimps2 [rewrite_rule [dmd_def] BoxDmdBox]) ]); |
|
3807 | 362 |
|
363 |
val more_temp_simps = more_temp_simps @ (map temp_rewrite [BoxDmdBox, DmdBoxDmd]); |
|
364 |
||
365 |
||
366 |
(* ------------------------ Miscellaneous ----------------------------------- *) |
|
367 |
||
368 |
qed_goal "BoxOr" TLA.thy |
|
6255 | 369 |
"!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)" |
3807 | 370 |
(fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]); |
371 |
||
6255 | 372 |
(* "persistently implies infinitely often" *) |
373 |
qed_goal "DBImplBD" TLA.thy "|- <>[]F --> []<>F" |
|
374 |
(fn _ => [Clarsimp_tac 1, |
|
3807 | 375 |
rtac ccontr 1, |
6255 | 376 |
asm_full_simp_tac (simpset() addsimps more_temp_simps) 1, |
377 |
dtac (temp_use STL6) 1, atac 1, |
|
378 |
Asm_full_simp_tac 1 |
|
3807 | 379 |
]); |
380 |
||
381 |
qed_goal "BoxDmdDmdBox" TLA.thy |
|
6255 | 382 |
"|- []<>F & <>[]G --> []<>(F & G)" |
383 |
(fn _ => [Clarsimp_tac 1, |
|
384 |
rtac ccontr 1, |
|
3807 | 385 |
rewrite_goals_tac more_temp_simps, |
6255 | 386 |
dtac (temp_use STL6) 1, atac 1, |
387 |
subgoal_tac "sigma |= <>[]~F" 1, |
|
5755
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
388 |
force_tac (temp_css addsimps2 [dmd_def]) 1, |
3807 | 389 |
fast_tac (temp_cs addEs [DmdImplE,STL4E]) 1 |
390 |
]); |
|
391 |
||
392 |
||
393 |
(* ------------------------------------------------------------------------- *) |
|
394 |
(*** TLA-specific theorems: primed formulas ***) |
|
395 |
(* ------------------------------------------------------------------------- *) |
|
396 |
section "priming"; |
|
397 |
||
398 |
(* ------------------------ TLA2 ------------------------------------------- *) |
|
6255 | 399 |
qed_goal "STL2_pr" TLA.thy |
400 |
"|- []P --> Init P & Init P`" |
|
401 |
(fn _ => [fast_tac (temp_cs addSIs [primeI, STL2_gen]) 1]); |
|
3807 | 402 |
|
403 |
(* Auxiliary lemma allows priming of boxed actions *) |
|
6255 | 404 |
qed_goal "BoxPrime" TLA.thy "|- []P --> []($P & P$)" |
405 |
(fn _ => [Clarsimp_tac 1, |
|
3807 | 406 |
etac dup_boxE 1, |
6255 | 407 |
rewtac boxInit_act, |
408 |
etac STL4E 1, |
|
409 |
auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_pr]) |
|
3807 | 410 |
]); |
411 |
||
6255 | 412 |
qed_goal "TLA2" TLA.thy "|- $P & P$ --> A ==> |- []P --> []A" |
413 |
(fn prems => [Clarsimp_tac 1, |
|
414 |
dtac (temp_use BoxPrime) 1, |
|
415 |
auto_tac (temp_css addsimps2 [Init_stp_act_rev] addSIs2 prems addSEs2 [STL4E]) |
|
416 |
]); |
|
3807 | 417 |
|
418 |
qed_goal "TLA2E" TLA.thy |
|
6255 | 419 |
"[| sigma |= []P; |- $P & P$ --> A |] ==> sigma |= []A" |
420 |
(fn prems => [REPEAT (resolve_tac (prems @ (prems RL [temp_use TLA2])) 1)]); |
|
3807 | 421 |
|
6255 | 422 |
qed_goalw "DmdPrime" TLA.thy [dmd_def] "|- (<>P`) --> (<>P)" |
3807 | 423 |
(fn _ => [ fast_tac (temp_cs addSEs [TLA2E]) 1 ]); |
424 |
||
6255 | 425 |
bind_thm("PrimeDmd", (temp_use InitDmd_gen) RS (temp_use DmdPrime)); |
3807 | 426 |
|
427 |
(* ------------------------ INV1, stable --------------------------------------- *) |
|
428 |
section "stable, invariant"; |
|
429 |
||
430 |
qed_goal "ind_rule" TLA.thy |
|
6255 | 431 |
"[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |] \ |
432 |
\ ==> sigma |= []F" |
|
433 |
(fn prems => [rtac (temp_use indT) 1, |
|
3807 | 434 |
REPEAT (resolve_tac (prems @ (prems RL [STL4E])) 1)]); |
6255 | 435 |
|
436 |
qed_goalw "box_stp_act" TLA.thy [boxInit_act] "|- ([]$P) = ([]P)" |
|
437 |
(K [simp_tac (simpset() addsimps Init_simps) 1]); |
|
438 |
bind_thm("box_stp_actI", zero_var_indexes ((temp_use box_stp_act) RS iffD2)); |
|
439 |
bind_thm("box_stp_actD", zero_var_indexes ((temp_use box_stp_act) RS iffD1)); |
|
3807 | 440 |
|
6255 | 441 |
val more_temp_simps = (temp_rewrite box_stp_act)::more_temp_simps; |
3807 | 442 |
|
6255 | 443 |
qed_goalw "INV1" TLA.thy [stable_def,boxInit_stp,boxInit_act] |
444 |
"|- (Init P) --> (stable P) --> []P" |
|
445 |
(K [Clarsimp_tac 1, |
|
446 |
etac ind_rule 1, |
|
447 |
auto_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule]) |
|
448 |
]); |
|
449 |
||
450 |
qed_goalw "StableT" TLA.thy [stable_def] |
|
451 |
"|- $P & A --> P` ==> |- []A --> stable P" |
|
452 |
(fn [prem] => [fast_tac (temp_cs addSEs [STL4E] addIs [prem]) 1]); |
|
3807 | 453 |
|
454 |
qed_goal "Stable" TLA.thy |
|
6255 | 455 |
"[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P" |
456 |
(fn prems => [ REPEAT (resolve_tac (prems @ [temp_use StableT]) 1) ]); |
|
3807 | 457 |
|
458 |
(* Generalization of INV1 *) |
|
459 |
qed_goalw "StableBox" TLA.thy [stable_def] |
|
6255 | 460 |
"|- (stable P) --> [](Init P --> []P)" |
461 |
(K [Clarsimp_tac 1, |
|
462 |
etac dup_boxE 1, |
|
463 |
force_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1]) 1]); |
|
464 |
||
3807 | 465 |
qed_goal "DmdStable" TLA.thy |
6255 | 466 |
"|- (stable P) & <>P --> <>[]P" |
467 |
(fn _ => [Clarsimp_tac 1, |
|
468 |
rtac DmdImpl2 1, |
|
469 |
etac (temp_use StableBox) 2, |
|
470 |
asm_simp_tac (simpset() addsimps [dmdInitD]) 1 |
|
3807 | 471 |
]); |
472 |
||
473 |
(* ---------------- (Semi-)automatic invariant tactics ---------------------- *) |
|
474 |
||
475 |
(* inv_tac reduces goals of the form ... ==> sigma |= []P *) |
|
5755
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
476 |
fun inv_tac css = SELECT_GOAL |
3807 | 477 |
(EVERY [auto_tac css, |
478 |
TRY (merge_box_tac 1), |
|
6255 | 479 |
rtac (temp_use INV1) 1, (* fail if the goal is not a box *) |
3807 | 480 |
TRYALL (etac Stable)]); |
481 |
||
482 |
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals; |
|
6255 | 483 |
in simple cases it may be able to handle goals like |- MyProg --> []Inv. |
3807 | 484 |
In these simple cases the simplifier seems to be more useful than the |
485 |
auto-tactic, which applies too much propositional logic and simplifies |
|
486 |
too late. |
|
487 |
*) |
|
488 |
||
5755
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
489 |
fun auto_inv_tac ss = SELECT_GOAL |
4089 | 490 |
((inv_tac (claset(),ss) 1) THEN |
6255 | 491 |
(TRYALL (action_simp_tac (ss addsimps [Init_stp,Init_act]) [] [squareE]))); |
3807 | 492 |
|
493 |
||
494 |
qed_goalw "unless" TLA.thy [dmd_def] |
|
6255 | 495 |
"|- []($P --> P` | Q`) --> (stable P) | <>Q" |
496 |
(fn _ => [clarsimp_tac (temp_css addSDs2 [BoxPrime]) 1, |
|
3807 | 497 |
merge_box_tac 1, |
6255 | 498 |
etac swap 1, |
3807 | 499 |
fast_tac (temp_cs addSEs [Stable]) 1 |
500 |
]); |
|
501 |
||
502 |
||
503 |
(* --------------------- Recursive expansions --------------------------------------- *) |
|
504 |
section "recursive expansions"; |
|
505 |
||
6255 | 506 |
(* Recursive expansions of [] and <> for state predicates *) |
507 |
qed_goal "BoxRec" TLA.thy "|- ([]P) = (Init P & []P`)" |
|
508 |
(fn _ => [auto_tac (temp_css addSIs2 [STL2_gen]), |
|
3807 | 509 |
fast_tac (temp_cs addSEs [TLA2E]) 1, |
6255 | 510 |
auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1,STL4E]) |
3807 | 511 |
]); |
512 |
||
6255 | 513 |
qed_goalw "DmdRec" TLA.thy [dmd_def, temp_rewrite BoxRec] "|- (<>P) = (Init P | <>P`)" |
514 |
(K [ auto_tac (temp_css addsimps2 Init_simps) ]); |
|
3807 | 515 |
|
516 |
qed_goal "DmdRec2" TLA.thy |
|
6255 | 517 |
"!!sigma. [| sigma |= <>P; sigma |= []~P` |] ==> sigma |= Init P" |
518 |
(K [ force_tac (temp_css addsimps2 [DmdRec,dmd_def]) 1]); |
|
3807 | 519 |
|
6255 | 520 |
(* The "-->" part of the following is a little intricate. *) |
521 |
qed_goal "InfinitePrime" TLA.thy "|- ([]<>P) = ([]<>P`)" |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
522 |
(fn _ => [Auto_tac, |
3807 | 523 |
rtac classical 1, |
6255 | 524 |
rtac (temp_use DBImplBD) 1, |
525 |
subgoal_tac "sigma |= <>[]P" 1, |
|
3807 | 526 |
fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1, |
6255 | 527 |
subgoal_tac "sigma |= <>[](<>P & []~P`)" 1, |
528 |
force_tac (temp_css addsimps2 [boxInit_stp] |
|
5755
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
529 |
addSEs2 [DmdImplE,STL4E,DmdRec2]) 1, |
6255 | 530 |
force_tac (temp_css addSIs2 [STL6] addsimps2 more_temp_simps) 1, |
531 |
fast_tac (temp_cs addIs [DmdPrime] addSEs [STL4E]) 1 |
|
3807 | 532 |
]); |
533 |
||
6255 | 534 |
qed_goal "InfiniteEnsures" TLA.thy |
535 |
"[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P" |
|
536 |
(fn prems => [rewtac (temp_rewrite InfinitePrime), |
|
537 |
rtac InfImpl 1, |
|
538 |
REPEAT (resolve_tac prems 1) |
|
539 |
]); |
|
540 |
||
3807 | 541 |
(* ------------------------ fairness ------------------------------------------- *) |
542 |
section "fairness"; |
|
543 |
||
544 |
(* alternative definitions of fairness *) |
|
545 |
qed_goalw "WF_alt" TLA.thy [WF_def,dmd_def] |
|
6255 | 546 |
"|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)" |
3807 | 547 |
(fn _ => [ fast_tac temp_cs 1 ]); |
548 |
||
549 |
qed_goalw "SF_alt" TLA.thy [SF_def,dmd_def] |
|
6255 | 550 |
"|- SF(A)_v = (<>[]~Enabled(<A>_v) | []<><A>_v)" |
3807 | 551 |
(fn _ => [ fast_tac temp_cs 1 ]); |
552 |
||
553 |
(* theorems to "box" fairness conditions *) |
|
6255 | 554 |
qed_goal "BoxWFI" TLA.thy "|- WF(A)_v --> []WF(A)_v" |
555 |
(fn _ => [ auto_tac (temp_css addsimps2 (WF_alt::more_temp_simps) |
|
556 |
addSIs2 [BoxOr]) ]); |
|
3807 | 557 |
|
6255 | 558 |
qed_goal "WF_Box" TLA.thy "|- ([]WF(A)_v) = WF(A)_v" |
559 |
(fn prems => [ fast_tac (temp_cs addSIs [BoxWFI] addSDs [STL2]) 1 ]); |
|
3807 | 560 |
|
6255 | 561 |
qed_goal "BoxSFI" TLA.thy "|- SF(A)_v --> []SF(A)_v" |
562 |
(fn _ => [ auto_tac (temp_css addsimps2 (SF_alt::more_temp_simps) |
|
563 |
addSIs2 [BoxOr]) ]); |
|
3807 | 564 |
|
6255 | 565 |
qed_goal "SF_Box" TLA.thy "|- ([]SF(A)_v) = SF(A)_v" |
566 |
(fn prems => [ fast_tac (temp_cs addSIs [BoxSFI] addSDs [STL2]) 1 ]); |
|
3807 | 567 |
|
568 |
val more_temp_simps = more_temp_simps @ (map temp_rewrite [WF_Box, SF_Box]); |
|
569 |
||
6255 | 570 |
qed_goalw "SFImplWF" TLA.thy [SF_def,WF_def] "|- SF(A)_v --> WF(A)_v" |
571 |
(fn _ => [ fast_tac (temp_cs addSDs [DBImplBD]) 1 ]); |
|
3807 | 572 |
|
573 |
(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *) |
|
574 |
val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1)); |
|
575 |
||
576 |
||
577 |
(* ------------------------------ leads-to ------------------------------ *) |
|
578 |
||
579 |
section "~>"; |
|
580 |
||
6255 | 581 |
qed_goalw "leadsto_init" TLA.thy [leadsto_def] |
582 |
"|- (Init F) & (F ~> G) --> <>G" |
|
583 |
(fn _ => [ auto_tac (temp_css addSDs2 [STL2]) ]); |
|
3807 | 584 |
|
6255 | 585 |
(* |- F & (F ~> G) --> <>G *) |
586 |
bind_thm("leadsto_init_temp", |
|
587 |
rewrite_rule Init_simps (read_instantiate [("'a","behavior")] leadsto_init)); |
|
588 |
||
589 |
qed_goalw "streett_leadsto" TLA.thy [leadsto_def] |
|
590 |
"|- ([]<>Init F --> []<>G) = (<>(F ~> G))" (K [ |
|
5755
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
591 |
Auto_tac, |
4089 | 592 |
asm_full_simp_tac (simpset() addsimps more_temp_simps) 1, |
6255 | 593 |
fast_tac (temp_cs addSEs [DmdImplE,STL4E]) 1, |
594 |
fast_tac (temp_cs addSIs [InitDmd] addSEs [STL4E]) 1, |
|
595 |
subgoal_tac "sigma |= []<><>G" 1, |
|
596 |
asm_full_simp_tac (simpset() addsimps more_temp_simps) 1, |
|
597 |
dtac (temp_use BoxDmdDmdBox) 1, atac 1, |
|
598 |
fast_tac (temp_cs addSEs [DmdImplE,STL4E]) 1 |
|
3807 | 599 |
]); |
600 |
||
601 |
qed_goal "leadsto_infinite" TLA.thy |
|
6255 | 602 |
"|- []<>F & (F ~> G) --> []<>G" |
603 |
(fn _ => [Clarsimp_tac 1, |
|
604 |
etac ((temp_use InitDmd) RS |
|
605 |
((temp_unlift streett_leadsto) RS iffD2 RS mp)) 1, |
|
606 |
asm_simp_tac (simpset() addsimps [dmdInitD]) 1 |
|
3807 | 607 |
]); |
608 |
||
609 |
(* In particular, strong fairness is a Streett condition. The following |
|
610 |
rules are sometimes easier to use than WF2 or SF2 below. |
|
611 |
*) |
|
612 |
qed_goalw "leadsto_SF" TLA.thy [SF_def] |
|
6255 | 613 |
"|- (Enabled(<A>_v) ~> <A>_v) --> SF(A)_v" |
614 |
(K [clarsimp_tac (temp_css addSEs2 [leadsto_infinite]) 1]); |
|
3807 | 615 |
|
6255 | 616 |
qed_goal "leadsto_WF" TLA.thy |
617 |
"|- (Enabled(<A>_v) ~> <A>_v) --> WF(A)_v" |
|
618 |
(K [ clarsimp_tac (temp_css addSIs2 [SFImplWF, leadsto_SF]) 1 ]); |
|
3807 | 619 |
|
620 |
(* introduce an invariant into the proof of a leadsto assertion. |
|
6255 | 621 |
[]I --> ((P ~> Q) = (P /\ I ~> Q)) |
3807 | 622 |
*) |
6255 | 623 |
qed_goalw "INV_leadsto" TLA.thy [leadsto_def] |
624 |
"|- []I & (P & I ~> Q) --> (P ~> Q)" |
|
625 |
(fn _ => [Clarsimp_tac 1, |
|
626 |
etac STL4Edup 1, atac 1, |
|
627 |
auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_gen]) |
|
3807 | 628 |
]); |
629 |
||
6255 | 630 |
qed_goalw "leadsto_classical" TLA.thy [leadsto_def,dmd_def] |
631 |
"|- (Init F & []~G ~> G) --> (F ~> G)" |
|
632 |
(fn _ => [force_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E]) 1]); |
|
3807 | 633 |
|
6255 | 634 |
qed_goalw "leadsto_false" TLA.thy [leadsto_def] |
635 |
"|- (F ~> #False) = ([]~F)" |
|
636 |
(fn _ => [ simp_tac (simpset() addsimps [boxNotInitD]) 1 ]); |
|
637 |
||
638 |
qed_goalw "leadsto_exists" TLA.thy [leadsto_def] |
|
639 |
"|- ((? x. F x) ~> G) = (!x. (F x ~> G))" |
|
640 |
(K [auto_tac (temp_css addsimps2 allT::Init_simps addSEs2 [STL4E])]); |
|
641 |
||
3807 | 642 |
|
643 |
(* basic leadsto properties, cf. Unity *) |
|
644 |
||
6255 | 645 |
qed_goalw "ImplLeadsto_gen" TLA.thy [leadsto_def] |
646 |
"|- [](Init F --> Init G) --> (F ~> G)" |
|
647 |
(fn _ => [auto_tac (temp_css addSIs2 [InitDmd_gen] |
|
648 |
addSEs2 [STL4E_gen] addsimps2 Init_simps) |
|
3807 | 649 |
]); |
650 |
||
6255 | 651 |
bind_thm("ImplLeadsto", |
652 |
rewrite_rule Init_simps |
|
653 |
(read_instantiate [("'a","behavior"), ("'b","behavior")] ImplLeadsto_gen)); |
|
654 |
||
655 |
qed_goal "ImplLeadsto_simple" TLA.thy |
|
656 |
"|- F --> G ==> |- F ~> G" |
|
657 |
(fn [prem] => [auto_tac (temp_css addsimps2 [Init_def] |
|
658 |
addSIs2 [ImplLeadsto_gen,necT,prem])]); |
|
659 |
||
660 |
qed_goalw "EnsuresLeadsto" TLA.thy [leadsto_def] |
|
661 |
"|- A & $P --> Q` ==> |- []A --> (P ~> Q)" (fn [prem] => [ |
|
662 |
clarsimp_tac (temp_css addSEs2 [INV_leadsto]) 1, |
|
663 |
etac STL4E_gen 1, |
|
664 |
auto_tac (temp_css addsimps2 Init_defs |
|
665 |
addSIs2 [PrimeDmd, prem]) |
|
666 |
]); |
|
667 |
||
668 |
qed_goalw "EnsuresLeadsto2" TLA.thy [leadsto_def] |
|
669 |
"|- []($P --> Q`) --> (P ~> Q)" |
|
670 |
(fn _ => [Clarsimp_tac 1, |
|
671 |
etac STL4E_gen 1, |
|
672 |
auto_tac (temp_css addsimps2 Init_simps addSIs2 [PrimeDmd]) |
|
673 |
]); |
|
3807 | 674 |
|
6255 | 675 |
qed_goalw "ensures" TLA.thy [leadsto_def] |
676 |
"[| |- $P & N --> P` | Q`; \ |
|
677 |
\ |- ($P & N) & A --> Q` \ |
|
678 |
\ |] ==> |- []N & []([]P --> <>A) --> (P ~> Q)" |
|
679 |
(fn [p1,p2] => [Clarsimp_tac 1, |
|
680 |
etac STL4Edup 1, atac 1, |
|
681 |
Clarsimp_tac 1, |
|
682 |
subgoal_tac "sigmaa |= []($P --> P` | Q`)" 1, |
|
683 |
dtac (temp_use unless) 1, |
|
684 |
clarsimp_tac (temp_css addSDs2 [INV1]) 1, |
|
685 |
rtac ((temp_use (p2 RS DmdImpl)) RS (temp_use DmdPrime)) 1, |
|
686 |
force_tac (temp_css addSIs2 [BoxDmd_simple] |
|
687 |
addsimps2 [split_box_conj,box_stp_act]) 1, |
|
688 |
force_tac (temp_css addEs2 [STL4E] addDs2 [p1]) 1 |
|
689 |
]); |
|
690 |
||
691 |
qed_goal "ensures_simple" TLA.thy |
|
692 |
"[| |- $P & N --> P` | Q`; \ |
|
693 |
\ |- ($P & N) & A --> Q` \ |
|
694 |
\ |] ==> |- []N & []<>A --> (P ~> Q)" |
|
695 |
(fn prems => [Clarsimp_tac 1, |
|
696 |
rtac (temp_use ensures) 1, |
|
697 |
TRYALL (ares_tac prems), |
|
698 |
force_tac (temp_css addSEs2 [STL4E]) 1 |
|
699 |
]); |
|
700 |
||
3807 | 701 |
qed_goal "EnsuresInfinite" TLA.thy |
6255 | 702 |
"[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q" |
703 |
(fn prems => [REPEAT (resolve_tac (prems @ [temp_use leadsto_infinite, |
|
704 |
temp_use EnsuresLeadsto]) 1)]); |
|
705 |
||
3807 | 706 |
|
707 |
(*** Gronning's lattice rules (taken from TLP) ***) |
|
708 |
section "Lattice rules"; |
|
709 |
||
6255 | 710 |
qed_goalw "LatticeReflexivity" TLA.thy [leadsto_def] "|- F ~> F" |
711 |
(fn _ => [REPEAT (resolve_tac [necT,InitDmd_gen] 1)]); |
|
3807 | 712 |
|
6255 | 713 |
qed_goalw "LatticeTransitivity" TLA.thy [leadsto_def] |
714 |
"|- (G ~> H) & (F ~> G) --> (F ~> H)" |
|
715 |
(fn _ => [Clarsimp_tac 1, |
|
716 |
etac dup_boxE 1, (* [][](Init G --> H) *) |
|
3807 | 717 |
merge_box_tac 1, |
6255 | 718 |
clarsimp_tac (temp_css addSEs2 [STL4E]) 1, |
719 |
rtac dup_dmdD 1, |
|
720 |
subgoal_tac "sigmaa |= <>Init G" 1, |
|
721 |
etac DmdImpl2 1, atac 1, |
|
722 |
asm_simp_tac (simpset() addsimps [dmdInitD]) 1 |
|
3807 | 723 |
]); |
724 |
||
6255 | 725 |
qed_goalw "LatticeDisjunctionElim1" TLA.thy [leadsto_def] |
726 |
"|- (F | G ~> H) --> (F ~> H)" |
|
727 |
(fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E]) ]); |
|
3807 | 728 |
|
6255 | 729 |
qed_goalw "LatticeDisjunctionElim2" TLA.thy [leadsto_def] |
730 |
"|- (F | G ~> H) --> (G ~> H)" |
|
731 |
(fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E]) ]); |
|
3807 | 732 |
|
6255 | 733 |
qed_goalw "LatticeDisjunctionIntro" TLA.thy [leadsto_def] |
734 |
"|- (F ~> H) & (G ~> H) --> (F | G ~> H)" |
|
735 |
(fn _ => [Clarsimp_tac 1, |
|
736 |
merge_box_tac 1, |
|
737 |
auto_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E]) |
|
3807 | 738 |
]); |
739 |
||
6255 | 740 |
qed_goal "LatticeDisjunction" TLA.thy |
741 |
"|- (F | G ~> H) = ((F ~> H) & (G ~> H))" |
|
742 |
(fn _ => [auto_tac (temp_css addIs2 [LatticeDisjunctionIntro, |
|
743 |
LatticeDisjunctionElim1, LatticeDisjunctionElim2])]); |
|
744 |
||
3807 | 745 |
qed_goal "LatticeDiamond" TLA.thy |
6255 | 746 |
"|- (A ~> B | C) & (B ~> D) & (C ~> D) --> (A ~> D)" |
747 |
(fn _ => [Clarsimp_tac 1, |
|
748 |
subgoal_tac "sigma |= (B | C) ~> D" 1, |
|
749 |
eres_inst_tac [("G", "LIFT (B | C)")] (temp_use LatticeTransitivity) 1, |
|
3807 | 750 |
ALLGOALS (fast_tac (temp_cs addSIs [LatticeDisjunctionIntro])) |
751 |
]); |
|
752 |
||
753 |
qed_goal "LatticeTriangle" TLA.thy |
|
6255 | 754 |
"|- (A ~> D | B) & (B ~> D) --> (A ~> D)" |
755 |
(fn _ => [Clarsimp_tac 1, |
|
756 |
subgoal_tac "sigma |= (D | B) ~> D" 1, |
|
757 |
eres_inst_tac [("G", "LIFT (D | B)")] (temp_use LatticeTransitivity) 1, atac 1, |
|
758 |
auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] |
|
759 |
addIs2 [LatticeReflexivity]) |
|
760 |
]); |
|
761 |
||
762 |
qed_goal "LatticeTriangle2" TLA.thy |
|
763 |
"|- (A ~> B | D) & (B ~> D) --> (A ~> D)" |
|
764 |
(fn _ => [Clarsimp_tac 1, |
|
765 |
subgoal_tac "sigma |= B | D ~> D" 1, |
|
766 |
eres_inst_tac [("G", "LIFT (B | D)")] (temp_use LatticeTransitivity) 1, atac 1, |
|
767 |
auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] |
|
768 |
addIs2 [LatticeReflexivity]) |
|
3807 | 769 |
]); |
770 |
||
771 |
(*** Lamport's fairness rules ***) |
|
772 |
section "Fairness rules"; |
|
773 |
||
6255 | 774 |
qed_goal "WF1" TLA.thy |
775 |
"[| |- $P & N --> P` | Q`; \ |
|
776 |
\ |- ($P & N) & <A>_v --> Q`; \ |
|
777 |
\ |- $P & N --> $(Enabled(<A>_v)) |] \ |
|
778 |
\ ==> |- []N & WF(A)_v --> (P ~> Q)" (fn prems => [ |
|
779 |
clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1, |
|
780 |
rtac (temp_use ensures) 1, |
|
781 |
TRYALL (ares_tac prems), |
|
782 |
etac STL4Edup 1, atac 1, |
|
783 |
clarsimp_tac (temp_css addsimps2 [WF_def]) 1, |
|
784 |
rtac (temp_use STL2) 1, |
|
785 |
clarsimp_tac (temp_css addSEs2 [mp] addSIs2 [InitDmd]) 1, |
|
786 |
resolve_tac ((map temp_use (prems RL [STL4])) RL [box_stp_actD]) 1, |
|
787 |
asm_simp_tac (simpset() addsimps [split_box_conj,box_stp_actI]) 1 |
|
788 |
]); |
|
3807 | 789 |
|
790 |
(* Sometimes easier to use; designed for action B rather than state predicate Q *) |
|
6255 | 791 |
qed_goalw "WF_leadsto" TLA.thy [leadsto_def] |
792 |
"[| |- N & $P --> $Enabled (<A>_v); \ |
|
793 |
\ |- N & <A>_v --> B; \ |
|
794 |
\ |- [](N & [~A]_v) --> stable P |] \ |
|
795 |
\ ==> |- []N & WF(A)_v --> (P ~> B)" |
|
3807 | 796 |
(fn [prem1,prem2,prem3] |
6255 | 797 |
=> [clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1, |
3807 | 798 |
etac STL4Edup 1, atac 1, |
6255 | 799 |
Clarsimp_tac 1, |
800 |
rtac (temp_use (prem2 RS DmdImpl)) 1, |
|
801 |
rtac (temp_use BoxDmd_simple) 1, atac 1, |
|
3807 | 802 |
rtac classical 1, |
6255 | 803 |
rtac (temp_use STL2) 1, |
804 |
clarsimp_tac (temp_css addsimps2 [WF_def] addSEs2 [mp] addSIs2 [InitDmd]) 1, |
|
805 |
rtac ((temp_use (prem1 RS STL4)) RS box_stp_actD) 1, |
|
806 |
asm_simp_tac (simpset() addsimps [split_box_conj,box_stp_act]) 1, |
|
807 |
etac (temp_use INV1) 1, |
|
808 |
rtac (temp_use prem3) 1, |
|
809 |
asm_full_simp_tac (simpset() addsimps [split_box_conj,temp_use NotDmd,not_angle]) 1 |
|
3807 | 810 |
]); |
811 |
||
6255 | 812 |
qed_goal "SF1" TLA.thy |
813 |
"[| |- $P & N --> P` | Q`; \ |
|
814 |
\ |- ($P & N) & <A>_v --> Q`; \ |
|
815 |
\ |- []P & []N & []F --> <>Enabled(<A>_v) |] \ |
|
816 |
\ ==> |- []N & SF(A)_v & []F --> (P ~> Q)" |
|
817 |
(fn prems => [ |
|
818 |
clarsimp_tac (temp_css addSDs2 [BoxSFI]) 1, |
|
819 |
rtac (temp_use ensures) 1, |
|
820 |
TRYALL (ares_tac prems), |
|
821 |
eres_inst_tac [("F","F")] dup_boxE 1, |
|
822 |
merge_temp_box_tac 1, |
|
823 |
etac STL4Edup 1, atac 1, |
|
824 |
clarsimp_tac (temp_css addsimps2 [SF_def]) 1, |
|
825 |
rtac (temp_use STL2) 1, etac mp 1, |
|
826 |
resolve_tac (map temp_use (prems RL [STL4])) 1, |
|
827 |
asm_simp_tac (simpset() addsimps [split_box_conj, STL3]) 1 |
|
828 |
]); |
|
3807 | 829 |
|
830 |
qed_goal "WF2" TLA.thy |
|
6255 | 831 |
"[| |- N & <B>_f --> <M>_g; \ |
832 |
\ |- $P & P` & <N & A>_f --> B; \ |
|
833 |
\ |- P & Enabled(<M>_g) --> Enabled(<A>_f); \ |
|
834 |
\ |- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P |] \ |
|
835 |
\ ==> |- []N & WF(A)_f & []F --> WF(M)_g" |
|
836 |
(fn [prem1,prem2,prem3,prem4] => [ |
|
837 |
clarsimp_tac (temp_css addSDs2 [BoxWFI, (temp_use BoxDmdBox) RS iffD2] |
|
838 |
addsimps2 [read_instantiate [("A","M")] WF_def]) 1, |
|
839 |
eres_inst_tac [("F","F")] dup_boxE 1, |
|
840 |
merge_temp_box_tac 1, |
|
841 |
etac STL4Edup 1, atac 1, |
|
842 |
clarsimp_tac (temp_css addSIs2 [(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1, |
|
843 |
rtac classical 1, |
|
844 |
subgoal_tac "sigmaa |= <>(($P & P` & N) & <A>_f)" 1, |
|
845 |
force_tac (temp_css addsimps2 [angle_def] addSIs2 [prem2] addSEs2 [DmdImplE]) 1, |
|
846 |
rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1, |
|
847 |
asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1, |
|
848 |
merge_act_box_tac 1, |
|
849 |
forward_tac [temp_use prem4] 1, TRYALL atac, |
|
850 |
dtac (temp_use STL6) 1, atac 1, |
|
851 |
eres_inst_tac [("V","sigmaa |= <>[]P")] thin_rl 1, |
|
852 |
eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1, |
|
853 |
dtac (temp_use BoxWFI) 1, |
|
854 |
eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1, |
|
855 |
merge_temp_box_tac 1, |
|
856 |
etac DmdImpldup 1, atac 1, |
|
857 |
auto_tac (temp_css addsimps2 [split_box_conj,STL3,WF_Box,box_stp_act]), |
|
858 |
force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1, |
|
859 |
rtac (temp_use STL2) 1, |
|
860 |
force_tac (temp_css addsimps2 [WF_def,split_box_conj] addSEs2 [mp] |
|
861 |
addSIs2 [InitDmd, prem3 RS STL4]) 1 |
|
3807 | 862 |
]); |
863 |
||
864 |
qed_goal "SF2" TLA.thy |
|
6255 | 865 |
"[| |- N & <B>_f --> <M>_g; \ |
866 |
\ |- $P & P` & <N & A>_f --> B; \ |
|
867 |
\ |- P & Enabled(<M>_g) --> Enabled(<A>_f); \ |
|
868 |
\ |- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P |] \ |
|
869 |
\ ==> |- []N & SF(A)_f & []F --> SF(M)_g" |
|
870 |
(fn [prem1,prem2,prem3,prem4] => [ |
|
871 |
clarsimp_tac (temp_css addSDs2 [BoxSFI] |
|
872 |
addsimps2 [read_instantiate [("A","M")] SF_def]) 1, |
|
873 |
eres_inst_tac [("F","F")] dup_boxE 1, |
|
874 |
eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1, |
|
875 |
merge_temp_box_tac 1, |
|
876 |
etac STL4Edup 1, atac 1, |
|
877 |
clarsimp_tac (temp_css addSIs2 [(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1, |
|
878 |
rtac classical 1, |
|
879 |
subgoal_tac "sigmaa |= <>(($P & P` & N) & <A>_f)" 1, |
|
880 |
force_tac (temp_css addsimps2 [angle_def] addSIs2 [prem2] addSEs2 [DmdImplE]) 1, |
|
881 |
rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1, |
|
882 |
asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1, |
|
883 |
merge_act_box_tac 1, |
|
884 |
forward_tac [temp_use prem4] 1, TRYALL atac, |
|
885 |
eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1, |
|
886 |
dtac (temp_use BoxSFI) 1, |
|
887 |
eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1, |
|
888 |
eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1, |
|
889 |
merge_temp_box_tac 1, |
|
890 |
etac DmdImpldup 1, atac 1, |
|
891 |
auto_tac (temp_css addsimps2 [split_box_conj,STL3,SF_Box,box_stp_act]), |
|
892 |
force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1, |
|
893 |
rtac (temp_use STL2) 1, |
|
894 |
force_tac (temp_css addsimps2 [SF_def,split_box_conj] addSEs2 [mp,InfImpl] |
|
895 |
addSIs2 [prem3]) 1 |
|
3807 | 896 |
]); |
897 |
||
898 |
(* ------------------------------------------------------------------------- *) |
|
899 |
(*** Liveness proofs by well-founded orderings ***) |
|
900 |
(* ------------------------------------------------------------------------- *) |
|
901 |
section "Well-founded orderings"; |
|
902 |
||
6255 | 903 |
qed_goal "wf_leadsto" TLA.thy |
904 |
"[| wf r; \ |
|
905 |
\ !!x. sigma |= F x ~> (G | (? y. #((y,x):r) & F y)) \ |
|
906 |
\ |] ==> sigma |= F x ~> G" |
|
907 |
(fn p1::prems => |
|
908 |
[rtac (p1 RS wf_induct) 1, |
|
909 |
rtac (temp_use LatticeTriangle) 1, |
|
910 |
resolve_tac prems 1, |
|
911 |
auto_tac (temp_css addsimps2 [leadsto_exists]), |
|
912 |
case_tac "(y,x):r" 1, |
|
913 |
Force_tac 1, |
|
914 |
force_tac (temp_css addsimps2 leadsto_def::Init_simps addSIs2 [necT]) 1]); |
|
3807 | 915 |
|
916 |
(* If r is well-founded, state function v cannot decrease forever *) |
|
917 |
qed_goal "wf_not_box_decrease" TLA.thy |
|
6255 | 918 |
"!!r. wf r ==> |- [][ (v`, $v) : #r ]_v --> <>[][#False]_v" |
919 |
(fn _ => [Clarsimp_tac 1, |
|
920 |
rtac ccontr 1, |
|
921 |
subgoal_tac "sigma |= (? x. v=#x) ~> #False" 1, |
|
922 |
dtac ((temp_use leadsto_false) RS iffD1 RS (temp_use STL2_gen)) 1, |
|
923 |
force_tac (temp_css addsimps2 Init_defs) 1, |
|
924 |
clarsimp_tac (temp_css addsimps2 [leadsto_exists,not_square]@more_temp_simps) 1, |
|
925 |
etac wf_leadsto 1, |
|
926 |
rtac (temp_use ensures_simple) 1, TRYALL atac, |
|
927 |
auto_tac (temp_css addsimps2 [square_def,angle_def]) |
|
3807 | 928 |
]); |
929 |
||
6255 | 930 |
(* "wf r ==> |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *) |
3807 | 931 |
bind_thm("wf_not_dmd_box_decrease", |
932 |
standard(rewrite_rule more_temp_simps (wf_not_box_decrease RS DmdImpl))); |
|
933 |
||
6255 | 934 |
(* If there are infinitely many steps where v decreases, then there |
3807 | 935 |
have to be infinitely many non-stuttering steps where v doesn't decrease. |
936 |
*) |
|
937 |
qed_goal "wf_box_dmd_decrease" TLA.thy |
|
6255 | 938 |
"wf r ==> |- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v" |
939 |
(fn [prem] => [ |
|
940 |
Clarsimp_tac 1, |
|
941 |
rtac ccontr 1, |
|
942 |
asm_full_simp_tac (simpset() addsimps not_angle::more_temp_simps) 1, |
|
943 |
dtac (prem RS (temp_use wf_not_dmd_box_decrease)) 1, |
|
944 |
dtac (temp_use BoxDmdDmdBox) 1, atac 1, |
|
945 |
subgoal_tac "sigma |= []<>((#False)::action)" 1, |
|
946 |
Force_tac 1, |
|
947 |
etac STL4E 1, |
|
948 |
rtac DmdImpl 1, |
|
949 |
force_tac (temp_css addSEs2 [prem RS wf_irrefl]) 1 |
|
950 |
]); |
|
3807 | 951 |
|
952 |
(* In particular, for natural numbers, if n decreases infinitely often |
|
953 |
then it has to increase infinitely often. |
|
954 |
*) |
|
6255 | 955 |
qed_goal "nat_box_dmd_decrease" TLA.thy |
956 |
"!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)" |
|
957 |
(K [Clarsimp_tac 1, |
|
958 |
subgoal_tac "sigma |= []<><~( (n`,$n) : #less_than )>_n" 1, |
|
959 |
etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1, |
|
960 |
clarsimp_tac (temp_css addsimps2 [angle_def]) 1, |
|
961 |
rtac nat_less_cases 1, |
|
962 |
Auto_tac, |
|
963 |
rtac (temp_use wf_box_dmd_decrease) 1, |
|
964 |
auto_tac (temp_css addSEs2 [STL4E,DmdImplE]) |
|
965 |
]); |
|
966 |
||
3807 | 967 |
|
968 |
(* ------------------------------------------------------------------------- *) |
|
969 |
(*** Flexible quantification over state variables ***) |
|
970 |
(* ------------------------------------------------------------------------- *) |
|
971 |
section "Flexible quantification"; |
|
972 |
||
973 |
qed_goal "aallI" TLA.thy |
|
6255 | 974 |
"[| basevars vs; (!!x. basevars (x,vs) ==> sigma |= F x) |] ==> sigma |= (AALL x. F x)" |
975 |
(fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] |
|
976 |
addSIs2 prems addSDs2 prems)]); |
|
3807 | 977 |
|
6255 | 978 |
qed_goalw "aallE" TLA.thy [aall_def] "|- (AALL x. F x) --> F x" |
979 |
(K [Clarsimp_tac 1, etac swap 1, |
|
980 |
force_tac (temp_css addSIs2 [eexI]) 1]); |
|
3807 | 981 |
|
982 |
(* monotonicity of quantification *) |
|
983 |
qed_goal "eex_mono" TLA.thy |
|
6255 | 984 |
"[| sigma |= EEX x. F x; !!x. sigma |= F x --> G x |] ==> sigma |= EEX x. G x" |
985 |
(fn [min,maj] => [rtac (unit_base RS (min RS eexE)) 1, |
|
986 |
rtac (temp_use eexI) 1, |
|
987 |
etac ((rewrite_rule intensional_rews maj) RS mp) 1 |
|
3807 | 988 |
]); |
989 |
||
990 |
qed_goal "aall_mono" TLA.thy |
|
6255 | 991 |
"[| sigma |= AALL x. F(x); !!x. sigma |= F(x) --> G(x) |] ==> sigma |= AALL x. G(x)" |
992 |
(fn [min,maj] => [rtac (unit_base RS aallI) 1, |
|
993 |
rtac ((rewrite_rule intensional_rews maj) RS mp) 1, |
|
994 |
rtac (min RS (temp_use aallE)) 1 |
|
3807 | 995 |
]); |
996 |
||
6255 | 997 |
(* Derived history introduction rule *) |
998 |
qed_goal "historyI" TLA.thy |
|
999 |
"[| sigma |= Init I; sigma |= []N; basevars vs; \ |
|
1000 |
\ (!!h. basevars(h,vs) ==> |- I & h = ha --> HI h); \ |
|
1001 |
\ (!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)) \ |
|
1002 |
\ |] ==> sigma |= EEX h. Init (HI h) & [](HN h)" |
|
1003 |
(fn [p1,p2,p3,p4,p5] |
|
1004 |
=> [rtac ((temp_use history) RS eexE) 1, |
|
1005 |
rtac p3 1, |
|
1006 |
rtac (temp_use eexI) 1, |
|
1007 |
Clarsimp_tac 1, rtac conjI 1, |
|
1008 |
cut_facts_tac [p2] 2, |
|
1009 |
merge_box_tac 2, |
|
1010 |
force_tac (temp_css addSEs2 [STL4E,p5]) 2, |
|
1011 |
cut_facts_tac [p1] 1, |
|
1012 |
force_tac (temp_css addsimps2 Init_defs addSEs2 [p4]) 1 |
|
1013 |
]); |
|
1014 |
||
3807 | 1015 |
(* ---------------------------------------------------------------------- |
1016 |
example of a history variable: existence of a clock |
|
1017 |
||
6255 | 1018 |
Goal "|- EEX h. Init(h = #True) & [](h` = (~$h))"; |
4423 | 1019 |
by (rtac tempI 1); |
1020 |
by (rtac historyI 1); |
|
6255 | 1021 |
by (REPEAT (force_tac (temp_css addsimps2 Init_defs addIs2 [unit_base, necT]) 1)); |
3807 | 1022 |
(** solved **) |
1023 |
||
1024 |
---------------------------------------------------------------------- *) |
|
6255 | 1025 |