author | mueller |
Mon, 19 Oct 1998 15:49:55 +0200 | |
changeset 5676 | 96b048840bb3 |
parent 5670 | 5e7d9455de96 |
child 5677 | 4feffde494cf |
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 |
||
5068 | 17 |
Goal "cex_abs f (s,UU) = (f s, UU)"; |
4559 | 18 |
by (simp_tac (simpset() addsimps [cex_abs_def]) 1); |
19 |
qed"cex_abs_UU"; |
|
20 |
||
5068 | 21 |
Goal "cex_abs f (s,nil) = (f s, nil)"; |
4559 | 22 |
by (simp_tac (simpset() addsimps [cex_abs_def]) 1); |
23 |
qed"cex_abs_nil"; |
|
24 |
||
5068 | 25 |
Goal "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))"; |
4559 | 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 |
||
5068 | 39 |
Goal "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))"; |
4559 | 40 |
by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def, |
41 |
NOT_def,temp_sat_def,satisfies_def]) 1); |
|
5132 | 42 |
by Auto_tac; |
4559 | 43 |
qed"temp_weakening_def2"; |
44 |
||
5068 | 45 |
Goal "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))"; |
4559 | 46 |
by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def, |
47 |
NOT_def]) 1); |
|
5132 | 48 |
by Auto_tac; |
4559 | 49 |
qed"state_weakening_def2"; |
50 |
||
51 |
||
52 |
section "Abstraction Rules for Properties"; |
|
53 |
||
54 |
(* ---------------------------------------------------------------- *) |
|
55 |
(* Abstraction Rules for Properties *) |
|
56 |
(* ---------------------------------------------------------------- *) |
|
57 |
||
58 |
||
5068 | 59 |
Goalw [cex_abs_def] |
4559 | 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); |
|
5670 | 72 |
qed_spec_mp"exec_frag_abstraction"; |
4559 | 73 |
|
74 |
||
5068 | 75 |
Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h"; |
4559 | 76 |
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1); |
5132 | 77 |
by Auto_tac; |
4559 | 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 *) |
|
5670 | 83 |
by (etac exec_frag_abstraction 1); |
4559 | 84 |
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1); |
85 |
qed"abs_is_weakening"; |
|
86 |
||
87 |
||
5068 | 88 |
Goal "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \ |
4559 | 89 |
\ ==> validIOA C P"; |
5132 | 90 |
by (dtac abs_is_weakening 1); |
4559 | 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 |
||
5068 | 100 |
Goal "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))"; |
4559 | 101 |
by (simp_tac (simpset() addsimps [IMPLIES_def,temp_sat_def, satisfies_def])1); |
102 |
qed"IMPLIES_temp_sat"; |
|
103 |
||
5068 | 104 |
Goal "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))"; |
4559 | 105 |
by (simp_tac (simpset() addsimps [AND_def,temp_sat_def, satisfies_def])1); |
106 |
qed"AND_temp_sat"; |
|
107 |
||
5068 | 108 |
Goal "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))"; |
4559 | 109 |
by (simp_tac (simpset() addsimps [OR_def,temp_sat_def, satisfies_def])1); |
110 |
qed"OR_temp_sat"; |
|
111 |
||
5068 | 112 |
Goal "(ex |== .~ P) = (~ (ex |== P))"; |
4559 | 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 |
||
5068 | 119 |
Goalw [is_live_abstraction_def] |
4559 | 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"; |
|
5132 | 123 |
by Auto_tac; |
124 |
by (dtac abs_is_weakening 1); |
|
4559 | 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 |
||
5068 | 132 |
Goalw [is_live_abstraction_def] |
4559 | 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"; |
|
5132 | 137 |
by Auto_tac; |
138 |
by (dtac abs_is_weakening 1); |
|
4559 | 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 |
||
5068 | 153 |
Goalw [is_abstraction_def,is_ref_map_def] |
4559 | 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 |
||
5068 | 161 |
Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \ |
4559 | 162 |
\ is_abstraction h C A |] \ |
163 |
\ ==> C =<| A"; |
|
164 |
by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1); |
|
5132 | 165 |
by (rtac trace_inclusion 1); |
4559 | 166 |
by (simp_tac (simpset() addsimps [externals_def])1); |
167 |
by (SELECT_GOAL (auto_tac (claset(),simpset()))1); |
|
5132 | 168 |
by (etac abstraction_is_ref_map 1); |
4559 | 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 *) |
|
5068 | 181 |
Goalw [cex_abs_def,mk_trace_def,filter_act_def] |
4559 | 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 |
||
5670 | 188 |
(* |
189 |
FIX: Is this needed anywhere? |
|
4559 | 190 |
|
5068 | 191 |
Goalw [cex_abs_def] |
4559 | 192 |
"!!f.[| is_abstraction h C A |] ==>\ |
193 |
\ !s. reachable C s & is_exec_frag C (s,xs) \ |
|
194 |
\ --> is_exec_frag A (cex_abs h (s,xs))"; |
|
195 |
||
196 |
by (Asm_full_simp_tac 1); |
|
197 |
by (pair_induct_tac "xs" [is_exec_frag_def] 1); |
|
198 |
(* main case *) |
|
199 |
by (safe_tac set_cs); |
|
200 |
(* Stepd correspond to each other *) |
|
201 |
by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1); |
|
202 |
(* IH *) |
|
203 |
(* reachable_n looping, therefore apply it manually *) |
|
204 |
by (eres_inst_tac [("x","y")] allE 1); |
|
205 |
by (Asm_full_simp_tac 1); |
|
206 |
by (forward_tac [reachable.reachable_n] 1); |
|
207 |
by (assume_tac 1); |
|
208 |
by (Asm_full_simp_tac 1); |
|
209 |
qed_spec_mp"correp_is_exec_abs"; |
|
5670 | 210 |
*) |
4559 | 211 |
|
212 |
(* Does not work with abstraction_is_ref_map as proof of abs_safety, because |
|
213 |
is_live_abstraction includes temp_strengthening which is necessarily based |
|
214 |
on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific |
|
215 |
way for cex_abs *) |
|
5068 | 216 |
Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \ |
4559 | 217 |
\ is_live_abstraction h (C,M) (A,L) |] \ |
218 |
\ ==> live_implements (C,M) (A,L)"; |
|
219 |
||
220 |
by (asm_full_simp_tac (simpset() addsimps [is_live_abstraction_def, live_implements_def, |
|
221 |
livetraces_def,liveexecutions_def]) 1); |
|
222 |
by (safe_tac set_cs); |
|
223 |
by (res_inst_tac[("x","cex_abs h ex")] exI 1); |
|
224 |
by (safe_tac set_cs); |
|
225 |
(* Traces coincide *) |
|
226 |
by (pair_tac "ex" 1); |
|
227 |
by (rtac traces_coincide_abs 1); |
|
228 |
by (simp_tac (simpset() addsimps [externals_def])1); |
|
229 |
by (SELECT_GOAL (auto_tac (claset(),simpset()))1); |
|
230 |
||
231 |
(* cex_abs is execution *) |
|
232 |
by (pair_tac "ex" 1); |
|
233 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
|
234 |
(* start state *) |
|
235 |
by (rtac conjI 1); |
|
236 |
by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1); |
|
237 |
(* is-execution-fragment *) |
|
5670 | 238 |
by (etac exec_frag_abstraction 1); |
4559 | 239 |
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1); |
240 |
||
241 |
(* Liveness *) |
|
242 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2]) 1); |
|
243 |
by (pair_tac "ex" 1); |
|
244 |
qed"abs_liveness"; |
|
245 |
||
246 |
(* FIX: NAch Traces.ML bringen *) |
|
247 |
||
5068 | 248 |
Goalw [ioa_implements_def] |
4559 | 249 |
"!! A. [| A =<| B; B =<| C|] ==> A =<| C"; |
5132 | 250 |
by Auto_tac; |
4559 | 251 |
qed"implements_trans"; |
252 |
||
253 |
||
254 |
section "Abstraction Rules for Automata"; |
|
255 |
||
256 |
(* ---------------------------------------------------------------- *) |
|
257 |
(* Abstraction Rules for Automata *) |
|
258 |
(* ---------------------------------------------------------------- *) |
|
259 |
||
5068 | 260 |
Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \ |
4559 | 261 |
\ inp(Q)=inp(P); out(Q)=out(P); \ |
262 |
\ is_abstraction h1 C A; \ |
|
263 |
\ A =<| Q ; \ |
|
264 |
\ is_abstraction h2 Q P |] \ |
|
265 |
\ ==> C =<| P"; |
|
5132 | 266 |
by (dtac abs_safety 1); |
4559 | 267 |
by (REPEAT (atac 1)); |
5132 | 268 |
by (dtac abs_safety 1); |
4559 | 269 |
by (REPEAT (atac 1)); |
5132 | 270 |
by (etac implements_trans 1); |
271 |
by (etac implements_trans 1); |
|
272 |
by (assume_tac 1); |
|
4559 | 273 |
qed"AbsRuleA1"; |
274 |
||
275 |
||
5068 | 276 |
Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \ |
4559 | 277 |
\ inp(Q)=inp(P); out(Q)=out(P); \ |
278 |
\ is_live_abstraction h1 (C,LC) (A,LA); \ |
|
279 |
\ live_implements (A,LA) (Q,LQ) ; \ |
|
280 |
\ is_live_abstraction h2 (Q,LQ) (P,LP) |] \ |
|
281 |
\ ==> live_implements (C,LC) (P,LP)"; |
|
5132 | 282 |
by (dtac abs_liveness 1); |
4559 | 283 |
by (REPEAT (atac 1)); |
5132 | 284 |
by (dtac abs_liveness 1); |
4559 | 285 |
by (REPEAT (atac 1)); |
5132 | 286 |
by (etac live_implements_trans 1); |
287 |
by (etac live_implements_trans 1); |
|
288 |
by (assume_tac 1); |
|
4559 | 289 |
qed"AbsRuleA2"; |
290 |
||
291 |
||
292 |
Delsimps [split_paired_All]; |
|
293 |
||
294 |
||
295 |
section "Localizing Temporal Strengthenings and Weakenings"; |
|
296 |
||
297 |
(* ---------------------------------------------------------------- *) |
|
298 |
(* Localizing Temproal Strengthenings - 1 *) |
|
299 |
(* ---------------------------------------------------------------- *) |
|
300 |
||
5068 | 301 |
Goalw [temp_strengthening_def] |
4559 | 302 |
"!! h. [| temp_strengthening P1 Q1 h; \ |
303 |
\ temp_strengthening P2 Q2 h |] \ |
|
304 |
\ ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h"; |
|
5132 | 305 |
by Auto_tac; |
4559 | 306 |
qed"strength_AND"; |
307 |
||
5068 | 308 |
Goalw [temp_strengthening_def] |
4559 | 309 |
"!! h. [| temp_strengthening P1 Q1 h; \ |
310 |
\ temp_strengthening P2 Q2 h |] \ |
|
311 |
\ ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h"; |
|
5132 | 312 |
by Auto_tac; |
4559 | 313 |
qed"strength_OR"; |
314 |
||
5068 | 315 |
Goalw [temp_strengthening_def] |
4559 | 316 |
"!! h. [| temp_weakening P Q h |] \ |
317 |
\ ==> temp_strengthening (.~ P) (.~ Q) h"; |
|
318 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
5132 | 319 |
by Auto_tac; |
4559 | 320 |
qed"strength_NOT"; |
321 |
||
5068 | 322 |
Goalw [temp_strengthening_def] |
4559 | 323 |
"!! h. [| temp_weakening P1 Q1 h; \ |
324 |
\ temp_strengthening P2 Q2 h |] \ |
|
325 |
\ ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h"; |
|
326 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
327 |
qed"strength_IMPLIES"; |
|
328 |
||
329 |
||
330 |
||
331 |
(* ---------------------------------------------------------------- *) |
|
332 |
(* Localizing Temproal Weakenings - Part 1 *) |
|
333 |
(* ---------------------------------------------------------------- *) |
|
334 |
||
5068 | 335 |
Goal |
4559 | 336 |
"!! h. [| temp_weakening P1 Q1 h; \ |
337 |
\ temp_weakening P2 Q2 h |] \ |
|
338 |
\ ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h"; |
|
339 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
340 |
qed"weak_AND"; |
|
341 |
||
5068 | 342 |
Goal |
4559 | 343 |
"!! h. [| temp_weakening P1 Q1 h; \ |
344 |
\ temp_weakening P2 Q2 h |] \ |
|
345 |
\ ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h"; |
|
346 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
347 |
qed"weak_OR"; |
|
348 |
||
5068 | 349 |
Goalw [temp_strengthening_def] |
4559 | 350 |
"!! h. [| temp_strengthening P Q h |] \ |
351 |
\ ==> temp_weakening (.~ P) (.~ Q) h"; |
|
352 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
5132 | 353 |
by Auto_tac; |
4559 | 354 |
qed"weak_NOT"; |
355 |
||
5068 | 356 |
Goalw [temp_strengthening_def] |
4559 | 357 |
"!! h. [| temp_strengthening P1 Q1 h; \ |
358 |
\ temp_weakening P2 Q2 h |] \ |
|
359 |
\ ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h"; |
|
360 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1); |
|
361 |
qed"weak_IMPLIES"; |
|
362 |
||
363 |
||
364 |
(* ---------------------------------------------------------------- *) |
|
365 |
(* Localizing Temproal Strengthenings - 2 *) |
|
366 |
(* ---------------------------------------------------------------- *) |
|
4577
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 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
369 |
(* ------------------ Box ----------------------------*) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
370 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
371 |
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *) |
5068 | 372 |
Goal "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
373 |
by (Seq_case_simp_tac "x" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
374 |
by Auto_tac; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
375 |
qed"UU_is_Conc"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
376 |
|
5068 | 377 |
Goal |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
378 |
"Finite s1 --> \ |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
379 |
\ (! 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
|
380 |
by (rtac impI 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
381 |
by (Seq_Finite_induct_tac 1); |
5670 | 382 |
by (Blast_tac 1); |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
383 |
(* main case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
384 |
by (clarify_tac set_cs 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
385 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
386 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
387 |
(* UU case *) |
5676 | 388 |
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1); |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
389 |
(* nil case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
390 |
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
|
391 |
(* cons case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
392 |
by (pair_tac "aa" 1); |
5132 | 393 |
by Auto_tac; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
394 |
qed_spec_mp"ex2seqConc"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
395 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
396 |
(* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
397 |
|
5068 | 398 |
Goalw [tsuffix_def,suffix_def] |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
399 |
"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')"; |
5132 | 400 |
by Auto_tac; |
401 |
by (dtac ex2seqConc 1); |
|
402 |
by Auto_tac; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
403 |
qed"ex2seq_tsuffix"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
404 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
405 |
|
5068 | 406 |
Goal "(Map f`s = nil) = (s=nil)"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
407 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
408 |
qed"Mapnil"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
409 |
|
5068 | 410 |
Goal "(Map f`s = UU) = (s=UU)"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
411 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
412 |
qed"MapUU"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
413 |
|
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 |
(* 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
|
416 |
properties carry over *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
417 |
|
5068 | 418 |
Goalw [tsuffix_def,suffix_def,cex_absSeq_def] |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
419 |
"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)"; |
5132 | 420 |
by Auto_tac; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
421 |
by (asm_full_simp_tac (simpset() addsimps [Mapnil])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
422 |
by (asm_full_simp_tac (simpset() addsimps [MapUU])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
423 |
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
|
424 |
by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
425 |
qed"cex_absSeq_tsuffix"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
426 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
427 |
|
5068 | 428 |
Goalw [temp_strengthening_def,state_strengthening_def, temp_sat_def, |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
429 |
satisfies_def,Box_def] |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
430 |
"!! h. [| temp_strengthening P Q h |]\ |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
431 |
\ ==> temp_strengthening ([] P) ([] Q) h"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
432 |
by (clarify_tac set_cs 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
433 |
by (forward_tac [ex2seq_tsuffix] 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
434 |
by (clarify_tac set_cs 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
435 |
by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
436 |
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
|
437 |
qed"strength_Box"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
438 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
439 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
440 |
(* ------------------ Init ----------------------------*) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
441 |
|
5068 | 442 |
Goalw [temp_strengthening_def,state_strengthening_def, |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
443 |
temp_sat_def,satisfies_def,Init_def,unlift_def] |
4559 | 444 |
"!! h. [| state_strengthening P Q h |]\ |
445 |
\ ==> temp_strengthening (Init P) (Init Q) h"; |
|
446 |
by (safe_tac set_cs); |
|
447 |
by (pair_tac "ex" 1); |
|
448 |
by (Seq_case_simp_tac "y" 1); |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
449 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
450 |
qed"strength_Init"; |
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 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
453 |
(* ------------------ Next ----------------------------*) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
454 |
|
5068 | 455 |
Goal |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
456 |
"(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
|
457 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
458 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
459 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
460 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
461 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
462 |
qed"TL_ex2seq_UU"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
463 |
|
5068 | 464 |
Goal |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
465 |
"(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
|
466 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
467 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
468 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
469 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
470 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
471 |
qed"TL_ex2seq_nil"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
472 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
473 |
(* FIX: put to Sequence Lemmas *) |
5068 | 474 |
Goal "Map f`(TL`s) = TL`(Map f`s)"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
475 |
by (Seq_induct_tac "s" [] 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
476 |
qed"MapTL"; |
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 |
(* 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
|
479 |
properties carry over *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
480 |
|
5068 | 481 |
Goalw [cex_absSeq_def] |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
482 |
"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
483 |
by (simp_tac (simpset() addsimps [MapTL]) 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
484 |
qed"cex_absSeq_TL"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
485 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
486 |
(* important property of ex2seq: can be shiftet, as defined "pointwise" *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
487 |
|
5068 | 488 |
Goal "!!ex. [| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
489 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
490 |
by (Seq_case_simp_tac "y" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
491 |
by (pair_tac "a" 1); |
5132 | 492 |
by Auto_tac; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
493 |
qed"TLex2seq"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
494 |
|
5068 | 495 |
Goal "(TL`(ex2seq ex)~=UU) = ((snd ex)~=UU)"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
496 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
497 |
by (Seq_case_simp_tac "y" 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 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
500 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
501 |
qed"ex2seqUUTL"; |
5670 | 502 |
|
5068 | 503 |
Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil)"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
504 |
by (pair_tac "ex" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
505 |
by (Seq_case_simp_tac "y" 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 |
by (Seq_case_simp_tac "s" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
508 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
509 |
qed"ex2seqnilTL"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
510 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
511 |
|
5068 | 512 |
Goalw [temp_strengthening_def,state_strengthening_def, |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
513 |
temp_sat_def, satisfies_def,Next_def] |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
514 |
"!! h. [| temp_strengthening P Q h |]\ |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
515 |
\ ==> temp_strengthening (Next P) (Next Q) h"; |
4833 | 516 |
by (Asm_full_simp_tac 1); |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
517 |
by (safe_tac set_cs); |
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 |
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
|
521 |
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
|
522 |
(* cons case *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
523 |
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
|
524 |
ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1); |
5132 | 525 |
by (dtac TLex2seq 1); |
526 |
by (assume_tac 1); |
|
527 |
by Auto_tac; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
528 |
qed"strength_Next"; |
4559 | 529 |
|
530 |
||
531 |
||
532 |
(* ---------------------------------------------------------------- *) |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
533 |
(* Localizing Temporal Weakenings - 2 *) |
4559 | 534 |
(* ---------------------------------------------------------------- *) |
535 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
536 |
|
5068 | 537 |
Goal |
4559 | 538 |
"!! h. [| state_weakening P Q h |]\ |
539 |
\ ==> temp_weakening (Init P) (Init Q) h"; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
540 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
541 |
state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1); |
4559 | 542 |
by (safe_tac set_cs); |
543 |
by (pair_tac "ex" 1); |
|
544 |
by (Seq_case_simp_tac "y" 1); |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
545 |
by (pair_tac "a" 1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
546 |
qed"weak_Init"; |
4559 | 547 |
|
548 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
549 |
(* |
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 |
(* analog to strengthening thm above, with analog lemmas used *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
552 |
|
5068 | 553 |
Goalw [state_weakening_def] |
4559 | 554 |
"!! h. [| temp_weakening P Q h |]\ |
555 |
\ ==> temp_weakening ([] P) ([] Q) h"; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
556 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
557 |
temp_sat_def,satisfies_def,Box_def])1); |
4559 | 558 |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
559 |
(* analog to strengthening thm above, with analog lemmas used *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
560 |
|
5068 | 561 |
Goalw [state_weakening_def] |
4559 | 562 |
"!! h. [| temp_weakening P Q h |]\ |
563 |
\ ==> temp_weakening (Next P) (Next Q) h"; |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
564 |
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2, |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
565 |
temp_sat_def,satisfies_def,Next_def])1); |
4559 | 566 |
|
567 |
*) |
|
568 |
||
569 |
(* ---------------------------------------------------------------- *) |
|
570 |
(* Localizing Temproal Strengthenings - 3 *) |
|
571 |
(* ---------------------------------------------------------------- *) |
|
572 |
||
573 |
||
5068 | 574 |
Goalw [Diamond_def] |
4559 | 575 |
"!! h. [| temp_strengthening P Q h |]\ |
576 |
\ ==> temp_strengthening (<> P) (<> Q) h"; |
|
5132 | 577 |
by (rtac strength_NOT 1); |
578 |
by (rtac weak_Box 1); |
|
579 |
by (etac weak_NOT 1); |
|
4559 | 580 |
qed"strength_Diamond"; |
581 |
||
5068 | 582 |
Goalw [Leadsto_def] |
4559 | 583 |
"!! h. [| temp_weakening P1 P2 h;\ |
584 |
\ temp_strengthening Q1 Q2 h |]\ |
|
585 |
\ ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h"; |
|
5132 | 586 |
by (rtac strength_Box 1); |
587 |
by (etac strength_IMPLIES 1); |
|
588 |
by (etac strength_Diamond 1); |
|
4559 | 589 |
qed"strength_Leadsto"; |
590 |
||
591 |
||
592 |
(* ---------------------------------------------------------------- *) |
|
593 |
(* Localizing Temporal Weakenings - 3 *) |
|
594 |
(* ---------------------------------------------------------------- *) |
|
595 |
||
596 |
||
5068 | 597 |
Goalw [Diamond_def] |
4559 | 598 |
"!! h. [| temp_weakening P Q h |]\ |
599 |
\ ==> temp_weakening (<> P) (<> Q) h"; |
|
5132 | 600 |
by (rtac weak_NOT 1); |
601 |
by (rtac strength_Box 1); |
|
602 |
by (etac strength_NOT 1); |
|
4559 | 603 |
qed"weak_Diamond"; |
604 |
||
5068 | 605 |
Goalw [Leadsto_def] |
4559 | 606 |
"!! h. [| temp_strengthening P1 P2 h;\ |
607 |
\ temp_weakening Q1 Q2 h |]\ |
|
608 |
\ ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h"; |
|
5132 | 609 |
by (rtac weak_Box 1); |
610 |
by (etac weak_IMPLIES 1); |
|
611 |
by (etac weak_Diamond 1); |
|
4559 | 612 |
qed"weak_Leadsto"; |
613 |
||
5068 | 614 |
Goalw [WF_def] |
4559 | 615 |
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ |
616 |
\ ==> temp_weakening (WF A acts) (WF C acts) h"; |
|
5132 | 617 |
by (rtac weak_IMPLIES 1); |
618 |
by (rtac strength_Diamond 1); |
|
619 |
by (rtac strength_Box 1); |
|
620 |
by (rtac strength_Init 1); |
|
621 |
by (rtac weak_Box 2); |
|
622 |
by (rtac weak_Diamond 2); |
|
623 |
by (rtac weak_Init 2); |
|
4559 | 624 |
by (auto_tac (claset(), |
625 |
simpset() addsimps [state_weakening_def,state_strengthening_def, |
|
626 |
xt2_def,plift_def,option_lift_def,NOT_def])); |
|
627 |
qed"weak_WF"; |
|
628 |
||
5068 | 629 |
Goalw [SF_def] |
4559 | 630 |
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ |
631 |
\ ==> temp_weakening (SF A acts) (SF C acts) h"; |
|
5132 | 632 |
by (rtac weak_IMPLIES 1); |
633 |
by (rtac strength_Box 1); |
|
634 |
by (rtac strength_Diamond 1); |
|
635 |
by (rtac strength_Init 1); |
|
636 |
by (rtac weak_Box 2); |
|
637 |
by (rtac weak_Diamond 2); |
|
638 |
by (rtac weak_Init 2); |
|
4559 | 639 |
by (auto_tac (claset(), |
640 |
simpset() addsimps [state_weakening_def,state_strengthening_def, |
|
641 |
xt2_def,plift_def,option_lift_def,NOT_def])); |
|
642 |
qed"weak_SF"; |
|
643 |
||
644 |
||
645 |
val weak_strength_lemmas = |
|
646 |
[weak_OR,weak_AND,weak_NOT,weak_IMPLIES,weak_Box,weak_Next,weak_Init, |
|
647 |
weak_Diamond,weak_Leadsto,strength_OR,strength_AND,strength_NOT, |
|
648 |
strength_IMPLIES,strength_Box,strength_Next,strength_Init, |
|
649 |
strength_Diamond,strength_Leadsto,weak_WF,weak_SF]; |
|
650 |
||
651 |
fun abstraction_tac i = |
|
652 |
SELECT_GOAL (auto_tac (claset() addSIs weak_strength_lemmas, |
|
4725 | 653 |
simpset() addsimps [state_strengthening_def,state_weakening_def])) i; |