author  paulson 
Thu, 29 Apr 1999 10:51:58 +0200  
changeset 6536  281d44905cab 
parent 6295  351b3c2b0d83 
child 6564  c09997086ca7 
permissions  rwrr 
4776  1 
(* Title: HOL/UNITY/WFair 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
Weak Fairness versions of transient, ensures, leadsTo. 

7 

8 
From Misra, "A Logic for Concurrent Programming", 1994 

9 
*) 

10 

11 

5648  12 
overload_1st_set "WFair.transient"; 
13 
overload_1st_set "WFair.ensures"; 

6536  14 
overload_1st_set "WFair.op leadsTo"; 
5340  15 

4776  16 
(*** transient ***) 
17 

5069  18 
Goalw [stable_def, constrains_def, transient_def] 
5648  19 
"[ F : stable A; F : transient A ] ==> A = {}"; 
4776  20 
by (Blast_tac 1); 
21 
qed "stable_transient_empty"; 

22 

5069  23 
Goalw [transient_def] 
5648  24 
"[ F : transient A; B<=A ] ==> F : transient B"; 
4776  25 
by (Clarify_tac 1); 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5971
diff
changeset

26 
by (blast_tac (claset() addSIs [rev_bexI]) 1); 
4776  27 
qed "transient_strengthen"; 
28 

5069  29 
Goalw [transient_def] 
5648  30 
"[ act: Acts F; A <= Domain act; act^^A <= A ] ==> F : transient A"; 
4776  31 
by (Blast_tac 1); 
32 
qed "transient_mem"; 

33 

34 

35 
(*** ensures ***) 

36 

5069  37 
Goalw [ensures_def] 
6536  38 
"[ F : (AB) co (A Un B); F : transient (AB) ] \ 
39 
\ ==> F : A ensures B"; 

4776  40 
by (Blast_tac 1); 
41 
qed "ensuresI"; 

42 

5069  43 
Goalw [ensures_def] 
6536  44 
"F : A ensures B ==> F : (AB) co (A Un B) & F : transient (AB)"; 
4776  45 
by (Blast_tac 1); 
46 
qed "ensuresD"; 

47 

48 
(*The Lversion (precondition strengthening) doesn't hold for ENSURES*) 

5069  49 
Goalw [ensures_def] 
6536  50 
"[ F : A ensures A'; A'<=B' ] ==> F : A ensures B'"; 
4776  51 
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); 
52 
qed "ensures_weaken_R"; 

53 

5069  54 
Goalw [ensures_def, constrains_def, transient_def] 
6536  55 
"F : A ensures UNIV"; 
5340  56 
by Auto_tac; 
4776  57 
qed "ensures_UNIV"; 
58 

5069  59 
Goalw [ensures_def] 
5648  60 
"[ F : stable C; \ 
6536  61 
\ F : (C Int (A  A')) co (A Un A'); \ 
5648  62 
\ F : transient (C Int (AA')) ] \ 
6536  63 
\ ==> F : (C Int A) ensures (C Int A')"; 
4776  64 
by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym, 
65 
Diff_Int_distrib RS sym, 

66 
stable_constrains_Int]) 1); 

67 
qed "stable_ensures_Int"; 

68 

6536  69 
Goal "[ F : stable A; F : transient C; A <= B Un C ] ==> F : A ensures B"; 
5640  70 
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); 
71 
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); 

72 
qed "stable_transient_ensures"; 

73 

4776  74 

75 
(*** leadsTo ***) 

76 

6536  77 
Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B"; 
5648  78 
by (blast_tac (claset() addIs [leadsto.Basis]) 1); 
79 
qed "leadsTo_Basis"; 

4776  80 

5648  81 
Goalw [leadsTo_def] 
6536  82 
"[ F : A leadsTo B; F : B leadsTo C ] ==> F : A leadsTo C"; 
5648  83 
by (blast_tac (claset() addIs [leadsto.Trans]) 1); 
84 
qed "leadsTo_Trans"; 

85 

6536  86 
Goal "F : transient A ==> F : A leadsTo (A)"; 
5640  87 
by (asm_simp_tac 
88 
(simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); 

89 
qed "transient_imp_leadsTo"; 

90 

6536  91 
Goal "F : A leadsTo UNIV"; 
4776  92 
by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1); 
93 
qed "leadsTo_UNIV"; 

94 
Addsimps [leadsTo_UNIV]; 

95 

96 
(*Useful with cancellation, disjunction*) 

6536  97 
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; 
4776  98 
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); 
99 
qed "leadsTo_Un_duplicate"; 

100 

6536  101 
Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"; 
4776  102 
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); 
103 
qed "leadsTo_Un_duplicate2"; 

104 

105 
(*The Union introduction rule as we should have liked to state it*) 

5648  106 
val prems = Goalw [leadsTo_def] 
6536  107 
"(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"; 
5648  108 
by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1); 
4776  109 
qed "leadsTo_Union"; 
110 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

111 
val prems = Goalw [leadsTo_def] 
6536  112 
"(!!A. A : S ==> F : (A Int C) leadsTo B) \ 
113 
\ ==> F : (Union S Int C) leadsTo B"; 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

114 
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1); 
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

115 
by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1); 
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

116 
qed "leadsTo_Union_Int"; 
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

117 

5648  118 
val prems = Goal 
6536  119 
"(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"; 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

120 
by (stac (Union_image_eq RS sym) 1); 
5648  121 
by (blast_tac (claset() addIs leadsTo_Union::prems) 1); 
4776  122 
qed "leadsTo_UN"; 
123 

124 
(*Binary union introduction rule*) 

6536  125 
Goal "[ F : A leadsTo C; F : B leadsTo C ] ==> F : (A Un B) leadsTo C"; 
4776  126 
by (stac Un_eq_Union 1); 
127 
by (blast_tac (claset() addIs [leadsTo_Union]) 1); 

128 
qed "leadsTo_Un"; 

129 

130 

131 
(*The INDUCTION rule as we should have liked to state it*) 

5648  132 
val major::prems = Goalw [leadsTo_def] 
6536  133 
"[ F : za leadsTo zb; \ 
134 
\ !!A B. F : A ensures B ==> P A B; \ 

135 
\ !!A B C. [ F : A leadsTo B; P A B; F : B leadsTo C; P B C ] \ 

4776  136 
\ ==> P A C; \ 
6536  137 
\ !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \ 
4776  138 
\ ] ==> P za zb"; 
5648  139 
by (rtac (major RS CollectD RS leadsto.induct) 1); 
4776  140 
by (REPEAT (blast_tac (claset() addIs prems) 1)); 
141 
qed "leadsTo_induct"; 

142 

143 

6536  144 
Goal "A<=B ==> F : A leadsTo B"; 
4776  145 
by (rtac leadsTo_Basis 1); 
146 
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); 

147 
by (Blast_tac 1); 

148 
qed "subset_imp_leadsTo"; 

149 

150 
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); 

151 
Addsimps [empty_leadsTo]; 

152 

153 

6536  154 
Goal "[ F : A leadsTo A'; A'<=B' ] ==> F : A leadsTo B'"; 
5648  155 
by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1); 
156 
qed "leadsTo_weaken_R"; 

4776  157 

6536  158 
Goal "[ F : A leadsTo A'; B<=A ] ==> F : B leadsTo A'"; 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

159 
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); 
4776  160 
qed_spec_mp "leadsTo_weaken_L"; 
161 

162 
(*Distributes over binary unions*) 

6536  163 
Goal "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)"; 
4776  164 
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); 
165 
qed "leadsTo_Un_distrib"; 

166 

6536  167 
Goal "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)"; 
4776  168 
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); 
169 
qed "leadsTo_UN_distrib"; 

170 

6536  171 
Goal "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)"; 
4776  172 
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); 
173 
qed "leadsTo_Union_distrib"; 

174 

175 

6536  176 
Goal "[ F : A leadsTo A'; B<=A; A'<=B' ] ==> F : B leadsTo B'"; 
5340  177 
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, 
178 
leadsTo_Trans]) 1); 

4776  179 
qed "leadsTo_weaken"; 
180 

181 

182 
(*Set difference: maybe combine with leadsTo_weaken_L??*) 

6536  183 
Goal "[ F : (AB) leadsTo C; F : B leadsTo C ] ==> F : A leadsTo C"; 
4776  184 
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1); 
185 
qed "leadsTo_Diff"; 

186 

187 

188 
(** Meta or object quantifier ??? 

189 
see ball_constrains_UN in UNITY.ML***) 

190 

191 
val prems = goal thy 

6536  192 
"(!! i. i:I ==> F : (A i) leadsTo (A' i)) \ 
193 
\ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"; 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

194 
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); 
4776  195 
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
196 
addIs prems) 1); 

197 
qed "leadsTo_UN_UN"; 

198 

199 

200 
(*Version with no index set*) 

201 
val prems = goal thy 

6536  202 
"(!! i. F : (A i) leadsTo (A' i)) \ 
203 
\ ==> F : (UN i. A i) leadsTo (UN i. A' i)"; 

4776  204 
by (blast_tac (claset() addIs [leadsTo_UN_UN] 
205 
addIs prems) 1); 

206 
qed "leadsTo_UN_UN_noindex"; 

207 

208 
(*Version with no index set*) 

6536  209 
Goal "ALL i. F : (A i) leadsTo (A' i) \ 
210 
\ ==> F : (UN i. A i) leadsTo (UN i. A' i)"; 

4776  211 
by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1); 
212 
qed "all_leadsTo_UN_UN"; 

213 

214 

215 
(*Binary union version*) 

6536  216 
Goal "[ F : A leadsTo A'; F : B leadsTo B' ] ==> F : (A Un B) leadsTo (A' Un B')"; 
4776  217 
by (blast_tac (claset() addIs [leadsTo_Un, 
218 
leadsTo_weaken_R]) 1); 

219 
qed "leadsTo_Un_Un"; 

220 

221 

222 
(** The cancellation law **) 

223 

6536  224 
Goal "[ F : A leadsTo (A' Un B); F : B leadsTo B' ] \ 
225 
\ ==> F : A leadsTo (A' Un B')"; 

4776  226 
by (blast_tac (claset() addIs [leadsTo_Un_Un, 
227 
subset_imp_leadsTo, leadsTo_Trans]) 1); 

228 
qed "leadsTo_cancel2"; 

229 

6536  230 
Goal "[ F : A leadsTo (A' Un B); F : (BA') leadsTo B' ] \ 
231 
\ ==> F : A leadsTo (A' Un B')"; 

4776  232 
by (rtac leadsTo_cancel2 1); 
233 
by (assume_tac 2); 

234 
by (ALLGOALS Asm_simp_tac); 

235 
qed "leadsTo_cancel_Diff2"; 

236 

6536  237 
Goal "[ F : A leadsTo (B Un A'); F : B leadsTo B' ] \ 
238 
\ ==> F : A leadsTo (B' Un A')"; 

4776  239 
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); 
240 
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); 

241 
qed "leadsTo_cancel1"; 

242 

6536  243 
Goal "[ F : A leadsTo (B Un A'); F : (BA') leadsTo B' ] \ 
244 
\ ==> F : A leadsTo (B' Un A')"; 

4776  245 
by (rtac leadsTo_cancel1 1); 
246 
by (assume_tac 2); 

247 
by (ALLGOALS Asm_simp_tac); 

248 
qed "leadsTo_cancel_Diff1"; 

249 

250 

251 

252 
(** The impossibility law **) 

253 

6536  254 
Goal "F : A leadsTo B ==> B={} > A={}"; 
4776  255 
by (etac leadsTo_induct 1); 
256 
by (ALLGOALS Asm_simp_tac); 

257 
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); 

258 
by (Blast_tac 1); 

259 
val lemma = result() RS mp; 

260 

6536  261 
Goal "F : A leadsTo {} ==> A={}"; 
4776  262 
by (blast_tac (claset() addSIs [lemma]) 1); 
263 
qed "leadsTo_empty"; 

264 

265 

266 
(** PSP: ProgressSafetyProgress **) 

267 

5640  268 
(*Special case of PSP: Misra's "stable conjunction"*) 
5069  269 
Goalw [stable_def] 
6536  270 
"[ F : A leadsTo A'; F : stable B ] \ 
271 
\ ==> F : (A Int B) leadsTo (A' Int B)"; 

4776  272 
by (etac leadsTo_induct 1); 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

273 
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); 
4776  274 
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); 
275 
by (rtac leadsTo_Basis 1); 

276 
by (asm_full_simp_tac 

277 
(simpset() addsimps [ensures_def, 

278 
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1); 

279 
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1); 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

280 
qed "psp_stable"; 
4776  281 

6536  282 
Goal "[ F : A leadsTo A'; F : stable B ] \ 
283 
\ ==> F : (B Int A) leadsTo (B Int A')"; 

5536  284 
by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

285 
qed "psp_stable2"; 
4776  286 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

287 
Goalw [ensures_def, constrains_def] 
6536  288 
"[ F : A ensures A'; F : B co B' ] \ 
289 
\ ==> F : (A Int B) ensures ((A' Int B) Un (B'  B))"; 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

290 
by (blast_tac (claset() addIs [transient_strengthen]) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

291 
qed "psp_ensures"; 
4776  292 

6536  293 
Goal "[ F : A leadsTo A'; F : B co B' ] \ 
294 
\ ==> F : (A Int B) leadsTo ((A' Int B) Un (B'  B))"; 

4776  295 
by (etac leadsTo_induct 1); 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

296 
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); 
4776  297 
(*Transitivity case has a delicate argument involving "cancellation"*) 
298 
by (rtac leadsTo_Un_duplicate2 2); 

299 
by (etac leadsTo_cancel_Diff1 2); 

300 
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); 

301 
(*Basis case*) 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

302 
by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

303 
qed "psp"; 
4776  304 

6536  305 
Goal "[ F : A leadsTo A'; F : B co B' ] \ 
306 
\ ==> F : (B Int A) leadsTo ((B Int A') Un (B'  B))"; 

5536  307 
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

308 
qed "psp2"; 
4776  309 

310 

5069  311 
Goalw [unless_def] 
6536  312 
"[ F : A leadsTo A'; F : B unless B' ] \ 
313 
\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')"; 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

314 
by (dtac psp 1); 
4776  315 
by (assume_tac 1); 
5648  316 
by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 1); 
317 
by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 1); 

318 
by (etac leadsTo_Diff 1); 

319 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

320 
qed "psp_unless"; 
4776  321 

322 

323 
(*** Proving the induction rules ***) 

324 

5257  325 
(** The most general rule: r is any wf relation; f is any variant function **) 
326 

5239  327 
Goal "[ wf r; \ 
6536  328 
\ ALL m. F : (A Int f``{m}) leadsTo \ 
5648  329 
\ ((A Int f``(r^1 ^^ {m})) Un B) ] \ 
6536  330 
\ ==> F : (A Int f``{m}) leadsTo B"; 
4776  331 
by (eres_inst_tac [("a","m")] wf_induct 1); 
6536  332 
by (subgoal_tac "F : (A Int (f `` (r^1 ^^ {x}))) leadsTo B" 1); 
4776  333 
by (stac vimage_eq_UN 2); 
334 
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2); 

335 
by (blast_tac (claset() addIs [leadsTo_UN]) 2); 

336 
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); 

337 
val lemma = result(); 

338 

339 

340 
(** Meta or object quantifier ????? **) 

5239  341 
Goal "[ wf r; \ 
6536  342 
\ ALL m. F : (A Int f``{m}) leadsTo \ 
5648  343 
\ ((A Int f``(r^1 ^^ {m})) Un B) ] \ 
6536  344 
\ ==> F : A leadsTo B"; 
4776  345 
by (res_inst_tac [("t", "A")] subst 1); 
346 
by (rtac leadsTo_UN 2); 

347 
by (etac lemma 2); 

348 
by (REPEAT (assume_tac 2)); 

349 
by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*) 

350 
qed "leadsTo_wf_induct"; 

351 

352 

5239  353 
Goal "[ wf r; \ 
6536  354 
\ ALL m:I. F : (A Int f``{m}) leadsTo \ 
5648  355 
\ ((A Int f``(r^1 ^^ {m})) Un B) ] \ 
6536  356 
\ ==> F : A leadsTo ((A  (f``I)) Un B)"; 
4776  357 
by (etac leadsTo_wf_induct 1); 
358 
by Safe_tac; 

359 
by (case_tac "m:I" 1); 

360 
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); 

361 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); 

362 
qed "bounded_induct"; 

363 

364 

6536  365 
(*Alternative proof is via the lemma F : (A Int f``(lessThan m)) leadsTo B*) 
366 
Goal "[ ALL m. F : (A Int f``{m}) leadsTo \ 

5648  367 
\ ((A Int f``(lessThan m)) Un B) ] \ 
6536  368 
\ ==> F : A leadsTo B"; 
4776  369 
by (rtac (wf_less_than RS leadsTo_wf_induct) 1); 
370 
by (Asm_simp_tac 1); 

371 
qed "lessThan_induct"; 

372 

6536  373 
Goal "[ ALL m:(greaterThan l). F : (A Int f``{m}) leadsTo \ 
5648  374 
\ ((A Int f``(lessThan m)) Un B) ] \ 
6536  375 
\ ==> F : A leadsTo ((A Int (f``(atMost l))) Un B)"; 
5648  376 
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
377 
Compl_greaterThan RS sym]) 1); 

4776  378 
by (rtac (wf_less_than RS bounded_induct) 1); 
379 
by (Asm_simp_tac 1); 

380 
qed "lessThan_bounded_induct"; 

381 

6536  382 
Goal "[ ALL m:(lessThan l). F : (A Int f``{m}) leadsTo \ 
5648  383 
\ ((A Int f``(greaterThan m)) Un B) ] \ 
6536  384 
\ ==> F : A leadsTo ((A Int (f``(atLeast l))) Un B)"; 
4776  385 
by (res_inst_tac [("f","f"),("f1", "%k. l  k")] 
386 
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1); 

387 
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); 

388 
by (Clarify_tac 1); 

389 
by (case_tac "m<l" 1); 

390 
by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2); 

391 
by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1); 

392 
qed "greaterThan_bounded_induct"; 

393 

394 

395 

396 
(*** wlt ****) 

397 

398 
(*Misra's property W3*) 

6536  399 
Goalw [wlt_def] "F : (wlt F B) leadsTo B"; 
4776  400 
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); 
401 
qed "wlt_leadsTo"; 

402 

6536  403 
Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B"; 
4776  404 
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); 
405 
qed "leadsTo_subset"; 

406 

407 
(*Misra's property W2*) 

6536  408 
Goal "F : A leadsTo B = (A <= wlt F B)"; 
4776  409 
by (blast_tac (claset() addSIs [leadsTo_subset, 
410 
wlt_leadsTo RS leadsTo_weaken_L]) 1); 

411 
qed "leadsTo_eq_subset_wlt"; 

412 

413 
(*Misra's property W4*) 

5648  414 
Goal "B <= wlt F B"; 
4776  415 
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym, 
416 
subset_imp_leadsTo]) 1); 

417 
qed "wlt_increasing"; 

418 

419 

420 
(*Used in the Trans case below*) 

5069  421 
Goalw [constrains_def] 
5111  422 
"[ B <= A2; \ 
6536  423 
\ F : (A1  B) co (A1 Un B); \ 
424 
\ F : (A2  C) co (A2 Un C) ] \ 

425 
\ ==> F : (A1 Un A2  C) co (A1 Un A2 Un C)"; 

5669  426 
by (Clarify_tac 1); 
5620  427 
by (Blast_tac 1); 
4776  428 
val lemma1 = result(); 
429 

430 

431 
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) 

6536  432 
Goal "F : A leadsTo A' ==> \ 
433 
\ EX B. A<=B & F : B leadsTo A' & F : (BA') co (B Un A')"; 

4776  434 
by (etac leadsTo_induct 1); 
435 
(*Basis*) 

436 
by (blast_tac (claset() addIs [leadsTo_Basis] 

437 
addDs [ensuresD]) 1); 

438 
(*Trans*) 

439 
by (Clarify_tac 1); 

440 
by (res_inst_tac [("x", "Ba Un Bb")] exI 1); 

441 
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1, 

442 
leadsTo_Un_duplicate]) 1); 

443 
(*Union*) 

444 
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, 

445 
bchoice, ball_constrains_UN]) 1);; 

446 
by (res_inst_tac [("x", "UN A:S. f A")] exI 1); 

447 
by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1); 

448 
qed "leadsTo_123"; 

449 

450 

451 
(*Misra's property W5*) 

6536  452 
Goal "F : (wlt F B  B) co (wlt F B)"; 
5648  453 
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); 
4776  454 
by (Clarify_tac 1); 
5648  455 
by (subgoal_tac "Ba = wlt F B" 1); 
456 
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2); 

4776  457 
by (Clarify_tac 1); 
458 
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1); 

459 
qed "wlt_constrains_wlt"; 

460 

461 

462 
(*** Completion: Binary and General Finite versions ***) 

463 

6536  464 
Goal "[ F : A leadsTo A'; F : stable A'; \ 
465 
\ F : B leadsTo B'; F : stable B' ] \ 

466 
\ ==> F : (A Int B) leadsTo (A' Int B')"; 

5648  467 
by (subgoal_tac "F : stable (wlt F B')" 1); 
4776  468 
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2); 
469 
by (EVERY [etac (constrains_Un RS constrains_weaken) 2, 

5648  470 
rtac wlt_constrains_wlt 2, 
4776  471 
fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3, 
472 
Blast_tac 2]); 

6536  473 
by (subgoal_tac "F : (A Int wlt F B') leadsTo (A' Int wlt F B')" 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

474 
by (blast_tac (claset() addIs [psp_stable]) 2); 
6536  475 
by (subgoal_tac "F : (A' Int wlt F B') leadsTo (A' Int B')" 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

476 
by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2); 
6536  477 
by (subgoal_tac "F : (A Int B) leadsTo (A Int wlt F B')" 1); 
4776  478 
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
479 
subset_imp_leadsTo]) 2); 

5479  480 
by (blast_tac (claset() addIs [leadsTo_Trans]) 1); 
4776  481 
qed "stable_completion"; 
482 

483 

6536  484 
Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i)) > \ 
5648  485 
\ (ALL i:I. F : stable (A' i)) > \ 
6536  486 
\ F : (INT i:I. A i) leadsTo (INT i:I. A' i)"; 
4776  487 
by (etac finite_induct 1); 
488 
by (Asm_simp_tac 1); 

489 
by (asm_simp_tac 

490 
(simpset() addsimps [stable_completion, stable_def, 

491 
ball_constrains_INT]) 1); 

492 
qed_spec_mp "finite_stable_completion"; 

493 

494 

5648  495 
Goal "[ W = wlt F (B' Un C); \ 
6536  496 
\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \ 
497 
\ F : B leadsTo (B' Un C); F : B' co (B' Un C) ] \ 

498 
\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"; 

499 
by (subgoal_tac "F : (WC) co (W Un B' Un C)" 1); 

4776  500 
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
501 
MRS constrains_Un RS constrains_weaken]) 2); 

6536  502 
by (subgoal_tac "F : (WC) co W" 1); 
4776  503 
by (asm_full_simp_tac 
504 
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); 

6536  505 
by (subgoal_tac "F : (A Int W  C) leadsTo (A' Int W Un C)" 1); 
4776  506 
by (simp_tac (simpset() addsimps [Int_Diff]) 2); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

507 
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2); 
5456  508 
(** LEVEL 7 **) 
6536  509 
by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); 
4776  510 
by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

511 
psp2 RS leadsTo_weaken_R, 
4776  512 
subset_refl RS subset_imp_leadsTo, 
513 
leadsTo_Un_duplicate2]) 2); 

514 
by (dtac leadsTo_Diff 1); 

515 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); 

516 
by (subgoal_tac "A Int B <= A Int W" 1); 

5456  517 
by (blast_tac (claset() addSDs [leadsTo_subset] 
518 
addSIs [subset_refl RS Int_mono]) 2); 

4776  519 
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); 
520 
bind_thm("completion", refl RS result()); 

521 

522 

6536  523 
Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) > \ 
524 
\ (ALL i:I. F : (A' i) co (A' i Un C)) > \ 

525 
\ F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"; 

4776  526 
by (etac finite_induct 1); 
527 
by (ALLGOALS Asm_simp_tac); 

528 
by (Clarify_tac 1); 

529 
by (dtac ball_constrains_INT 1); 

530 
by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 

531 
qed "finite_completion"; 

532 