author | nipkow |
Tue, 10 Mar 1998 19:15:00 +0100 | |
changeset 4725 | 7edba45a6998 |
parent 4577 | 674b0b354feb |
child 4833 | 2e53109d4bc8 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/Abstraction.thy |
2 |
ID: $Id$ |
|
3 |
Author: Olaf M"uller |
|
4 |
Copyright 1997 TU Muenchen |
|
5 |
||
6 |
Abstraction Theory -- tailored for I/O automata |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
section "cex_abs"; |
|
11 |
||
12 |
||
13 |
(* ---------------------------------------------------------------- *) |
|
14 |
(* cex_abs *) |
|
15 |
(* ---------------------------------------------------------------- *) |
|
16 |
||
17 |
goal thy "cex_abs f (s,UU) = (f s, UU)"; |
|
18 |
by (simp_tac (simpset() addsimps [cex_abs_def]) 1); |
|
19 |
qed"cex_abs_UU"; |
|
20 |
||
21 |
goal thy "cex_abs f (s,nil) = (f s, nil)"; |
|
22 |
by (simp_tac (simpset() addsimps [cex_abs_def]) 1); |
|
23 |
qed"cex_abs_nil"; |
|
24 |
||
25 |
goal thy "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))"; |
|
26 |
by (simp_tac (simpset() addsimps [cex_abs_def]) 1); |
|
27 |
qed"cex_abs_cons"; |
|
28 |
||
29 |
Addsimps [cex_abs_UU, cex_abs_nil, cex_abs_cons]; |
|
30 |
||
31 |
||
32 |
||
33 |
section "lemmas"; |
|
34 |
||
35 |
(* ---------------------------------------------------------------- *) |
|
36 |
(* Lemmas *) |
|
37 |
(* ---------------------------------------------------------------- *) |
|
38 |
||
39 |
goal thy "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))"; |
|
40 |
by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def, |
|
41 |
NOT_def,temp_sat_def,satisfies_def]) 1); |
|
42 |
auto(); |
|
43 |
qed"temp_weakening_def2"; |
|
44 |
||
45 |
goal thy "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))"; |
|
46 |
by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def, |
|
47 |
NOT_def]) 1); |
|
48 |
auto(); |
|
49 |
qed"state_weakening_def2"; |
|
50 |
||
51 |
||
52 |
section "Abstraction Rules for Properties"; |
|
53 |
||
54 |
(* ---------------------------------------------------------------- *) |
|
55 |
(* Abstraction Rules for Properties *) |
|
56 |
(* ---------------------------------------------------------------- *) |
|
57 |
||
58 |
||
59 |
goalw thy [cex_abs_def] |
|
60 |
"!!h.[| is_abstraction h C A |] ==>\ |
|
61 |
\ !s. reachable C s & is_exec_frag C (s,xs) \ |
|
62 |
\ --> is_exec_frag A (cex_abs h (s,xs))"; |
|
63 |
||
64 |
by (Asm_full_simp_tac 1); |
|
65 |
by (pair_induct_tac "xs" [is_exec_frag_def] 1); |
|
66 |
(* main case *) |
|
67 |
by (safe_tac set_cs); |
|
68 |
by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1); |
|
69 |
by (forward_tac [reachable.reachable_n] 1); |
|
70 |
by (assume_tac 1); |
|
71 |
by (Asm_full_simp_tac 1); |
|
72 |
qed"exec_frag_abstraction"; |
|
73 |
||
74 |
||
75 |
goal thy "!!A. is_abstraction h C A ==> weakeningIOA A C h"; |
|
76 |
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1); |
|
77 |
auto(); |
|
78 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
|
79 |
(* start state *) |
|
80 |
by (rtac conjI 1); |
|
81 |
by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1); |
|
82 |
(* is-execution-fragment *) |
|
83 |
by (etac (exec_frag_abstraction RS spec RS mp) 1); |
|
84 |
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1); |
|
85 |
qed"abs_is_weakening"; |
|
86 |
||
87 |
||
88 |
goal thy "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \ |
|
89 |
\ ==> validIOA C P"; |
|
90 |
bd abs_is_weakening 1; |
|
91 |
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, |
|
92 |
validIOA_def, temp_strengthening_def])1); |
|
93 |
by (safe_tac set_cs); |
|
94 |
by (pair_tac "ex" 1); |
|
95 |
qed"AbsRuleT1"; |
|
96 |
||
97 |
||
98 |
(* FIX: Nach TLS.ML *) |
|
99 |
||
100 |
goal thy "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))"; |
|
101 |
by (simp_tac (simpset() addsimps [IMPLIES_def,temp_sat_def, satisfies_def])1); |
|
102 |
qed"IMPLIES_temp_sat"; |
|
103 |
||
104 |
goal thy "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))"; |
|
105 |
by (simp_tac (simpset() addsimps [AND_def,temp_sat_def, satisfies_def])1); |
|
106 |
qed"AND_temp_sat"; |
|
107 |
||
108 |
goal thy "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))"; |
|
109 |
by (simp_tac (simpset() addsimps [OR_def,temp_sat_def, satisfies_def])1); |
|
110 |
qed"OR_temp_sat"; |
|
111 |
||
112 |
goal thy "(ex |== .~ P) = (~ (ex |== P))"; |
|
113 |
by (simp_tac (simpset() addsimps [NOT_def,temp_sat_def, satisfies_def])1); |
|
114 |
qed"NOT_temp_sat"; |
|
115 |
||
116 |
Addsimps [IMPLIES_temp_sat,AND_temp_sat,OR_temp_sat,NOT_temp_sat]; |
|
117 |
||
118 |
||
119 |
goalw thy [is_live_abstraction_def] |
|
120 |
"!!A. [|is_live_abstraction h (C,L) (A,M); \ |
|
121 |
\ validLIOA (A,M) Q; temp_strengthening Q P h |] \ |
|
122 |
\ ==> validLIOA (C,L) P"; |
|
123 |
auto(); |
|
124 |
bd abs_is_weakening 1; |
|
125 |
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2, |
|
126 |
validLIOA_def, validIOA_def, temp_strengthening_def])1); |
|
127 |
by (safe_tac set_cs); |
|
128 |
by (pair_tac "ex" 1); |
|
129 |
qed"AbsRuleT2"; |
|
130 |
||
131 |
||
132 |
goalw thy [is_live_abstraction_def] |
|
133 |
"!!A. [|is_live_abstraction h (C,L) (A,M); \ |
|
134 |
\ validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; \ |
|
135 |
\ temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \ |
|
136 |
\ ==> validLIOA (C,L) P"; |
|
137 |
auto(); |
|
138 |
bd abs_is_weakening 1; |
|
139 |
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2, |
|
140 |
validLIOA_def, validIOA_def, temp_strengthening_def])1); |
|
141 |
by (safe_tac set_cs); |
|
142 |
by (pair_tac "ex" 1); |
|
143 |
qed"AbsRuleTImprove"; |
|
144 |
||
145 |
||
146 |
section "Correctness of safe abstraction"; |
|
147 |
||
148 |
(* ---------------------------------------------------------------- *) |
|
149 |
(* Correctness of safe abstraction *) |
|
150 |
(* ---------------------------------------------------------------- *) |
|
151 |
||
152 |
||
153 |
goalw thy [is_abstraction_def,is_ref_map_def] |
|
154 |
"!! h. is_abstraction h C A ==> is_ref_map h C A"; |
|
155 |
by (safe_tac set_cs); |
|
156 |
by (res_inst_tac[("x","(a,h t)>>nil")] exI 1); |
|
157 |
by (asm_full_simp_tac (simpset() addsimps [move_def])1); |
|
158 |
qed"abstraction_is_ref_map"; |
|
159 |
||
160 |
||
161 |
goal thy "!! h. [| inp(C)=inp(A); out(C)=out(A); \ |
|
162 |
\ is_abstraction h C A |] \ |
|
163 |
\ ==> C =<| A"; |
|
164 |
by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1); |
|
165 |
br trace_inclusion 1; |
|
166 |
by (simp_tac (simpset() addsimps [externals_def])1); |
|
167 |
by (SELECT_GOAL (auto_tac (claset(),simpset()))1); |
|
168 |
be abstraction_is_ref_map 1; |
|
169 |
qed"abs_safety"; |
|
170 |
||
171 |
||
172 |
section "Correctness of life abstraction"; |
|
173 |
||
174 |
(* ---------------------------------------------------------------- *) |
|
175 |
(* Correctness of life abstraction *) |
|
176 |
(* ---------------------------------------------------------------- *) |
|
177 |
||
178 |
||
179 |
(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x), |
|
180 |
that is to special Map Lemma *) |
|
181 |
goalw thy [cex_abs_def,mk_trace_def,filter_act_def] |
|
182 |
"!! f. ext C = ext A \ |
|
183 |
\ ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))"; |
|
184 |
by (Asm_full_simp_tac 1); |
|
185 |
by (pair_induct_tac "xs" [] 1); |
|
186 |
qed"traces_coincide_abs"; |
|
187 |
||
188 |
||
189 |
goalw thy [cex_abs_def] |
|
190 |
"!!f.[| is_abstraction h C A |] ==>\ |
|
191 |
\ !s. reachable C s & is_exec_frag C (s,xs) \ |
|
192 |
\ --> is_exec_frag A (cex_abs h (s,xs))"; |
|
193 |
||
194 |
by (Asm_full_simp_tac 1); |
|
195 |
by (pair_induct_tac "xs" [is_exec_frag_def] 1); |
|
196 |
(* main case *) |
|
197 |
by (safe_tac set_cs); |
|
198 |
(* Stepd correspond to each other *) |
|
199 |
by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1); |
|
200 |
(* IH *) |
|
201 |
(* reachable_n looping, therefore apply it manually *) |
|
202 |
by (eres_inst_tac [("x","y")] allE 1); |
|
203 |
by (Asm_full_simp_tac 1); |
|
204 |
by (forward_tac [reachable.reachable_n] 1); |
|
205 |
by (assume_tac 1); |
|
206 |
by (Asm_full_simp_tac 1); |
|
207 |
qed_spec_mp"correp_is_exec_abs"; |
|
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 |
goal thy "!! h. [| 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 |
||
217 |
by (asm_full_simp_tac (simpset() addsimps [is_live_abstraction_def, live_implements_def, |
|
218 |
livetraces_def,liveexecutions_def]) 1); |
|
219 |
by (safe_tac set_cs); |
|
220 |
by (res_inst_tac[("x","cex_abs h ex")] exI 1); |
|
221 |
by (safe_tac set_cs); |
|
222 |
(* Traces coincide *) |
|
223 |
by (pair_tac "ex" 1); |
|
224 |
by (rtac traces_coincide_abs 1); |
|
225 |
by (simp_tac (simpset() addsimps [externals_def])1); |
|
226 |
by (SELECT_GOAL (auto_tac (claset(),simpset()))1); |
|
227 |
||
228 |
(* cex_abs is execution *) |
|
229 |
by (pair_tac "ex" 1); |
|
230 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
|
231 |
(* start state *) |
|
232 |
by (rtac conjI 1); |
|
233 |
by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1); |
|
234 |
(* is-execution-fragment *) |
|
235 |
by (etac correp_is_exec_abs 1); |
|
236 |
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1); |
|
237 |
||
238 |
(* Liveness *) |
|
239 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2]) 1); |
|
240 |
by (pair_tac "ex" 1); |
|
241 |
qed"abs_liveness"; |
|
242 |
||
243 |
(* FIX: NAch Traces.ML bringen *) |
|
244 |
||
245 |
goalw thy [ioa_implements_def] |
|
246 |
"!! A. [| A =<| B; B =<| C|] ==> A =<| C"; |
|
247 |
auto(); |
|
248 |
qed"implements_trans"; |
|
249 |
||
250 |
||
251 |
section "Abstraction Rules for Automata"; |
|
252 |
||
253 |
(* ---------------------------------------------------------------- *) |
|
254 |
(* Abstraction Rules for Automata *) |
|
255 |
(* ---------------------------------------------------------------- *) |
|
256 |
||
257 |
goal thy "!! C. [| inp(C)=inp(A); out(C)=out(A); \ |
|
258 |
\ inp(Q)=inp(P); out(Q)=out(P); \ |
|
259 |
\ is_abstraction h1 C A; \ |
|
260 |
\ A =<| Q ; \ |
|
261 |
\ is_abstraction h2 Q P |] \ |
|
262 |
\ ==> C =<| P"; |
|
263 |
bd abs_safety 1; |
|
264 |
by (REPEAT (atac 1)); |
|
265 |
bd abs_safety 1; |
|
266 |
by (REPEAT (atac 1)); |
|
267 |
be implements_trans 1; |
|
268 |
be implements_trans 1; |
|
269 |
ba 1; |
|
270 |
qed"AbsRuleA1"; |
|
271 |
||
272 |
||
273 |
goal thy "!! C. [| inp(C)=inp(A); out(C)=out(A); \ |
|
274 |
\ inp(Q)=inp(P); out(Q)=out(P); \ |
|
275 |
\ is_live_abstraction h1 (C,LC) (A,LA); \ |
|
276 |
\ live_implements (A,LA) (Q,LQ) ; \ |
|
277 |
\ is_live_abstraction h2 (Q,LQ) (P,LP) |] \ |
|
278 |
\ ==> live_implements (C,LC) (P,LP)"; |
|
279 |
bd abs_liveness 1; |
|
280 |
by (REPEAT (atac 1)); |
|
281 |
bd abs_liveness 1; |
|
282 |
by (REPEAT (atac 1)); |
|
283 |
be live_implements_trans 1; |
|
284 |
be live_implements_trans 1; |
|
285 |
ba 1; |
|
286 |
qed"AbsRuleA2"; |
|
287 |
||
288 |
||
289 |
Delsimps [split_paired_All]; |
|
290 |
||
291 |
||
292 |
section "Localizing Temporal Strengthenings and Weakenings"; |
|
293 |
||
294 |
(* ---------------------------------------------------------------- *) |
|
295 |
(* Localizing Temproal Strengthenings - 1 *) |
|
296 |
(* ---------------------------------------------------------------- *) |
|
297 |
||
298 |
goalw thy [temp_strengthening_def] |
|
299 |
"!! h. [| temp_strengthening P1 Q1 h; \ |
|
300 |
\ temp_strengthening P2 Q2 h |] \ |
|
301 |
\ ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h"; |
|
302 |
auto(); |
|
303 |
qed"strength_AND"; |
|
304 |
||
305 |
goalw thy [temp_strengthening_def] |
|
306 |
"!! h. [| temp_strengthening P1 Q1 h; \ |
|
307 |
\ temp_strengthening P2 Q2 h |] \ |
|
308 |
\ ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h"; |
|
309 |
auto(); |
|
310 |
qed"strength_OR"; |
|
311 |
||
312 |
goalw thy [temp_strengthening_def] |
|
313 |
"!! h. [| temp_weakening P Q h |] \ |
|
314 |
\ ==> temp_strengthening (.~ P) (.~ Q) h"; |
|
315 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
316 |
auto(); |
|
317 |
qed"strength_NOT"; |
|
318 |
||
319 |
goalw thy [temp_strengthening_def] |
|
320 |
"!! h. [| temp_weakening P1 Q1 h; \ |
|
321 |
\ temp_strengthening P2 Q2 h |] \ |
|
322 |
\ ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h"; |
|
323 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
324 |
qed"strength_IMPLIES"; |
|
325 |
||
326 |
||
327 |
||
328 |
(* ---------------------------------------------------------------- *) |
|
329 |
(* Localizing Temproal Weakenings - Part 1 *) |
|
330 |
(* ---------------------------------------------------------------- *) |
|
331 |
||
332 |
goal thy |
|
333 |
"!! h. [| temp_weakening P1 Q1 h; \ |
|
334 |
\ temp_weakening P2 Q2 h |] \ |
|
335 |
\ ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h"; |
|
336 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
337 |
qed"weak_AND"; |
|
338 |
||
339 |
goal thy |
|
340 |
"!! h. [| temp_weakening P1 Q1 h; \ |
|
341 |
\ temp_weakening P2 Q2 h |] \ |
|
342 |
\ ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h"; |
|
343 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
344 |
qed"weak_OR"; |
|
345 |
||
346 |
goalw thy [temp_strengthening_def] |
|
347 |
"!! h. [| temp_strengthening P Q h |] \ |
|
348 |
\ ==> temp_weakening (.~ P) (.~ Q) h"; |
|
349 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
350 |
auto(); |
|
351 |
qed"weak_NOT"; |
|
352 |
||
353 |
goalw thy [temp_strengthening_def] |
|
354 |
"!! h. [| temp_strengthening P1 Q1 h; \ |
|
355 |
\ temp_weakening P2 Q2 h |] \ |
|
356 |
\ ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h"; |
|
357 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
358 |
qed"weak_IMPLIES"; |
|
359 |
||
360 |
||
361 |
(* ---------------------------------------------------------------- *) |
|
362 |
(* Localizing Temproal Strengthenings - 2 *) |
|
363 |
(* ---------------------------------------------------------------- *) |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
364 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
365 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
366 |
(* ------------------ Box ----------------------------*) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
367 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
368 |
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
369 |
goal thy "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
370 |
by (Seq_case_simp_tac "x" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
371 |
by Auto_tac; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
372 |
qed"UU_is_Conc"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
373 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
374 |
goal thy |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
375 |
"Finite s1 --> \ |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
376 |
\ (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
377 |
by (rtac impI 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
378 |
by (Seq_Finite_induct_tac 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
379 |
(* main case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
380 |
by (Blast_tac 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
381 |
by (clarify_tac set_cs 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
382 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
383 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
384 |
(* UU case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
385 |
by (asm_full_simp_tac (simpset() addsimps [UU_is_Conc])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
386 |
(* nil case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
387 |
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
388 |
(* cons case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
389 |
by (pair_tac "aa" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
390 |
auto(); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
391 |
qed_spec_mp"ex2seqConc"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
392 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
393 |
(* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
394 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
395 |
goalw thy [tsuffix_def,suffix_def] |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
396 |
"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
397 |
auto(); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
398 |
bd ex2seqConc 1; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
399 |
auto(); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
400 |
qed"ex2seq_tsuffix"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
401 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
402 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
403 |
goal thy "(Map f`s = nil) = (s=nil)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
404 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
405 |
qed"Mapnil"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
406 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
407 |
goal thy "(Map f`s = UU) = (s=UU)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
408 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
409 |
qed"MapUU"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
410 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
411 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
412 |
(* important property of cex_absSeq: As it is a 1to1 correspondence, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
413 |
properties carry over *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
414 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
415 |
goalw thy [tsuffix_def,suffix_def,cex_absSeq_def] |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
416 |
"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
417 |
auto(); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
418 |
by (asm_full_simp_tac (simpset() addsimps [Mapnil])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
419 |
by (asm_full_simp_tac (simpset() addsimps [MapUU])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
420 |
by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
421 |
by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
422 |
qed"cex_absSeq_tsuffix"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
423 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
424 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
425 |
goalw thy [temp_strengthening_def,state_strengthening_def, temp_sat_def, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
426 |
satisfies_def,Box_def] |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
427 |
"!! h. [| temp_strengthening P Q h |]\ |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
428 |
\ ==> temp_strengthening ([] P) ([] Q) h"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
429 |
by (clarify_tac set_cs 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
430 |
by (forward_tac [ex2seq_tsuffix] 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
431 |
by (clarify_tac set_cs 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
432 |
by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
433 |
by (asm_full_simp_tac (simpset() addsimps [ex2seq_abs_cex])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
434 |
qed"strength_Box"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
435 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
436 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
437 |
(* ------------------ Init ----------------------------*) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
438 |
|
4559 | 439 |
goalw thy [temp_strengthening_def,state_strengthening_def, |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
440 |
temp_sat_def,satisfies_def,Init_def,unlift_def] |
4559 | 441 |
"!! h. [| state_strengthening P Q h |]\ |
442 |
\ ==> temp_strengthening (Init P) (Init Q) h"; |
|
443 |
by (safe_tac set_cs); |
|
444 |
by (pair_tac "ex" 1); |
|
445 |
by (Seq_case_simp_tac "y" 1); |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
446 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
447 |
qed"strength_Init"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
448 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
449 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
450 |
(* ------------------ Next ----------------------------*) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
451 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
452 |
goal thy |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
453 |
"(TL`(ex2seq (cex_abs h ex))=UU) = (TL`(ex2seq ex)=UU)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
454 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
455 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
456 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
457 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
458 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
459 |
qed"TL_ex2seq_UU"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
460 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
461 |
goal thy |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
462 |
"(TL`(ex2seq (cex_abs h ex))=nil) = (TL`(ex2seq ex)=nil)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
463 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
464 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
465 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
466 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
467 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
468 |
qed"TL_ex2seq_nil"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
469 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
470 |
(* FIX: put to Sequence Lemmas *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
471 |
goal thy "Map f`(TL`s) = TL`(Map f`s)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
472 |
by (Seq_induct_tac "s" [] 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
473 |
qed"MapTL"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
474 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
475 |
(* important property of cex_absSeq: As it is a 1to1 correspondence, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
476 |
properties carry over *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
477 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
478 |
goalw thy [cex_absSeq_def] |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
479 |
"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
480 |
by (simp_tac (simpset() addsimps [MapTL]) 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
481 |
qed"cex_absSeq_TL"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
482 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
483 |
(* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
484 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
485 |
goal thy "!!ex. [| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
486 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
487 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
488 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
489 |
auto(); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
490 |
qed"TLex2seq"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
491 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
492 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
493 |
goal thy "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
494 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
495 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
496 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
497 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
498 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
499 |
qed"ex2seqUUTL"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
500 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
501 |
goal thy "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
502 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
503 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
504 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
505 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
506 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
507 |
qed"ex2seqnilTL"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
508 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
509 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
510 |
goalw thy [temp_strengthening_def,state_strengthening_def, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
511 |
temp_sat_def, satisfies_def,Next_def] |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
512 |
"!! h. [| temp_strengthening P Q h |]\ |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
513 |
\ ==> temp_strengthening (Next P) (Next Q) h"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
514 |
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
515 |
by (safe_tac set_cs); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
516 |
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
517 |
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
518 |
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
519 |
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
520 |
(* cons case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
521 |
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
522 |
ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
523 |
bd TLex2seq 1; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
524 |
ba 1; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
525 |
auto(); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
526 |
qed"strength_Next"; |
4559 | 527 |
|
528 |
||
529 |
||
530 |
(* ---------------------------------------------------------------- *) |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
531 |
(* Localizing Temporal Weakenings - 2 *) |
4559 | 532 |
(* ---------------------------------------------------------------- *) |
533 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
534 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
535 |
goal thy |
4559 | 536 |
"!! h. [| state_weakening P Q h |]\ |
537 |
\ ==> temp_weakening (Init P) (Init Q) h"; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
538 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
539 |
state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1); |
4559 | 540 |
by (safe_tac set_cs); |
541 |
by (pair_tac "ex" 1); |
|
542 |
by (Seq_case_simp_tac "y" 1); |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
543 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
544 |
qed"weak_Init"; |
4559 | 545 |
|
546 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
547 |
(* |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
548 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
549 |
(* analog to strengthening thm above, with analog lemmas used *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
550 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
551 |
goalw thy [state_weakening_def] |
4559 | 552 |
"!! h. [| temp_weakening P Q h |]\ |
553 |
\ ==> temp_weakening ([] P) ([] Q) h"; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
554 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
555 |
temp_sat_def,satisfies_def,Box_def])1); |
4559 | 556 |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
557 |
(* analog to strengthening thm above, with analog lemmas used *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
558 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
559 |
goalw thy [state_weakening_def] |
4559 | 560 |
"!! h. [| temp_weakening P Q h |]\ |
561 |
\ ==> temp_weakening (Next P) (Next Q) h"; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
562 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
563 |
temp_sat_def,satisfies_def,Next_def])1); |
4559 | 564 |
|
565 |
*) |
|
566 |
||
567 |
(* ---------------------------------------------------------------- *) |
|
568 |
(* Localizing Temproal Strengthenings - 3 *) |
|
569 |
(* ---------------------------------------------------------------- *) |
|
570 |
||
571 |
||
572 |
goalw thy [Diamond_def] |
|
573 |
"!! h. [| temp_strengthening P Q h |]\ |
|
574 |
\ ==> temp_strengthening (<> P) (<> Q) h"; |
|
575 |
br strength_NOT 1; |
|
576 |
br weak_Box 1; |
|
577 |
be weak_NOT 1; |
|
578 |
qed"strength_Diamond"; |
|
579 |
||
580 |
goalw thy [Leadsto_def] |
|
581 |
"!! h. [| temp_weakening P1 P2 h;\ |
|
582 |
\ temp_strengthening Q1 Q2 h |]\ |
|
583 |
\ ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h"; |
|
584 |
br strength_Box 1; |
|
585 |
be strength_IMPLIES 1; |
|
586 |
be strength_Diamond 1; |
|
587 |
qed"strength_Leadsto"; |
|
588 |
||
589 |
||
590 |
(* ---------------------------------------------------------------- *) |
|
591 |
(* Localizing Temporal Weakenings - 3 *) |
|
592 |
(* ---------------------------------------------------------------- *) |
|
593 |
||
594 |
||
595 |
goalw thy [Diamond_def] |
|
596 |
"!! h. [| temp_weakening P Q h |]\ |
|
597 |
\ ==> temp_weakening (<> P) (<> Q) h"; |
|
598 |
br weak_NOT 1; |
|
599 |
br strength_Box 1; |
|
600 |
be strength_NOT 1; |
|
601 |
qed"weak_Diamond"; |
|
602 |
||
603 |
goalw thy [Leadsto_def] |
|
604 |
"!! h. [| temp_strengthening P1 P2 h;\ |
|
605 |
\ temp_weakening Q1 Q2 h |]\ |
|
606 |
\ ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h"; |
|
607 |
br weak_Box 1; |
|
608 |
be weak_IMPLIES 1; |
|
609 |
be weak_Diamond 1; |
|
610 |
qed"weak_Leadsto"; |
|
611 |
||
612 |
goalw thy [WF_def] |
|
613 |
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ |
|
614 |
\ ==> temp_weakening (WF A acts) (WF C acts) h"; |
|
615 |
br weak_IMPLIES 1; |
|
616 |
br strength_Diamond 1; |
|
617 |
br strength_Box 1; |
|
618 |
br strength_Init 1; |
|
619 |
br weak_Box 2; |
|
620 |
br weak_Diamond 2; |
|
621 |
br weak_Init 2; |
|
622 |
by (auto_tac (claset(), |
|
623 |
simpset() addsimps [state_weakening_def,state_strengthening_def, |
|
624 |
xt2_def,plift_def,option_lift_def,NOT_def])); |
|
625 |
qed"weak_WF"; |
|
626 |
||
627 |
goalw thy [SF_def] |
|
628 |
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ |
|
629 |
\ ==> temp_weakening (SF A acts) (SF C acts) h"; |
|
630 |
br weak_IMPLIES 1; |
|
631 |
br strength_Box 1; |
|
632 |
br strength_Diamond 1; |
|
633 |
br strength_Init 1; |
|
634 |
br weak_Box 2; |
|
635 |
br weak_Diamond 2; |
|
636 |
br weak_Init 2; |
|
637 |
by (auto_tac (claset(), |
|
638 |
simpset() addsimps [state_weakening_def,state_strengthening_def, |
|
639 |
xt2_def,plift_def,option_lift_def,NOT_def])); |
|
640 |
qed"weak_SF"; |
|
641 |
||
642 |
||
643 |
val weak_strength_lemmas = |
|
644 |
[weak_OR,weak_AND,weak_NOT,weak_IMPLIES,weak_Box,weak_Next,weak_Init, |
|
645 |
weak_Diamond,weak_Leadsto,strength_OR,strength_AND,strength_NOT, |
|
646 |
strength_IMPLIES,strength_Box,strength_Next,strength_Init, |
|
647 |
strength_Diamond,strength_Leadsto,weak_WF,weak_SF]; |
|
648 |
||
649 |
fun abstraction_tac i = |
|
650 |
SELECT_GOAL (auto_tac (claset() addSIs weak_strength_lemmas, |
|
4725 | 651 |
simpset() addsimps [state_strengthening_def,state_weakening_def])) i; |