src/HOL/IMP/Abs_Int3.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61890 f6ded81f5690
child 63882 018998c00003
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Abs_Int3
     4 imports Abs_Int2_ivl
     5 begin
     6 
     7 
     8 subsection "Widening and Narrowing"
     9 
    10 class widen =
    11 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
    12 
    13 class narrow =
    14 fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
    15 
    16 class wn = widen + narrow + order +
    17 assumes widen1: "x \<le> x \<nabla> y"
    18 assumes widen2: "y \<le> x \<nabla> y"
    19 assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
    20 assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
    21 begin
    22 
    23 lemma narrowid[simp]: "x \<triangle> x = x"
    24 by (metis eq_iff narrow1 narrow2)
    25 
    26 end
    27 
    28 lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,order_top})"
    29 by (metis eq_iff top_greatest widen2)
    30 
    31 instantiation ivl :: wn
    32 begin
    33 
    34 definition "widen_rep p1 p2 =
    35   (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else
    36    let (l1,h1) = p1; (l2,h2) = p2
    37    in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))"
    38 
    39 lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep
    40 by(auto simp: widen_rep_def eq_ivl_iff)
    41 
    42 definition "narrow_rep p1 p2 =
    43   (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
    44    let (l1,h1) = p1; (l2,h2) = p2
    45    in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))"
    46 
    47 lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep
    48 by(auto simp: narrow_rep_def eq_ivl_iff)
    49 
    50 instance
    51 proof
    52 qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset \<gamma>_rep_def subset_eq is_empty_rep_def empty_rep_def eq_ivl_def split: if_splits extended.splits)+
    53 
    54 end
    55 
    56 instantiation st :: ("{order_top,wn}")wn
    57 begin
    58 
    59 lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)"
    60 by(auto simp: eq_st_def)
    61 
    62 lift_definition narrow_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<triangle>)"
    63 by(auto simp: eq_st_def)
    64 
    65 instance
    66 proof (standard, goal_cases)
    67   case 1 thus ?case by transfer (simp add: less_eq_st_rep_iff widen1)
    68 next
    69   case 2 thus ?case by transfer (simp add: less_eq_st_rep_iff widen2)
    70 next
    71   case 3 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow1)
    72 next
    73   case 4 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow2)
    74 qed
    75 
    76 end
    77 
    78 
    79 instantiation option :: (wn)wn
    80 begin
    81 
    82 fun widen_option where
    83 "None \<nabla> x = x" |
    84 "x \<nabla> None = x" |
    85 "(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
    86 
    87 fun narrow_option where
    88 "None \<triangle> x = None" |
    89 "x \<triangle> None = None" |
    90 "(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
    91 
    92 instance
    93 proof (standard, goal_cases)
    94   case (1 x y) thus ?case
    95     by(induct x y rule: widen_option.induct)(simp_all add: widen1)
    96 next
    97   case (2 x y) thus ?case
    98     by(induct x y rule: widen_option.induct)(simp_all add: widen2)
    99 next
   100   case (3 x y) thus ?case
   101     by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
   102 next
   103   case (4 y x) thus ?case
   104     by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
   105 qed
   106 
   107 end
   108 
   109 definition map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom"
   110 where
   111 "map2_acom f C1 C2 = annotate (\<lambda>p. f (anno C1 p) (anno C2 p)) (strip C1)"
   112 
   113 
   114 instantiation acom :: (widen)widen
   115 begin
   116 definition "widen_acom = map2_acom (op \<nabla>)"
   117 instance ..
   118 end
   119 
   120 instantiation acom :: (narrow)narrow
   121 begin
   122 definition "narrow_acom = map2_acom (op \<triangle>)"
   123 instance ..
   124 end
   125 
   126 lemma strip_map2_acom[simp]:
   127  "strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1"
   128 by(simp add: map2_acom_def)
   129 (*by(induct f C1 C2 rule: map2_acom.induct) simp_all*)
   130 
   131 lemma strip_widen_acom[simp]:
   132   "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1"
   133 by(simp add: widen_acom_def)
   134 
   135 lemma strip_narrow_acom[simp]:
   136   "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1"
   137 by(simp add: narrow_acom_def)
   138 
   139 lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::wn acom)"
   140 by(simp add: narrow_acom_def narrow1 map2_acom_def less_eq_acom_def size_annos)
   141 
   142 lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::wn acom) \<le> C1"
   143 by(simp add: narrow_acom_def narrow2 map2_acom_def less_eq_acom_def size_annos)
   144 
   145 
   146 subsubsection "Pre-fixpoint computation"
   147 
   148 definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option"
   149 where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)"
   150 
   151 definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option"
   152 where "iter_narrow f = while_option (\<lambda>x. x \<triangle> f x < x) (\<lambda>x. x \<triangle> f x)"
   153 
   154 definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
   155 where "pfp_wn f x =
   156   (case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
   157 
   158 
   159 lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p"
   160 by(auto simp add: iter_widen_def dest: while_option_stop)
   161 
   162 lemma iter_widen_inv:
   163 assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x"
   164 and "iter_widen f x = Some y" shows "P y"
   165 using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]]
   166 by (blast intro: assms(1-3))
   167 
   168 lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
   169 assumes "\<forall>C. strip (f C) = strip C" and "while_option P f C = Some C'"
   170 shows "strip C' = strip C"
   171 using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
   172 by (metis assms(1))
   173 
   174 lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom"
   175 assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
   176 shows "strip C' = strip C"
   177 proof-
   178   have "\<forall>C. strip(C \<nabla> f C) = strip C"
   179     by (metis assms(1) strip_map2_acom widen_acom_def)
   180   from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
   181 qed
   182 
   183 lemma iter_narrow_pfp:
   184 assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
   185 and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   186 and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p"
   187 shows "P p \<and> f p \<le> p"
   188 proof-
   189   let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
   190   { fix p assume "?Q p"
   191     note P = conjunct1[OF this] and 12 = conjunct2[OF this]
   192     note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
   193     let ?p' = "p \<triangle> f p"
   194     have "?Q ?p'"
   195     proof auto
   196       show "P ?p'" by (blast intro: P Pinv)
   197       have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2_acom[OF 1]])
   198       also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1])
   199       finally show "f ?p' \<le> ?p'" .
   200       have "?p' \<le> p" by (rule narrow2_acom[OF 1])
   201       also have "p \<le> p0" by(rule 2)
   202       finally show "?p' \<le> p0" .
   203     qed
   204   }
   205   thus ?thesis
   206     using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
   207     by (blast intro: assms(4,5) le_refl)
   208 qed
   209 
   210 lemma pfp_wn_pfp:
   211 assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
   212 and Pinv: "P x"  "!!x. P x \<Longrightarrow> P(f x)"
   213   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
   214   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   215 and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p"
   216 proof-
   217   from pfp_wn obtain p0
   218     where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
   219     by(auto simp: pfp_wn_def split: option.splits)
   220   have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
   221   thus ?thesis
   222     by - (assumption |
   223           rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+
   224 qed
   225 
   226 lemma strip_pfp_wn:
   227   "\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C"
   228 by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
   229   (metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
   230 
   231 
   232 locale Abs_Int_wn = Abs_Int_inv_mono where \<gamma>=\<gamma>
   233   for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set"
   234 begin
   235 
   236 definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
   237 "AI_wn c = pfp_wn (step' \<top>) (bot c)"
   238 
   239 lemma AI_wn_correct: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c C"
   240 proof(simp add: CS_def AI_wn_def)
   241   assume 1: "pfp_wn (step' \<top>) (bot c) = Some C"
   242   have 2: "strip C = c \<and> step' \<top> C \<le> C"
   243     by(rule pfp_wn_pfp[where x="bot c"]) (simp_all add: 1 mono_step'_top)
   244   have pfp: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C"
   245   proof(rule order_trans)
   246     show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le>  \<gamma>\<^sub>c (step' \<top> C)"
   247       by(rule step_step')
   248     show "... \<le> \<gamma>\<^sub>c C"
   249       by(rule mono_gamma_c[OF conjunct2[OF 2]])
   250   qed
   251   have 3: "strip (\<gamma>\<^sub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
   252   have "lfp c (step (\<gamma>\<^sub>o \<top>)) \<le> \<gamma>\<^sub>c C"
   253     by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^sub>o \<top>)", OF 3 pfp])
   254   thus "lfp c (step UNIV) \<le> \<gamma>\<^sub>c C" by simp
   255 qed
   256 
   257 end
   258 
   259 global_interpretation Abs_Int_wn
   260 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   261 and test_num' = in_ivl
   262 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
   263 defines AI_wn_ivl = AI_wn
   264 ..
   265 
   266 
   267 subsubsection "Tests"
   268 
   269 definition "step_up_ivl n = ((\<lambda>C. C \<nabla> step_ivl \<top> C)^^n)"
   270 definition "step_down_ivl n = ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)"
   271 
   272 text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
   273 the loop took to execute. In contrast, @{const AI_wn_ivl} converges in a
   274 constant number of steps: *}
   275 
   276 value "show_acom (step_up_ivl 1 (bot test3_ivl))"
   277 value "show_acom (step_up_ivl 2 (bot test3_ivl))"
   278 value "show_acom (step_up_ivl 3 (bot test3_ivl))"
   279 value "show_acom (step_up_ivl 4 (bot test3_ivl))"
   280 value "show_acom (step_up_ivl 5 (bot test3_ivl))"
   281 value "show_acom (step_up_ivl 6 (bot test3_ivl))"
   282 value "show_acom (step_up_ivl 7 (bot test3_ivl))"
   283 value "show_acom (step_up_ivl 8 (bot test3_ivl))"
   284 value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))"
   285 value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
   286 value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
   287 value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
   288 value "show_acom_opt (AI_wn_ivl test3_ivl)"
   289 
   290 
   291 text{* Now all the analyses terminate: *}
   292 
   293 value "show_acom_opt (AI_wn_ivl test4_ivl)"
   294 value "show_acom_opt (AI_wn_ivl test5_ivl)"
   295 value "show_acom_opt (AI_wn_ivl test6_ivl)"
   296 
   297 
   298 subsubsection "Generic Termination Proof"
   299 
   300 lemma top_on_opt_widen:
   301   "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<nabla> o2 :: _ st option) X"
   302 apply(induct o1 o2 rule: widen_option.induct)
   303 apply (auto)
   304 by transfer simp
   305 
   306 lemma top_on_opt_narrow:
   307   "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<triangle> o2 :: _ st option) X"
   308 apply(induct o1 o2 rule: narrow_option.induct)
   309 apply (auto)
   310 by transfer simp
   311 
   312 (* FIXME mk anno abbrv *)
   313 lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
   314   annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
   315 by(simp add: map2_acom_def list_eq_iff_nth_eq size_annos anno_def[symmetric] size_annos_same[of C1 C2])
   316 
   317 lemma top_on_acom_widen:
   318   "\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk>
   319   \<Longrightarrow> top_on_acom (C1 \<nabla> C2 :: _ st option acom) X"
   320 by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE)
   321 
   322 lemma top_on_acom_narrow:
   323   "\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk>
   324   \<Longrightarrow> top_on_acom (C1 \<triangle> C2 :: _ st option acom) X"
   325 by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE)
   326 
   327 text{* The assumptions for widening and narrowing differ because during
   328 narrowing we have the invariant @{prop"y \<le> x"} (where @{text y} is the next
   329 iterate), but during widening there is no such invariant, there we only have
   330 that not yet @{prop"y \<le> x"}. This complicates the termination proof for
   331 widening. *}
   332 
   333 locale Measure_wn = Measure1 where m=m
   334   for m :: "'av::{order_top,wn} \<Rightarrow> nat" +
   335 fixes n :: "'av \<Rightarrow> nat"
   336 assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
   337 assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
   338 assumes n_narrow: "y \<le> x \<Longrightarrow> x \<triangle> y < x \<Longrightarrow> n(x \<triangle> y) < n x"
   339 
   340 begin
   341 
   342 lemma m_s_anti_mono_rep: assumes "\<forall>x. S1 x \<le> S2 x"
   343 shows "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))"
   344 proof-
   345   from assms have "\<forall>x. m(S1 x) \<ge> m(S2 x)" by (metis m_anti_mono)
   346   thus "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" by (metis setsum_mono)
   347 qed
   348 
   349 lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s S1 X \<ge> m_s S2 X"
   350 unfolding m_s_def
   351 apply (transfer fixing: m)
   352 apply(simp add: less_eq_st_rep_iff eq_st_def m_s_anti_mono_rep)
   353 done
   354 
   355 lemma m_s_widen_rep: assumes "finite X" "S1 = S2 on -X" "\<not> S2 x \<le> S1 x"
   356   shows "(\<Sum>x\<in>X. m (S1 x \<nabla> S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
   357 proof-
   358   have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S1 x \<nabla> S2 x)"
   359     by (metis m_anti_mono wn_class.widen1)
   360   have "x \<in> X" using assms(2,3)
   361     by(auto simp add: Ball_def)
   362   hence 2: "\<exists>x\<in>X. m(S1 x) > m(S1 x \<nabla> S2 x)"
   363     using assms(3) m_widen by blast
   364   from setsum_strict_mono_ex1[OF `finite X` 1 2]
   365   show ?thesis .
   366 qed
   367 
   368 lemma m_s_widen: "finite X \<Longrightarrow> fun S1 = fun S2 on -X ==>
   369   ~ S2 \<le> S1 \<Longrightarrow> m_s (S1 \<nabla> S2) X < m_s S1 X"
   370 apply(auto simp add: less_st_def m_s_def)
   371 apply (transfer fixing: m)
   372 apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep)
   373 done
   374 
   375 lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
   376   o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X"
   377 proof(induction o1 o2 rule: less_eq_option.induct)
   378   case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
   379 next
   380   case 2 thus ?case
   381     by(simp add: m_o_def le_SucI m_s_h split: option.splits)
   382 next
   383   case 3 thus ?case by simp
   384 qed
   385 
   386 lemma m_o_widen: "\<lbrakk> finite X; top_on_opt S1 (-X); top_on_opt S2 (-X); \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
   387   m_o (S1 \<nabla> S2) X < m_o S1 X"
   388 by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
   389 
   390 lemma m_c_widen:
   391   "strip C1 = strip C2  \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
   392    \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
   393 apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]listsum_setsum_nth)
   394 apply(subgoal_tac "length(annos C2) = length(annos C1)")
   395  prefer 2 apply (simp add: size_annos_same2)
   396 apply (auto)
   397 apply(rule setsum_strict_mono_ex1)
   398  apply(auto simp add: m_o_anti_mono vars_acom_def anno_def top_on_acom_def top_on_opt_widen widen1 less_eq_acom_def listrel_iff_nth)
   399 apply(rule_tac x=p in bexI)
   400  apply (auto simp: vars_acom_def m_o_widen top_on_acom_def)
   401 done
   402 
   403 
   404 definition n_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>s") where
   405 "n\<^sub>s S X = (\<Sum>x\<in>X. n(fun S x))"
   406 
   407 lemma n_s_narrow_rep:
   408 assumes "finite X"  "S1 = S2 on -X"  "\<forall>x. S2 x \<le> S1 x"  "\<forall>x. S1 x \<triangle> S2 x \<le> S1 x"
   409   "S1 x \<noteq> S1 x \<triangle> S2 x"
   410 shows "(\<Sum>x\<in>X. n (S1 x \<triangle> S2 x)) < (\<Sum>x\<in>X. n (S1 x))"
   411 proof-
   412   have 1: "\<forall>x. n(S1 x \<triangle> S2 x) \<le> n(S1 x)"
   413       by (metis assms(3) assms(4) eq_iff less_le_not_le n_narrow)
   414   have "x \<in> X" by (metis Compl_iff assms(2) assms(5) narrowid)
   415   hence 2: "\<exists>x\<in>X. n(S1 x \<triangle> S2 x) < n(S1 x)"
   416     by (metis assms(3-5) eq_iff less_le_not_le n_narrow)
   417   show ?thesis
   418     apply(rule setsum_strict_mono_ex1[OF `finite X`]) using 1 2 by blast+
   419 qed
   420 
   421 lemma n_s_narrow: "finite X \<Longrightarrow> fun S1 = fun S2 on -X \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1
   422   \<Longrightarrow> n\<^sub>s (S1 \<triangle> S2) X < n\<^sub>s S1 X"
   423 apply(auto simp add: less_st_def n_s_def)
   424 apply (transfer fixing: n)
   425 apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep)
   426 done
   427 
   428 definition n_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>o") where
   429 "n\<^sub>o opt X = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^sub>s S X + 1)"
   430 
   431 lemma n_o_narrow:
   432   "top_on_opt S1 (-X) \<Longrightarrow> top_on_opt S2 (-X) \<Longrightarrow> finite X
   433   \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^sub>o (S1 \<triangle> S2) X < n\<^sub>o S1 X"
   434 apply(induction S1 S2 rule: narrow_option.induct)
   435 apply(auto simp: n_o_def n_s_narrow)
   436 done
   437 
   438 
   439 definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^sub>c") where
   440 "n\<^sub>c C = listsum (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
   441 
   442 lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
   443   (\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
   444 by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
   445 
   446 lemma n_c_narrow: "strip C1 = strip C2
   447   \<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2)
   448   \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^sub>c (C1 \<triangle> C2) < n\<^sub>c C1"
   449 apply(auto simp: n_c_def narrow_acom_def listsum_setsum_nth)
   450 apply(subgoal_tac "length(annos C2) = length(annos C1)")
   451 prefer 2 apply (simp add: size_annos_same2)
   452 apply (auto)
   453 apply(simp add: less_annos_iff le_iff_le_annos)
   454 apply(rule setsum_strict_mono_ex1)
   455 apply (auto simp: vars_acom_def top_on_acom_def)
   456 apply (metis n_o_narrow nth_mem finite_cvars less_imp_le le_less order_refl)
   457 apply(rule_tac x=i in bexI)
   458 prefer 2 apply simp
   459 apply(rule n_o_narrow[where X = "vars(strip C2)"])
   460 apply (simp_all)
   461 done
   462 
   463 end
   464 
   465 
   466 lemma iter_widen_termination:
   467 fixes m :: "'a::wn acom \<Rightarrow> nat"
   468 assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   469 and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
   470 and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
   471 and "P C" shows "EX C'. iter_widen f C = Some C'"
   472 proof(simp add: iter_widen_def,
   473       rule measure_while_option_Some[where P = P and f=m])
   474   show "P C" by(rule `P C`)
   475 next
   476   fix C assume "P C" "\<not> f C \<le> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
   477     by(simp add: P_f P_widen m_widen)
   478 qed
   479 
   480 lemma iter_narrow_termination:
   481 fixes n :: "'a::wn acom \<Rightarrow> nat"
   482 assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   483 and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
   484 and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2"
   485 and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
   486 and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'"
   487 proof(simp add: iter_narrow_def,
   488       rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"])
   489   show "P C \<and> f C \<le> C" using init by blast
   490 next
   491   fix C assume 1: "P C \<and> f C \<le> C" and 2: "C \<triangle> f C < C"
   492   hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
   493   moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C"
   494     by (metis narrow1_acom narrow2_acom 1 mono order_trans)
   495   moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f)
   496   ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<le> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C"
   497     by blast
   498 qed
   499 
   500 locale Abs_Int_wn_measure = Abs_Int_wn where \<gamma>=\<gamma> + Measure_wn where m=m
   501   for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
   502 
   503 
   504 subsubsection "Termination: Intervals"
   505 
   506 definition m_rep :: "eint2 \<Rightarrow> nat" where
   507 "m_rep p = (if is_empty_rep p then 3 else
   508   let (l,h) = p in (case l of Minf \<Rightarrow> 0 | _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | _ \<Rightarrow> 1))"
   509 
   510 lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep
   511 by(auto simp: m_rep_def eq_ivl_iff)
   512 
   513 lemma m_ivl_nice: "m_ivl[l,h] = (if [l,h] = \<bottom> then 3 else
   514    (if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))"
   515 unfolding bot_ivl_def
   516 by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split)
   517 
   518 lemma m_ivl_height: "m_ivl iv \<le> 3"
   519 by transfer (simp add: m_rep_def split: prod.split extended.split)
   520 
   521 lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
   522 by transfer
   523    (auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
   524          split: prod.split extended.splits if_splits)
   525 
   526 lemma m_ivl_widen:
   527   "~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
   528 by transfer
   529    (auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
   530          split: prod.split extended.splits if_splits)
   531 
   532 definition n_ivl :: "ivl \<Rightarrow> nat" where
   533 "n_ivl iv = 3 - m_ivl iv"
   534 
   535 lemma n_ivl_narrow:
   536   "x \<triangle> y < x \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
   537 unfolding n_ivl_def
   538 apply(subst (asm) less_le_not_le)
   539 apply transfer
   540 by(auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset
   541          split: prod.splits if_splits extended.split)
   542 
   543 
   544 global_interpretation Abs_Int_wn_measure
   545 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   546 and test_num' = in_ivl
   547 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
   548 and m = m_ivl and n = n_ivl and h = 3
   549 proof (standard, goal_cases)
   550   case 2 thus ?case by(rule m_ivl_anti_mono)
   551 next
   552   case 1 thus ?case by(rule m_ivl_height)
   553 next
   554   case 3 thus ?case by(rule m_ivl_widen)
   555 next
   556   case 4 from 4(2) show ?case by(rule n_ivl_narrow)
   557   -- "note that the first assms is unnecessary for intervals"
   558 qed
   559 
   560 lemma iter_winden_step_ivl_termination:
   561   "\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C"
   562 apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on_acom C (- vars C)"])
   563 apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def]
   564   vars_acom_def top_on_acom_widen)
   565 done
   566 
   567 lemma iter_narrow_step_ivl_termination:
   568   "top_on_acom C (- vars C) \<Longrightarrow> step_ivl \<top> C \<le> C \<Longrightarrow>
   569   \<exists>C'. iter_narrow (step_ivl \<top>) C = Some C'"
   570 apply(rule iter_narrow_termination[where n = "n_c" and P = "%C'. strip C = strip C' \<and> top_on_acom C' (-vars C')"])
   571 apply(auto simp: top_on_step'[simplified comp_def vars_acom_def]
   572         mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow)
   573 done
   574 
   575 theorem AI_wn_ivl_termination:
   576   "\<exists>C. AI_wn_ivl c = Some C"
   577 apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
   578            split: option.split)
   579 apply(rule iter_narrow_step_ivl_termination)
   580 apply(rule conjunct2)
   581 apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on_acom C (- vars C)"])
   582 apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def]
   583   iter_widen_pfp top_on_bot vars_acom_def)
   584 done
   585 
   586 (*unused_thms Abs_Int_init - *)
   587 
   588 subsubsection "Counterexamples"
   589 
   590 text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.
   591 It can already be lost after the first step: *}
   592 
   593 lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
   594 and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"
   595 nitpick[card = 3, expect = genuine, show_consts, timeout = 120]
   596 (*
   597 1 < 2 < 3,
   598 f x = 2,
   599 x widen y = 3 -- guarantees termination with top=3
   600 x = 1
   601 Now f is mono, x <= f x, not f x <= x
   602 but x widen f x = 3, f 3 = 2, but not 3 <= 2
   603 *)
   604 oops
   605 
   606 text{* Widening terminates but may converge more slowly than Kleene iteration.
   607 In the following model, Kleene iteration goes from 0 to the least pfp
   608 in one step but widening takes 2 steps to reach a strictly larger pfp: *}
   609 lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
   610 and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"
   611 shows "f(x \<nabla> f x) \<le> x \<nabla> f x"
   612 nitpick[card = 4, expect = genuine, show_consts, timeout = 120]
   613 (*
   614 
   615    0 < 1 < 2 < 3
   616 f: 1   1   3   3
   617 
   618 0 widen 1 = 2
   619 2 widen 3 = 3
   620 and x widen y arbitrary, eg 3, which guarantees termination
   621 
   622 Kleene: f(f 0) = f 1 = 1 <= 1 = f 1
   623 
   624 but
   625 
   626 because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2,
   627 which is again not a pfp: not f 2 = 3 <= 2
   628 Another widening step yields 2 widen f 2 = 2 widen 3 = 3
   629 *)
   630 oops
   631 
   632 end