src/HOL/IMP/Abs_Int2_ivl.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 67399 eab6ce8368fa
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Abs_Int2_ivl
     4 imports Abs_Int2
     5 begin
     6 
     7 subsection "Interval Analysis"
     8 
     9 type_synonym eint = "int extended"
    10 type_synonym eint2 = "eint * eint"
    11 
    12 definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where
    13 "\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})"
    14 
    15 definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
    16 "eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)"
    17 
    18 lemma refl_eq_ivl[simp]: "eq_ivl p p"
    19 by(auto simp: eq_ivl_def)
    20 
    21 quotient_type ivl = eint2 / eq_ivl
    22 by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
    23 
    24 abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_, _]") where
    25 "[l,h] == abs_ivl(l,h)"
    26 
    27 lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
    28 by(simp add: eq_ivl_def)
    29 
    30 lemma \<gamma>_ivl_nice: "\<gamma>_ivl[l,h] = {i. l \<le> Fin i \<and> Fin i \<le> h}"
    31 by transfer (simp add: \<gamma>_rep_def)
    32 
    33 lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" .
    34 
    35 lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool"
    36   is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h"
    37 by(auto simp: eq_ivl_def \<gamma>_rep_def)
    38 
    39 lemma in_ivl_nice: "in_ivl i [l,h] = (l \<le> Fin i \<and> Fin i \<le> h)"
    40 by transfer simp
    41 
    42 definition is_empty_rep :: "eint2 \<Rightarrow> bool" where
    43 "is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)"
    44 
    45 lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} |
    46   (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})"
    47 by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits)
    48 
    49 lift_definition  is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
    50 apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
    51 apply(auto simp: not_less less_eq_extended_case split: extended.splits)
    52 done
    53 
    54 lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"
    55 by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits)
    56 
    57 definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
    58 
    59 lift_definition empty_ivl :: ivl is empty_rep .
    60 
    61 lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
    62 by(auto simp add: is_empty_rep_def empty_rep_def)
    63 
    64 lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})"
    65 by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits)
    66 
    67 declare is_empty_rep_iff[THEN iffD1, simp]
    68 
    69 
    70 instantiation ivl :: semilattice_sup_top
    71 begin
    72 
    73 definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
    74 "le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in
    75   if is_empty_rep(l1,h1) then True else
    76   if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)"
    77 
    78 lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2"
    79 apply rule
    80 apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1]
    81 apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def)
    82 apply(auto simp: not_less split: extended.splits)
    83 done
    84 
    85 lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep
    86 by(auto simp: eq_ivl_def le_iff_subset)
    87 
    88 definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))"
    89 
    90 lemma le_ivl_iff_subset: "iv1 \<le> iv2 \<longleftrightarrow> \<gamma>_ivl iv1 \<subseteq> \<gamma>_ivl iv2"
    91 by transfer (rule le_iff_subset)
    92 
    93 definition sup_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
    94 "sup_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
    95   else let (l1,h1) = p1; (l2,h2) = p2 in  (min l1 l2, max h1 h2))"
    96 
    97 lift_definition sup_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is sup_rep
    98 by(auto simp: eq_ivl_iff sup_rep_def)
    99 
   100 lift_definition top_ivl :: ivl is "(Minf,Pinf)" .
   101 
   102 lemma is_empty_min_max:
   103   "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
   104 by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
   105 
   106 instance
   107 proof (standard, goal_cases)
   108   case 1 show ?case by (rule less_ivl_def)
   109 next
   110   case 2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
   111 next
   112   case 3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
   113 next
   114   case 4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
   115 next
   116   case 5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
   117 next
   118   case 6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
   119 next
   120   case 7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def)
   121 next
   122   case 8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
   123 qed
   124 
   125 end
   126 
   127 text{* Implement (naive) executable equality: *}
   128 instantiation ivl :: equal
   129 begin
   130 
   131 definition equal_ivl where
   132 "equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
   133 
   134 instance
   135 proof (standard, goal_cases)
   136   case 1 show ?case by(simp add: equal_ivl_def eq_iff)
   137 qed
   138 
   139 end
   140 
   141 lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)"
   142 by(simp add: not_less)
   143 lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)"
   144 by(simp add: not_less)
   145 
   146 instantiation ivl :: bounded_lattice
   147 begin
   148 
   149 definition inf_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   150 "inf_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
   151 
   152 lemma \<gamma>_inf_rep: "\<gamma>_rep(inf_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
   153 by(auto simp:inf_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
   154 
   155 lift_definition inf_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is inf_rep
   156 by(auto simp: \<gamma>_inf_rep eq_ivl_def)
   157 
   158 lemma \<gamma>_inf: "\<gamma>_ivl (iv1 \<sqinter> iv2) = \<gamma>_ivl iv1 \<inter> \<gamma>_ivl iv2"
   159 by transfer (rule \<gamma>_inf_rep)
   160 
   161 definition "\<bottom> = empty_ivl"
   162 
   163 instance
   164 proof (standard, goal_cases)
   165   case 1 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
   166 next
   167   case 2 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
   168 next
   169   case 3 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
   170 next
   171   case 4 show ?case
   172     unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
   173 qed
   174 
   175 end
   176 
   177 
   178 lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p"
   179 by (metis eq_ivl_iff is_empty_empty_rep)
   180 
   181 lemma le_ivl_nice: "[l1,h1] \<le> [l2,h2] \<longleftrightarrow>
   182   (if [l1,h1] = \<bottom> then True else
   183    if [l2,h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)"
   184 unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty)
   185 
   186 lemma sup_ivl_nice: "[l1,h1] \<squnion> [l2,h2] =
   187   (if [l1,h1] = \<bottom> then [l2,h2] else
   188    if [l2,h2] = \<bottom> then [l1,h1] else [min l1 l2,max h1 h2])"
   189 unfolding bot_ivl_def by transfer (simp add: sup_rep_def eq_ivl_empty)
   190 
   191 lemma inf_ivl_nice: "[l1,h1] \<sqinter> [l2,h2] = [max l1 l2,min h1 h2]"
   192 by transfer (simp add: inf_rep_def)
   193 
   194 lemma top_ivl_nice: "\<top> = [-\<infinity>,\<infinity>]"
   195 by (simp add: top_ivl_def)
   196 
   197 
   198 instantiation ivl :: plus
   199 begin
   200 
   201 definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   202 "plus_rep p1 p2 =
   203   (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
   204    let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))"
   205 
   206 lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep
   207 by(auto simp: plus_rep_def eq_ivl_iff)
   208 
   209 instance ..
   210 end
   211 
   212 lemma plus_ivl_nice: "[l1,h1] + [l2,h2] =
   213   (if [l1,h1] = \<bottom> \<or> [l2,h2] = \<bottom> then \<bottom> else [l1+l2 , h1+h2])"
   214 unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty)
   215 
   216 lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf"
   217 by(cases x) auto
   218 lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf"
   219 by(cases x) auto
   220 
   221 lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)"
   222 by(cases x) auto
   223 lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)"
   224 by(cases x) auto
   225 
   226 instantiation ivl :: uminus
   227 begin
   228 
   229 definition uminus_rep :: "eint2 \<Rightarrow> eint2" where
   230 "uminus_rep p = (let (l,h) = p in (-h, -l))"
   231 
   232 lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)"
   233 by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff
   234         split: prod.split)
   235 
   236 lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep
   237 by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases)
   238    (auto simp: Icc_eq_Icc split: extended.splits)
   239 
   240 instance ..
   241 end
   242 
   243 lemma \<gamma>_uminus: "i : \<gamma>_ivl iv \<Longrightarrow> -i \<in> \<gamma>_ivl(- iv)"
   244 by transfer (rule \<gamma>_uminus_rep)
   245 
   246 lemma uminus_nice: "-[l,h] = [-h,-l]"
   247 by transfer (simp add: uminus_rep_def)
   248 
   249 instantiation ivl :: minus
   250 begin
   251 
   252 definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where
   253 "(iv1::ivl) - iv2 = iv1 + -iv2"
   254 
   255 instance ..
   256 end
   257 
   258 
   259 definition inv_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where
   260 "inv_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))"
   261 
   262 definition above_rep :: "eint2 \<Rightarrow> eint2" where
   263 "above_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (l,\<infinity>))"
   264 
   265 definition below_rep :: "eint2 \<Rightarrow> eint2" where
   266 "below_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (-\<infinity>,h))"
   267 
   268 lift_definition above :: "ivl \<Rightarrow> ivl" is above_rep
   269 by(auto simp: above_rep_def eq_ivl_iff)
   270 
   271 lift_definition below :: "ivl \<Rightarrow> ivl" is below_rep
   272 by(auto simp: below_rep_def eq_ivl_iff)
   273 
   274 lemma \<gamma>_aboveI: "i \<in> \<gamma>_ivl iv \<Longrightarrow> i \<le> j \<Longrightarrow> j \<in> \<gamma>_ivl(above iv)"
   275 by transfer 
   276    (auto simp add: above_rep_def \<gamma>_rep_cases is_empty_rep_def
   277          split: extended.splits)
   278 
   279 lemma \<gamma>_belowI: "i : \<gamma>_ivl iv \<Longrightarrow> j \<le> i \<Longrightarrow> j : \<gamma>_ivl(below iv)"
   280 by transfer 
   281    (auto simp add: below_rep_def \<gamma>_rep_cases is_empty_rep_def
   282          split: extended.splits)
   283 
   284 definition inv_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
   285 "inv_less_ivl res iv1 iv2 =
   286   (if res
   287    then (iv1 \<sqinter> (below iv2 - [1,1]),
   288          iv2 \<sqinter> (above iv1 + [1,1]))
   289    else (iv1 \<sqinter> above iv2, iv2 \<sqinter> below iv1))"
   290 
   291 lemma above_nice: "above[l,h] = (if [l,h] = \<bottom> then \<bottom> else [l,\<infinity>])"
   292 unfolding bot_ivl_def by transfer (simp add: above_rep_def eq_ivl_empty)
   293 
   294 lemma below_nice: "below[l,h] = (if [l,h] = \<bottom> then \<bottom> else [-\<infinity>,h])"
   295 unfolding bot_ivl_def by transfer (simp add: below_rep_def eq_ivl_empty)
   296 
   297 lemma add_mono_le_Fin:
   298   "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))"
   299 by(drule (1) add_mono) simp
   300 
   301 lemma add_mono_Fin_le:
   302   "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
   303 by(drule (1) add_mono) simp
   304 
   305 global_interpretation Val_semilattice
   306 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   307 proof (standard, goal_cases)
   308   case 1 thus ?case by transfer (simp add: le_iff_subset)
   309 next
   310   case 2 show ?case by transfer (simp add: \<gamma>_rep_def)
   311 next
   312   case 3 show ?case by transfer (simp add: \<gamma>_rep_def)
   313 next
   314   case 4 thus ?case
   315     apply transfer
   316     apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
   317     by(auto simp: empty_rep_def is_empty_rep_def)
   318 qed
   319 
   320 
   321 global_interpretation Val_lattice_gamma
   322 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   323 defines aval_ivl = aval'
   324 proof (standard, goal_cases)
   325   case 1 show ?case by(simp add: \<gamma>_inf)
   326 next
   327   case 2 show ?case unfolding bot_ivl_def by transfer simp
   328 qed
   329 
   330 global_interpretation Val_inv
   331 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   332 and test_num' = in_ivl
   333 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
   334 proof (standard, goal_cases)
   335   case 1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
   336 next
   337   case (2 _ _ _ _ _ i1 i2) thus ?case
   338     unfolding inv_plus_ivl_def minus_ivl_def
   339     apply(clarsimp simp add: \<gamma>_inf)
   340     using gamma_plus'[of "i1+i2" _ "-i1"] gamma_plus'[of "i1+i2" _ "-i2"]
   341     by(simp add:  \<gamma>_uminus)
   342 next
   343   case (3 i1 i2) thus ?case
   344     unfolding inv_less_ivl_def minus_ivl_def one_extended_def
   345     apply(clarsimp simp add: \<gamma>_inf split: if_splits)
   346     using gamma_plus'[of "i1+1" _ "-1"] gamma_plus'[of "i2 - 1" _ "1"]
   347     apply(simp add: \<gamma>_belowI[of i2] \<gamma>_aboveI[of i1]
   348       uminus_ivl.abs_eq uminus_rep_def \<gamma>_ivl_nice)
   349     apply(simp add: \<gamma>_aboveI[of i2] \<gamma>_belowI[of i1])
   350     done
   351 qed
   352 
   353 global_interpretation Abs_Int_inv
   354 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   355 and test_num' = in_ivl
   356 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
   357 defines inv_aval_ivl = inv_aval'
   358 and inv_bval_ivl = inv_bval'
   359 and step_ivl = step'
   360 and AI_ivl = AI
   361 and aval_ivl' = aval''
   362 ..
   363 
   364 
   365 text{* Monotonicity: *}
   366 
   367 lemma mono_plus_ivl: "iv1 \<le> iv2 \<Longrightarrow> iv3 \<le> iv4 \<Longrightarrow> iv1+iv3 \<le> iv2+(iv4::ivl)"
   368 apply transfer
   369 apply(auto simp: plus_rep_def le_iff_subset split: if_splits)
   370 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
   371 
   372 lemma mono_minus_ivl: "iv1 \<le> iv2 \<Longrightarrow> -iv1 \<le> -(iv2::ivl)"
   373 apply transfer
   374 apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split)
   375 by(auto simp: \<gamma>_rep_cases split: extended.splits)
   376 
   377 lemma mono_above: "iv1 \<le> iv2 \<Longrightarrow> above iv1 \<le> above iv2"
   378 apply transfer
   379 apply(auto simp: above_rep_def le_iff_subset split: if_splits prod.split)
   380 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
   381 
   382 lemma mono_below: "iv1 \<le> iv2 \<Longrightarrow> below iv1 \<le> below iv2"
   383 apply transfer
   384 apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
   385 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
   386 
   387 global_interpretation Abs_Int_inv_mono
   388 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   389 and test_num' = in_ivl
   390 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
   391 proof (standard, goal_cases)
   392   case 1 thus ?case by (rule mono_plus_ivl)
   393 next
   394   case 2 thus ?case
   395     unfolding inv_plus_ivl_def minus_ivl_def less_eq_prod_def
   396     by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_minus_ivl)
   397 next
   398   case 3 thus ?case
   399     unfolding less_eq_prod_def inv_less_ivl_def minus_ivl_def
   400     by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_above mono_below)
   401 qed
   402 
   403 
   404 subsubsection "Tests"
   405 
   406 value "show_acom_opt (AI_ivl test1_ivl)"
   407 
   408 text{* Better than @{text AI_const}: *}
   409 value "show_acom_opt (AI_ivl test3_const)"
   410 value "show_acom_opt (AI_ivl test4_const)"
   411 value "show_acom_opt (AI_ivl test6_const)"
   412 
   413 definition "steps c i = (step_ivl \<top> ^^ i) (bot c)"
   414 
   415 value "show_acom_opt (AI_ivl test2_ivl)"
   416 value "show_acom (steps test2_ivl 0)"
   417 value "show_acom (steps test2_ivl 1)"
   418 value "show_acom (steps test2_ivl 2)"
   419 value "show_acom (steps test2_ivl 3)"
   420 
   421 text{* Fixed point reached in 2 steps.
   422  Not so if the start value of x is known: *}
   423 
   424 value "show_acom_opt (AI_ivl test3_ivl)"
   425 value "show_acom (steps test3_ivl 0)"
   426 value "show_acom (steps test3_ivl 1)"
   427 value "show_acom (steps test3_ivl 2)"
   428 value "show_acom (steps test3_ivl 3)"
   429 value "show_acom (steps test3_ivl 4)"
   430 value "show_acom (steps test3_ivl 5)"
   431 
   432 text{* Takes as many iterations as the actual execution. Would diverge if
   433 loop did not terminate. Worse still, as the following example shows: even if
   434 the actual execution terminates, the analysis may not. The value of y keeps
   435 decreasing as the analysis is iterated, no matter how long: *}
   436 
   437 value "show_acom (steps test4_ivl 50)"
   438 
   439 text{* Relationships between variables are NOT captured: *}
   440 value "show_acom_opt (AI_ivl test5_ivl)"
   441 
   442 text{* Again, the analysis would not terminate: *}
   443 value "show_acom (steps test6_ivl 50)"
   444 
   445 end