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