176 proof- |
164 proof- |
177 have "\<forall>c. strip(c \<nabla>\<^sub>c f c) = strip c" by (metis assms(1) strip_map2_acom) |
165 have "\<forall>c. strip(c \<nabla>\<^sub>c f c) = strip c" by (metis assms(1) strip_map2_acom) |
178 from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def) |
166 from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def) |
179 qed |
167 qed |
180 |
168 |
181 lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" |
169 lemma iter_narrow_pfp: assumes "mono f" and "f c0 \<sqsubseteq> c0" |
182 and "prefp (\<lambda>c. c \<triangle>\<^sub>c f c) x0 = Some x" |
170 and "iter_narrow f c0 = Some c" |
183 shows "f x \<sqsubseteq> x \<and> x \<sqsubseteq> x0" (is "?P x") |
171 shows "f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0" (is "?P c") |
184 proof- |
172 proof- |
185 { fix x assume "?P x" |
173 { fix c assume "?P c" |
186 note 1 = conjunct1[OF this] and 2 = conjunct2[OF this] |
174 note 1 = conjunct1[OF this] and 2 = conjunct2[OF this] |
187 let ?x' = "x \<triangle>\<^sub>c f x" |
175 let ?c' = "c \<triangle>\<^sub>c f c" |
188 have "?P ?x'" |
176 have "?P ?c'" |
189 proof |
177 proof |
190 have "f ?x' \<sqsubseteq> f x" by(rule monoD[OF `mono f` narrow2_acom[OF 1]]) |
178 have "f ?c' \<sqsubseteq> f c" by(rule monoD[OF `mono f` narrow2_acom[OF 1]]) |
191 also have "\<dots> \<sqsubseteq> ?x'" by(rule narrow1_acom[OF 1]) |
179 also have "\<dots> \<sqsubseteq> ?c'" by(rule narrow1_acom[OF 1]) |
192 finally show "f ?x' \<sqsubseteq> ?x'" . |
180 finally show "f ?c' \<sqsubseteq> ?c'" . |
193 have "?x' \<sqsubseteq> x" by (rule narrow2_acom[OF 1]) |
181 have "?c' \<sqsubseteq> c" by (rule narrow2_acom[OF 1]) |
194 also have "x \<sqsubseteq> x0" by(rule 2) |
182 also have "c \<sqsubseteq> c0" by(rule 2) |
195 finally show "?x' \<sqsubseteq> x0" . |
183 finally show "?c' \<sqsubseteq> c0" . |
196 qed |
184 qed |
197 } |
185 } |
198 with while_option_rule[where P = ?P, OF _ assms(3)[simplified prefp_def]] |
186 with while_option_rule[where P = ?P, OF _ assms(3)[simplified iter_narrow_def]] |
199 assms(2) le_refl |
187 assms(2) le_refl |
200 show ?thesis by blast |
188 show ?thesis by blast |
201 qed |
189 qed |
202 |
190 |
203 lemma pfp_WN_pfp: |
191 lemma pfp_wn_pfp: |
204 "\<lbrakk> mono f; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'" |
192 "\<lbrakk> mono f; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'" |
205 unfolding pfp_WN_def |
193 unfolding pfp_wn_def |
206 by (auto dest: iter_down_pfp iter_widen_pfp split: option.splits) |
194 by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits) |
207 |
195 |
208 lemma strip_pfp_WN: |
196 lemma strip_pfp_wn: |
209 "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c" |
197 "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c" |
210 apply(auto simp add: pfp_WN_def prefp_def split: option.splits) |
198 apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) |
211 by (metis (no_types) strip_map2_acom strip_while strip_bot_acom strip_iter_widen) |
199 by (metis (no_types) strip_map2_acom strip_while strip_bot_acom strip_iter_widen) |
212 |
200 |
213 locale Abs_Int2 = Abs_Int1_mono |
201 locale Abs_Int2 = Abs_Int1_mono |
214 where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set" |
202 where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set" |
215 begin |
203 begin |
216 |
204 |
217 definition AI_WN :: "com \<Rightarrow> 'av st option acom option" where |
205 definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where |
218 "AI_WN = pfp_WN (step' \<top>)" |
206 "AI_wn = pfp_wn (step' \<top>)" |
219 |
207 |
220 lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'" |
208 lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'" |
221 proof(simp add: CS_def AI_WN_def) |
209 proof(simp add: CS_def AI_wn_def) |
222 assume 1: "pfp_WN (step' \<top>) c = Some c'" |
210 assume 1: "pfp_wn (step' \<top>) c = Some c'" |
223 from pfp_WN_pfp[OF mono_step'2 1] |
211 from pfp_wn_pfp[OF mono_step'2 1] |
224 have 2: "step' \<top> c' \<sqsubseteq> c'" . |
212 have 2: "step' \<top> c' \<sqsubseteq> c'" . |
225 have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1]) |
213 have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_wn[OF _ 1]) |
226 have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')" |
214 have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')" |
227 proof(rule lfp_lowerbound[simplified,OF 3]) |
215 proof(rule lfp_lowerbound[simplified,OF 3]) |
228 show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
216 show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
229 proof(rule step_preserves_le[OF _ _]) |
217 proof(rule step_preserves_le[OF _ _]) |
230 show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp |
218 show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp |
268 value [code] "show_acom_opt (AI_ivl' test5_ivl)" |
256 value [code] "show_acom_opt (AI_ivl' test5_ivl)" |
269 value [code] "show_acom_opt (AI_ivl' test6_ivl)" |
257 value [code] "show_acom_opt (AI_ivl' test6_ivl)" |
270 |
258 |
271 |
259 |
272 subsubsection "Termination: Intervals" |
260 subsubsection "Termination: Intervals" |
|
261 |
|
262 definition m_ivl :: "ivl \<Rightarrow> nat" where |
|
263 "m_ivl ivl = (case ivl of I l h \<Rightarrow> |
|
264 (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))" |
|
265 |
|
266 lemma m_ivl_height: "m_ivl ivl \<le> 2" |
|
267 by(simp add: m_ivl_def split: ivl.split option.split) |
|
268 |
|
269 lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y" |
|
270 by(auto simp: m_ivl_def le_option_def le_ivl_def |
|
271 split: ivl.split option.split if_splits) |
|
272 |
|
273 lemma m_ivl_widen: |
|
274 "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x" |
|
275 by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def |
|
276 split: ivl.splits option.splits if_splits) |
|
277 |
|
278 lemma Top_less_ivl: "\<top> \<sqsubseteq> x \<Longrightarrow> m_ivl x = 0" |
|
279 by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def |
|
280 split: ivl.split option.split if_splits) |
|
281 |
|
282 |
|
283 definition n_ivl :: "ivl \<Rightarrow> nat" where |
|
284 "n_ivl ivl = 2 - m_ivl ivl" |
|
285 |
|
286 lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y" |
|
287 unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono) |
|
288 |
|
289 lemma n_ivl_narrow: |
|
290 "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x" |
|
291 by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def |
|
292 split: ivl.splits option.splits if_splits) |
|
293 |
|
294 |
|
295 subsubsection "Termination: Abstract State" |
|
296 |
|
297 definition "m_st m st = (\<Sum>x\<in>set(dom st). m(fun st x))" |
|
298 |
|
299 lemma m_st_height: assumes "finite X" and "set (dom S) \<subseteq> X" |
|
300 shows "m_st m_ivl S \<le> 2 * card X" |
|
301 proof(auto simp: m_st_def) |
|
302 have "(\<Sum>x\<in>set(dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set(dom S). 2)" (is "?L \<le> _") |
|
303 by(rule setsum_mono)(simp add:m_ivl_height) |
|
304 also have "\<dots> \<le> (\<Sum>x\<in>X. 2)" |
|
305 by(rule setsum_mono3[OF assms]) simp |
|
306 also have "\<dots> = 2 * card X" by(simp add: setsum_constant) |
|
307 finally show "?L \<le> \<dots>" . |
|
308 qed |
|
309 |
|
310 lemma m_st_anti_mono: |
|
311 "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st m_ivl S2 \<le> m_st m_ivl S1" |
|
312 proof(auto simp: m_st_def le_st_def lookup_def split: if_splits) |
|
313 let ?X = "set(dom S1)" let ?Y = "set(dom S2)" |
|
314 let ?f = "fun S1" let ?g = "fun S2" |
|
315 assume asm: "\<forall>x\<in>?Y. (x \<in> ?X \<longrightarrow> ?f x \<sqsubseteq> ?g x) \<and> (x \<in> ?X \<or> \<top> \<sqsubseteq> ?g x)" |
|
316 hence 1: "\<forall>y\<in>?Y\<inter>?X. m_ivl(?g y) \<le> m_ivl(?f y)" by(simp add: m_ivl_anti_mono) |
|
317 have 0: "\<forall>x\<in>?Y-?X. m_ivl(?g x) = 0" using asm by (auto simp: Top_less_ivl) |
|
318 have "(\<Sum>y\<in>?Y. m_ivl(?g y)) = (\<Sum>y\<in>(?Y-?X) \<union> (?Y\<inter>?X). m_ivl(?g y))" |
|
319 by (metis Un_Diff_Int) |
|
320 also have "\<dots> = (\<Sum>y\<in>?Y-?X. m_ivl(?g y)) + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" |
|
321 by(subst setsum_Un_disjoint) auto |
|
322 also have "(\<Sum>y\<in>?Y-?X. m_ivl(?g y)) = 0" using 0 by simp |
|
323 also have "0 + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y)) = (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" by simp |
|
324 also have "\<dots> \<le> (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?f y))" |
|
325 by(rule setsum_mono)(simp add: 1) |
|
326 also have "\<dots> \<le> (\<Sum>y\<in>?X. m_ivl(?f y))" |
|
327 by(simp add: setsum_mono3[of "?X" "?Y Int ?X", OF _ Int_lower2]) |
|
328 finally show "(\<Sum>y\<in>?Y. m_ivl(?g y)) \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" |
|
329 by (metis add_less_cancel_left) |
|
330 qed |
|
331 |
|
332 lemma m_st_widen: |
|
333 assumes "\<not> S2 \<sqsubseteq> S1" shows "m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1" |
|
334 proof- |
|
335 { let ?X = "set(dom S1)" let ?Y = "set(dom S2)" |
|
336 let ?f = "fun S1" let ?g = "fun S2" |
|
337 fix x assume "x \<in> ?X" "\<not> lookup S2 x \<sqsubseteq> ?f x" |
|
338 have "(\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x)) < (\<Sum>x\<in>?X. m_ivl(?f x))" (is "?L < ?R") |
|
339 proof cases |
|
340 assume "x : ?Y" |
|
341 have "?L < (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" |
|
342 proof(rule setsum_strict_mono1, simp) |
|
343 show "\<forall>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" |
|
344 by (metis m_ivl_anti_mono widen1) |
|
345 next |
|
346 show "\<exists>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) < m_ivl(?f x)" |
|
347 using `x:?X` `x:?Y` `\<not> lookup S2 x \<sqsubseteq> ?f x` |
|
348 by (metis IntI m_ivl_widen lookup_def) |
|
349 qed |
|
350 also have "\<dots> \<le> ?R" by(simp add: setsum_mono3[OF _ Int_lower1]) |
|
351 finally show ?thesis . |
|
352 next |
|
353 assume "x ~: ?Y" |
|
354 have "?L \<le> (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" |
|
355 proof(rule setsum_mono, simp) |
|
356 fix x assume "x:?X \<and> x:?Y" show "m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" |
|
357 by (metis m_ivl_anti_mono widen1) |
|
358 qed |
|
359 also have "\<dots> < m_ivl(?f x) + \<dots>" |
|
360 using m_ivl_widen[OF `\<not> lookup S2 x \<sqsubseteq> ?f x`] |
|
361 by (metis Nat.le_refl add_strict_increasing gr0I not_less0) |
|
362 also have "\<dots> = (\<Sum>y\<in>insert x (?X\<inter>?Y). m_ivl(?f y))" |
|
363 using `x ~: ?Y` by simp |
|
364 also have "\<dots> \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" |
|
365 by(rule setsum_mono3)(insert `x:?X`, auto) |
|
366 finally show ?thesis . |
|
367 qed |
|
368 } with assms show ?thesis |
|
369 by(auto simp: le_st_def widen_st_def m_st_def Int_def) |
|
370 qed |
|
371 |
|
372 definition "n_st m X st = (\<Sum>x\<in>X. m(lookup st x))" |
|
373 |
|
374 lemma n_st_mono: assumes "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" "S1 \<sqsubseteq> S2" |
|
375 shows "n_st n_ivl X S1 \<le> n_st n_ivl X S2" |
|
376 proof- |
|
377 have "(\<Sum>x\<in>X. n_ivl(lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl(lookup S2 x))" |
|
378 apply(rule setsum_mono) using assms |
|
379 by(auto simp: le_st_def lookup_def n_ivl_mono split: if_splits) |
|
380 thus ?thesis by(simp add: n_st_def) |
|
381 qed |
|
382 |
|
383 lemma n_st_narrow: |
|
384 assumes "finite X" and "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" |
|
385 and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2" |
|
386 shows "n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1" |
|
387 proof- |
|
388 have 1: "\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)" |
|
389 using assms(2-4) |
|
390 by(auto simp: le_st_def narrow_st_def lookup_def n_ivl_mono narrow2 |
|
391 split: if_splits) |
|
392 have 2: "\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)" |
|
393 using assms(2-5) |
|
394 by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow |
|
395 split: if_splits) |
|
396 have "(\<Sum>x\<in>X. n_ivl(lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl(lookup S1 x))" |
|
397 apply(rule setsum_strict_mono1[OF `finite X`]) using 1 2 by blast+ |
|
398 thus ?thesis by(simp add: n_st_def) |
|
399 qed |
|
400 |
|
401 |
|
402 subsubsection "Termination: Option" |
|
403 |
|
404 definition "m_o m n opt = (case opt of None \<Rightarrow> n+1 | Some x \<Rightarrow> m x)" |
|
405 |
|
406 lemma m_o_anti_mono: "finite X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> |
|
407 m_o (m_st m_ivl) (2 * card X) S2 \<le> m_o (m_st m_ivl) (2 * card X) S1" |
|
408 apply(induction S1 S2 rule: le_option.induct) |
|
409 apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height |
|
410 split: option.splits) |
|
411 done |
|
412 |
|
413 lemma m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow> |
|
414 m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1" |
|
415 by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le m_st_widen |
|
416 split: option.split) |
|
417 |
|
418 definition "n_o n opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n x + 1)" |
|
419 |
|
420 lemma n_o_mono: "domo S1 \<subseteq> X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> |
|
421 n_o (n_st n_ivl X) S1 \<le> n_o (n_st n_ivl X) S2" |
|
422 apply(induction S1 S2 rule: le_option.induct) |
|
423 apply(auto simp: domo_def n_o_def n_st_mono |
|
424 split: option.splits) |
|
425 done |
|
426 |
|
427 lemma n_o_narrow: |
|
428 "\<lbrakk> finite X; domo S1 \<subseteq> X; domo S2 \<subseteq> X; S2 \<sqsubseteq> S1; \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<rbrakk> |
|
429 \<Longrightarrow> n_o (n_st n_ivl X) (S1 \<triangle> S2) < n_o (n_st n_ivl X) S1" |
|
430 apply(induction S1 S2 rule: narrow_option.induct) |
|
431 apply(auto simp: n_o_def domo_def n_st_narrow) |
|
432 done |
|
433 |
|
434 lemma domo_widen_subset: "domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2" |
|
435 apply(induction S1 S2 rule: widen_option.induct) |
|
436 apply (auto simp: domo_def widen_st_def) |
|
437 done |
|
438 |
|
439 lemma domo_narrow_subset: "domo (S1 \<triangle> S2) \<subseteq> domo S1 \<union> domo S2" |
|
440 apply(induction S1 S2 rule: narrow_option.induct) |
|
441 apply (auto simp: domo_def narrow_st_def) |
|
442 done |
|
443 |
|
444 subsubsection "Termination: Commands" |
|
445 |
|
446 lemma strip_widen_acom[simp]: |
|
447 "strip c' = strip (c::'a::WN acom) \<Longrightarrow> strip (c \<nabla>\<^sub>c c') = strip c" |
|
448 by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all |
|
449 |
|
450 lemma strip_narrow_acom[simp]: |
|
451 "strip c' = strip (c::'a::WN acom) \<Longrightarrow> strip (c \<triangle>\<^sub>c c') = strip c" |
|
452 by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all |
|
453 |
|
454 lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow> |
|
455 annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))" |
|
456 by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct) |
|
457 (simp_all add: size_annos_same2) |
|
458 |
|
459 lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow> |
|
460 annos(c1 \<triangle>\<^sub>c c2) = map (%(x,y).x\<triangle>y) (zip (annos c1) (annos(c2::'a::WN acom)))" |
|
461 by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct) |
|
462 (simp_all add: size_annos_same2) |
|
463 |
|
464 lemma widen_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow> |
|
465 c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<nabla>\<^sub>c c2) : Com X" |
|
466 apply(auto simp add: Com_def) |
|
467 apply(rename_tac S S' x) |
|
468 apply(erule in_set_zipE) |
|
469 apply(auto simp: domo_def split: option.splits) |
|
470 apply(case_tac S) |
|
471 apply(case_tac S') |
|
472 apply simp |
|
473 apply fastforce |
|
474 apply(case_tac S') |
|
475 apply fastforce |
|
476 apply (fastforce simp: widen_st_def) |
|
477 done |
|
478 |
|
479 lemma narrow_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow> |
|
480 c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<triangle>\<^sub>c c2) : Com X" |
|
481 apply(auto simp add: Com_def) |
|
482 apply(rename_tac S S' x) |
|
483 apply(erule in_set_zipE) |
|
484 apply(auto simp: domo_def split: option.splits) |
|
485 apply(case_tac S) |
|
486 apply(case_tac S') |
|
487 apply simp |
|
488 apply fastforce |
|
489 apply(case_tac S') |
|
490 apply fastforce |
|
491 apply (fastforce simp: narrow_st_def) |
|
492 done |
|
493 |
|
494 definition "m_c m c = (let as = annos c in \<Sum>i=0..<size as. m(as!i))" |
|
495 |
|
496 lemma measure_m_c: "finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') |c c'\<Colon>ivl st option acom. |
|
497 strip c' = strip c \<and> c : Com X \<and> c' : Com X \<and> \<not> c' \<sqsubseteq> c}\<inverse> |
|
498 \<subseteq> measure(m_c(m_o (m_st m_ivl) (2*card(X))))" |
|
499 apply(auto simp: m_c_def Let_def Com_def) |
|
500 apply(subgoal_tac "length(annos c') = length(annos c)") |
|
501 prefer 2 apply (simp add: size_annos_same2) |
|
502 apply (auto) |
|
503 apply(rule setsum_strict_mono1) |
|
504 apply simp |
|
505 apply (clarsimp) |
|
506 apply(erule m_o_anti_mono) |
|
507 apply(rule subset_trans[OF domo_widen_subset]) |
|
508 apply fastforce |
|
509 apply(rule widen1) |
|
510 apply(auto simp: le_iff_le_annos listrel_iff_nth) |
|
511 apply(rule_tac x=n in bexI) |
|
512 prefer 2 apply simp |
|
513 apply(erule m_o_widen) |
|
514 apply (simp)+ |
|
515 done |
|
516 |
|
517 lemma measure_n_c: "finite X \<Longrightarrow> {(c, c \<triangle>\<^sub>c c') |c c'. |
|
518 strip c = strip c' \<and> c \<in> Com X \<and> c' \<in> Com X \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse> |
|
519 \<subseteq> measure(m_c(n_o (n_st n_ivl X)))" |
|
520 apply(auto simp: m_c_def Let_def Com_def) |
|
521 apply(subgoal_tac "length(annos c') = length(annos c)") |
|
522 prefer 2 apply (simp add: size_annos_same2) |
|
523 apply (auto) |
|
524 apply(rule setsum_strict_mono1) |
|
525 apply simp |
|
526 apply (clarsimp) |
|
527 apply(rule n_o_mono) |
|
528 using domo_narrow_subset apply fastforce |
|
529 apply fastforce |
|
530 apply(rule narrow2) |
|
531 apply(fastforce simp: le_iff_le_annos listrel_iff_nth) |
|
532 apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom) |
|
533 apply(rule_tac x=n in bexI) |
|
534 prefer 2 apply simp |
|
535 apply(erule n_o_narrow) |
|
536 apply (simp)+ |
|
537 done |
|
538 |
|
539 |
|
540 subsubsection "Termination: Post-Fixed Point Iterations" |
|
541 |
|
542 lemma iter_widen_termination: |
|
543 fixes c0 :: "'a::WN acom" |
|
544 assumes P_f: "\<And>c. P c \<Longrightarrow> P(f c)" |
|
545 assumes P_widen: "\<And>c c'. P c \<Longrightarrow> P c' \<Longrightarrow> P(c \<nabla>\<^sub>c c')" |
|
546 and "wf({(c::'a acom,c \<nabla>\<^sub>c c')|c c'. P c \<and> P c' \<and> ~ c' \<sqsubseteq> c}^-1)" |
|
547 and "P c0" and "c0 \<sqsubseteq> f c0" shows "EX c. iter_widen f c0 = Some c" |
|
548 proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"]) |
|
549 show "wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}" |
|
550 apply(rule wf_subset[OF assms(3)]) by(blast intro: P_f) |
|
551 next |
|
552 show "P c0" by(rule `P c0`) |
|
553 next |
|
554 fix c assume "P c" thus "P (c \<nabla>\<^sub>c f c)" by(simp add: P_f P_widen) |
|
555 qed |
|
556 |
|
557 lemma iter_narrow_termination: |
|
558 assumes P_f: "\<And>c. P c \<Longrightarrow> P(c \<triangle>\<^sub>c f c)" |
|
559 and wf: "wf({(c, c \<triangle>\<^sub>c f c)|c c'. P c \<and> ~ c \<sqsubseteq> c \<triangle>\<^sub>c f c}^-1)" |
|
560 and "P c0" shows "EX c. iter_narrow f c0 = Some c" |
|
561 proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "P"]) |
|
562 show "wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}" |
|
563 apply(rule wf_subset[OF wf]) by(blast intro: P_f) |
|
564 next |
|
565 show "P c0" by(rule `P c0`) |
|
566 next |
|
567 fix c assume "P c" thus "P (c \<triangle>\<^sub>c f c)" by(simp add: P_f) |
|
568 qed |
|
569 |
|
570 lemma iter_winden_step_ivl_termination: |
|
571 "EX c. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c" |
|
572 apply(rule iter_widen_termination[where |
|
573 P = "%c. strip c = c0 \<and> c : Com(vars c0)"]) |
|
574 apply (simp_all add: step'_Com bot_acom) |
|
575 apply(rule wf_subset) |
|
576 apply(rule wf_measure) |
|
577 apply(rule subset_trans) |
|
578 prefer 2 |
|
579 apply(rule measure_m_c[where X = "vars c0", OF finite_cvars]) |
|
580 apply blast |
|
581 done |
|
582 |
|
583 lemma iter_narrow_step_ivl_termination: |
|
584 "c0 \<in> Com (vars(strip c0)) \<Longrightarrow> step_ivl \<top> c0 \<sqsubseteq> c0 \<Longrightarrow> |
|
585 EX c. iter_narrow (step_ivl \<top>) c0 = Some c" |
|
586 apply(rule iter_narrow_termination[where |
|
587 P = "%c. strip c = strip c0 \<and> c : Com(vars(strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c"]) |
|
588 apply (simp_all add: step'_Com) |
|
589 apply(clarify) |
|
590 apply(frule narrow2_acom, drule mono_step'[OF le_refl], erule le_trans[OF _ narrow1_acom]) |
|
591 apply assumption |
|
592 apply(rule wf_subset) |
|
593 apply(rule wf_measure) |
|
594 apply(rule subset_trans) |
|
595 prefer 2 |
|
596 apply(rule measure_n_c[where X = "vars(strip c0)", OF finite_cvars]) |
|
597 apply auto |
|
598 by (metis bot_least domo_Top order_refl step'_Com strip_step') |
|
599 |
|
600 (* FIXME: simplify type system: Combine Com(X) and vars <= X?? *) |
|
601 lemma while_Com: |
|
602 fixes c :: "'a st option acom" |
|
603 assumes "while_option P f c = Some c'" |
|
604 and "!!c. strip(f c) = strip c" |
|
605 and "\<forall>c::'a st option acom. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)" |
|
606 and "c : Com(X)" and "vars(strip c) \<subseteq> X" shows "c' : Com(X)" |
|
607 using while_option_rule[where P = "\<lambda>c'. c' : Com(X) \<and> vars(strip c') \<subseteq> X", OF _ assms(1)] |
|
608 by(simp add: assms(2-)) |
|
609 |
|
610 lemma iter_widen_Com: fixes f :: "'a::WN st option acom \<Rightarrow> 'a st option acom" |
|
611 assumes "iter_widen f c = Some c'" |
|
612 and "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)" |
|
613 and "!!c. strip(f c) = strip c" |
|
614 and "c : Com(X)" and "vars (strip c) \<subseteq> X" shows "c' : Com(X)" |
|
615 proof- |
|
616 have "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c : Com(X)" |
|
617 by (metis (full_types) widen_acom_Com assms(2,3)) |
|
618 from while_Com[OF assms(1)[simplified iter_widen_def] _ this assms(4,5)] |
|
619 show ?thesis using assms(3) by(simp) |
|
620 qed |
|
621 |
|
622 (* step' = step_ivl! mv into locale*) |
|
623 lemma iter_widen_step'_Com: |
|
624 "iter_widen (step' \<top>) c = Some c' \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com(X) |
|
625 \<Longrightarrow> c' : Com(X)" |
|
626 apply(subgoal_tac "strip c'= strip c") |
|
627 prefer 2 apply (metis strip_iter_widen strip_step') |
|
628 apply(drule iter_widen_Com) |
|
629 prefer 3 apply assumption |
|
630 prefer 3 apply assumption |
|
631 apply (auto simp: step'_Com) |
|
632 done |
|
633 |
|
634 theorem step_ivl_termination: |
|
635 "EX c. AI_ivl' c0 = Some c" |
|
636 apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split) |
|
637 apply(rule iter_narrow_step_ivl_termination) |
|
638 apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step') |
|
639 apply(erule iter_widen_pfp) |
|
640 done |
|
641 |
|
642 end |
|
643 |
273 |
644 |
274 (* interesting(?) relic |
645 (* interesting(?) relic |
275 lemma widen_assoc: |
646 lemma widen_assoc: |
276 "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> ((x::ivl) \<nabla> y) \<nabla> z = x \<nabla> (y \<nabla> z)" |
647 "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> ((x::ivl) \<nabla> y) \<nabla> z = x \<nabla> (y \<nabla> z)" |
277 apply(cases x) |
648 apply(cases x) |
302 |
673 |
303 lemma widen_step_trans: |
674 lemma widen_step_trans: |
304 "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> EX u. (x \<nabla> y) \<nabla> z = x \<nabla> u \<and> ~ u \<sqsubseteq> x" |
675 "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> EX u. (x \<nabla> y) \<nabla> z = x \<nabla> u \<and> ~ u \<sqsubseteq> x" |
305 by (metis widen_assoc preord_class.le_trans widen1) |
676 by (metis widen_assoc preord_class.le_trans widen1) |
306 *) |
677 *) |
307 |
|
308 definition m_ivl :: "ivl \<Rightarrow> nat" where |
|
309 "m_ivl ivl = (case ivl of I l h \<Rightarrow> |
|
310 (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))" |
|
311 |
|
312 lemma m_ivl_height: "m_ivl ivl \<le> 2" |
|
313 by(simp add: m_ivl_def split: ivl.split option.split) |
|
314 |
|
315 lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y" |
|
316 by(auto simp: m_ivl_def le_option_def le_ivl_def |
|
317 split: ivl.split option.split if_splits) |
|
318 |
|
319 lemma less_m_ivl_widen: |
|
320 "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x" |
|
321 by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def |
|
322 split: ivl.splits option.splits if_splits) |
|
323 |
|
324 lemma Top_less_ivl: "\<top> \<sqsubseteq> x \<Longrightarrow> m_ivl x = 0" |
|
325 by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def |
|
326 split: ivl.split option.split if_splits) |
|
327 |
|
328 |
|
329 subsubsection "Termination: Abstract State" |
|
330 |
|
331 definition "m_st m st = (\<Sum>x\<in>set(dom st). m(fun st x))" |
|
332 |
|
333 lemma m_st_height: assumes "finite X" and "set (dom S) \<subseteq> X" |
|
334 shows "m_st m_ivl S \<le> 2 * card X" |
|
335 proof(auto simp: m_st_def) |
|
336 have "(\<Sum>x\<in>set(dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set(dom S). 2)" (is "?L \<le> _") |
|
337 by(rule setsum_mono)(simp add:m_ivl_height) |
|
338 also have "\<dots> \<le> (\<Sum>x\<in>X. 2)" |
|
339 by(rule setsum_mono3[OF assms]) simp |
|
340 also have "\<dots> = 2 * card X" by(simp add: setsum_constant) |
|
341 finally show "?L \<le> \<dots>" . |
|
342 qed |
|
343 |
|
344 lemma m_st_anti_mono: |
|
345 "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st m_ivl S2 \<le> m_st m_ivl S1" |
|
346 proof(auto simp: m_st_def le_st_def lookup_def split: if_splits) |
|
347 let ?X = "set(dom S1)" let ?Y = "set(dom S2)" |
|
348 let ?f = "fun S1" let ?g = "fun S2" |
|
349 assume asm: "\<forall>x\<in>?Y. (x \<in> ?X \<longrightarrow> ?f x \<sqsubseteq> ?g x) \<and> (x \<in> ?X \<or> \<top> \<sqsubseteq> ?g x)" |
|
350 hence 1: "\<forall>y\<in>?Y\<inter>?X. m_ivl(?g y) \<le> m_ivl(?f y)" by(simp add: m_ivl_anti_mono) |
|
351 have 0: "\<forall>x\<in>?Y-?X. m_ivl(?g x) = 0" using asm by (auto simp: Top_less_ivl) |
|
352 have "(\<Sum>y\<in>?Y. m_ivl(?g y)) = (\<Sum>y\<in>(?Y-?X) \<union> (?Y\<inter>?X). m_ivl(?g y))" |
|
353 by (metis Un_Diff_Int) |
|
354 also have "\<dots> = (\<Sum>y\<in>?Y-?X. m_ivl(?g y)) + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" |
|
355 by(subst setsum_Un_disjoint) auto |
|
356 also have "(\<Sum>y\<in>?Y-?X. m_ivl(?g y)) = 0" using 0 by simp |
|
357 also have "0 + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y)) = (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" by simp |
|
358 also have "\<dots> \<le> (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?f y))" |
|
359 by(rule setsum_mono)(simp add: 1) |
|
360 also have "\<dots> \<le> (\<Sum>y\<in>?X. m_ivl(?f y))" |
|
361 by(simp add: setsum_mono3[of "?X" "?Y Int ?X", OF _ Int_lower2]) |
|
362 finally show "(\<Sum>y\<in>?Y. m_ivl(?g y)) \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" |
|
363 by (metis add_less_cancel_left) |
|
364 qed |
|
365 |
|
366 lemma less_m_st_widen: |
|
367 assumes "\<not> S2 \<sqsubseteq> S1" shows "m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1" |
|
368 proof- |
|
369 { let ?X = "set(dom S1)" let ?Y = "set(dom S2)" |
|
370 let ?f = "fun S1" let ?g = "fun S2" |
|
371 fix x assume "x \<in> ?X" "\<not> lookup S2 x \<sqsubseteq> ?f x" |
|
372 have "(\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x)) < (\<Sum>x\<in>?X. m_ivl(?f x))" (is "?L < ?R") |
|
373 proof cases |
|
374 assume "x : ?Y" |
|
375 have "?L < (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" |
|
376 proof(rule setsum_strict_mono1, simp) |
|
377 show "\<forall>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" |
|
378 by (metis m_ivl_anti_mono widen1) |
|
379 next |
|
380 show "\<exists>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) < m_ivl(?f x)" |
|
381 using `x:?X` `x:?Y` `\<not> lookup S2 x \<sqsubseteq> ?f x` |
|
382 by (metis IntI less_m_ivl_widen lookup_def) |
|
383 qed |
|
384 also have "\<dots> \<le> ?R" by(simp add: setsum_mono3[OF _ Int_lower1]) |
|
385 finally show ?thesis . |
|
386 next |
|
387 assume "x ~: ?Y" |
|
388 have "?L \<le> (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" |
|
389 proof(rule setsum_mono, simp) |
|
390 fix x assume "x:?X \<and> x:?Y" show "m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" |
|
391 by (metis m_ivl_anti_mono widen1) |
|
392 qed |
|
393 also have "\<dots> < m_ivl(?f x) + \<dots>" |
|
394 using less_m_ivl_widen[OF `\<not> lookup S2 x \<sqsubseteq> ?f x`] |
|
395 by (metis Nat.le_refl add_strict_increasing gr0I not_less0) |
|
396 also have "\<dots> = (\<Sum>y\<in>insert x (?X\<inter>?Y). m_ivl(?f y))" |
|
397 using `x ~: ?Y` by simp |
|
398 also have "\<dots> \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" |
|
399 by(rule setsum_mono3)(insert `x:?X`, auto) |
|
400 finally show ?thesis . |
|
401 qed |
|
402 } with assms show ?thesis |
|
403 by(auto simp: le_st_def widen_st_def m_st_def Int_def) |
|
404 qed |
|
405 |
|
406 |
|
407 subsubsection "Termination: Option" |
|
408 |
|
409 definition "m_o m n opt = (case opt of None \<Rightarrow> n+1 | Some x \<Rightarrow> m x)" |
|
410 |
|
411 lemma m_o_anti_mono: "finite X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> |
|
412 m_o (m_st m_ivl) (2 * card X) S2 \<le> m_o (m_st m_ivl) (2 * card X) S1" |
|
413 apply(induction S1 S2 rule: le_option.induct) |
|
414 apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height |
|
415 split: option.splits) |
|
416 done |
|
417 |
|
418 lemma less_m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow> |
|
419 m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1" |
|
420 by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le less_m_st_widen |
|
421 split: option.split) |
|
422 |
|
423 |
|
424 lemma domo_widen_subset: "domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2" |
|
425 apply(induction S1 S2 rule: widen_option.induct) |
|
426 apply (auto simp: domo_def widen_st_def) |
|
427 done |
|
428 |
|
429 subsubsection "Termination: Commands" |
|
430 |
|
431 lemma strip_widen_acom: |
|
432 "strip c' = strip (c::'a::WN acom) \<Longrightarrow> strip (c \<nabla>\<^sub>c c') = strip c" |
|
433 by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all |
|
434 |
|
435 lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow> |
|
436 annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))" |
|
437 by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct) |
|
438 (simp_all add: size_annos_same2) |
|
439 |
|
440 lemma Com_widen_acom: "strip c2 = strip c1 \<Longrightarrow> |
|
441 c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<nabla>\<^sub>c c2) : Com X" |
|
442 apply(auto simp add: Com_def split: option.splits) |
|
443 apply(rename_tac S S' x) |
|
444 apply(erule in_set_zipE) |
|
445 apply(simp add: domo_def) |
|
446 apply (auto split: option.splits) |
|
447 apply(case_tac S) |
|
448 apply(case_tac S') |
|
449 apply simp |
|
450 apply fastforce |
|
451 apply(case_tac S') |
|
452 apply fastforce |
|
453 apply (fastforce simp: widen_st_def) |
|
454 done |
|
455 |
|
456 definition "m_c m c = (let as = annos c in \<Sum>i=0..<size as. m(as!i))" |
|
457 |
|
458 lemma measure_m_c: "finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') |c c'\<Colon>ivl st option acom. |
|
459 strip c' = strip c \<and> c : Com X \<and> c' : Com X \<and> \<not> c' \<sqsubseteq> c}\<inverse> |
|
460 \<subseteq> measure(m_c(m_o (m_st m_ivl) (2*card(X))))" |
|
461 apply(auto simp: m_c_def Let_def Com_def) |
|
462 apply(subgoal_tac "length(annos c') = length(annos c)") |
|
463 prefer 2 apply (simp add: size_annos_same2) |
|
464 apply (auto) |
|
465 apply(rule setsum_strict_mono1) |
|
466 apply simp |
|
467 apply (clarsimp) |
|
468 apply(erule m_o_anti_mono) |
|
469 apply(rule subset_trans[OF domo_widen_subset]) |
|
470 apply fastsimp |
|
471 apply(rule widen1) |
|
472 apply(auto simp: le_iff_le_annos listrel_iff_nth) |
|
473 apply(rule_tac x=n in bexI) |
|
474 prefer 2 apply simp |
|
475 apply(erule less_m_o_widen) |
|
476 apply (simp)+ |
|
477 done |
|
478 |
|
479 |
|
480 subsubsection "Termination: Post-Fixed Point Iterations" |
|
481 |
|
482 lemma iter_widen_termination: |
|
483 fixes c0 :: "'a::WN acom" |
|
484 assumes P_f: "\<And>c. P c \<Longrightarrow> P(f c)" |
|
485 assumes P_widen: "\<And>c c'. P c \<Longrightarrow> P c' \<Longrightarrow> P(c \<nabla>\<^sub>c c')" |
|
486 and "wf({(c::'a acom,c \<nabla>\<^sub>c c')|c c'. P c \<and> P c' \<and> ~ c' \<sqsubseteq> c}^-1)" |
|
487 and "P c0" and "c0 \<sqsubseteq> f c0" shows "EX c. iter_widen f c0 = Some c" |
|
488 proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"]) |
|
489 show "wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}" |
|
490 apply(rule wf_subset[OF assms(3)]) by(blast intro: P_f) |
|
491 next |
|
492 show "P c0" by(rule `P c0`) |
|
493 next |
|
494 fix c assume "P c" thus "P (c \<nabla>\<^sub>c f c)" by(simp add: P_f P_widen) |
|
495 qed |
|
496 |
|
497 lemma |
|
498 "EX c::ivl st option acom. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c" |
|
499 apply(rule iter_widen_termination[where |
|
500 P = "%c. strip c = c0 \<and> c : Com(vars c0)"]) |
|
501 apply (simp_all add: strip_step' step'_Com Com_widen_acom strip_widen_acom bot_acom domo_Top) |
|
502 apply(rule wf_subset) |
|
503 apply(rule wf_measure) |
|
504 apply(rule subset_trans) |
|
505 prefer 2 |
|
506 apply(rule measure_m_c[where X = "vars c0", OF finite_cvars]) |
|
507 apply blast |
|
508 done |
|
509 |
|
510 end |
|