77 (* analog to the proved thm strength_Next - proof skipped as trivial *) |
77 (* analog to the proved thm strength_Next - proof skipped as trivial *) |
78 weak_Next: |
78 weak_Next: |
79 "temp_weakening P Q h |
79 "temp_weakening P Q h |
80 ==> temp_weakening (Next P) (Next Q) h" |
80 ==> temp_weakening (Next P) (Next Q) h" |
81 |
81 |
82 ML {* use_legacy_bindings (the_context ()) *} |
82 |
83 |
83 subsection "cex_abs" |
|
84 |
|
85 lemma cex_abs_UU: "cex_abs f (s,UU) = (f s, UU)" |
|
86 by (simp add: cex_abs_def) |
|
87 |
|
88 lemma cex_abs_nil: "cex_abs f (s,nil) = (f s, nil)" |
|
89 by (simp add: cex_abs_def) |
|
90 |
|
91 lemma cex_abs_cons: "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))" |
|
92 by (simp add: cex_abs_def) |
|
93 |
|
94 declare cex_abs_UU [simp] cex_abs_nil [simp] cex_abs_cons [simp] |
|
95 |
|
96 |
|
97 subsection "lemmas" |
|
98 |
|
99 lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))" |
|
100 apply (simp add: temp_weakening_def temp_strengthening_def NOT_def temp_sat_def satisfies_def) |
|
101 apply auto |
|
102 done |
|
103 |
|
104 lemma state_weakening_def2: "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))" |
|
105 apply (simp add: state_weakening_def state_strengthening_def NOT_def) |
|
106 apply auto |
|
107 done |
|
108 |
|
109 |
|
110 subsection "Abstraction Rules for Properties" |
|
111 |
|
112 lemma exec_frag_abstraction [rule_format]: |
|
113 "[| is_abstraction h C A |] ==> |
|
114 !s. reachable C s & is_exec_frag C (s,xs) |
|
115 --> is_exec_frag A (cex_abs h (s,xs))" |
|
116 apply (unfold cex_abs_def) |
|
117 apply simp |
|
118 apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *}) |
|
119 txt {* main case *} |
|
120 apply (tactic "safe_tac set_cs") |
|
121 apply (simp add: is_abstraction_def) |
|
122 apply (frule reachable.reachable_n) |
|
123 apply assumption |
|
124 apply simp |
|
125 done |
|
126 |
|
127 |
|
128 lemma abs_is_weakening: "is_abstraction h C A ==> weakeningIOA A C h" |
|
129 apply (simp add: weakeningIOA_def) |
|
130 apply auto |
|
131 apply (simp add: executions_def) |
|
132 txt {* start state *} |
|
133 apply (rule conjI) |
|
134 apply (simp add: is_abstraction_def cex_abs_def) |
|
135 txt {* is-execution-fragment *} |
|
136 apply (erule exec_frag_abstraction) |
|
137 apply (simp add: reachable.reachable_0) |
|
138 done |
|
139 |
|
140 |
|
141 lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] |
|
142 ==> validIOA C P" |
|
143 apply (drule abs_is_weakening) |
|
144 apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def) |
|
145 apply (tactic "safe_tac set_cs") |
|
146 apply (tactic {* pair_tac "ex" 1 *}) |
|
147 done |
|
148 |
|
149 |
|
150 (* FIX: Nach TLS.ML *) |
|
151 |
|
152 lemma IMPLIES_temp_sat: "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))" |
|
153 by (simp add: IMPLIES_def temp_sat_def satisfies_def) |
|
154 |
|
155 lemma AND_temp_sat: "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))" |
|
156 by (simp add: AND_def temp_sat_def satisfies_def) |
|
157 |
|
158 lemma OR_temp_sat: "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))" |
|
159 by (simp add: OR_def temp_sat_def satisfies_def) |
|
160 |
|
161 lemma NOT_temp_sat: "(ex |== .~ P) = (~ (ex |== P))" |
|
162 by (simp add: NOT_def temp_sat_def satisfies_def) |
|
163 |
|
164 declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp] |
|
165 |
|
166 |
|
167 lemma AbsRuleT2: |
|
168 "[|is_live_abstraction h (C,L) (A,M); |
|
169 validLIOA (A,M) Q; temp_strengthening Q P h |] |
|
170 ==> validLIOA (C,L) P" |
|
171 apply (unfold is_live_abstraction_def) |
|
172 apply auto |
|
173 apply (drule abs_is_weakening) |
|
174 apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def) |
|
175 apply (tactic "safe_tac set_cs") |
|
176 apply (tactic {* pair_tac "ex" 1 *}) |
|
177 done |
|
178 |
|
179 |
|
180 lemma AbsRuleTImprove: |
|
181 "[|is_live_abstraction h (C,L) (A,M); |
|
182 validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; |
|
183 temp_weakening H1 H2 h; validLIOA (C,L) H2 |] |
|
184 ==> validLIOA (C,L) P" |
|
185 apply (unfold is_live_abstraction_def) |
|
186 apply auto |
|
187 apply (drule abs_is_weakening) |
|
188 apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def) |
|
189 apply (tactic "safe_tac set_cs") |
|
190 apply (tactic {* pair_tac "ex" 1 *}) |
|
191 done |
|
192 |
|
193 |
|
194 subsection "Correctness of safe abstraction" |
|
195 |
|
196 lemma abstraction_is_ref_map: |
|
197 "is_abstraction h C A ==> is_ref_map h C A" |
|
198 apply (unfold is_abstraction_def is_ref_map_def) |
|
199 apply (tactic "safe_tac set_cs") |
|
200 apply (rule_tac x = "(a,h t) >>nil" in exI) |
|
201 apply (simp add: move_def) |
|
202 done |
|
203 |
|
204 |
|
205 lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A); |
|
206 is_abstraction h C A |] |
|
207 ==> C =<| A" |
|
208 apply (simp add: ioa_implements_def) |
|
209 apply (rule trace_inclusion) |
|
210 apply (simp (no_asm) add: externals_def) |
|
211 apply (auto)[1] |
|
212 apply (erule abstraction_is_ref_map) |
|
213 done |
|
214 |
|
215 |
|
216 subsection "Correctness of life abstraction" |
|
217 |
|
218 (* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x), |
|
219 that is to special Map Lemma *) |
|
220 lemma traces_coincide_abs: |
|
221 "ext C = ext A |
|
222 ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))" |
|
223 apply (unfold cex_abs_def mk_trace_def filter_act_def) |
|
224 apply simp |
|
225 apply (tactic {* pair_induct_tac "xs" [] 1 *}) |
|
226 done |
|
227 |
|
228 |
|
229 (* Does not work with abstraction_is_ref_map as proof of abs_safety, because |
|
230 is_live_abstraction includes temp_strengthening which is necessarily based |
|
231 on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific |
|
232 way for cex_abs *) |
|
233 lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A); |
|
234 is_live_abstraction h (C,M) (A,L) |] |
|
235 ==> live_implements (C,M) (A,L)" |
|
236 apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def) |
|
237 apply (tactic "safe_tac set_cs") |
|
238 apply (rule_tac x = "cex_abs h ex" in exI) |
|
239 apply (tactic "safe_tac set_cs") |
|
240 (* Traces coincide *) |
|
241 apply (tactic {* pair_tac "ex" 1 *}) |
|
242 apply (rule traces_coincide_abs) |
|
243 apply (simp (no_asm) add: externals_def) |
|
244 apply (auto)[1] |
|
245 |
|
246 (* cex_abs is execution *) |
|
247 apply (tactic {* pair_tac "ex" 1 *}) |
|
248 apply (simp add: executions_def) |
|
249 (* start state *) |
|
250 apply (rule conjI) |
|
251 apply (simp add: is_abstraction_def cex_abs_def) |
|
252 (* is-execution-fragment *) |
|
253 apply (erule exec_frag_abstraction) |
|
254 apply (simp add: reachable.reachable_0) |
|
255 |
|
256 (* Liveness *) |
|
257 apply (simp add: temp_weakening_def2) |
|
258 apply (tactic {* pair_tac "ex" 1 *}) |
|
259 done |
|
260 |
|
261 (* FIX: NAch Traces.ML bringen *) |
|
262 |
|
263 lemma implements_trans: |
|
264 "[| A =<| B; B =<| C|] ==> A =<| C" |
|
265 apply (unfold ioa_implements_def) |
|
266 apply auto |
|
267 done |
|
268 |
|
269 |
|
270 subsection "Abstraction Rules for Automata" |
|
271 |
|
272 lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A); |
|
273 inp(Q)=inp(P); out(Q)=out(P); |
|
274 is_abstraction h1 C A; |
|
275 A =<| Q ; |
|
276 is_abstraction h2 Q P |] |
|
277 ==> C =<| P" |
|
278 apply (drule abs_safety) |
|
279 apply assumption+ |
|
280 apply (drule abs_safety) |
|
281 apply assumption+ |
|
282 apply (erule implements_trans) |
|
283 apply (erule implements_trans) |
|
284 apply assumption |
|
285 done |
|
286 |
|
287 |
|
288 lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A); |
|
289 inp(Q)=inp(P); out(Q)=out(P); |
|
290 is_live_abstraction h1 (C,LC) (A,LA); |
|
291 live_implements (A,LA) (Q,LQ) ; |
|
292 is_live_abstraction h2 (Q,LQ) (P,LP) |] |
|
293 ==> live_implements (C,LC) (P,LP)" |
|
294 apply (drule abs_liveness) |
|
295 apply assumption+ |
|
296 apply (drule abs_liveness) |
|
297 apply assumption+ |
|
298 apply (erule live_implements_trans) |
|
299 apply (erule live_implements_trans) |
|
300 apply assumption |
|
301 done |
|
302 |
|
303 |
|
304 declare split_paired_All [simp del] |
|
305 |
|
306 |
|
307 subsection "Localizing Temporal Strengthenings and Weakenings" |
|
308 |
|
309 lemma strength_AND: |
|
310 "[| temp_strengthening P1 Q1 h; |
|
311 temp_strengthening P2 Q2 h |] |
|
312 ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h" |
|
313 apply (unfold temp_strengthening_def) |
|
314 apply auto |
|
315 done |
|
316 |
|
317 lemma strength_OR: |
|
318 "[| temp_strengthening P1 Q1 h; |
|
319 temp_strengthening P2 Q2 h |] |
|
320 ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h" |
|
321 apply (unfold temp_strengthening_def) |
|
322 apply auto |
|
323 done |
|
324 |
|
325 lemma strength_NOT: |
|
326 "[| temp_weakening P Q h |] |
|
327 ==> temp_strengthening (.~ P) (.~ Q) h" |
|
328 apply (unfold temp_strengthening_def) |
|
329 apply (simp add: temp_weakening_def2) |
|
330 apply auto |
|
331 done |
|
332 |
|
333 lemma strength_IMPLIES: |
|
334 "[| temp_weakening P1 Q1 h; |
|
335 temp_strengthening P2 Q2 h |] |
|
336 ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h" |
|
337 apply (unfold temp_strengthening_def) |
|
338 apply (simp add: temp_weakening_def2) |
|
339 done |
|
340 |
|
341 |
|
342 lemma weak_AND: |
|
343 "[| temp_weakening P1 Q1 h; |
|
344 temp_weakening P2 Q2 h |] |
|
345 ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h" |
|
346 apply (simp add: temp_weakening_def2) |
|
347 done |
|
348 |
|
349 lemma weak_OR: |
|
350 "[| temp_weakening P1 Q1 h; |
|
351 temp_weakening P2 Q2 h |] |
|
352 ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h" |
|
353 apply (simp add: temp_weakening_def2) |
|
354 done |
|
355 |
|
356 lemma weak_NOT: |
|
357 "[| temp_strengthening P Q h |] |
|
358 ==> temp_weakening (.~ P) (.~ Q) h" |
|
359 apply (unfold temp_strengthening_def) |
|
360 apply (simp add: temp_weakening_def2) |
|
361 apply auto |
|
362 done |
|
363 |
|
364 lemma weak_IMPLIES: |
|
365 "[| temp_strengthening P1 Q1 h; |
|
366 temp_weakening P2 Q2 h |] |
|
367 ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h" |
|
368 apply (unfold temp_strengthening_def) |
|
369 apply (simp add: temp_weakening_def2) |
|
370 done |
|
371 |
|
372 |
|
373 subsubsection {* Box *} |
|
374 |
|
375 (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *) |
|
376 lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))" |
|
377 apply (tactic {* Seq_case_simp_tac "x" 1 *}) |
|
378 done |
|
379 |
|
380 lemma ex2seqConc [rule_format]: |
|
381 "Finite s1 --> |
|
382 (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))" |
|
383 apply (rule impI) |
|
384 apply (tactic {* Seq_Finite_induct_tac 1 *}) |
|
385 apply blast |
|
386 (* main case *) |
|
387 apply (tactic "clarify_tac set_cs 1") |
|
388 apply (tactic {* pair_tac "ex" 1 *}) |
|
389 apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
390 (* UU case *) |
|
391 apply (simp add: nil_is_Conc) |
|
392 (* nil case *) |
|
393 apply (simp add: nil_is_Conc) |
|
394 (* cons case *) |
|
395 apply (tactic {* pair_tac "aa" 1 *}) |
|
396 apply auto |
|
397 done |
|
398 |
|
399 (* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
|
400 |
|
401 lemma ex2seq_tsuffix: |
|
402 "tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')" |
|
403 apply (unfold tsuffix_def suffix_def) |
|
404 apply auto |
|
405 apply (drule ex2seqConc) |
|
406 apply auto |
|
407 done |
|
408 |
|
409 |
|
410 (* FIX: NAch Sequence.ML bringen *) |
|
411 |
|
412 lemma Mapnil: "(Map f$s = nil) = (s=nil)" |
|
413 apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
414 done |
|
415 |
|
416 lemma MapUU: "(Map f$s = UU) = (s=UU)" |
|
417 apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
418 done |
|
419 |
|
420 |
|
421 (* important property of cex_absSeq: As it is a 1to1 correspondence, |
|
422 properties carry over *) |
|
423 |
|
424 lemma cex_absSeq_tsuffix: |
|
425 "tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)" |
|
426 apply (unfold tsuffix_def suffix_def cex_absSeq_def) |
|
427 apply auto |
|
428 apply (simp add: Mapnil) |
|
429 apply (simp add: MapUU) |
|
430 apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))$s1" in exI) |
|
431 apply (simp add: Map2Finite MapConc) |
|
432 done |
|
433 |
|
434 |
|
435 lemma strength_Box: |
|
436 "[| temp_strengthening P Q h |] |
|
437 ==> temp_strengthening ([] P) ([] Q) h" |
|
438 apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def) |
|
439 apply (tactic "clarify_tac set_cs 1") |
|
440 apply (frule ex2seq_tsuffix) |
|
441 apply (tactic "clarify_tac set_cs 1") |
|
442 apply (drule_tac h = "h" in cex_absSeq_tsuffix) |
|
443 apply (simp add: ex2seq_abs_cex) |
|
444 done |
|
445 |
|
446 |
|
447 subsubsection {* Init *} |
|
448 |
|
449 lemma strength_Init: |
|
450 "[| state_strengthening P Q h |] |
|
451 ==> temp_strengthening (Init P) (Init Q) h" |
|
452 apply (unfold temp_strengthening_def state_strengthening_def |
|
453 temp_sat_def satisfies_def Init_def unlift_def) |
|
454 apply (tactic "safe_tac set_cs") |
|
455 apply (tactic {* pair_tac "ex" 1 *}) |
|
456 apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
457 apply (tactic {* pair_tac "a" 1 *}) |
|
458 done |
|
459 |
|
460 |
|
461 subsubsection {* Next *} |
|
462 |
|
463 lemma TL_ex2seq_UU: |
|
464 "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)" |
|
465 apply (tactic {* pair_tac "ex" 1 *}) |
|
466 apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
467 apply (tactic {* pair_tac "a" 1 *}) |
|
468 apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
469 apply (tactic {* pair_tac "a" 1 *}) |
|
470 done |
|
471 |
|
472 lemma TL_ex2seq_nil: |
|
473 "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)" |
|
474 apply (tactic {* pair_tac "ex" 1 *}) |
|
475 apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
476 apply (tactic {* pair_tac "a" 1 *}) |
|
477 apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
478 apply (tactic {* pair_tac "a" 1 *}) |
|
479 done |
|
480 |
|
481 (* FIX: put to Sequence Lemmas *) |
|
482 lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)" |
|
483 apply (tactic {* Seq_induct_tac "s" [] 1 *}) |
|
484 done |
|
485 |
|
486 (* important property of cex_absSeq: As it is a 1to1 correspondence, |
|
487 properties carry over *) |
|
488 |
|
489 lemma cex_absSeq_TL: |
|
490 "cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))" |
|
491 apply (unfold cex_absSeq_def) |
|
492 apply (simp add: MapTL) |
|
493 done |
|
494 |
|
495 (* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
|
496 |
|
497 lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')" |
|
498 apply (tactic {* pair_tac "ex" 1 *}) |
|
499 apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
500 apply (tactic {* pair_tac "a" 1 *}) |
|
501 apply auto |
|
502 done |
|
503 |
|
504 |
|
505 lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)" |
|
506 apply (tactic {* pair_tac "ex" 1 *}) |
|
507 apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
508 apply (tactic {* pair_tac "a" 1 *}) |
|
509 apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
510 apply (tactic {* pair_tac "a" 1 *}) |
|
511 done |
|
512 |
|
513 |
|
514 lemma strength_Next: |
|
515 "[| temp_strengthening P Q h |] |
|
516 ==> temp_strengthening (Next P) (Next Q) h" |
|
517 apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def) |
|
518 apply simp |
|
519 apply (tactic "safe_tac set_cs") |
|
520 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
|
521 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
|
522 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
|
523 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU) |
|
524 (* cons case *) |
|
525 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU ex2seq_abs_cex cex_absSeq_TL [symmetric] ex2seqnilTL) |
|
526 apply (erule conjE) |
|
527 apply (drule TLex2seq) |
|
528 apply assumption |
|
529 apply auto |
|
530 done |
|
531 |
|
532 |
|
533 text {* Localizing Temporal Weakenings - 2 *} |
|
534 |
|
535 lemma weak_Init: |
|
536 "[| state_weakening P Q h |] |
|
537 ==> temp_weakening (Init P) (Init Q) h" |
|
538 apply (simp add: temp_weakening_def2 state_weakening_def2 |
|
539 temp_sat_def satisfies_def Init_def unlift_def) |
|
540 apply (tactic "safe_tac set_cs") |
|
541 apply (tactic {* pair_tac "ex" 1 *}) |
|
542 apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
543 apply (tactic {* pair_tac "a" 1 *}) |
|
544 done |
|
545 |
|
546 |
|
547 text {* Localizing Temproal Strengthenings - 3 *} |
|
548 |
|
549 lemma strength_Diamond: |
|
550 "[| temp_strengthening P Q h |] |
|
551 ==> temp_strengthening (<> P) (<> Q) h" |
|
552 apply (unfold Diamond_def) |
|
553 apply (rule strength_NOT) |
|
554 apply (rule weak_Box) |
|
555 apply (erule weak_NOT) |
|
556 done |
|
557 |
|
558 lemma strength_Leadsto: |
|
559 "[| temp_weakening P1 P2 h; |
|
560 temp_strengthening Q1 Q2 h |] |
|
561 ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h" |
|
562 apply (unfold Leadsto_def) |
|
563 apply (rule strength_Box) |
|
564 apply (erule strength_IMPLIES) |
|
565 apply (erule strength_Diamond) |
|
566 done |
|
567 |
|
568 |
|
569 text {* Localizing Temporal Weakenings - 3 *} |
|
570 |
|
571 lemma weak_Diamond: |
|
572 "[| temp_weakening P Q h |] |
|
573 ==> temp_weakening (<> P) (<> Q) h" |
|
574 apply (unfold Diamond_def) |
|
575 apply (rule weak_NOT) |
|
576 apply (rule strength_Box) |
|
577 apply (erule strength_NOT) |
|
578 done |
|
579 |
|
580 lemma weak_Leadsto: |
|
581 "[| temp_strengthening P1 P2 h; |
|
582 temp_weakening Q1 Q2 h |] |
|
583 ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h" |
|
584 apply (unfold Leadsto_def) |
|
585 apply (rule weak_Box) |
|
586 apply (erule weak_IMPLIES) |
|
587 apply (erule weak_Diamond) |
|
588 done |
|
589 |
|
590 lemma weak_WF: |
|
591 " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] |
|
592 ==> temp_weakening (WF A acts) (WF C acts) h" |
|
593 apply (unfold WF_def) |
|
594 apply (rule weak_IMPLIES) |
|
595 apply (rule strength_Diamond) |
|
596 apply (rule strength_Box) |
|
597 apply (rule strength_Init) |
|
598 apply (rule_tac [2] weak_Box) |
|
599 apply (rule_tac [2] weak_Diamond) |
|
600 apply (rule_tac [2] weak_Init) |
|
601 apply (auto simp add: state_weakening_def state_strengthening_def |
|
602 xt2_def plift_def option_lift_def NOT_def) |
|
603 done |
|
604 |
|
605 lemma weak_SF: |
|
606 " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] |
|
607 ==> temp_weakening (SF A acts) (SF C acts) h" |
|
608 apply (unfold SF_def) |
|
609 apply (rule weak_IMPLIES) |
|
610 apply (rule strength_Box) |
|
611 apply (rule strength_Diamond) |
|
612 apply (rule strength_Init) |
|
613 apply (rule_tac [2] weak_Box) |
|
614 apply (rule_tac [2] weak_Diamond) |
|
615 apply (rule_tac [2] weak_Init) |
|
616 apply (auto simp add: state_weakening_def state_strengthening_def |
|
617 xt2_def plift_def option_lift_def NOT_def) |
|
618 done |
|
619 |
|
620 |
|
621 lemmas weak_strength_lemmas = |
|
622 weak_OR weak_AND weak_NOT weak_IMPLIES weak_Box weak_Next weak_Init |
|
623 weak_Diamond weak_Leadsto strength_OR strength_AND strength_NOT |
|
624 strength_IMPLIES strength_Box strength_Next strength_Init |
|
625 strength_Diamond strength_Leadsto weak_WF weak_SF |
|
626 |
|
627 ML {* |
|
628 |
|
629 local |
|
630 val weak_strength_lemmas = thms "weak_strength_lemmas" |
|
631 val state_strengthening_def = thm "state_strengthening_def" |
|
632 val state_weakening_def = thm "state_weakening_def" |
|
633 in |
|
634 |
|
635 fun abstraction_tac i = |
|
636 SELECT_GOAL (CLASIMPSET (fn (cs, ss) => |
|
637 auto_tac (cs addSIs weak_strength_lemmas, |
|
638 ss addsimps [state_strengthening_def, state_weakening_def]))) i |
84 end |
639 end |
|
640 *} |
|
641 |
|
642 end |