equal
deleted
inserted
replaced
348 qed |
348 qed |
349 |
349 |
350 lemma strip_pfp_wn: |
350 lemma strip_pfp_wn: |
351 "\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C" |
351 "\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C" |
352 by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) |
352 by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) |
353 (metis (no_types) narrow_acom_def strip_iter_widen strip_map2_acom strip_while) |
353 (metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while) |
354 |
354 |
355 |
355 |
356 locale Abs_Int2 = Abs_Int1_mono |
356 locale Abs_Int2 = Abs_Int1_mono |
357 where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set" |
357 where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set" |
358 begin |
358 begin |
476 |
476 |
477 lemma m_c_widen: |
477 lemma m_c_widen: |
478 "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1" |
478 "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1" |
479 apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def) |
479 apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def) |
480 apply(subgoal_tac "length(annos C2) = length(annos C1)") |
480 apply(subgoal_tac "length(annos C2) = length(annos C1)") |
481 prefer 2 apply (simp add: size_annos_same2) |
481 prefer 2 apply (simp add: size_annos_same2) |
482 apply (auto) |
482 apply (auto) |
483 apply(rule setsum_strict_mono_ex1) |
483 apply(rule setsum_strict_mono_ex1) |
484 apply simp |
484 apply simp |
485 apply (clarsimp) |
485 apply (clarsimp) |
486 apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"]) |
486 apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"]) |
487 apply(auto simp: le_iff_le_annos listrel_iff_nth) |
487 apply(auto simp: le_iff_le_annos listrel_iff_nth) |
488 apply(rule_tac x=i in bexI) |
488 apply(rule_tac x=i in bexI) |
489 prefer 2 apply simp |
489 prefer 2 apply simp |
490 apply(rule m_o_widen) |
490 apply(rule m_o_widen) |
491 apply (simp add: finite_cvars)+ |
491 apply (simp add: finite_cvars)+ |
492 done |
492 done |
493 |
493 |
494 |
494 |
495 definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where |
495 definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where |
496 "n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))" |
496 "n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))" |
523 |
523 |
524 |
524 |
525 definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where |
525 definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where |
526 "n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)" |
526 "n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)" |
527 |
527 |
528 (* FIXME mv *) |
|
529 lemma [simp]: "(Some x < Some y) = (x < y)" |
|
530 by(auto simp: less_le) |
|
531 |
|
532 lemma n_o_narrow: |
528 lemma n_o_narrow: |
533 "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X |
529 "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X |
534 \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1" |
530 \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1" |
535 apply(induction S1 S2 rule: narrow_option.induct) |
531 apply(induction S1 S2 rule: narrow_option.induct) |
536 apply(auto simp: n_o_def L_st_def n_s_narrow) |
532 apply(auto simp: n_o_def L_st_def n_s_narrow) |
687 apply(rule iter_narrow_step_ivl_termination) |
683 apply(rule iter_narrow_step_ivl_termination) |
688 apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>vars c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>vars c\<^esub>" and c=c, simplified]) |
684 apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>vars c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>vars c\<^esub>" and c=c, simplified]) |
689 apply(erule iter_widen_pfp) |
685 apply(erule iter_widen_pfp) |
690 done |
686 done |
691 |
687 |
692 (*unused_thms Abs_Int_init -*) |
688 (*unused_thms Abs_Int_init - *) |
693 |
689 |
694 subsubsection "Counterexamples" |
690 subsubsection "Counterexamples" |
695 |
691 |
696 text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening. |
692 text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening. |
697 It can already be lost after the first step: *} |
693 It can already be lost after the first step: *} |