# HG changeset patch
# User nipkow
# Date 1316072667 -7200
# Node ID 9795fdc87965c45782c8b6c95ff37a248365a2e4
# Parent  74b6ead3c3659b37963dca21c14a3fae3c3df880# Parent  7c93ee993caee802022e454e4fb46da1e786e978
merged

diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/AbsInt0.thy
--- a/src/HOL/IMP/AbsInt0.thy	Wed Sep 14 23:47:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt0.thy	Thu Sep 15 09:44:27 2011 +0200
@@ -9,10 +9,13 @@
 text{* Abstract interpretation over type @{text astate} instead of
 functions. *}
 
-locale Abs_Int = Val_abs
+locale Abs_Int = Val_abs +
+fixes pfp_above :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
+assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
+assumes above: "x0 \<sqsubseteq> pfp_above f x0"
 begin
 
-fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a"  ("aval\<^isup>#") where
+fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
 "aval' (N n) _ = num' n" |
 "aval' (V x) S = lookup S x" |
 "aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
@@ -32,7 +35,7 @@
 "AI (x ::= a) S = update S x (aval' a S)" |
 "AI (c1;c2) S = AI c2 (AI c1 S)" |
 "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = iter_above (AI c) 3 S"
+"AI (WHILE b DO c) S = pfp_above (AI c) S"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
 proof(induct c arbitrary: s t S0)
@@ -47,8 +50,7 @@
     by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
 next
   case (While b c)
-  let ?P = "iter_above (AI c) 3 S0"
-  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by(simp_all add: iter_above_pfp)
+  let ?P = "pfp_above (AI c) S0"
   { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
     proof(induct "WHILE b DO c" s t rule: big_step_induct)
       case WhileFalse thus ?case by simp
@@ -56,7 +58,7 @@
       case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis
     qed
   }
-  with astate_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
+  with astate_in_rep_le[OF `s <: S0` above]
   show ?case by (metis While(2) AI.simps(5))
 qed
 
diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/AbsInt0_const.thy
--- a/src/HOL/IMP/AbsInt0_const.thy	Wed Sep 14 23:47:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_const.thy	Thu Sep 15 09:44:27 2011 +0200
@@ -61,50 +61,51 @@
     by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
 qed
 
-interpretation Abs_Int rep_cval Const plus_cval
+interpretation Abs_Int rep_cval Const plus_cval "(iter_above 3)"
 defines AI_const is AI
 and aval'_const is aval'
-..
+proof qed (auto simp: iter_above_pfp)
 
 text{* Straight line code: *}
 definition "test1_const =
  ''y'' ::= N 7;
  ''z'' ::= Plus (V ''y'') (N 2);
  ''y'' ::= Plus (V ''x'') (N 0)"
-value [code] "list (AI_const test1_const Top)"
 
 text{* Conditional: *}
 definition "test2_const =
  IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
-value "list (AI_const test2_const Top)"
 
 text{* Conditional, test is ignored: *}
 definition "test3_const =
  ''x'' ::= N 42;
  IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
-value "list (AI_const test3_const Top)"
 
 text{* While: *}
 definition "test4_const =
  ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
-value [code] "list (AI_const test4_const Top)"
 
 text{* While, test is ignored: *}
 definition "test5_const =
  ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
-value [code] "list (AI_const test5_const Top)"
 
 text{* Iteration is needed: *}
 definition "test6_const =
   ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
   WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
-value [code] "list (AI_const test6_const Top)"
 
 text{* More iteration would be needed: *}
 definition "test7_const =
   ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
-  WHILE B True DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+  WHILE Less (V ''x'') (N 1)
+  DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+
+value [code] "list (AI_const test1_const Top)"
+value [code] "list (AI_const test2_const Top)"
+value [code] "list (AI_const test3_const Top)"
+value [code] "list (AI_const test4_const Top)"
+value [code] "list (AI_const test5_const Top)"
+value [code] "list (AI_const test6_const Top)"
 value [code] "list (AI_const test7_const Top)"
 
-
 end
diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/AbsInt0_fun.thy
--- a/src/HOL/IMP/AbsInt0_fun.thy	Wed Sep 14 23:47:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_fun.thy	Thu Sep 15 09:44:27 2011 +0200
@@ -31,44 +31,44 @@
 lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
 by (metis join_ge1 join_ge2 join_least le_trans)
 
-fun iter where
-"iter f 0 _ = Top" |
-"iter f (Suc n) x = (if f x \<sqsubseteq> x then x else iter f n (f x))"
+fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter 0 f _ = Top" |
+"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
 
-lemma iter_pfp: "f(iter f n x) \<sqsubseteq> iter f n x"
+lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
 apply (induct n arbitrary: x)
  apply (simp)
 apply (simp)
 done
 
-definition "iter_above f n x0 = iter (\<lambda>x. x0 \<squnion> f x) n x0"
+definition iter_above :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_above n f x0 = iter n (\<lambda>x. x0 \<squnion> f x) x0"
 
 lemma iter_above_pfp:
-shows "f(iter_above f n x0) \<sqsubseteq> iter_above f n x0" and "x0 \<sqsubseteq> iter_above f n x0"
+shows "f(iter_above n f x0) \<sqsubseteq> iter_above n f x0" and "x0 \<sqsubseteq> iter_above n f x0"
 using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"]
 by(auto simp add: iter_above_def)
 
 text{* So much for soundness. But how good an approximation of the post-fixed
 point does @{const iter_above} yield? *}
 
-lemma iter_funpow: "iter f n x \<noteq> Top \<Longrightarrow> EX k. iter f n x = (f^^k) x"
+lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
 apply(induct n arbitrary: x)
  apply simp
 apply (auto)
-apply(rule_tac x=0 in exI)
-apply simp
+ apply(metis funpow.simps(1) id_def)
 by (metis funpow.simps(2) funpow_swap1 o_apply)
 
 text{* For monotone @{text f}, @{term "iter_above f n x0"} yields the least
 post-fixed point above @{text x0}, unless it yields @{text Top}. *}
 
 lemma iter_least_pfp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above f n x0 \<sqsubseteq> p"
+assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above n f x0 \<sqsubseteq> p"
 proof-
   let ?F = "\<lambda>x. x0 \<squnion> f x"
-  obtain k where "iter_above f n x0 = (?F^^k) x0"
-    using iter_funpow `iter_above f n x0 \<noteq> Top`
+  obtain k where "iter_above n f x0 = (?F^^k) x0"
+    using iter_funpow `iter_above n f x0 \<noteq> Top`
     by(fastforce simp add: iter_above_def)
   moreover
   { fix n have "(?F^^n) x0 \<sqsubseteq> p"
@@ -89,10 +89,10 @@
 by (metis assms join_ge2 le_trans)
 
 lemma iter_above_almost_fp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
-shows "iter_above f n x0 \<sqsubseteq> x0 \<squnion> f(iter_above f n x0)"
+assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
+shows "iter_above n f x0 \<sqsubseteq> x0 \<squnion> f(iter_above n f x0)"
 proof-
-  let ?p = "iter_above f n x0"
+  let ?p = "iter_above n f x0"
   obtain k where 1: "?p = ((\<lambda>x. x0 \<squnion> f x)^^k) x0"
     using iter_funpow `?p \<noteq> Top`
     by(fastforce simp add: iter_above_def)
@@ -117,8 +117,8 @@
 
 locale Val_abs = Rep rep
   for rep :: "'a::SL_top \<Rightarrow> val set" +
-fixes num' :: "val \<Rightarrow> 'a"  ("num\<^isup>#")
-and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  ("plus\<^isup>#")
+fixes num' :: "val \<Rightarrow> 'a"
+and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 assumes rep_num': "rep(num' n) = {n}"
 and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
 
@@ -143,13 +143,18 @@
 
 subsection "Abstract Interpretation Abstractly"
 
-text{* Abstract interpretation over abstract values.
-Abstract states are simply functions. *}
+text{* Abstract interpretation over abstract values. Abstract states are
+simply functions. The post-fixed point finder is parameterized over. *}
+
+type_synonym 'a st = "name \<Rightarrow> 'a"
 
-locale Abs_Int_Fun = Val_abs
+locale Abs_Int_Fun = Val_abs +
+fixes pfp_above :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
+assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
+assumes above: "x0 \<sqsubseteq> pfp_above f x0"
 begin
 
-fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" ("aval\<^isup>#") where
+fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
 "aval' (N n) _ = num' n" |
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
@@ -168,7 +173,7 @@
 "AI (x ::= a) S = S(x := aval' a S)" |
 "AI (c1;c2) S = AI c2 (AI c1 S)" |
 "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = iter_above (AI c) 3 S"
+"AI (WHILE b DO c) S = pfp_above (AI c) S"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
 proof(induct c arbitrary: s t S0)
@@ -181,8 +186,7 @@
   case If thus ?case by(auto simp: in_rep_join)
 next
   case (While b c)
-  let ?P = "iter_above (AI c) 3 S0"
-  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by (simp_all add: iter_above_pfp)
+  let ?P = "pfp_above (AI c) S0"
   { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
     proof(induct "WHILE b DO c" s t rule: big_step_induct)
       case WhileFalse thus ?case by simp
@@ -190,7 +194,7 @@
       case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
     qed
   }
-  with fun_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
+  with fun_in_rep_le[OF `s <: S0` above]
   show ?case by (metis While(2) AI.simps(5))
 qed
 
diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/AbsInt1.thy
--- a/src/HOL/IMP/AbsInt1.thy	Wed Sep 14 23:47:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy	Thu Sep 15 09:44:27 2011 +0200
@@ -64,8 +64,6 @@
 
 definition "Top = Up Top"
 
-(* register <= as transitive - see orderings *)
-
 instance proof
   case goal1 show ?case by(cases x, simp_all)
 next
@@ -84,7 +82,10 @@
 end
 
 
-locale Abs_Int1 = Val_abs1
+locale Abs_Int1 = Val_abs1 +
+fixes pfp_above :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
+assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
+assumes above: "x0 \<sqsubseteq> pfp_above f x0"
 begin
 
 (* FIXME avoid duplicating this defn *)
@@ -114,11 +115,21 @@
 "afilter (N n) a S = (if n <: a then S else bot)" |
 "afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
   let a' = lookup S x \<sqinter> a in
-  if a'\<sqsubseteq> Bot then bot else Up(update S x a'))" |
+  if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
 "afilter (Plus e1 e2) a S =
  (let (a1,a2) = inv_plus' (aval' e1 S) (aval' e2 S) a
   in afilter e1 a1 (afilter e2 a2 S))"
 
+text{* The test for @{const Bot} in the @{const V}-case is important: @{const
+Bot} indicates that a variable has no possible values, i.e.\ that the current
+program point is unreachable. But then the abstract state should collaps to
+@{const bot}. Put differently, we maintain the invariant that in an abstract
+state all variables are mapped to non-@{const Bot} values. Otherwise the
+(pointwise) join of two abstract states, one of which contains @{const Bot}
+values, may produce too large a result, thus making the analysis less
+precise. *}
+
+
 fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
 "bfilter (B bv) res S = (if bv=res then S else bot)" |
 "bfilter (Not b) res S = bfilter b (\<not> res) S" |
@@ -167,7 +178,7 @@
 "AI (IF b THEN c1 ELSE c2) S =
   AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
 "AI (WHILE b DO c) S =
-  bfilter b False (iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S)"
+  bfilter b False (pfp_above (\<lambda>S. AI c (bfilter b True S)) S)"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
 proof(induct c arbitrary: s t S)
@@ -181,9 +192,7 @@
   case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
 next
   case (While b c)
-  let ?P = "iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S"
-  have pfp: "AI c (bfilter b True ?P) \<sqsubseteq> ?P" and "S \<sqsubseteq> ?P"
-    by (rule iter_above_pfp(1), rule iter_above_pfp(2))
+  let ?P = "pfp_above (\<lambda>S. AI c (bfilter b True S)) S"
   { fix s t
     have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
           t <:: bfilter b False ?P"
@@ -196,7 +205,7 @@
            rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
     qed
   }
-  with in_rep_up_trans[OF `s <:: S` `S \<sqsubseteq> ?P`] While(2,3) AI.simps(5)
+  with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
   show ?case by simp
 qed
 
diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/AbsInt1_ivl.thy
--- a/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 14 23:47:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt1_ivl.thy	Thu Sep 15 09:44:27 2011 +0200
@@ -8,10 +8,19 @@
 
 datatype ivl = I "int option" "int option"
 
+text{* We assume an important invariant: arithmetic operations are never
+applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
+i"}. This avoids special cases. Why can we assume this? Because an empty
+interval of values for a variable means that the current program point is
+unreachable. But this should actually translate into the bottom state, not a
+state where some variables have empty intervals. *}
+
 definition "rep_ivl i =
  (case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
   | I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
 
+definition "num_ivl n = I (Some n) (Some n)"
+
 instantiation option :: (plus)plus
 begin
 
@@ -36,16 +45,16 @@
 lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
 by(auto simp add: rep_ivl_def split: ivl.split option.split)
 
-definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty
-  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
+definition "plus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
+  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
 
 instantiation ivl :: SL_top
 begin
 
 definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
 "le_option pos x y =
- (case x of (Some i) \<Rightarrow> (case y of (Some j) \<Rightarrow> (i<=j) | None \<Rightarrow> pos)
-  | None \<Rightarrow> (case y of Some j \<Rightarrow> (~pos) | None \<Rightarrow> True))"
+ (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
+  | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
 
 fun le_aux where
 "le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
@@ -95,8 +104,9 @@
 instantiation ivl :: L_top_bot
 begin
 
-definition "i1 \<sqinter> i2 = (if is_empty i1 | is_empty i2 then empty
-  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (max_option False l1 l2) (min_option True h1 h2))"
+definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
+  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
+    I (max_option False l1 l2) (min_option True h1 h2))"
 
 definition "Bot = empty"
 
@@ -127,24 +137,22 @@
 
 end
 
-definition "minus_ivl i1 i2 =
- (if is_empty i1 | is_empty i2 then empty
-  else case (i1,i2) of
-    (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
+definition "minus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
+  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
 
 lemma rep_minus_ivl:
   "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
 by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
 
 
-definition "inv_plus_ivl i1 i2 i =
-  (if is_empty i then empty
-   else i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
+definition "inv_plus_ivl i1 i2 i = ((*if is_empty i then empty else*)
+  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
 
 fun inv_less_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool \<Rightarrow> ivl * ivl" where
 "inv_less_ivl (I l1 h1) (I l2 h2) res =
   (if res
-   then (I l1 (min_option True h1 (h2 - Some 1)), I (max_option False (l1 + Some 1) l2) h2)
+   then (I l1 (min_option True h1 (h2 - Some 1)),
+         I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
 interpretation Rep rep_ivl
@@ -153,9 +161,9 @@
     by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
 qed
 
-interpretation Val_abs rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl
+interpretation Val_abs rep_ivl num_ivl plus_ivl
 proof
-  case goal1 thus ?case by(simp add: rep_ivl_def)
+  case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
 next
   case goal2 thus ?case
     by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
@@ -169,7 +177,8 @@
   case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
 qed
 
-interpretation Val_abs1 rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
+interpretation
+  Val_abs1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl
 proof
   case goal1 thus ?case
     by(auto simp add: inv_plus_ivl_def)
@@ -180,12 +189,13 @@
       auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
-interpretation Abs_Int1 rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
+interpretation
+  Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3)"
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
 and AI_ivl is AI
 and aval_ivl is aval'
-..
+proof qed (auto simp: iter_above_pfp)
 
 
 fun list_up where
@@ -228,4 +238,16 @@
  WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
 value [code] "list_up(AI_ivl test2_ivl Top)"
 
+definition "test3_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ WHILE Less (V ''x'') (N 11)
+ DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
+value [code] "list_up(AI_ivl test3_ivl Top)"
+
+definition "test4_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 0;
+ WHILE Less (V ''x'') (N 1001)
+ DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+value [code] "list_up(AI_ivl test4_ivl Top)"
+
 end
diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/AbsInt2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/AbsInt2.thy	Thu Sep 15 09:44:27 2011 +0200
@@ -0,0 +1,139 @@
+(* Author: Tobias Nipkow *)
+
+theory AbsInt2
+imports AbsInt1_ivl
+begin
+
+subsection "Widening and Narrowing"
+
+text{* The assumptions about winden and narrow are merely sanity checks. They
+are only needed in case we want to prove termination of the fixedpoint
+iteration, which we do not --- we limit the number of iterations as before. *}
+
+class WN = SL_top +
+fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
+assumes widen: "y \<sqsubseteq> x \<nabla> y"
+fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
+assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
+assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+begin
+
+fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_up f 0 x = Top" |
+"iter_up f (Suc n) x =
+  (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
+
+lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
+apply (induct n arbitrary: x)
+ apply (simp)
+apply (simp add: Let_def)
+done
+
+fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_down f 0 x = x" |
+"iter_down f (Suc n) x =
+  (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
+
+lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
+apply (induct n arbitrary: x)
+ apply (simp)
+apply (simp add: Let_def)
+done
+
+definition iter_above :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_above m n f x =
+  (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
+
+lemma iter_above_pfp:
+shows "f(iter_above m n f x0) \<sqsubseteq> iter_above m n f x0"
+and "x0 \<sqsubseteq> iter_above m n f x0"
+using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
+by(auto simp add: iter_above_def Let_def)
+
+end
+
+
+instantiation ivl :: WN
+begin
+
+definition "widen_ivl ivl1 ivl2 =
+  ((*if is_empty ivl1 then ivl2 else
+   if is_empty ivl2 then ivl1 else*)
+     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
+       I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
+         (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
+
+definition "narrow_ivl ivl1 ivl2 =
+  ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
+     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
+       I (if l1 = None then l2 else l1)
+         (if h1 = None then h2 else h1))"
+
+instance
+proof qed
+  (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
+
+end
+
+instantiation astate :: (WN)WN
+begin
+
+definition "widen_astate F1 F2 =
+  FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
+
+definition "narrow_astate F1 F2 =
+  FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
+
+instance
+proof
+  case goal1 thus ?case
+    by(simp add: widen_astate_def le_astate_def lookup_def widen)
+next
+  case goal2 thus ?case
+    by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
+next
+  case goal3 thus ?case
+    by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
+qed
+
+end
+
+instantiation up :: (WN)WN
+begin
+
+fun widen_up where
+"widen_up bot x = x" |
+"widen_up x bot = x" |
+"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
+
+fun narrow_up where
+"narrow_up bot x = bot" |
+"narrow_up x bot = bot" |
+"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
+
+instance
+proof
+  case goal1 show ?case
+    by(induct x y rule: widen_up.induct) (simp_all add: widen)
+next
+  case goal2 thus ?case
+    by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
+next
+  case goal3 thus ?case
+    by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
+qed
+
+end
+
+interpretation
+  Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3 2)"
+defines afilter_ivl' is afilter
+and bfilter_ivl' is bfilter
+and AI_ivl' is AI
+and aval_ivl' is aval'
+proof qed (auto simp: iter_above_pfp)
+
+value [code] "list_up(AI_ivl' test3_ivl Top)"
+value [code] "list_up(AI_ivl' test4_ivl Top)"
+
+end
diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/Astate.thy
--- a/src/HOL/IMP/Astate.thy	Wed Sep 14 23:47:04 2011 +0200
+++ b/src/HOL/IMP/Astate.thy	Thu Sep 15 09:44:27 2011 +0200
@@ -2,6 +2,8 @@
 
 theory Astate
 imports AbsInt0_fun
+  "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
+  (* Library import merely to allow string lists to be sorted for output *)
 begin
 
 subsection "Abstract State with Computable Ordering"
@@ -13,12 +15,14 @@
 fun "fun" where "fun (FunDom f _) = f"
 fun dom where "dom (FunDom _ A) = A"
 
-definition "list S = [(x,fun S x). x \<leftarrow> dom S]"
+definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
+
+definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
 
 definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
 
 definition "update F x y =
-  FunDom ((fun F)(x:=y)) (if x : set(dom F) then dom F else x # dom F)"
+  FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
 
 lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
 by(rule ext)(auto simp: lookup_def update_def)
@@ -30,7 +34,7 @@
 
 definition
 "join_astate F G =
- FunDom (\<lambda>x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
 
 definition "Top = FunDom (\<lambda>x. Top) []"
 
diff -r 74b6ead3c365 -r 9795fdc87965 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Wed Sep 14 23:47:04 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML	Thu Sep 15 09:44:27 2011 +0200
@@ -1,4 +1,7 @@
-no_document use_thys ["~~/src/HOL/ex/Interpretation_with_Defs"];
+no_document use_thys
+  ["~~/src/HOL/ex/Interpretation_with_Defs",
+   "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
+  ];
 
 use_thys
 ["BExp",
@@ -12,7 +15,7 @@
  "Def_Ass_Sound_Big",
  "Def_Ass_Sound_Small",
  "Live",
- "AbsInt1_ivl",
+ "AbsInt2",
  "Hoare_Examples",
  "VC",
  "HoareT",