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