author  mueller 
Mon, 19 Oct 1998 15:49:55 +0200  
changeset 5676  96b048840bb3 
parent 5670  5e7d9455de96 
child 5677  4feffde494cf 
permissions  rwrr 
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 
(* isexecutionfragment *) 

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 
(* isexecutionfragment *) 

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; 