28 definition |
28 definition |
29 weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where |
29 weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where |
30 "weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)" |
30 "weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)" |
31 definition |
31 definition |
32 temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where |
32 temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where |
33 "temp_strengthening Q P h = (!ex. (cex_abs h ex |== Q) --> (ex |== P))" |
33 "temp_strengthening Q P h = (!ex. (cex_abs h ex \<TTurnstile> Q) --> (ex \<TTurnstile> P))" |
34 definition |
34 definition |
35 temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where |
35 temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where |
36 "temp_weakening Q P h = temp_strengthening (.~ Q) (.~ P) h" |
36 "temp_weakening Q P h = temp_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h" |
37 |
37 |
38 definition |
38 definition |
39 state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where |
39 state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where |
40 "state_strengthening Q P h = (!s t a. Q (h(s),a,h(t)) --> P (s,a,t))" |
40 "state_strengthening Q P h = (!s t a. Q (h(s),a,h(t)) --> P (s,a,t))" |
41 definition |
41 definition |
42 state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where |
42 state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where |
43 "state_weakening Q P h = state_strengthening (.~Q) (.~P) h" |
43 "state_weakening Q P h = state_strengthening (\<^bold>\<not>Q) (\<^bold>\<not>P) h" |
44 |
44 |
45 definition |
45 definition |
46 is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where |
46 is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where |
47 "is_live_abstraction h CL AM = |
47 "is_live_abstraction h CL AM = |
48 (is_abstraction h (fst CL) (fst AM) & |
48 (is_abstraction h (fst CL) (fst AM) & |
129 done |
129 done |
130 |
130 |
131 |
131 |
132 (* FIX: Nach TLS.ML *) |
132 (* FIX: Nach TLS.ML *) |
133 |
133 |
134 lemma IMPLIES_temp_sat: "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))" |
134 lemma IMPLIES_temp_sat: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) = ((ex \<TTurnstile> P) --> (ex \<TTurnstile> Q))" |
135 by (simp add: IMPLIES_def temp_sat_def satisfies_def) |
135 by (simp add: IMPLIES_def temp_sat_def satisfies_def) |
136 |
136 |
137 lemma AND_temp_sat: "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))" |
137 lemma AND_temp_sat: "(ex \<TTurnstile> P \<^bold>\<and> Q) = ((ex \<TTurnstile> P) & (ex \<TTurnstile> Q))" |
138 by (simp add: AND_def temp_sat_def satisfies_def) |
138 by (simp add: AND_def temp_sat_def satisfies_def) |
139 |
139 |
140 lemma OR_temp_sat: "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))" |
140 lemma OR_temp_sat: "(ex \<TTurnstile> P \<^bold>\<or> Q) = ((ex \<TTurnstile> P) | (ex \<TTurnstile> Q))" |
141 by (simp add: OR_def temp_sat_def satisfies_def) |
141 by (simp add: OR_def temp_sat_def satisfies_def) |
142 |
142 |
143 lemma NOT_temp_sat: "(ex |== .~ P) = (~ (ex |== P))" |
143 lemma NOT_temp_sat: "(ex \<TTurnstile> \<^bold>\<not> P) = (~ (ex \<TTurnstile> P))" |
144 by (simp add: NOT_def temp_sat_def satisfies_def) |
144 by (simp add: NOT_def temp_sat_def satisfies_def) |
145 |
145 |
146 declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp] |
146 declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp] |
147 |
147 |
148 |
148 |
158 done |
158 done |
159 |
159 |
160 |
160 |
161 lemma AbsRuleTImprove: |
161 lemma AbsRuleTImprove: |
162 "[|is_live_abstraction h (C,L) (A,M); |
162 "[|is_live_abstraction h (C,L) (A,M); |
163 validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; |
163 validLIOA (A,M) (H1 \<^bold>\<longrightarrow> Q); temp_strengthening Q P h; |
164 temp_weakening H1 H2 h; validLIOA (C,L) H2 |] |
164 temp_weakening H1 H2 h; validLIOA (C,L) H2 |] |
165 ==> validLIOA (C,L) P" |
165 ==> validLIOA (C,L) P" |
166 apply (unfold is_live_abstraction_def) |
166 apply (unfold is_live_abstraction_def) |
167 apply auto |
167 apply auto |
168 apply (drule abs_is_weakening) |
168 apply (drule abs_is_weakening) |
285 subsection "Localizing Temporal Strengthenings and Weakenings" |
285 subsection "Localizing Temporal Strengthenings and Weakenings" |
286 |
286 |
287 lemma strength_AND: |
287 lemma strength_AND: |
288 "[| temp_strengthening P1 Q1 h; |
288 "[| temp_strengthening P1 Q1 h; |
289 temp_strengthening P2 Q2 h |] |
289 temp_strengthening P2 Q2 h |] |
290 ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h" |
290 ==> temp_strengthening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h" |
291 apply (unfold temp_strengthening_def) |
291 apply (unfold temp_strengthening_def) |
292 apply auto |
292 apply auto |
293 done |
293 done |
294 |
294 |
295 lemma strength_OR: |
295 lemma strength_OR: |
296 "[| temp_strengthening P1 Q1 h; |
296 "[| temp_strengthening P1 Q1 h; |
297 temp_strengthening P2 Q2 h |] |
297 temp_strengthening P2 Q2 h |] |
298 ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h" |
298 ==> temp_strengthening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h" |
299 apply (unfold temp_strengthening_def) |
299 apply (unfold temp_strengthening_def) |
300 apply auto |
300 apply auto |
301 done |
301 done |
302 |
302 |
303 lemma strength_NOT: |
303 lemma strength_NOT: |
304 "[| temp_weakening P Q h |] |
304 "[| temp_weakening P Q h |] |
305 ==> temp_strengthening (.~ P) (.~ Q) h" |
305 ==> temp_strengthening (\<^bold>\<not> P) (\<^bold>\<not> Q) h" |
306 apply (unfold temp_strengthening_def) |
306 apply (unfold temp_strengthening_def) |
307 apply (simp add: temp_weakening_def2) |
307 apply (simp add: temp_weakening_def2) |
308 apply auto |
308 apply auto |
309 done |
309 done |
310 |
310 |
311 lemma strength_IMPLIES: |
311 lemma strength_IMPLIES: |
312 "[| temp_weakening P1 Q1 h; |
312 "[| temp_weakening P1 Q1 h; |
313 temp_strengthening P2 Q2 h |] |
313 temp_strengthening P2 Q2 h |] |
314 ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h" |
314 ==> temp_strengthening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h" |
315 apply (unfold temp_strengthening_def) |
315 apply (unfold temp_strengthening_def) |
316 apply (simp add: temp_weakening_def2) |
316 apply (simp add: temp_weakening_def2) |
317 done |
317 done |
318 |
318 |
319 |
319 |
320 lemma weak_AND: |
320 lemma weak_AND: |
321 "[| temp_weakening P1 Q1 h; |
321 "[| temp_weakening P1 Q1 h; |
322 temp_weakening P2 Q2 h |] |
322 temp_weakening P2 Q2 h |] |
323 ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h" |
323 ==> temp_weakening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h" |
324 apply (simp add: temp_weakening_def2) |
324 apply (simp add: temp_weakening_def2) |
325 done |
325 done |
326 |
326 |
327 lemma weak_OR: |
327 lemma weak_OR: |
328 "[| temp_weakening P1 Q1 h; |
328 "[| temp_weakening P1 Q1 h; |
329 temp_weakening P2 Q2 h |] |
329 temp_weakening P2 Q2 h |] |
330 ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h" |
330 ==> temp_weakening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h" |
331 apply (simp add: temp_weakening_def2) |
331 apply (simp add: temp_weakening_def2) |
332 done |
332 done |
333 |
333 |
334 lemma weak_NOT: |
334 lemma weak_NOT: |
335 "[| temp_strengthening P Q h |] |
335 "[| temp_strengthening P Q h |] |
336 ==> temp_weakening (.~ P) (.~ Q) h" |
336 ==> temp_weakening (\<^bold>\<not> P) (\<^bold>\<not> Q) h" |
337 apply (unfold temp_strengthening_def) |
337 apply (unfold temp_strengthening_def) |
338 apply (simp add: temp_weakening_def2) |
338 apply (simp add: temp_weakening_def2) |
339 apply auto |
339 apply auto |
340 done |
340 done |
341 |
341 |
342 lemma weak_IMPLIES: |
342 lemma weak_IMPLIES: |
343 "[| temp_strengthening P1 Q1 h; |
343 "[| temp_strengthening P1 Q1 h; |
344 temp_weakening P2 Q2 h |] |
344 temp_weakening P2 Q2 h |] |
345 ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h" |
345 ==> temp_weakening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h" |
346 apply (unfold temp_strengthening_def) |
346 apply (unfold temp_strengthening_def) |
347 apply (simp add: temp_weakening_def2) |
347 apply (simp add: temp_weakening_def2) |
348 done |
348 done |
349 |
349 |
350 |
350 |