author | haftmann |
Fri, 01 Nov 2013 18:51:14 +0100 | |
changeset 54230 | b1d955791529 |
parent 51717 | 9e7d1c139569 |
child 54742 | 7a86358a3c0b |
permissions | -rw-r--r-- |
35108 | 1 |
(* Title: HOL/TLA/TLA.thy |
2 |
Author: Stephan Merz |
|
3 |
Copyright: 1998 University of Munich |
|
21624 | 4 |
*) |
3807 | 5 |
|
21624 | 6 |
header {* The temporal level of TLA *} |
3807 | 7 |
|
17309 | 8 |
theory TLA |
9 |
imports Init |
|
10 |
begin |
|
3807 | 11 |
|
12 |
consts |
|
6255 | 13 |
(** abstract syntax **) |
17309 | 14 |
Box :: "('w::world) form => temporal" |
15 |
Dmd :: "('w::world) form => temporal" |
|
16 |
leadsto :: "['w::world form, 'v::world form] => temporal" |
|
17 |
Stable :: "stpred => temporal" |
|
18 |
WF :: "[action, 'a stfun] => temporal" |
|
19 |
SF :: "[action, 'a stfun] => temporal" |
|
3807 | 20 |
|
21 |
(* Quantification over (flexible) state variables *) |
|
17309 | 22 |
EEx :: "('a stfun => temporal) => temporal" (binder "Eex " 10) |
23 |
AAll :: "('a stfun => temporal) => temporal" (binder "Aall " 10) |
|
6255 | 24 |
|
25 |
(** concrete syntax **) |
|
26 |
syntax |
|
17309 | 27 |
"_Box" :: "lift => lift" ("([]_)" [40] 40) |
28 |
"_Dmd" :: "lift => lift" ("(<>_)" [40] 40) |
|
29 |
"_leadsto" :: "[lift,lift] => lift" ("(_ ~> _)" [23,22] 22) |
|
30 |
"_stable" :: "lift => lift" ("(stable/ _)") |
|
31 |
"_WF" :: "[lift,lift] => lift" ("(WF'(_')'_(_))" [0,60] 55) |
|
32 |
"_SF" :: "[lift,lift] => lift" ("(SF'(_')'_(_))" [0,60] 55) |
|
6255 | 33 |
|
17309 | 34 |
"_EEx" :: "[idts, lift] => lift" ("(3EEX _./ _)" [0,10] 10) |
35 |
"_AAll" :: "[idts, lift] => lift" ("(3AALL _./ _)" [0,10] 10) |
|
3807 | 36 |
|
37 |
translations |
|
35068 | 38 |
"_Box" == "CONST Box" |
39 |
"_Dmd" == "CONST Dmd" |
|
40 |
"_leadsto" == "CONST leadsto" |
|
41 |
"_stable" == "CONST Stable" |
|
42 |
"_WF" == "CONST WF" |
|
43 |
"_SF" == "CONST SF" |
|
6255 | 44 |
"_EEx v A" == "Eex v. A" |
45 |
"_AAll v A" == "Aall v. A" |
|
46 |
||
47 |
"sigma |= []F" <= "_Box F sigma" |
|
48 |
"sigma |= <>F" <= "_Dmd F sigma" |
|
49 |
"sigma |= F ~> G" <= "_leadsto F G sigma" |
|
50 |
"sigma |= stable P" <= "_stable P sigma" |
|
51 |
"sigma |= WF(A)_v" <= "_WF A v sigma" |
|
52 |
"sigma |= SF(A)_v" <= "_SF A v sigma" |
|
53 |
"sigma |= EEX x. F" <= "_EEx x F sigma" |
|
54 |
"sigma |= AALL x. F" <= "_AAll x F sigma" |
|
3807 | 55 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9517
diff
changeset
|
56 |
syntax (xsymbols) |
17309 | 57 |
"_Box" :: "lift => lift" ("(\<box>_)" [40] 40) |
58 |
"_Dmd" :: "lift => lift" ("(\<diamond>_)" [40] 40) |
|
59 |
"_leadsto" :: "[lift,lift] => lift" ("(_ \<leadsto> _)" [23,22] 22) |
|
60 |
"_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10) |
|
61 |
"_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10) |
|
3808 | 62 |
|
14565 | 63 |
syntax (HTML output) |
17309 | 64 |
"_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10) |
65 |
"_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10) |
|
14565 | 66 |
|
47968 | 67 |
axiomatization where |
6255 | 68 |
(* Definitions of derived operators *) |
47968 | 69 |
dmd_def: "\<And>F. TEMP <>F == TEMP ~[]~F" |
70 |
||
71 |
axiomatization where |
|
72 |
boxInit: "\<And>F. TEMP []F == TEMP []Init F" and |
|
73 |
leadsto_def: "\<And>F G. TEMP F ~> G == TEMP [](Init F --> <>G)" and |
|
74 |
stable_def: "\<And>P. TEMP stable P == TEMP []($P --> P$)" and |
|
75 |
WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v" and |
|
76 |
SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v" and |
|
17309 | 77 |
aall_def: "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)" |
3807 | 78 |
|
47968 | 79 |
axiomatization where |
6255 | 80 |
(* Base axioms for raw TLA. *) |
47968 | 81 |
normalT: "\<And>F G. |- [](F --> G) --> ([]F --> []G)" and (* polymorphic *) |
82 |
reflT: "\<And>F. |- []F --> F" and (* F::temporal *) |
|
83 |
transT: "\<And>F. |- []F --> [][]F" and (* polymorphic *) |
|
84 |
linT: "\<And>F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and |
|
85 |
discT: "\<And>F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and |
|
86 |
primeI: "\<And>P. |- []P --> Init P`" and |
|
87 |
primeE: "\<And>P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and |
|
88 |
indT: "\<And>P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and |
|
89 |
allT: "\<And>F. |- (ALL x. [](F x)) = ([](ALL x. F x))" |
|
3807 | 90 |
|
47968 | 91 |
axiomatization where |
92 |
necT: "\<And>F. |- F ==> |- []F" (* polymorphic *) |
|
3807 | 93 |
|
47968 | 94 |
axiomatization where |
3807 | 95 |
(* Flexible quantification: refinement mappings, history variables *) |
47968 | 96 |
eexI: "|- F x --> (EEX x. F x)" and |
17309 | 97 |
eexE: "[| sigma |= (EEX x. F x); basevars vs; |
98 |
(!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) |
|
47968 | 99 |
|] ==> G sigma" and |
17309 | 100 |
history: "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)" |
101 |
||
21624 | 102 |
|
103 |
(* Specialize intensional introduction/elimination rules for temporal formulas *) |
|
104 |
||
51668 | 105 |
lemma tempI [intro!]: "(!!sigma. sigma |= (F::temporal)) ==> |- F" |
21624 | 106 |
apply (rule intI) |
107 |
apply (erule meta_spec) |
|
108 |
done |
|
109 |
||
51668 | 110 |
lemma tempD [dest]: "|- (F::temporal) ==> sigma |= F" |
21624 | 111 |
by (erule intD) |
112 |
||
113 |
||
114 |
(* ======== Functions to "unlift" temporal theorems ====== *) |
|
115 |
||
116 |
ML {* |
|
117 |
(* The following functions are specialized versions of the corresponding |
|
118 |
functions defined in theory Intensional in that they introduce a |
|
119 |
"world" parameter of type "behavior". |
|
120 |
*) |
|
121 |
fun temp_unlift th = |
|
26305 | 122 |
(rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th; |
21624 | 123 |
|
124 |
(* Turn |- F = G into meta-level rewrite rule F == G *) |
|
125 |
val temp_rewrite = int_rewrite |
|
126 |
||
127 |
fun temp_use th = |
|
128 |
case (concl_of th) of |
|
26305 | 129 |
Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) => |
21624 | 130 |
((flatten (temp_unlift th)) handle THM _ => th) |
131 |
| _ => th; |
|
132 |
||
133 |
fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th; |
|
134 |
*} |
|
135 |
||
42814 | 136 |
attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} |
137 |
attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} |
|
138 |
attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} |
|
139 |
attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} |
|
30528 | 140 |
|
21624 | 141 |
|
142 |
(* ------------------------------------------------------------------------- *) |
|
143 |
(*** "Simple temporal logic": only [] and <> ***) |
|
144 |
(* ------------------------------------------------------------------------- *) |
|
145 |
section "Simple temporal logic" |
|
146 |
||
147 |
(* []~F == []~Init F *) |
|
45605 | 148 |
lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F |
21624 | 149 |
|
150 |
lemma dmdInit: "TEMP <>F == TEMP <> Init F" |
|
151 |
apply (unfold dmd_def) |
|
152 |
apply (unfold boxInit [of "LIFT ~F"]) |
|
153 |
apply (simp (no_asm) add: Init_simps) |
|
154 |
done |
|
155 |
||
45605 | 156 |
lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F |
21624 | 157 |
|
158 |
(* boxInit and dmdInit cannot be used as rewrites, because they loop. |
|
159 |
Non-looping instances for state predicates and actions are occasionally useful. |
|
160 |
*) |
|
45605 | 161 |
lemmas boxInit_stp = boxInit [where 'a = state] |
162 |
lemmas boxInit_act = boxInit [where 'a = "state * state"] |
|
163 |
lemmas dmdInit_stp = dmdInit [where 'a = state] |
|
164 |
lemmas dmdInit_act = dmdInit [where 'a = "state * state"] |
|
21624 | 165 |
|
166 |
(* The symmetric equations can be used to get rid of Init *) |
|
167 |
lemmas boxInitD = boxInit [symmetric] |
|
168 |
lemmas dmdInitD = dmdInit [symmetric] |
|
169 |
lemmas boxNotInitD = boxNotInit [symmetric] |
|
170 |
lemmas dmdNotInitD = dmdNotInit [symmetric] |
|
171 |
||
172 |
lemmas Init_simps = Init_simps boxInitD dmdInitD boxNotInitD dmdNotInitD |
|
173 |
||
174 |
(* ------------------------ STL2 ------------------------------------------- *) |
|
175 |
lemmas STL2 = reflT |
|
176 |
||
177 |
(* The "polymorphic" (generic) variant *) |
|
178 |
lemma STL2_gen: "|- []F --> Init F" |
|
179 |
apply (unfold boxInit [of F]) |
|
180 |
apply (rule STL2) |
|
181 |
done |
|
182 |
||
183 |
(* see also STL2_pr below: "|- []P --> Init P & Init (P`)" *) |
|
184 |
||
185 |
||
186 |
(* Dual versions for <> *) |
|
187 |
lemma InitDmd: "|- F --> <> F" |
|
188 |
apply (unfold dmd_def) |
|
189 |
apply (auto dest!: STL2 [temp_use]) |
|
190 |
done |
|
191 |
||
192 |
lemma InitDmd_gen: "|- Init F --> <>F" |
|
193 |
apply clarsimp |
|
194 |
apply (drule InitDmd [temp_use]) |
|
195 |
apply (simp add: dmdInitD) |
|
196 |
done |
|
197 |
||
198 |
||
199 |
(* ------------------------ STL3 ------------------------------------------- *) |
|
200 |
lemma STL3: "|- ([][]F) = ([]F)" |
|
201 |
by (auto elim: transT [temp_use] STL2 [temp_use]) |
|
202 |
||
203 |
(* corresponding elimination rule introduces double boxes: |
|
204 |
[| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W |
|
205 |
*) |
|
206 |
lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format] |
|
45605 | 207 |
lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1] |
21624 | 208 |
|
209 |
(* dual versions for <> *) |
|
210 |
lemma DmdDmd: "|- (<><>F) = (<>F)" |
|
211 |
by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite]) |
|
212 |
||
213 |
lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format] |
|
45605 | 214 |
lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1] |
21624 | 215 |
|
216 |
||
217 |
(* ------------------------ STL4 ------------------------------------------- *) |
|
218 |
lemma STL4: |
|
219 |
assumes "|- F --> G" |
|
220 |
shows "|- []F --> []G" |
|
221 |
apply clarsimp |
|
222 |
apply (rule normalT [temp_use]) |
|
223 |
apply (rule assms [THEN necT, temp_use]) |
|
224 |
apply assumption |
|
225 |
done |
|
226 |
||
227 |
(* Unlifted version as an elimination rule *) |
|
228 |
lemma STL4E: "[| sigma |= []F; |- F --> G |] ==> sigma |= []G" |
|
229 |
by (erule (1) STL4 [temp_use]) |
|
230 |
||
231 |
lemma STL4_gen: "|- Init F --> Init G ==> |- []F --> []G" |
|
232 |
apply (drule STL4) |
|
233 |
apply (simp add: boxInitD) |
|
234 |
done |
|
235 |
||
236 |
lemma STL4E_gen: "[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G" |
|
237 |
by (erule (1) STL4_gen [temp_use]) |
|
238 |
||
239 |
(* see also STL4Edup below, which allows an auxiliary boxed formula: |
|
240 |
[]A /\ F => G |
|
241 |
----------------- |
|
242 |
[]A /\ []F => []G |
|
243 |
*) |
|
244 |
||
245 |
(* The dual versions for <> *) |
|
246 |
lemma DmdImpl: |
|
247 |
assumes prem: "|- F --> G" |
|
248 |
shows "|- <>F --> <>G" |
|
249 |
apply (unfold dmd_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
250 |
apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use]) |
21624 | 251 |
done |
252 |
||
253 |
lemma DmdImplE: "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G" |
|
254 |
by (erule (1) DmdImpl [temp_use]) |
|
255 |
||
256 |
(* ------------------------ STL5 ------------------------------------------- *) |
|
257 |
lemma STL5: "|- ([]F & []G) = ([](F & G))" |
|
258 |
apply auto |
|
259 |
apply (subgoal_tac "sigma |= [] (G --> (F & G))") |
|
260 |
apply (erule normalT [temp_use]) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
261 |
apply (fastforce elim!: STL4E [temp_use])+ |
21624 | 262 |
done |
263 |
||
264 |
(* rewrite rule to split conjunctions under boxes *) |
|
45605 | 265 |
lemmas split_box_conj = STL5 [temp_unlift, symmetric] |
21624 | 266 |
|
267 |
||
268 |
(* the corresponding elimination rule allows to combine boxes in the hypotheses |
|
269 |
(NB: F and G must have the same type, i.e., both actions or temporals.) |
|
270 |
Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop! |
|
271 |
*) |
|
272 |
lemma box_conjE: |
|
273 |
assumes "sigma |= []F" |
|
274 |
and "sigma |= []G" |
|
275 |
and "sigma |= [](F&G) ==> PROP R" |
|
276 |
shows "PROP R" |
|
277 |
by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+ |
|
278 |
||
279 |
(* Instances of box_conjE for state predicates, actions, and temporals |
|
280 |
in case the general rule is "too polymorphic". |
|
281 |
*) |
|
45605 | 282 |
lemmas box_conjE_temp = box_conjE [where 'a = behavior] |
283 |
lemmas box_conjE_stp = box_conjE [where 'a = state] |
|
284 |
lemmas box_conjE_act = box_conjE [where 'a = "state * state"] |
|
21624 | 285 |
|
286 |
(* Define a tactic that tries to merge all boxes in an antecedent. The definition is |
|
287 |
a bit kludgy in order to simulate "double elim-resolution". |
|
288 |
*) |
|
289 |
||
290 |
lemma box_thin: "[| sigma |= []F; PROP W |] ==> PROP W" . |
|
291 |
||
292 |
ML {* |
|
293 |
fun merge_box_tac i = |
|
26305 | 294 |
REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i]) |
21624 | 295 |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26305
diff
changeset
|
296 |
fun merge_temp_box_tac ctxt i = |
26305 | 297 |
REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i, |
27239 | 298 |
eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i]) |
21624 | 299 |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26305
diff
changeset
|
300 |
fun merge_stp_box_tac ctxt i = |
26305 | 301 |
REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i, |
27239 | 302 |
eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i]) |
21624 | 303 |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26305
diff
changeset
|
304 |
fun merge_act_box_tac ctxt i = |
26305 | 305 |
REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i, |
27239 | 306 |
eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i]) |
21624 | 307 |
*} |
308 |
||
42814 | 309 |
method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} |
310 |
method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *} |
|
311 |
method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *} |
|
312 |
method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} |
|
42787 | 313 |
|
21624 | 314 |
(* rewrite rule to push universal quantification through box: |
315 |
(sigma |= [](! x. F x)) = (! x. (sigma |= []F x)) |
|
316 |
*) |
|
45605 | 317 |
lemmas all_box = allT [temp_unlift, symmetric] |
21624 | 318 |
|
319 |
lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)" |
|
320 |
apply (auto simp add: dmd_def split_box_conj [try_rewrite]) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
321 |
apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+ |
21624 | 322 |
done |
323 |
||
324 |
lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))" |
|
325 |
by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite]) |
|
326 |
||
45605 | 327 |
lemmas ex_dmd = exT [temp_unlift, symmetric] |
21624 | 328 |
|
329 |
lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G" |
|
330 |
apply (erule dup_boxE) |
|
42787 | 331 |
apply merge_box |
21624 | 332 |
apply (erule STL4E) |
333 |
apply assumption |
|
334 |
done |
|
335 |
||
336 |
lemma DmdImpl2: |
|
337 |
"!!sigma. [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G" |
|
338 |
apply (unfold dmd_def) |
|
339 |
apply auto |
|
340 |
apply (erule notE) |
|
42787 | 341 |
apply merge_box |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
342 |
apply (fastforce elim!: STL4E [temp_use]) |
21624 | 343 |
done |
344 |
||
345 |
lemma InfImpl: |
|
346 |
assumes 1: "sigma |= []<>F" |
|
347 |
and 2: "sigma |= []G" |
|
348 |
and 3: "|- F & G --> H" |
|
349 |
shows "sigma |= []<>H" |
|
350 |
apply (insert 1 2) |
|
351 |
apply (erule_tac F = G in dup_boxE) |
|
42787 | 352 |
apply merge_box |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
353 |
apply (fastforce elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use]) |
21624 | 354 |
done |
355 |
||
356 |
(* ------------------------ STL6 ------------------------------------------- *) |
|
357 |
(* Used in the proof of STL6, but useful in itself. *) |
|
358 |
lemma BoxDmd: "|- []F & <>G --> <>([]F & G)" |
|
359 |
apply (unfold dmd_def) |
|
360 |
apply clarsimp |
|
361 |
apply (erule dup_boxE) |
|
42787 | 362 |
apply merge_box |
21624 | 363 |
apply (erule contrapos_np) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
364 |
apply (fastforce elim!: STL4E [temp_use]) |
21624 | 365 |
done |
366 |
||
367 |
(* weaker than BoxDmd, but more polymorphic (and often just right) *) |
|
368 |
lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)" |
|
369 |
apply (unfold dmd_def) |
|
370 |
apply clarsimp |
|
42787 | 371 |
apply merge_box |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
372 |
apply (fastforce elim!: notE STL4E [temp_use]) |
21624 | 373 |
done |
374 |
||
375 |
lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)" |
|
376 |
apply (unfold dmd_def) |
|
377 |
apply clarsimp |
|
42787 | 378 |
apply merge_box |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
379 |
apply (fastforce elim!: notE STL4E [temp_use]) |
21624 | 380 |
done |
381 |
||
382 |
lemma DmdImpldup: |
|
383 |
assumes 1: "sigma |= []A" |
|
384 |
and 2: "sigma |= <>F" |
|
385 |
and 3: "|- []A & F --> G" |
|
386 |
shows "sigma |= <>G" |
|
387 |
apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE]) |
|
388 |
apply (rule 3) |
|
389 |
done |
|
390 |
||
391 |
lemma STL6: "|- <>[]F & <>[]G --> <>[](F & G)" |
|
392 |
apply (auto simp: STL5 [temp_rewrite, symmetric]) |
|
393 |
apply (drule linT [temp_use]) |
|
394 |
apply assumption |
|
395 |
apply (erule thin_rl) |
|
396 |
apply (rule DmdDmd [temp_unlift, THEN iffD1]) |
|
397 |
apply (erule disjE) |
|
398 |
apply (erule DmdImplE) |
|
399 |
apply (rule BoxDmd) |
|
400 |
apply (erule DmdImplE) |
|
401 |
apply auto |
|
402 |
apply (drule BoxDmd [temp_use]) |
|
403 |
apply assumption |
|
404 |
apply (erule thin_rl) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
405 |
apply (fastforce elim!: DmdImplE [temp_use]) |
21624 | 406 |
done |
407 |
||
408 |
||
409 |
(* ------------------------ True / False ----------------------------------------- *) |
|
410 |
section "Simplification of constants" |
|
411 |
||
412 |
lemma BoxConst: "|- ([]#P) = #P" |
|
413 |
apply (rule tempI) |
|
414 |
apply (cases P) |
|
415 |
apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps) |
|
416 |
done |
|
417 |
||
418 |
lemma DmdConst: "|- (<>#P) = #P" |
|
419 |
apply (unfold dmd_def) |
|
420 |
apply (cases P) |
|
421 |
apply (simp_all add: BoxConst [try_rewrite]) |
|
422 |
done |
|
423 |
||
424 |
lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst |
|
425 |
||
426 |
||
427 |
(* ------------------------ Further rewrites ----------------------------------------- *) |
|
428 |
section "Further rewrites" |
|
429 |
||
430 |
lemma NotBox: "|- (~[]F) = (<>~F)" |
|
431 |
by (simp add: dmd_def) |
|
432 |
||
433 |
lemma NotDmd: "|- (~<>F) = ([]~F)" |
|
434 |
by (simp add: dmd_def) |
|
435 |
||
436 |
(* These are not declared by default, because they could be harmful, |
|
437 |
e.g. []F & ~[]F becomes []F & <>~F !! *) |
|
26305 | 438 |
lemmas more_temp_simps1 = |
21624 | 439 |
STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite] |
440 |
NotBox [temp_unlift, THEN eq_reflection] |
|
441 |
NotDmd [temp_unlift, THEN eq_reflection] |
|
442 |
||
443 |
lemma BoxDmdBox: "|- ([]<>[]F) = (<>[]F)" |
|
444 |
apply (auto dest!: STL2 [temp_use]) |
|
445 |
apply (rule ccontr) |
|
446 |
apply (subgoal_tac "sigma |= <>[][]F & <>[]~[]F") |
|
447 |
apply (erule thin_rl) |
|
448 |
apply auto |
|
449 |
apply (drule STL6 [temp_use]) |
|
450 |
apply assumption |
|
451 |
apply simp |
|
26305 | 452 |
apply (simp_all add: more_temp_simps1) |
21624 | 453 |
done |
454 |
||
455 |
lemma DmdBoxDmd: "|- (<>[]<>F) = ([]<>F)" |
|
456 |
apply (unfold dmd_def) |
|
457 |
apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite]) |
|
458 |
done |
|
459 |
||
26305 | 460 |
lemmas more_temp_simps2 = more_temp_simps1 BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite] |
21624 | 461 |
|
462 |
||
463 |
(* ------------------------ Miscellaneous ----------------------------------- *) |
|
464 |
||
465 |
lemma BoxOr: "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
466 |
by (fastforce elim!: STL4E [temp_use]) |
21624 | 467 |
|
468 |
(* "persistently implies infinitely often" *) |
|
469 |
lemma DBImplBD: "|- <>[]F --> []<>F" |
|
470 |
apply clarsimp |
|
471 |
apply (rule ccontr) |
|
26305 | 472 |
apply (simp add: more_temp_simps2) |
21624 | 473 |
apply (drule STL6 [temp_use]) |
474 |
apply assumption |
|
475 |
apply simp |
|
476 |
done |
|
477 |
||
478 |
lemma BoxDmdDmdBox: "|- []<>F & <>[]G --> []<>(F & G)" |
|
479 |
apply clarsimp |
|
480 |
apply (rule ccontr) |
|
26305 | 481 |
apply (unfold more_temp_simps2) |
21624 | 482 |
apply (drule STL6 [temp_use]) |
483 |
apply assumption |
|
484 |
apply (subgoal_tac "sigma |= <>[]~F") |
|
485 |
apply (force simp: dmd_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
486 |
apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use]) |
21624 | 487 |
done |
488 |
||
489 |
||
490 |
(* ------------------------------------------------------------------------- *) |
|
491 |
(*** TLA-specific theorems: primed formulas ***) |
|
492 |
(* ------------------------------------------------------------------------- *) |
|
493 |
section "priming" |
|
494 |
||
495 |
(* ------------------------ TLA2 ------------------------------------------- *) |
|
496 |
lemma STL2_pr: "|- []P --> Init P & Init P`" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
497 |
by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use]) |
21624 | 498 |
|
499 |
(* Auxiliary lemma allows priming of boxed actions *) |
|
500 |
lemma BoxPrime: "|- []P --> []($P & P$)" |
|
501 |
apply clarsimp |
|
502 |
apply (erule dup_boxE) |
|
503 |
apply (unfold boxInit_act) |
|
504 |
apply (erule STL4E) |
|
505 |
apply (auto simp: Init_simps dest!: STL2_pr [temp_use]) |
|
506 |
done |
|
507 |
||
508 |
lemma TLA2: |
|
509 |
assumes "|- $P & P$ --> A" |
|
510 |
shows "|- []P --> []A" |
|
511 |
apply clarsimp |
|
512 |
apply (drule BoxPrime [temp_use]) |
|
41529 | 513 |
apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use] |
21624 | 514 |
elim!: STL4E [temp_use]) |
515 |
done |
|
516 |
||
517 |
lemma TLA2E: "[| sigma |= []P; |- $P & P$ --> A |] ==> sigma |= []A" |
|
518 |
by (erule (1) TLA2 [temp_use]) |
|
519 |
||
520 |
lemma DmdPrime: "|- (<>P`) --> (<>P)" |
|
521 |
apply (unfold dmd_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
522 |
apply (fastforce elim!: TLA2E [temp_use]) |
21624 | 523 |
done |
524 |
||
45605 | 525 |
lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use]] |
21624 | 526 |
|
527 |
(* ------------------------ INV1, stable --------------------------------------- *) |
|
528 |
section "stable, invariant" |
|
529 |
||
530 |
lemma ind_rule: |
|
531 |
"[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |] |
|
532 |
==> sigma |= []F" |
|
533 |
apply (rule indT [temp_use]) |
|
534 |
apply (erule (2) STL4E) |
|
535 |
done |
|
536 |
||
537 |
lemma box_stp_act: "|- ([]$P) = ([]P)" |
|
538 |
by (simp add: boxInit_act Init_simps) |
|
539 |
||
45605 | 540 |
lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2] |
541 |
lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1] |
|
21624 | 542 |
|
26305 | 543 |
lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2 |
21624 | 544 |
|
545 |
lemma INV1: |
|
546 |
"|- (Init P) --> (stable P) --> []P" |
|
547 |
apply (unfold stable_def boxInit_stp boxInit_act) |
|
548 |
apply clarsimp |
|
549 |
apply (erule ind_rule) |
|
550 |
apply (auto simp: Init_simps elim: ind_rule) |
|
551 |
done |
|
552 |
||
553 |
lemma StableT: |
|
554 |
"!!P. |- $P & A --> P` ==> |- []A --> stable P" |
|
555 |
apply (unfold stable_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
556 |
apply (fastforce elim!: STL4E [temp_use]) |
21624 | 557 |
done |
558 |
||
559 |
lemma Stable: "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P" |
|
560 |
by (erule (1) StableT [temp_use]) |
|
561 |
||
562 |
(* Generalization of INV1 *) |
|
563 |
lemma StableBox: "|- (stable P) --> [](Init P --> []P)" |
|
564 |
apply (unfold stable_def) |
|
565 |
apply clarsimp |
|
566 |
apply (erule dup_boxE) |
|
567 |
apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use]) |
|
568 |
done |
|
569 |
||
570 |
lemma DmdStable: "|- (stable P) & <>P --> <>[]P" |
|
571 |
apply clarsimp |
|
572 |
apply (rule DmdImpl2) |
|
573 |
prefer 2 |
|
574 |
apply (erule StableBox [temp_use]) |
|
575 |
apply (simp add: dmdInitD) |
|
576 |
done |
|
577 |
||
578 |
(* ---------------- (Semi-)automatic invariant tactics ---------------------- *) |
|
579 |
||
580 |
ML {* |
|
581 |
(* inv_tac reduces goals of the form ... ==> sigma |= []P *) |
|
42793 | 582 |
fun inv_tac ctxt = |
583 |
SELECT_GOAL |
|
584 |
(EVERY |
|
585 |
[auto_tac ctxt, |
|
586 |
TRY (merge_box_tac 1), |
|
587 |
rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *) |
|
588 |
TRYALL (etac @{thm Stable})]); |
|
21624 | 589 |
|
590 |
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals |
|
591 |
in simple cases it may be able to handle goals like |- MyProg --> []Inv. |
|
592 |
In these simple cases the simplifier seems to be more useful than the |
|
593 |
auto-tactic, which applies too much propositional logic and simplifies |
|
594 |
too late. |
|
595 |
*) |
|
42803 | 596 |
fun auto_inv_tac ctxt = |
42793 | 597 |
SELECT_GOAL |
42803 | 598 |
(inv_tac ctxt 1 THEN |
42793 | 599 |
(TRYALL (action_simp_tac |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51668
diff
changeset
|
600 |
(ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}]))); |
21624 | 601 |
*} |
602 |
||
42769 | 603 |
method_setup invariant = {* |
42793 | 604 |
Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac)) |
42814 | 605 |
*} |
42769 | 606 |
|
607 |
method_setup auto_invariant = {* |
|
42803 | 608 |
Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac)) |
42814 | 609 |
*} |
42769 | 610 |
|
21624 | 611 |
lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q" |
612 |
apply (unfold dmd_def) |
|
613 |
apply (clarsimp dest!: BoxPrime [temp_use]) |
|
42787 | 614 |
apply merge_box |
21624 | 615 |
apply (erule contrapos_np) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
616 |
apply (fastforce elim!: Stable [temp_use]) |
21624 | 617 |
done |
618 |
||
619 |
||
620 |
(* --------------------- Recursive expansions --------------------------------------- *) |
|
621 |
section "recursive expansions" |
|
622 |
||
623 |
(* Recursive expansions of [] and <> for state predicates *) |
|
624 |
lemma BoxRec: "|- ([]P) = (Init P & []P`)" |
|
625 |
apply (auto intro!: STL2_gen [temp_use]) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
626 |
apply (fastforce elim!: TLA2E [temp_use]) |
21624 | 627 |
apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use]) |
628 |
done |
|
629 |
||
630 |
lemma DmdRec: "|- (<>P) = (Init P | <>P`)" |
|
631 |
apply (unfold dmd_def BoxRec [temp_rewrite]) |
|
632 |
apply (auto simp: Init_simps) |
|
633 |
done |
|
634 |
||
635 |
lemma DmdRec2: "!!sigma. [| sigma |= <>P; sigma |= []~P` |] ==> sigma |= Init P" |
|
636 |
apply (force simp: DmdRec [temp_rewrite] dmd_def) |
|
637 |
done |
|
638 |
||
639 |
lemma InfinitePrime: "|- ([]<>P) = ([]<>P`)" |
|
640 |
apply auto |
|
641 |
apply (rule classical) |
|
642 |
apply (rule DBImplBD [temp_use]) |
|
643 |
apply (subgoal_tac "sigma |= <>[]P") |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
644 |
apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use]) |
21624 | 645 |
apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)") |
646 |
apply (force simp: boxInit_stp [temp_use] |
|
647 |
elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use]) |
|
26305 | 648 |
apply (force intro!: STL6 [temp_use] simp: more_temp_simps3) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
649 |
apply (fastforce intro: DmdPrime [temp_use] elim!: STL4E [temp_use]) |
21624 | 650 |
done |
651 |
||
652 |
lemma InfiniteEnsures: |
|
653 |
"[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P" |
|
654 |
apply (unfold InfinitePrime [temp_rewrite]) |
|
655 |
apply (rule InfImpl) |
|
656 |
apply assumption+ |
|
657 |
done |
|
658 |
||
659 |
(* ------------------------ fairness ------------------------------------------- *) |
|
660 |
section "fairness" |
|
661 |
||
662 |
(* alternative definitions of fairness *) |
|
663 |
lemma WF_alt: "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)" |
|
664 |
apply (unfold WF_def dmd_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
665 |
apply fastforce |
21624 | 666 |
done |
667 |
||
668 |
lemma SF_alt: "|- SF(A)_v = (<>[]~Enabled(<A>_v) | []<><A>_v)" |
|
669 |
apply (unfold SF_def dmd_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
670 |
apply fastforce |
21624 | 671 |
done |
672 |
||
673 |
(* theorems to "box" fairness conditions *) |
|
674 |
lemma BoxWFI: "|- WF(A)_v --> []WF(A)_v" |
|
26305 | 675 |
by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) |
21624 | 676 |
|
677 |
lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
678 |
by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use]) |
21624 | 679 |
|
680 |
lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v" |
|
26305 | 681 |
by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) |
21624 | 682 |
|
683 |
lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
684 |
by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use]) |
21624 | 685 |
|
26305 | 686 |
lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite] |
21624 | 687 |
|
688 |
lemma SFImplWF: "|- SF(A)_v --> WF(A)_v" |
|
689 |
apply (unfold SF_def WF_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
690 |
apply (fastforce dest!: DBImplBD [temp_use]) |
21624 | 691 |
done |
692 |
||
693 |
(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *) |
|
694 |
ML {* |
|
26305 | 695 |
val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [@{thm BoxWFI}, @{thm BoxSFI}] 1)) |
21624 | 696 |
*} |
697 |
||
698 |
||
699 |
(* ------------------------------ leads-to ------------------------------ *) |
|
700 |
||
701 |
section "~>" |
|
702 |
||
703 |
lemma leadsto_init: "|- (Init F) & (F ~> G) --> <>G" |
|
704 |
apply (unfold leadsto_def) |
|
705 |
apply (auto dest!: STL2 [temp_use]) |
|
706 |
done |
|
707 |
||
708 |
(* |- F & (F ~> G) --> <>G *) |
|
45605 | 709 |
lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps] |
21624 | 710 |
|
711 |
lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))" |
|
712 |
apply (unfold leadsto_def) |
|
713 |
apply auto |
|
714 |
apply (simp add: more_temp_simps) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
715 |
apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
716 |
apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use]) |
21624 | 717 |
apply (subgoal_tac "sigma |= []<><>G") |
718 |
apply (simp add: more_temp_simps) |
|
719 |
apply (drule BoxDmdDmdBox [temp_use]) |
|
720 |
apply assumption |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
721 |
apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) |
21624 | 722 |
done |
723 |
||
724 |
lemma leadsto_infinite: "|- []<>F & (F ~> G) --> []<>G" |
|
725 |
apply clarsimp |
|
726 |
apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]]) |
|
727 |
apply (simp add: dmdInitD) |
|
728 |
done |
|
729 |
||
730 |
(* In particular, strong fairness is a Streett condition. The following |
|
731 |
rules are sometimes easier to use than WF2 or SF2 below. |
|
732 |
*) |
|
733 |
lemma leadsto_SF: "|- (Enabled(<A>_v) ~> <A>_v) --> SF(A)_v" |
|
734 |
apply (unfold SF_def) |
|
735 |
apply (clarsimp elim!: leadsto_infinite [temp_use]) |
|
736 |
done |
|
737 |
||
738 |
lemma leadsto_WF: "|- (Enabled(<A>_v) ~> <A>_v) --> WF(A)_v" |
|
739 |
by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use]) |
|
740 |
||
741 |
(* introduce an invariant into the proof of a leadsto assertion. |
|
742 |
[]I --> ((P ~> Q) = (P /\ I ~> Q)) |
|
743 |
*) |
|
744 |
lemma INV_leadsto: "|- []I & (P & I ~> Q) --> (P ~> Q)" |
|
745 |
apply (unfold leadsto_def) |
|
746 |
apply clarsimp |
|
747 |
apply (erule STL4Edup) |
|
748 |
apply assumption |
|
749 |
apply (auto simp: Init_simps dest!: STL2_gen [temp_use]) |
|
750 |
done |
|
751 |
||
752 |
lemma leadsto_classical: "|- (Init F & []~G ~> G) --> (F ~> G)" |
|
753 |
apply (unfold leadsto_def dmd_def) |
|
754 |
apply (force simp: Init_simps elim!: STL4E [temp_use]) |
|
755 |
done |
|
756 |
||
757 |
lemma leadsto_false: "|- (F ~> #False) = ([]~F)" |
|
758 |
apply (unfold leadsto_def) |
|
759 |
apply (simp add: boxNotInitD) |
|
760 |
done |
|
761 |
||
762 |
lemma leadsto_exists: "|- ((EX x. F x) ~> G) = (ALL x. (F x ~> G))" |
|
763 |
apply (unfold leadsto_def) |
|
764 |
apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use]) |
|
765 |
done |
|
766 |
||
767 |
(* basic leadsto properties, cf. Unity *) |
|
768 |
||
769 |
lemma ImplLeadsto_gen: "|- [](Init F --> Init G) --> (F ~> G)" |
|
770 |
apply (unfold leadsto_def) |
|
771 |
apply (auto intro!: InitDmd_gen [temp_use] |
|
772 |
elim!: STL4E_gen [temp_use] simp: Init_simps) |
|
773 |
done |
|
774 |
||
45605 | 775 |
lemmas ImplLeadsto = |
776 |
ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps] |
|
21624 | 777 |
|
778 |
lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G" |
|
779 |
by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use]) |
|
780 |
||
781 |
lemma EnsuresLeadsto: |
|
782 |
assumes "|- A & $P --> Q`" |
|
783 |
shows "|- []A --> (P ~> Q)" |
|
784 |
apply (unfold leadsto_def) |
|
785 |
apply (clarsimp elim!: INV_leadsto [temp_use]) |
|
786 |
apply (erule STL4E_gen) |
|
787 |
apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use]) |
|
788 |
done |
|
789 |
||
790 |
lemma EnsuresLeadsto2: "|- []($P --> Q`) --> (P ~> Q)" |
|
791 |
apply (unfold leadsto_def) |
|
792 |
apply clarsimp |
|
793 |
apply (erule STL4E_gen) |
|
794 |
apply (auto simp: Init_simps intro!: PrimeDmd [temp_use]) |
|
795 |
done |
|
796 |
||
797 |
lemma ensures: |
|
798 |
assumes 1: "|- $P & N --> P` | Q`" |
|
799 |
and 2: "|- ($P & N) & A --> Q`" |
|
800 |
shows "|- []N & []([]P --> <>A) --> (P ~> Q)" |
|
801 |
apply (unfold leadsto_def) |
|
802 |
apply clarsimp |
|
803 |
apply (erule STL4Edup) |
|
804 |
apply assumption |
|
805 |
apply clarsimp |
|
806 |
apply (subgoal_tac "sigmaa |= [] ($P --> P` | Q`) ") |
|
807 |
apply (drule unless [temp_use]) |
|
808 |
apply (clarsimp dest!: INV1 [temp_use]) |
|
809 |
apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]]) |
|
810 |
apply (force intro!: BoxDmd_simple [temp_use] |
|
811 |
simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]) |
|
812 |
apply (force elim: STL4E [temp_use] dest: 1 [temp_use]) |
|
813 |
done |
|
814 |
||
815 |
lemma ensures_simple: |
|
816 |
"[| |- $P & N --> P` | Q`; |
|
817 |
|- ($P & N) & A --> Q` |
|
818 |
|] ==> |- []N & []<>A --> (P ~> Q)" |
|
819 |
apply clarsimp |
|
820 |
apply (erule (2) ensures [temp_use]) |
|
821 |
apply (force elim!: STL4E [temp_use]) |
|
822 |
done |
|
823 |
||
824 |
lemma EnsuresInfinite: |
|
825 |
"[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q" |
|
826 |
apply (erule leadsto_infinite [temp_use]) |
|
827 |
apply (erule EnsuresLeadsto [temp_use]) |
|
828 |
apply assumption |
|
829 |
done |
|
830 |
||
831 |
||
832 |
(*** Gronning's lattice rules (taken from TLP) ***) |
|
833 |
section "Lattice rules" |
|
834 |
||
835 |
lemma LatticeReflexivity: "|- F ~> F" |
|
836 |
apply (unfold leadsto_def) |
|
837 |
apply (rule necT InitDmd_gen)+ |
|
838 |
done |
|
839 |
||
840 |
lemma LatticeTransitivity: "|- (G ~> H) & (F ~> G) --> (F ~> H)" |
|
841 |
apply (unfold leadsto_def) |
|
842 |
apply clarsimp |
|
843 |
apply (erule dup_boxE) (* [][] (Init G --> H) *) |
|
42787 | 844 |
apply merge_box |
21624 | 845 |
apply (clarsimp elim!: STL4E [temp_use]) |
846 |
apply (rule dup_dmdD) |
|
847 |
apply (subgoal_tac "sigmaa |= <>Init G") |
|
848 |
apply (erule DmdImpl2) |
|
849 |
apply assumption |
|
850 |
apply (simp add: dmdInitD) |
|
851 |
done |
|
852 |
||
853 |
lemma LatticeDisjunctionElim1: "|- (F | G ~> H) --> (F ~> H)" |
|
854 |
apply (unfold leadsto_def) |
|
855 |
apply (auto simp: Init_simps elim!: STL4E [temp_use]) |
|
856 |
done |
|
857 |
||
858 |
lemma LatticeDisjunctionElim2: "|- (F | G ~> H) --> (G ~> H)" |
|
859 |
apply (unfold leadsto_def) |
|
860 |
apply (auto simp: Init_simps elim!: STL4E [temp_use]) |
|
861 |
done |
|
862 |
||
863 |
lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)" |
|
864 |
apply (unfold leadsto_def) |
|
865 |
apply clarsimp |
|
42787 | 866 |
apply merge_box |
21624 | 867 |
apply (auto simp: Init_simps elim!: STL4E [temp_use]) |
868 |
done |
|
869 |
||
870 |
lemma LatticeDisjunction: "|- (F | G ~> H) = ((F ~> H) & (G ~> H))" |
|
871 |
by (auto intro: LatticeDisjunctionIntro [temp_use] |
|
872 |
LatticeDisjunctionElim1 [temp_use] |
|
873 |
LatticeDisjunctionElim2 [temp_use]) |
|
874 |
||
875 |
lemma LatticeDiamond: "|- (A ~> B | C) & (B ~> D) & (C ~> D) --> (A ~> D)" |
|
876 |
apply clarsimp |
|
877 |
apply (subgoal_tac "sigma |= (B | C) ~> D") |
|
878 |
apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use]) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42814
diff
changeset
|
879 |
apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+ |
21624 | 880 |
done |
881 |
||
882 |
lemma LatticeTriangle: "|- (A ~> D | B) & (B ~> D) --> (A ~> D)" |
|
883 |
apply clarsimp |
|
884 |
apply (subgoal_tac "sigma |= (D | B) ~> D") |
|
885 |
apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use]) |
|
886 |
apply assumption |
|
887 |
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) |
|
888 |
done |
|
889 |
||
890 |
lemma LatticeTriangle2: "|- (A ~> B | D) & (B ~> D) --> (A ~> D)" |
|
891 |
apply clarsimp |
|
892 |
apply (subgoal_tac "sigma |= B | D ~> D") |
|
893 |
apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use]) |
|
894 |
apply assumption |
|
895 |
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) |
|
896 |
done |
|
897 |
||
898 |
(*** Lamport's fairness rules ***) |
|
899 |
section "Fairness rules" |
|
900 |
||
901 |
lemma WF1: |
|
902 |
"[| |- $P & N --> P` | Q`; |
|
903 |
|- ($P & N) & <A>_v --> Q`; |
|
904 |
|- $P & N --> $(Enabled(<A>_v)) |] |
|
905 |
==> |- []N & WF(A)_v --> (P ~> Q)" |
|
906 |
apply (clarsimp dest!: BoxWFI [temp_use]) |
|
907 |
apply (erule (2) ensures [temp_use]) |
|
908 |
apply (erule (1) STL4Edup) |
|
909 |
apply (clarsimp simp: WF_def) |
|
910 |
apply (rule STL2 [temp_use]) |
|
911 |
apply (clarsimp elim!: mp intro!: InitDmd [temp_use]) |
|
912 |
apply (erule STL4 [temp_use, THEN box_stp_actD [temp_use]]) |
|
913 |
apply (simp add: split_box_conj box_stp_actI) |
|
914 |
done |
|
915 |
||
916 |
(* Sometimes easier to use; designed for action B rather than state predicate Q *) |
|
917 |
lemma WF_leadsto: |
|
918 |
assumes 1: "|- N & $P --> $Enabled (<A>_v)" |
|
919 |
and 2: "|- N & <A>_v --> B" |
|
920 |
and 3: "|- [](N & [~A]_v) --> stable P" |
|
921 |
shows "|- []N & WF(A)_v --> (P ~> B)" |
|
922 |
apply (unfold leadsto_def) |
|
923 |
apply (clarsimp dest!: BoxWFI [temp_use]) |
|
924 |
apply (erule (1) STL4Edup) |
|
925 |
apply clarsimp |
|
926 |
apply (rule 2 [THEN DmdImpl, temp_use]) |
|
927 |
apply (rule BoxDmd_simple [temp_use]) |
|
928 |
apply assumption |
|
929 |
apply (rule classical) |
|
930 |
apply (rule STL2 [temp_use]) |
|
931 |
apply (clarsimp simp: WF_def elim!: mp intro!: InitDmd [temp_use]) |
|
932 |
apply (rule 1 [THEN STL4, temp_use, THEN box_stp_actD]) |
|
933 |
apply (simp (no_asm_simp) add: split_box_conj [try_rewrite] box_stp_act [try_rewrite]) |
|
934 |
apply (erule INV1 [temp_use]) |
|
935 |
apply (rule 3 [temp_use]) |
|
936 |
apply (simp add: split_box_conj [try_rewrite] NotDmd [temp_use] not_angle [try_rewrite]) |
|
937 |
done |
|
938 |
||
939 |
lemma SF1: |
|
940 |
"[| |- $P & N --> P` | Q`; |
|
941 |
|- ($P & N) & <A>_v --> Q`; |
|
942 |
|- []P & []N & []F --> <>Enabled(<A>_v) |] |
|
943 |
==> |- []N & SF(A)_v & []F --> (P ~> Q)" |
|
944 |
apply (clarsimp dest!: BoxSFI [temp_use]) |
|
945 |
apply (erule (2) ensures [temp_use]) |
|
946 |
apply (erule_tac F = F in dup_boxE) |
|
42787 | 947 |
apply merge_temp_box |
21624 | 948 |
apply (erule STL4Edup) |
949 |
apply assumption |
|
950 |
apply (clarsimp simp: SF_def) |
|
951 |
apply (rule STL2 [temp_use]) |
|
952 |
apply (erule mp) |
|
953 |
apply (erule STL4 [temp_use]) |
|
954 |
apply (simp add: split_box_conj [try_rewrite] STL3 [try_rewrite]) |
|
955 |
done |
|
956 |
||
957 |
lemma WF2: |
|
958 |
assumes 1: "|- N & <B>_f --> <M>_g" |
|
959 |
and 2: "|- $P & P` & <N & A>_f --> B" |
|
960 |
and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)" |
|
961 |
and 4: "|- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P" |
|
962 |
shows "|- []N & WF(A)_f & []F --> WF(M)_g" |
|
963 |
apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2] |
|
964 |
simp: WF_def [where A = M]) |
|
965 |
apply (erule_tac F = F in dup_boxE) |
|
42787 | 966 |
apply merge_temp_box |
21624 | 967 |
apply (erule STL4Edup) |
968 |
apply assumption |
|
969 |
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) |
|
970 |
apply (rule classical) |
|
971 |
apply (subgoal_tac "sigmaa |= <> (($P & P` & N) & <A>_f)") |
|
972 |
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) |
|
973 |
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) |
|
974 |
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) |
|
42787 | 975 |
apply merge_act_box |
21624 | 976 |
apply (frule 4 [temp_use]) |
977 |
apply assumption+ |
|
978 |
apply (drule STL6 [temp_use]) |
|
979 |
apply assumption |
|
980 |
apply (erule_tac V = "sigmaa |= <>[]P" in thin_rl) |
|
981 |
apply (erule_tac V = "sigmaa |= []F" in thin_rl) |
|
982 |
apply (drule BoxWFI [temp_use]) |
|
983 |
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE) |
|
42787 | 984 |
apply merge_temp_box |
21624 | 985 |
apply (erule DmdImpldup) |
986 |
apply assumption |
|
987 |
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite] |
|
988 |
WF_Box [try_rewrite] box_stp_act [try_rewrite]) |
|
989 |
apply (force elim!: TLA2E [where P = P, temp_use]) |
|
990 |
apply (rule STL2 [temp_use]) |
|
991 |
apply (force simp: WF_def split_box_conj [try_rewrite] |
|
992 |
elim!: mp intro!: InitDmd [temp_use] 3 [THEN STL4, temp_use]) |
|
993 |
done |
|
994 |
||
995 |
lemma SF2: |
|
996 |
assumes 1: "|- N & <B>_f --> <M>_g" |
|
997 |
and 2: "|- $P & P` & <N & A>_f --> B" |
|
998 |
and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)" |
|
999 |
and 4: "|- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P" |
|
1000 |
shows "|- []N & SF(A)_f & []F --> SF(M)_g" |
|
1001 |
apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M]) |
|
1002 |
apply (erule_tac F = F in dup_boxE) |
|
1003 |
apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE) |
|
42787 | 1004 |
apply merge_temp_box |
21624 | 1005 |
apply (erule STL4Edup) |
1006 |
apply assumption |
|
1007 |
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) |
|
1008 |
apply (rule classical) |
|
1009 |
apply (subgoal_tac "sigmaa |= <> (($P & P` & N) & <A>_f)") |
|
1010 |
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) |
|
1011 |
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) |
|
1012 |
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) |
|
42787 | 1013 |
apply merge_act_box |
21624 | 1014 |
apply (frule 4 [temp_use]) |
1015 |
apply assumption+ |
|
1016 |
apply (erule_tac V = "sigmaa |= []F" in thin_rl) |
|
1017 |
apply (drule BoxSFI [temp_use]) |
|
1018 |
apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE) |
|
1019 |
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE) |
|
42787 | 1020 |
apply merge_temp_box |
21624 | 1021 |
apply (erule DmdImpldup) |
1022 |
apply assumption |
|
1023 |
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite] |
|
1024 |
SF_Box [try_rewrite] box_stp_act [try_rewrite]) |
|
1025 |
apply (force elim!: TLA2E [where P = P, temp_use]) |
|
1026 |
apply (rule STL2 [temp_use]) |
|
1027 |
apply (force simp: SF_def split_box_conj [try_rewrite] |
|
1028 |
elim!: mp InfImpl [temp_use] intro!: 3 [temp_use]) |
|
1029 |
done |
|
1030 |
||
1031 |
(* ------------------------------------------------------------------------- *) |
|
1032 |
(*** Liveness proofs by well-founded orderings ***) |
|
1033 |
(* ------------------------------------------------------------------------- *) |
|
1034 |
section "Well-founded orderings" |
|
1035 |
||
1036 |
lemma wf_leadsto: |
|
1037 |
assumes 1: "wf r" |
|
1038 |
and 2: "!!x. sigma |= F x ~> (G | (EX y. #((y,x):r) & F y)) " |
|
1039 |
shows "sigma |= F x ~> G" |
|
1040 |
apply (rule 1 [THEN wf_induct]) |
|
1041 |
apply (rule LatticeTriangle [temp_use]) |
|
1042 |
apply (rule 2) |
|
1043 |
apply (auto simp: leadsto_exists [try_rewrite]) |
|
1044 |
apply (case_tac "(y,x) :r") |
|
1045 |
apply force |
|
1046 |
apply (force simp: leadsto_def Init_simps intro!: necT [temp_use]) |
|
1047 |
done |
|
1048 |
||
1049 |
(* If r is well-founded, state function v cannot decrease forever *) |
|
1050 |
lemma wf_not_box_decrease: "!!r. wf r ==> |- [][ (v`, $v) : #r ]_v --> <>[][#False]_v" |
|
1051 |
apply clarsimp |
|
1052 |
apply (rule ccontr) |
|
1053 |
apply (subgoal_tac "sigma |= (EX x. v=#x) ~> #False") |
|
1054 |
apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]]) |
|
1055 |
apply (force simp: Init_defs) |
|
1056 |
apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps) |
|
1057 |
apply (erule wf_leadsto) |
|
1058 |
apply (rule ensures_simple [temp_use]) |
|
1059 |
apply (auto simp: square_def angle_def) |
|
1060 |
done |
|
1061 |
||
1062 |
(* "wf r ==> |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *) |
|
1063 |
lemmas wf_not_dmd_box_decrease = |
|
45605 | 1064 |
wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps] |
21624 | 1065 |
|
1066 |
(* If there are infinitely many steps where v decreases, then there |
|
1067 |
have to be infinitely many non-stuttering steps where v doesn't decrease. |
|
1068 |
*) |
|
1069 |
lemma wf_box_dmd_decrease: |
|
1070 |
assumes 1: "wf r" |
|
1071 |
shows "|- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v" |
|
1072 |
apply clarsimp |
|
1073 |
apply (rule ccontr) |
|
1074 |
apply (simp add: not_angle [try_rewrite] more_temp_simps) |
|
1075 |
apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]]) |
|
1076 |
apply (drule BoxDmdDmdBox [temp_use]) |
|
1077 |
apply assumption |
|
1078 |
apply (subgoal_tac "sigma |= []<> ((#False) ::action)") |
|
1079 |
apply force |
|
1080 |
apply (erule STL4E) |
|
1081 |
apply (rule DmdImpl) |
|
1082 |
apply (force intro: 1 [THEN wf_irrefl, temp_use]) |
|
1083 |
done |
|
1084 |
||
1085 |
(* In particular, for natural numbers, if n decreases infinitely often |
|
1086 |
then it has to increase infinitely often. |
|
1087 |
*) |
|
1088 |
lemma nat_box_dmd_decrease: "!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)" |
|
1089 |
apply clarsimp |
|
1090 |
apply (subgoal_tac "sigma |= []<><~ ((n`,$n) : #less_than) >_n") |
|
1091 |
apply (erule thin_rl) |
|
1092 |
apply (erule STL4E) |
|
1093 |
apply (rule DmdImpl) |
|
1094 |
apply (clarsimp simp: angle_def [try_rewrite]) |
|
1095 |
apply (rule wf_box_dmd_decrease [temp_use]) |
|
1096 |
apply (auto elim!: STL4E [temp_use] DmdImplE [temp_use]) |
|
1097 |
done |
|
1098 |
||
1099 |
||
1100 |
(* ------------------------------------------------------------------------- *) |
|
1101 |
(*** Flexible quantification over state variables ***) |
|
1102 |
(* ------------------------------------------------------------------------- *) |
|
1103 |
section "Flexible quantification" |
|
1104 |
||
1105 |
lemma aallI: |
|
1106 |
assumes 1: "basevars vs" |
|
1107 |
and 2: "(!!x. basevars (x,vs) ==> sigma |= F x)" |
|
1108 |
shows "sigma |= (AALL x. F x)" |
|
1109 |
by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use]) |
|
1110 |
||
1111 |
lemma aallE: "|- (AALL x. F x) --> F x" |
|
1112 |
apply (unfold aall_def) |
|
1113 |
apply clarsimp |
|
1114 |
apply (erule contrapos_np) |
|
1115 |
apply (force intro!: eexI [temp_use]) |
|
1116 |
done |
|
1117 |
||
1118 |
(* monotonicity of quantification *) |
|
1119 |
lemma eex_mono: |
|
1120 |
assumes 1: "sigma |= EEX x. F x" |
|
1121 |
and 2: "!!x. sigma |= F x --> G x" |
|
1122 |
shows "sigma |= EEX x. G x" |
|
1123 |
apply (rule unit_base [THEN 1 [THEN eexE]]) |
|
1124 |
apply (rule eexI [temp_use]) |
|
1125 |
apply (erule 2 [unfolded intensional_rews, THEN mp]) |
|
1126 |
done |
|
1127 |
||
1128 |
lemma aall_mono: |
|
1129 |
assumes 1: "sigma |= AALL x. F(x)" |
|
1130 |
and 2: "!!x. sigma |= F(x) --> G(x)" |
|
1131 |
shows "sigma |= AALL x. G(x)" |
|
1132 |
apply (rule unit_base [THEN aallI]) |
|
1133 |
apply (rule 2 [unfolded intensional_rews, THEN mp]) |
|
1134 |
apply (rule 1 [THEN aallE [temp_use]]) |
|
1135 |
done |
|
1136 |
||
1137 |
(* Derived history introduction rule *) |
|
1138 |
lemma historyI: |
|
1139 |
assumes 1: "sigma |= Init I" |
|
1140 |
and 2: "sigma |= []N" |
|
1141 |
and 3: "basevars vs" |
|
1142 |
and 4: "!!h. basevars(h,vs) ==> |- I & h = ha --> HI h" |
|
1143 |
and 5: "!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)" |
|
1144 |
shows "sigma |= EEX h. Init (HI h) & [](HN h)" |
|
1145 |
apply (rule history [temp_use, THEN eexE]) |
|
1146 |
apply (rule 3) |
|
1147 |
apply (rule eexI [temp_use]) |
|
1148 |
apply clarsimp |
|
1149 |
apply (rule conjI) |
|
1150 |
prefer 2 |
|
1151 |
apply (insert 2) |
|
42787 | 1152 |
apply merge_box |
21624 | 1153 |
apply (force elim!: STL4E [temp_use] 5 [temp_use]) |
1154 |
apply (insert 1) |
|
1155 |
apply (force simp: Init_defs elim!: 4 [temp_use]) |
|
1156 |
done |
|
1157 |
||
1158 |
(* ---------------------------------------------------------------------- |
|
1159 |
example of a history variable: existence of a clock |
|
1160 |
*) |
|
1161 |
||
1162 |
lemma "|- EEX h. Init(h = #True) & [](h` = (~$h))" |
|
1163 |
apply (rule tempI) |
|
1164 |
apply (rule historyI) |
|
1165 |
apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+ |
|
1166 |
done |
|
1167 |
||
1168 |
end |