src/HOL/IMP/Abs_Int3.thy
author nipkow
Fri Jan 25 16:45:09 2013 +0100 (2013-01-25)
changeset 50995 3371f5ee4ace
parent 50986 c54ea7f5418f
child 51036 e7b54119c436
permissions -rw-r--r--
tuned
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Abs_Int3
     4 imports Abs_Int2_ivl
     5 begin
     6 
     7 subsubsection "Welltypedness"
     8 
     9 class Lc =
    10 fixes Lc :: "com \<Rightarrow> 'a set"
    11 
    12 instantiation st :: (type)Lc
    13 begin
    14 
    15 definition Lc_st :: "com \<Rightarrow> 'a st set" where
    16 "Lc_st c = L (vars c)"
    17 
    18 instance ..
    19 
    20 end
    21 
    22 instantiation acom :: (Lc)Lc
    23 begin
    24 
    25 definition Lc_acom :: "com \<Rightarrow> 'a acom set" where
    26 "Lc c = {C. strip C = c \<and> (\<forall>a\<in>set(annos C). a \<in> Lc c)}"
    27 
    28 instance ..
    29 
    30 end
    31 
    32 instantiation option :: (Lc)Lc
    33 begin
    34 
    35 definition Lc_option :: "com \<Rightarrow> 'a option set" where
    36 "Lc c = {None} \<union> Some ` Lc c"
    37 
    38 lemma Lc_option_simps[simp]: "None \<in> Lc c" "(Some x \<in> Lc c) = (x \<in> Lc c)"
    39 by(auto simp: Lc_option_def)
    40 
    41 instance ..
    42 
    43 end
    44 
    45 lemma Lc_option_iff_wt[simp]: fixes a :: "_ st option"
    46 shows "(a \<in> Lc c) = (a \<in> L (vars c))"
    47 by(auto simp add: L_option_def Lc_st_def split: option.splits)
    48 
    49 
    50 context Abs_Int1
    51 begin
    52 
    53 lemma step'_in_Lc: "C \<in> Lc c \<Longrightarrow> S \<in> Lc c \<Longrightarrow> step' S C \<in> Lc c"
    54 apply(auto simp add: Lc_acom_def)
    55 by(metis step'_in_L[simplified L_acom_def mem_Collect_eq] order_refl)
    56 
    57 end
    58 
    59 
    60 subsection "Widening and Narrowing"
    61 
    62 class widen =
    63 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
    64 
    65 class narrow =
    66 fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
    67 
    68 class WN = widen + narrow + preord +
    69 assumes widen1: "x \<sqsubseteq> x \<nabla> y"
    70 assumes widen2: "y \<sqsubseteq> x \<nabla> y"
    71 assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    72 assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    73 
    74 class WN_Lc = widen + narrow + preord + Lc +
    75 assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
    76 assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
    77 assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    78 assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    79 assumes Lc_widen[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<nabla> y \<in> Lc c"
    80 assumes Lc_narrow[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<triangle> y \<in> Lc c"
    81 
    82 
    83 instantiation ivl :: WN
    84 begin
    85 
    86 definition "widen_ivl ivl1 ivl2 =
    87   ((*if is_empty ivl1 then ivl2 else
    88    if is_empty ivl2 then ivl1 else*)
    89      case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
    90        Ivl (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
    91            (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
    92 
    93 definition "narrow_ivl ivl1 ivl2 =
    94   ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
    95      case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
    96        Ivl (if l1 = None then l2 else l1)
    97            (if h1 = None then h2 else h1))"
    98 
    99 instance
   100 proof qed
   101   (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
   102 
   103 end
   104 
   105 
   106 instantiation st :: (WN)WN_Lc
   107 begin
   108 
   109 definition "widen_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
   110 
   111 definition "narrow_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
   112 
   113 instance
   114 proof
   115   case goal1 thus ?case
   116     by(simp add: widen_st_def le_st_def WN_class.widen1)
   117 next
   118   case goal2 thus ?case
   119     by(simp add: widen_st_def le_st_def WN_class.widen2 Lc_st_def L_st_def)
   120 next
   121   case goal3 thus ?case
   122     by(auto simp: narrow_st_def le_st_def WN_class.narrow1)
   123 next
   124   case goal4 thus ?case
   125     by(auto simp: narrow_st_def le_st_def WN_class.narrow2)
   126 next
   127   case goal5 thus ?case by(auto simp: widen_st_def Lc_st_def L_st_def)
   128 next
   129   case goal6 thus ?case by(auto simp: narrow_st_def Lc_st_def L_st_def)
   130 qed
   131 
   132 end
   133 
   134 
   135 instantiation option :: (WN_Lc)WN_Lc
   136 begin
   137 
   138 fun widen_option where
   139 "None \<nabla> x = x" |
   140 "x \<nabla> None = x" |
   141 "(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
   142 
   143 fun narrow_option where
   144 "None \<triangle> x = None" |
   145 "x \<triangle> None = None" |
   146 "(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
   147 
   148 instance
   149 proof
   150   case goal1 thus ?case
   151     by(induct x y rule: widen_option.induct)(simp_all add: widen1)
   152 next
   153   case goal2 thus ?case
   154     by(induct x y rule: widen_option.induct)(simp_all add: widen2)
   155 next
   156   case goal3 thus ?case
   157     by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
   158 next
   159   case goal4 thus ?case
   160     by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
   161 next
   162   case goal5 thus ?case
   163     by(induction x y rule: widen_option.induct)(auto simp: Lc_st_def)
   164 next
   165   case goal6 thus ?case
   166     by(induction x y rule: narrow_option.induct)(auto simp: Lc_st_def)
   167 qed
   168 
   169 end
   170 
   171 
   172 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
   173 "map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
   174 "map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
   175 "map2_acom f (C1;C2) (D1;D2) = (map2_acom f C1 D1; map2_acom f C2 D2)" |
   176 "map2_acom f (IF b THEN {p1} C1 ELSE {p2} C2 {a1}) (IF b' THEN {q1} D1 ELSE {q2} D2 {a2}) =
   177   (IF b THEN {f p1 q1} map2_acom f C1 D1 ELSE {f p2 q2} map2_acom f C2 D2 {f a1 a2})" |
   178 "map2_acom f ({a1} WHILE b DO {p} C {a2}) ({a3} WHILE b' DO {p'} C' {a4}) =
   179   ({f a1 a3} WHILE b DO {f p p'} map2_acom f C C' {f a2 a4})"
   180 
   181 
   182 instantiation acom :: (widen)widen
   183 begin
   184 definition "widen_acom = map2_acom (op \<nabla>)"
   185 instance ..
   186 end
   187 
   188 instantiation acom :: (narrow)narrow
   189 begin
   190 definition "narrow_acom = map2_acom (op \<triangle>)"
   191 instance ..
   192 end
   193 
   194 instantiation acom :: (WN_Lc)WN_Lc
   195 begin
   196 
   197 lemma widen_acom1: fixes C1 :: "'a acom" shows
   198   "\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk>
   199    \<Longrightarrow> C1 \<sqsubseteq> C1 \<nabla> C2"
   200 by(induct C1 C2 rule: le_acom.induct)
   201   (auto simp: widen_acom_def widen1 Lc_acom_def)
   202 
   203 lemma widen_acom2: fixes C1 :: "'a acom" shows
   204   "\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk>
   205    \<Longrightarrow> C2 \<sqsubseteq> C1 \<nabla> C2"
   206 by(induct C1 C2 rule: le_acom.induct)
   207   (auto simp: widen_acom_def widen2 Lc_acom_def)
   208 
   209 lemma strip_map2_acom[simp]:
   210  "strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1"
   211 by(induct f C1 C2 rule: map2_acom.induct) simp_all
   212 
   213 lemma strip_widen_acom[simp]:
   214   "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1"
   215 by(simp add: widen_acom_def)
   216 
   217 lemma strip_narrow_acom[simp]:
   218   "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1"
   219 by(simp add: narrow_acom_def)
   220 
   221 lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
   222   annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
   223 by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2)
   224 
   225 instance
   226 proof
   227   case goal1 thus ?case by(auto simp: Lc_acom_def widen_acom1)
   228 next
   229   case goal2 thus ?case by(auto simp: Lc_acom_def widen_acom2)
   230 next
   231   case goal3 thus ?case
   232     by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow1)
   233 next
   234   case goal4 thus ?case
   235     by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow2)
   236 next
   237   case goal5 thus ?case
   238     by(auto simp: Lc_acom_def widen_acom_def split_conv elim!: in_set_zipE)
   239 next
   240   case goal6 thus ?case
   241     by(auto simp: Lc_acom_def narrow_acom_def split_conv elim!: in_set_zipE)
   242 qed
   243 
   244 end
   245 
   246 lemma widen_o_in_L[simp]: fixes x1 x2 :: "_ st option"
   247 shows "x1 \<in> L X \<Longrightarrow> x2 \<in> L X \<Longrightarrow> x1 \<nabla> x2 \<in> L X"
   248 by(induction x1 x2 rule: widen_option.induct)
   249   (simp_all add: widen_st_def L_st_def)
   250 
   251 lemma narrow_o_in_L[simp]: fixes x1 x2 :: "_ st option"
   252 shows "x1 \<in> L X \<Longrightarrow> x2 \<in> L X \<Longrightarrow> x1 \<triangle> x2 \<in> L X"
   253 by(induction x1 x2 rule: narrow_option.induct)
   254   (simp_all add: narrow_st_def L_st_def)
   255 
   256 lemma widen_c_in_L: fixes C1 C2 :: "_ st option acom"
   257 shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<nabla> C2 \<in> L X"
   258 by(induction C1 C2 rule: le_acom.induct)
   259   (auto simp: widen_acom_def)
   260 
   261 lemma narrow_c_in_L: fixes C1 C2 :: "_ st option acom"
   262 shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<triangle> C2 \<in> L X"
   263 by(induction C1 C2 rule: le_acom.induct)
   264   (auto simp: narrow_acom_def)
   265 
   266 lemma bot_in_Lc[simp]: "bot c \<in> Lc c"
   267 by(simp add: Lc_acom_def bot_def)
   268 
   269 
   270 subsubsection "Post-fixed point computation"
   271 
   272 definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,widen})option"
   273 where "iter_widen f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) (\<lambda>x. x \<nabla> f x)"
   274 
   275 definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,narrow})option"
   276 where "iter_narrow f = while_option (\<lambda>x. \<not> x \<sqsubseteq> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
   277 
   278 definition pfp_wn :: "('a::{preord,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
   279 where "pfp_wn f x =
   280   (case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
   281 
   282 
   283 lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<sqsubseteq> p"
   284 by(auto simp add: iter_widen_def dest: while_option_stop)
   285 
   286 lemma iter_widen_inv:
   287 assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x"
   288 and "iter_widen f x = Some y" shows "P y"
   289 using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]]
   290 by (blast intro: assms(1-3))
   291 
   292 lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
   293 assumes "\<forall>C. strip (f C) = strip C" and "while_option P f C = Some C'"
   294 shows "strip C' = strip C"
   295 using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
   296 by (metis assms(1))
   297 
   298 lemma strip_iter_widen: fixes f :: "'a::{preord,widen} acom \<Rightarrow> 'a acom"
   299 assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
   300 shows "strip C' = strip C"
   301 proof-
   302   have "\<forall>C. strip(C \<nabla> f C) = strip C"
   303     by (metis assms(1) strip_map2_acom widen_acom_def)
   304   from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
   305 qed
   306 
   307 lemma iter_narrow_pfp:
   308 assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
   309 and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   310 and "P p0" and "f p0 \<sqsubseteq> p0" and "iter_narrow f p0 = Some p"
   311 shows "P p \<and> f p \<sqsubseteq> p"
   312 proof-
   313   let ?Q = "%p. P p \<and> f p \<sqsubseteq> p \<and> p \<sqsubseteq> p0"
   314   { fix p assume "?Q p"
   315     note P = conjunct1[OF this] and 12 = conjunct2[OF this]
   316     note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
   317     let ?p' = "p \<triangle> f p"
   318     have "?Q ?p'"
   319     proof auto
   320       show "P ?p'" by (blast intro: P Pinv)
   321       have "f ?p' \<sqsubseteq> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
   322       also have "\<dots> \<sqsubseteq> ?p'" by(rule narrow1[OF 1])
   323       finally show "f ?p' \<sqsubseteq> ?p'" .
   324       have "?p' \<sqsubseteq> p" by (rule narrow2[OF 1])
   325       also have "p \<sqsubseteq> p0" by(rule 2)
   326       finally show "?p' \<sqsubseteq> p0" .
   327     qed
   328   }
   329   thus ?thesis
   330     using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
   331     by (blast intro: assms(4,5) le_refl)
   332 qed
   333 
   334 lemma pfp_wn_pfp:
   335 assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
   336 and Pinv: "P x"  "!!x. P x \<Longrightarrow> P(f x)"
   337   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
   338   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   339 and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<sqsubseteq> p"
   340 proof-
   341   from pfp_wn obtain p0
   342     where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
   343     by(auto simp: pfp_wn_def split: option.splits)
   344   have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
   345   thus ?thesis
   346     by - (assumption |
   347           rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+
   348 qed
   349 
   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"
   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)
   354 
   355 
   356 locale Abs_Int2 = Abs_Int1_mono
   357 where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set"
   358 begin
   359 
   360 definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
   361 "AI_wn c = pfp_wn (step' (top c)) (bot c)"
   362 
   363 lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
   364 proof(simp add: CS_def AI_wn_def)
   365   assume 1: "pfp_wn (step' (top c)) (bot c) = Some C"
   366   have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
   367     by(rule pfp_wn_pfp[where x="bot c"])
   368       (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
   369   have pfp: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   370   proof(rule order_trans)
   371     show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
   372       by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
   373     show "... \<le> \<gamma>\<^isub>c C"
   374       by(rule mono_gamma_c[OF conjunct2[OF 2]])
   375   qed
   376   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
   377   have "lfp c (step (\<gamma>\<^isub>o (top c))) \<le> \<gamma>\<^isub>c C"
   378     by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 pfp])
   379   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
   380 qed
   381 
   382 end
   383 
   384 interpretation Abs_Int2
   385 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   386 and test_num' = in_ivl
   387 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   388 defines AI_ivl' is AI_wn
   389 ..
   390 
   391 
   392 subsubsection "Tests"
   393 
   394 (* Trick to make the code generator happy. *)
   395 lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y"
   396 by(rule refl)
   397 
   398 definition "step_up_ivl n =
   399   ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)"
   400 definition "step_down_ivl n =
   401   ((\<lambda>C. C \<triangle> step_ivl (top (strip C)) C)^^n)"
   402 
   403 text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
   404 the loop took to execute. In contrast, @{const AI_ivl'} converges in a
   405 constant number of steps: *}
   406 
   407 value "show_acom (step_up_ivl 1 (bot test3_ivl))"
   408 value "show_acom (step_up_ivl 2 (bot test3_ivl))"
   409 value "show_acom (step_up_ivl 3 (bot test3_ivl))"
   410 value "show_acom (step_up_ivl 4 (bot test3_ivl))"
   411 value "show_acom (step_up_ivl 5 (bot test3_ivl))"
   412 value "show_acom (step_up_ivl 6 (bot test3_ivl))"
   413 value "show_acom (step_up_ivl 7 (bot test3_ivl))"
   414 value "show_acom (step_up_ivl 8 (bot test3_ivl))"
   415 value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))"
   416 value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
   417 value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
   418 value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
   419 value "show_acom (the(AI_ivl' test3_ivl))"
   420 
   421 
   422 text{* Now all the analyses terminate: *}
   423 
   424 value "show_acom (the(AI_ivl' test4_ivl))"
   425 value "show_acom (the(AI_ivl' test5_ivl))"
   426 value "show_acom (the(AI_ivl' test6_ivl))"
   427 
   428 
   429 subsubsection "Generic Termination Proof"
   430 
   431 locale Measure_WN = Measure1 where m=m for m :: "'av::WN \<Rightarrow> nat" +
   432 fixes n :: "'av \<Rightarrow> nat"
   433 assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
   434 assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
   435 assumes n_narrow: "y \<sqsubseteq> x \<Longrightarrow> ~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
   436 
   437 begin
   438 
   439 lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
   440   ~ S2 \<sqsubseteq> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
   441 proof(auto simp add: le_st_def m_s_def L_st_def widen_st_def)
   442   assume "finite(dom S1)"
   443   have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
   444     by (metis m1 WN_class.widen1)
   445   fix x assume "x \<in> dom S1" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
   446   hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
   447     using m_widen by blast
   448   from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2]
   449   show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
   450 qed
   451 
   452 lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
   453   m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1"
   454 by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen
   455         split: option.split)
   456 
   457 lemma m_c_widen:
   458   "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
   459 apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
   460 apply(subgoal_tac "length(annos C2) = length(annos C1)")
   461 prefer 2 apply (simp add: size_annos_same2)
   462 apply (auto)
   463 apply(rule setsum_strict_mono_ex1)
   464 apply simp
   465 apply (clarsimp)
   466 apply(simp add: m_o1 finite_cvars widen1[where c = "strip C2"])
   467 apply(auto simp: le_iff_le_annos listrel_iff_nth)
   468 apply(rule_tac x=i in bexI)
   469 prefer 2 apply simp
   470 apply(rule m_o_widen)
   471 apply (simp add: finite_cvars)+
   472 done
   473 
   474 
   475 definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where
   476 "n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))"
   477 
   478 lemma n_s_mono: assumes "S1 \<sqsubseteq> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
   479 proof-
   480   from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
   481     by(simp_all add: le_st_def)
   482   have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))"
   483     by(rule setsum_mono)(simp add: le_st_def n_mono)
   484   thus ?thesis by(simp add: n_s_def)
   485 qed
   486 
   487 lemma n_s_narrow:
   488 assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
   489 shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1"
   490 proof-
   491   from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
   492     by(simp_all add: le_st_def)
   493   have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
   494     by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
   495   have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<sqsubseteq> S1 \<triangle> S2`
   496     by(force simp: le_st_def narrow_st_def intro: n_narrow)
   497   have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
   498     apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
   499   moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
   500   ultimately show ?thesis by(simp add: n_s_def)
   501 qed
   502 
   503 
   504 definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
   505 "n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
   506 
   507 lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
   508 by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_s_mono)
   509 
   510 lemma n_o_narrow:
   511   "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
   512   \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
   513 apply(induction S1 S2 rule: narrow_option.induct)
   514 apply(auto simp: n_o_def L_st_def n_s_narrow)
   515 done
   516 
   517 
   518 definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^isub>c") where
   519 "n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))"
   520 
   521 lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow>
   522   C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
   523 apply(auto simp: n_c_def Let_def Lc_acom_def narrow_acom_def)
   524 apply(subgoal_tac "length(annos C2) = length(annos C1)")
   525 prefer 2 apply (simp add: size_annos_same2)
   526 apply (auto)
   527 apply(rule setsum_strict_mono_ex1)
   528 apply simp
   529 apply (clarsimp)
   530 apply(rule n_o_mono)
   531 apply(rule narrow2)
   532 apply(fastforce simp: le_iff_le_annos listrel_iff_nth)
   533 apply(auto simp: le_iff_le_annos listrel_iff_nth)
   534 apply(rule_tac x=i in bexI)
   535 prefer 2 apply simp
   536 apply(rule n_o_narrow[where X = "vars(strip C1)"])
   537 apply (simp add: finite_cvars)+
   538 done
   539 
   540 end
   541 
   542 
   543 lemma iter_widen_termination:
   544 fixes m :: "'a::WN_Lc \<Rightarrow> nat"
   545 assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   546 and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
   547 and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<sqsubseteq> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
   548 and "P C" shows "EX C'. iter_widen f C = Some C'"
   549 proof(simp add: iter_widen_def,
   550       rule measure_while_option_Some[where P = P and f=m])
   551   show "P C" by(rule `P C`)
   552 next
   553   fix C assume "P C" "\<not> f C \<sqsubseteq> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
   554     by(simp add: P_f P_widen m_widen)
   555 qed
   556 
   557 lemma iter_narrow_termination:
   558 fixes n :: "'a::WN_Lc \<Rightarrow> nat"
   559 assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   560 and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
   561 and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"
   562 and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<sqsubseteq> C1 \<Longrightarrow> ~ C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
   563 and init: "P C" "f C \<sqsubseteq> C" shows "EX C'. iter_narrow f C = Some C'"
   564 proof(simp add: iter_narrow_def,
   565       rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<sqsubseteq> C"])
   566   show "P C \<and> f C \<sqsubseteq> C" using init by blast
   567 next
   568   fix C assume 1: "P C \<and> f C \<sqsubseteq> C" and 2: "\<not> C \<sqsubseteq> C \<triangle> f C"
   569   hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
   570   moreover then have "f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C"
   571     by (metis narrow1 narrow2 1 mono preord_class.le_trans)
   572   moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f)
   573   ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C"
   574     by blast
   575 qed
   576 
   577 locale Abs_Int2_measure =
   578   Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m
   579   for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
   580 
   581 
   582 subsubsection "Termination: Intervals"
   583 
   584 definition m_ivl :: "ivl \<Rightarrow> nat" where
   585 "m_ivl ivl = (case ivl of Ivl l h \<Rightarrow>
   586      (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))"
   587 
   588 lemma m_ivl_height: "m_ivl ivl \<le> 2"
   589 by(simp add: m_ivl_def split: ivl.split option.split)
   590 
   591 lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
   592 by(auto simp: m_ivl_def le_option_def le_ivl_def
   593         split: ivl.split option.split if_splits)
   594 
   595 lemma m_ivl_widen:
   596   "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
   597 by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def
   598         split: ivl.splits option.splits if_splits)
   599 
   600 definition n_ivl :: "ivl \<Rightarrow> nat" where
   601 "n_ivl ivl = 2 - m_ivl ivl"
   602 
   603 lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
   604 unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
   605 
   606 lemma n_ivl_narrow:
   607   "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
   608 by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def
   609         split: ivl.splits option.splits if_splits)
   610 
   611 
   612 interpretation Abs_Int2_measure
   613 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   614 and test_num' = in_ivl
   615 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   616 and m = m_ivl and n = n_ivl and h = 2
   617 proof
   618   case goal1 thus ?case by(rule m_ivl_anti_mono)
   619 next
   620   case goal2 thus ?case by(rule m_ivl_height)
   621 next
   622   case goal3 thus ?case by(rule m_ivl_widen)
   623 next
   624   case goal4 thus ?case by(rule n_ivl_mono)
   625 next
   626   case goal5 from goal5(2) show ?case by(rule n_ivl_narrow)
   627   -- "note that the first assms is unnecessary for intervals"
   628 qed
   629 
   630 
   631 lemma iter_winden_step_ivl_termination:
   632   "\<exists>C. iter_widen (step_ivl (top c)) (bot c) = Some C"
   633 apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
   634 apply (simp_all add: step'_in_Lc m_c_widen)
   635 done
   636 
   637 lemma iter_narrow_step_ivl_termination:
   638   "C0 \<in> Lc c \<Longrightarrow> step_ivl (top c) C0 \<sqsubseteq> C0 \<Longrightarrow>
   639   \<exists>C. iter_narrow (step_ivl (top c)) C0 = Some C"
   640 apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
   641 apply (simp add: step'_in_Lc)
   642 apply (simp)
   643 apply(rule mono_step'_top)
   644 apply(simp add: Lc_acom_def L_acom_def)
   645 apply(simp add: Lc_acom_def L_acom_def)
   646 apply assumption
   647 apply(erule (3) n_c_narrow)
   648 apply assumption
   649 apply assumption
   650 done
   651 
   652 theorem AI_ivl'_termination:
   653   "\<exists>C. AI_ivl' c = Some C"
   654 apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
   655            split: option.split)
   656 apply(rule iter_narrow_step_ivl_termination)
   657 apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>c\<^esub>" and c=c, simplified])
   658 apply(erule iter_widen_pfp)
   659 done
   660 
   661 (*unused_thms Abs_Int_init -*)
   662 
   663 subsubsection "Counterexamples"
   664 
   665 text{* Widening is increasing by assumption,
   666 but @{prop"x \<sqsubseteq> f x"} is not an invariant of widening. It can already
   667 be lost after the first step: *}
   668 
   669 lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   670 and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" shows "x \<nabla> f x \<sqsubseteq> f(x \<nabla> f x)"
   671 nitpick[card = 3, expect = genuine, show_consts]
   672 (*
   673 1 < 2 < 3,
   674 f x = 2,
   675 x widen y = 3 -- guarantees termination with top=3
   676 x = 1
   677 Now f is mono, x <= f x, not f x <= x
   678 but x widen f x = 3, f 3 = 2, but not 3 <= 2
   679 *)
   680 oops
   681 
   682 text{* Widening terminates but may converge more slowly than Kleene iteration.
   683 In the following model, Kleene iteration goes from 0 to the least pfp
   684 in one step but widening takes 2 steps to reach a strictly larger pfp: *}
   685 lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   686 and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" and "f(f x) \<sqsubseteq> f x"
   687 shows "f(x \<nabla> f x) \<sqsubseteq> x \<nabla> f x"
   688 nitpick[card = 4, expect = genuine, show_consts]
   689 (*
   690 
   691    0 < 1 < 2 < 3
   692 f: 1   1   3   3
   693 
   694 0 widen 1 = 2
   695 2 widen 3 = 3
   696 and x widen y arbitrary, eg 3, which guarantees termination
   697 
   698 Kleene: f(f 0) = f 1 = 1 <= 1 = f 1
   699 
   700 but
   701 
   702 because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2,
   703 which is again not a pfp: not f 2 = 3 <= 2
   704 Another widening step yields 2 widen f 2 = 2 widen 3 = 3
   705 *)
   706 oops
   707 
   708 end