# HG changeset patch
# User nipkow
# Date 1317196511 -7200
# Node ID 054a9ac0d7ef8ebd015d33e9326dd019a05c9946
# Parent  305f83b6da5473ce1826d39d9decb76d84813969
Added Hoare-like Abstract Interpretation

diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int0.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,101 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int0
+imports Abs_State
+begin
+
+subsection "Computable Abstract Interpretation"
+
+text{* Abstract interpretation over type @{text astate} instead of
+functions. *}
+
+locale Abs_Int = Val_abs +
+fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
+assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
+and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
+begin
+
+fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
+"aval' (N n) _ = num' n" |
+"aval' (V x) S = lookup S x" |
+"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+
+fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
+"step S (SKIP {P}) = (SKIP {S})" |
+"step S (x ::= e {P}) =
+  x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(update S x (aval' e S))}" |
+"step S (c1; c2) = step S c1; step (post c1) c2" |
+"step S (IF b THEN c1 ELSE c2 {P}) =
+  (let c1' = step S c1; c2' = step S c2
+   in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
+"step S ({Inv} WHILE b DO c {P}) =
+   {S \<squnion> post c} WHILE b DO step Inv c {Inv}"
+
+lemma strip_step[simp]: "strip(step S c) = strip c"
+by(induct c arbitrary: S) (simp_all add: Let_def)
+
+definition AI :: "com \<Rightarrow> 'a st up acom" where
+"AI c = pfp (step Top) (bot_acom c)"
+
+
+subsubsection "Monotonicity"
+
+lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+by(induction e) (auto simp: le_st_def lookup_def mono_plus')
+
+lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
+by(auto simp add: le_st_def lookup_def update_def)
+
+lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
+apply(induction c arbitrary: S S')
+apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
+done
+
+subsubsection "Soundness"
+
+lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
+
+lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
+by(simp add: rep_st_def lookup_update)
+
+lemma step_sound:
+  "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
+proof(induction c arbitrary: S s t)
+  case SKIP thus ?case
+    by simp (metis skipE up_fun_in_rep_le)
+next
+  case Assign thus ?case
+    apply (auto simp del: fun_upd_apply simp: split: up.splits)
+    by (metis aval'_sound fun_in_rep_le in_rep_update)
+next
+  case Semi thus ?case by simp blast
+next
+  case (If b c1 c2 S0) thus ?case
+    apply(auto simp: Let_def)
+    apply (metis up_fun_in_rep_le)+
+    done
+next
+  case (While Inv b c P)
+  from While.prems have inv: "step Inv c \<sqsubseteq> c"
+    and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
+  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
+    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
+      case WhileFalse thus ?case by simp
+    next
+      case (WhileTrue s1 s2 s3)
+      from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
+      show ?case .
+    qed
+  }
+  thus ?case using While.prems(2)
+    by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
+qed
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
+by(fastforce simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
+
+end
+
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int0_const.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,150 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int0_const
+imports Abs_Int0
+begin
+
+subsection "Constant Propagation"
+
+datatype cval = Const val | Any
+
+fun rep_cval where
+"rep_cval (Const n) = {n}" |
+"rep_cval (Any) = UNIV"
+
+fun plus_cval where
+"plus_cval (Const m) (Const n) = Const(m+n)" |
+"plus_cval _ _ = Any"
+
+lemma plus_cval_cases: "plus_cval a1 a2 =
+  (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
+by(auto split: prod.split cval.split)
+
+instantiation cval :: SL_top
+begin
+
+fun le_cval where
+"_ \<sqsubseteq> Any = True" |
+"Const n \<sqsubseteq> Const m = (n=m)" |
+"Any \<sqsubseteq> Const _ = False"
+
+fun join_cval where
+"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
+"_ \<squnion> _ = Any"
+
+definition "\<top> = Any"
+
+instance
+proof
+  case goal1 thus ?case by (cases x) simp_all
+next
+  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
+next
+  case goal3 thus ?case by(cases x, cases y, simp_all)
+next
+  case goal4 thus ?case by(cases y, cases x, simp_all)
+next
+  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
+next
+  case goal6 thus ?case by(simp add: Top_cval_def)
+qed
+
+end
+
+interpretation Rep rep_cval
+proof
+  case goal1 thus ?case
+    by(cases a, cases b, simp, simp, cases b, simp, simp)
+next
+  case goal2 show ?case by(simp add: Top_cval_def)
+qed
+
+interpretation Val_abs rep_cval Const plus_cval
+proof
+  case goal1 show ?case by simp
+next
+  case goal2 thus ?case
+    by(auto simp: plus_cval_cases split: cval.split)
+next
+  case goal3 thus ?case
+    by(auto simp: plus_cval_cases split: cval.split)
+qed
+
+text{* Could set the limit of the number of iterations to an arbitrarily
+large number because all ascending chains in this semilattice are finite. *}
+
+interpretation Abs_Int rep_cval Const plus_cval "(iter 15)"
+defines AI_const is AI
+and aval'_const is aval'
+and step_const is step
+proof qed (auto simp: iter_pfp strip_iter)
+
+text{* Straight line code: *}
+definition "test1_const =
+ ''y'' ::= N 7;
+ ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= Plus (V ''x'') (N 0)"
+
+text{* Conditional: *}
+definition "test2_const =
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
+
+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"
+
+text{* While: *}
+definition "test4_const =
+ ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
+
+text{* While, test is ignored: *}
+definition "test5_const =
+ ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+
+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'')"
+
+text{* More iteration would be needed: *}
+definition "test7_const =
+  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
+  WHILE Less (V ''x'') (N 1)
+  DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+
+text{* For readability: *}
+translations "x" <= "CONST V x"
+translations "x" <= "CONST N x"
+translations "x" <= "CONST Const x"
+translations "x < y" <= "CONST Less x y"
+translations "x" <= "CONST B x"
+translations "x" <= "CONST Up x"
+
+value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
+value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
+value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
+value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
+value [code] "show_acom (AI_const test1_const)"
+
+value [code] "show_acom (AI_const test2_const)"
+value [code] "show_acom (AI_const test3_const)"
+
+value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
+value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
+value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
+value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
+value [code] "show_acom (AI_const test4_const)"
+
+value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
+value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
+value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))"
+value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
+value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
+value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
+value [code] "show_acom (AI_const test5_const)"
+
+value [code] "show_acom (AI_const test6_const)"
+value [code] "show_acom (AI_const test7_const)"
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int0_fun.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,423 @@
+(* Author: Tobias Nipkow *)
+
+header "Abstract Interpretation"
+
+theory Abs_Int0_fun
+imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+begin
+
+subsection "Annotated Commands"
+
+datatype 'a acom =
+  SKIP   'a                           ("SKIP {_}") |
+  Assign name aexp 'a                 ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
+  Semi   "'a acom" "'a acom"          ("_;// _"  [60, 61] 60) |
+  If     bexp "'a acom" "'a acom" 'a
+    ("((IF _/ THEN _/ ELSE _)/ {_})"  [0, 0, 61, 0] 61) |
+  While  'a bexp "'a acom" 'a
+    ("({_}// WHILE _/ DO (_)// {_})"  [0, 0, 61, 0] 61)
+
+fun post :: "'a acom \<Rightarrow>'a" where
+"post (SKIP {P}) = P" |
+"post (x ::= e {P}) = P" |
+"post (c1; c2) = post c2" |
+"post (IF b THEN c1 ELSE c2 {P}) = P" |
+"post ({Inv} WHILE b DO c {P}) = P"
+
+fun strip :: "'a acom \<Rightarrow> com" where
+"strip (SKIP {a}) = com.SKIP" |
+"strip (x ::= e {a}) = (x ::= e)" |
+"strip (c1;c2) = (strip c1; strip c2)" |
+"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
+"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
+
+fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
+"anno a com.SKIP = SKIP {a}" |
+"anno a (x ::= e) = (x ::= e {a})" |
+"anno a (c1;c2) = (anno a c1; anno a c2)" |
+"anno a (IF b THEN c1 ELSE c2) =
+  (IF b THEN anno a c1 ELSE anno a c2 {a})" |
+"anno a (WHILE b DO c) =
+  ({a} WHILE b DO anno a c {a})"
+
+lemma strip_anno[simp]: "strip (anno a c) = c"
+by(induct c) simp_all
+
+fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
+"map_acom f (SKIP {a}) = SKIP {f a}" |
+"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
+"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
+"map_acom f (IF b THEN c1 ELSE c2 {a}) =
+  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
+"map_acom f ({a1} WHILE b DO c {a2}) =
+  ({f a1} WHILE b DO map_acom f c {f a2})"
+
+
+subsection "Orderings"
+
+class preord =
+fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
+assumes le_refl[simp]: "x \<sqsubseteq> x"
+and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+begin
+
+definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+
+lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
+
+lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
+by(simp add: mono_def)
+
+declare le_trans[trans]
+
+end
+
+text{* Note: no antisymmetry. Allows implementations where some abstract
+element is implemented by two different values @{prop "x \<noteq> y"}
+such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
+needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
+*}
+
+class SL_top = preord +
+fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+fixes Top :: "'a" ("\<top>")
+assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
+and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
+and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
+and top[simp]: "x \<sqsubseteq> \<top>"
+begin
+
+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)
+
+lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
+by (metis join_ge1 join_ge2 le_trans)
+
+end
+
+instantiation "fun" :: (type, SL_top) SL_top
+begin
+
+definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
+definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+definition "\<top> = (\<lambda>x. \<top>)"
+
+lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
+by (simp add: join_fun_def)
+
+instance
+proof
+  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
+qed (simp_all add: le_fun_def Top_fun_def)
+
+end
+
+
+instantiation acom :: (preord) preord
+begin
+
+fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
+"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
+"le_acom (c1;c2) (c1';c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" |
+"le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
+  (b=b' \<and> le_acom c1 c1' \<and> le_acom c2 c2' \<and> S \<sqsubseteq> S')" |
+"le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
+  (b=b' \<and> le_acom c c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')" |
+"le_acom _ _ = False"
+
+lemma [simp]: "SKIP {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<sqsubseteq> S')"
+by (cases c) auto
+
+lemma [simp]: "x ::= e {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<sqsubseteq> S')"
+by (cases c) auto
+
+lemma [simp]: "c1;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')"
+by (cases c) auto
+
+lemma [simp]: "IF b THEN c1 ELSE c2 {S} \<sqsubseteq> c \<longleftrightarrow>
+  (\<exists>c1' c2' S'. c = IF b THEN c1' ELSE c2' {S'} \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2' \<and> S \<sqsubseteq> S')"
+by (cases c) auto
+
+lemma [simp]: "{Inv} WHILE b DO c {P} \<sqsubseteq> w \<longleftrightarrow>
+  (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<sqsubseteq> c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')"
+by (cases w) auto
+
+instance
+proof
+  case goal1 thus ?case by (induct x) auto
+next
+  case goal2 thus ?case
+  apply(induct x y arbitrary: z rule: le_acom.induct)
+  apply (auto intro: le_trans)
+  done
+qed
+
+end
+
+definition Top_acom :: "com \<Rightarrow> ('a::SL_top) acom" ("\<top>\<^sub>c") where
+"\<top>\<^sub>c = anno \<top>"
+
+lemma strip_Top_acom[simp]: "strip (\<top>\<^sub>c c) = c"
+by(simp add: Top_acom_def)
+
+lemma le_Top_acomp[simp]: "strip c' = c \<Longrightarrow> c' \<sqsubseteq> \<top>\<^sub>c c"
+by(induct c' arbitrary: c) (auto simp: Top_acom_def)
+
+
+subsubsection "Lifting"
+
+datatype 'a up = Bot | Up 'a
+
+instantiation up :: (SL_top)SL_top
+begin
+
+fun le_up where
+"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
+"Bot \<sqsubseteq> y = True" |
+"Up _ \<sqsubseteq> Bot = False"
+
+lemma [simp]: "(x \<sqsubseteq> Bot) = (x = Bot)"
+by (cases x) simp_all
+
+lemma [simp]: "(Up x \<sqsubseteq> u) = (\<exists>y. u = Up y & x \<sqsubseteq> y)"
+by (cases u) auto
+
+fun join_up where
+"Up x \<squnion> Up y = Up(x \<squnion> y)" |
+"Bot \<squnion> y = y" |
+"x \<squnion> Bot = x"
+
+lemma [simp]: "x \<squnion> Bot = x"
+by (cases x) simp_all
+
+definition "\<top> = Up \<top>"
+
+instance proof
+  case goal1 show ?case by(cases x, simp_all)
+next
+  case goal2 thus ?case
+    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
+next
+  case goal3 thus ?case by(cases x, simp, cases y, simp_all)
+next
+  case goal4 thus ?case by(cases y, simp, cases x, simp_all)
+next
+  case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+next
+  case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
+qed
+
+end
+
+definition bot_acom :: "com \<Rightarrow> ('a::SL_top)up acom" ("\<bottom>\<^sub>c") where
+"\<bottom>\<^sub>c = anno Bot"
+
+lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c"
+by(simp add: bot_acom_def)
+
+
+subsection "Absract Interpretation"
+
+text{* The representation of abstract by a set of concrete values: *}
+
+locale Rep =
+fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
+assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
+and rep_Top: "rep \<top> = UNIV"
+begin
+
+abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
+
+lemma in_rep_Top[simp]: "x <: \<top>"
+by(simp add: rep_Top)
+
+end
+
+definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
+"rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
+
+fun rep_up :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a up \<Rightarrow> 'b set" where
+"rep_up rep Bot = {}" |
+"rep_up rep (Up a) = rep a"
+
+text{* The interface for abstract values: *}
+
+(* FIXME: separate Rep interface needed? *)
+locale Val_abs = Rep rep for rep :: "'a::SL_top \<Rightarrow> val set" +
+fixes num' :: "val \<Rightarrow> 'a"
+and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+assumes rep_num': "n <: num' n"
+and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
+and mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+
+
+subsubsection "Post-fixed point iteration"
+
+fun iter :: "nat \<Rightarrow> (('a::SL_top) acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"iter 0 f c = \<top>\<^sub>c (strip c)" |
+"iter (Suc n) f c = (let fc = f c in if fc \<sqsubseteq> c then c else iter n f fc)"
+(* code lemma?? *)
+
+lemma strip_iter: assumes "\<forall>c. strip(f c) = strip c"
+shows "strip(iter n f c) = strip c"
+apply (induction n arbitrary: c)
+ apply (metis iter.simps(1) strip_Top_acom)
+apply (simp add:Let_def)
+by (metis assms)
+
+lemma iter_pfp: assumes "\<forall>c. strip(f c) = strip c"
+shows "f(iter n f c) \<sqsubseteq> iter n f c"
+apply (induction n arbitrary: c)
+ apply(simp add: assms)
+apply (simp add:Let_def)
+done
+
+lemma iter_funpow: assumes "\<forall>c. strip(f c) = strip c"
+shows "iter n f x \<noteq> \<top>\<^sub>c (strip x) \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
+apply(induction n arbitrary: x)
+ apply simp
+apply (auto simp: Let_def assms)
+ apply(metis funpow.simps(1) id_def)
+by (metis assms funpow.simps(2) funpow_swap1 o_apply)
+
+text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
+post-fixed point above @{text x0}, unless it yields @{text Top}. *}
+
+lemma iter_least_pfp:
+assumes strip: "\<forall>c. strip(f c) = strip c"
+and mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+and not_top: "iter n f x0 \<noteq> \<top>\<^sub>c (strip x0)"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
+proof-
+  obtain k where "iter n f x0 = (f^^k) x0"
+    using iter_funpow[OF strip not_top] by blast
+  moreover
+  { fix n have "(f^^n) x0 \<sqsubseteq> p"
+    proof(induction n)
+      case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
+    next
+      case (Suc n) thus ?case
+        by (simp add: `x0 \<sqsubseteq> p`)(metis Suc `f p \<sqsubseteq> p` le_trans mono)
+    qed
+  } ultimately show ?thesis by simp
+qed
+
+type_synonym 'a st = "(name \<Rightarrow> 'a)"
+
+locale Abs_Int_Fun = Val_abs +
+fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
+assumes pfp: "f(pfp f c) \<sqsubseteq> pfp f c"
+and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
+begin
+
+fun aval' :: "aexp \<Rightarrow> 'a st \<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)"
+
+fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
+"step S (SKIP {P}) = (SKIP {S})" |
+"step S (x ::= e {P}) =
+  x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(S(x := aval' e S))}" |
+"step S (c1; c2) = step S c1; step (post c1) c2" |
+"step S (IF b THEN c1 ELSE c2 {P}) =
+  (let c1' = step S c1; c2' = step S c2
+   in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
+"step S ({Inv} WHILE b DO c {P}) =
+  {S \<squnion> post c} WHILE b DO (step Inv c) {Inv}"
+
+lemma strip_step[simp]: "strip(step S c) = strip c"
+by(induct c arbitrary: S) (simp_all add: Let_def)
+
+
+definition AI :: "com \<Rightarrow> 'a st up acom" where
+"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
+
+
+abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
+"s <:f S == s \<in> rep_fun rep S"
+
+notation fun_in_rep (infix "<:\<^sub>f" 50)
+
+lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
+by(auto simp add: rep_fun_def le_fun_def dest: le_rep)
+
+abbreviation up_in_rep :: "state \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50) where
+"s <:up S == s : rep_up (rep_fun rep) S"
+
+notation (output) up_in_rep (infix "<:\<^sub>u\<^sub>p" 50)
+
+lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
+by (cases S) (auto intro:fun_in_rep_le)
+
+lemma in_rep_Top_fun: "s <:f Top"
+by(simp add: Top_fun_def rep_fun_def)
+
+lemma in_rep_Top_up: "s <:up Top"
+by(simp add: Top_up_def in_rep_Top_fun)
+
+
+subsubsection "Monotonicity"
+
+lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+by(induction e)(auto simp: le_fun_def mono_plus')
+
+lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
+by(simp add: le_fun_def)
+
+lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
+apply(induction c arbitrary: S S')
+apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
+done
+
+subsubsection "Soundness"
+
+lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def)
+
+lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f S(x := a)"
+by(simp add: rep_fun_def)
+
+lemma step_sound:
+  "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
+proof(induction c arbitrary: S s t)
+  case SKIP thus ?case
+    by simp (metis skipE up_fun_in_rep_le)
+next
+  case Assign thus ?case
+    apply (auto simp del: fun_upd_apply split: up.splits)
+    by (metis aval'_sound fun_in_rep_le in_rep_update)
+next
+  case Semi thus ?case by simp blast
+next
+  case (If b c1 c2 S0) thus ?case
+    apply(auto simp: Let_def)
+    apply (metis up_fun_in_rep_le)+
+    done
+next
+  case (While Inv b c P)
+  from While.prems have inv: "step Inv c \<sqsubseteq> c"
+    and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
+  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
+    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
+      case WhileFalse thus ?case by simp
+    next
+      case (WhileTrue s1 s2 s3)
+      from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
+      show ?case .
+    qed
+  }
+  thus ?case using While.prems(2)
+    by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
+qed
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
+by(auto simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
+
+end
+
+text{* Problem: not executable because of the comparison of abstract states,
+i.e. functions, in the post-fixedpoint computation. *}
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int1.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,266 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int1
+imports Abs_Int0_const
+begin
+
+instantiation prod :: (preord,preord) preord
+begin
+
+definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
+
+instance
+proof
+  case goal1 show ?case by(simp add: le_prod_def)
+next
+  case goal2 thus ?case unfolding le_prod_def by(metis le_trans)
+qed
+
+end
+
+
+subsection "Backward Analysis of Expressions"
+
+hide_const bot
+
+class L_top_bot = SL_top +
+fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
+and bot :: "'a" ("\<bottom>")
+assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
+and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
+and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+assumes bot[simp]: "\<bottom> \<sqsubseteq> x"
+
+locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
+assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
+  -- "this means the meet is precise"
+and rep_Bot: "rep \<bottom> = {}"
+begin
+
+lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
+by (metis IntI inter_rep_subset_rep_meet set_mp)
+
+lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
+by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
+
+lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
+by (metis meet_greatest meet_le1 meet_le2 le_trans)
+
+end
+
+
+locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
+  for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
+fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
+  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
+  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
+  filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
+and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
+  filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
+
+locale Abs_Int1 = Val_abs1 +
+fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
+assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> mono f \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
+and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
+begin
+
+lemma in_rep_join_UpI: "s <:up S1 | s <:up S2 \<Longrightarrow> s <:up S1 \<squnion> S2"
+by (metis join_ge1 join_ge2 up_fun_in_rep_le)
+
+fun aval' :: "aexp \<Rightarrow> 'a st up \<Rightarrow> 'a" where
+"aval' _ Bot = \<bottom>" |
+"aval' (N n) _ = num' n" |
+"aval' (V x) (Up S) = lookup S x" |
+"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+
+lemma aval'_sound: "s <:up S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def)
+
+fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
+"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> \<bottom> then Bot else Up(update S x a'))" |
+"afilter (Plus e1 e2) a S =
+ (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
+  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 collapse 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 st up \<Rightarrow> 'a st up" where
+"bfilter (B bv) res S = (if bv=res then S else Bot)" |
+"bfilter (Not b) res S = bfilter b (\<not> res) S" |
+"bfilter (And b1 b2) res S =
+  (if res then bfilter b1 True (bfilter b2 True S)
+   else bfilter b1 False S \<squnion> bfilter b2 False S)" |
+"bfilter (Less e1 e2) res S =
+  (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
+   in afilter e1 res1 (afilter e2 res2 S))"
+
+lemma afilter_sound: "s <:up S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:up afilter e a S"
+proof(induction e arbitrary: a S)
+  case N thus ?case by simp
+next
+  case (V x)
+  obtain S' where "S = Up S'" and "s <:f S'" using `s <:up S`
+    by(auto simp: in_rep_up_iff)
+  moreover hence "s x <: lookup S' x" by(simp add: rep_st_def)
+  moreover have "s x <: a" using V by simp
+  ultimately show ?case using V(1)
+    by(simp add: lookup_update Let_def rep_st_def)
+      (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
+next
+  case (Plus e1 e2) thus ?case
+    using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+    by (auto split: prod.split)
+qed
+
+lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S"
+proof(induction b arbitrary: S bv)
+  case B thus ?case by simp
+next
+  case (Not b) thus ?case by simp
+next
+  case (And b1 b2) thus ?case by(fastforce simp: in_rep_join_UpI)
+next
+  case (Less e1 e2) thus ?case
+    by (auto split: prod.split)
+       (metis afilter_sound filter_less' aval'_sound Less)
+qed
+
+
+fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
+"step S (SKIP {P}) = (SKIP {S})" |
+"step S (x ::= e {P}) =
+  x ::= e {case S of Bot \<Rightarrow> Bot
+           | Up S \<Rightarrow> Up(update S x (aval' e (Up S)))}" |
+"step S (c1; c2) = step S c1; step (post c1) c2" |
+"step S (IF b THEN c1 ELSE c2 {P}) =
+  (let c1' = step (bfilter b True S) c1; c2' = step (bfilter b False S) c2
+   in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
+"step S ({Inv} WHILE b DO c {P}) =
+   {S \<squnion> post c}
+   WHILE b DO step (bfilter b True Inv) c
+   {bfilter b False Inv}"
+
+lemma strip_step[simp]: "strip(step S c) = strip c"
+by(induct c arbitrary: S) (simp_all add: Let_def)
+
+
+definition AI :: "com \<Rightarrow> 'a st up acom" where
+"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
+
+
+subsubsection "Monotonicity"
+
+lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+apply(cases S)
+ apply simp
+apply(cases S')
+ apply simp
+apply simp
+by(induction e) (auto simp: le_st_def lookup_def mono_plus')
+
+lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
+apply(induction e arbitrary: r r' S S')
+apply(auto simp: Let_def split: up.splits prod.splits)
+apply (metis le_rep subsetD)
+apply(drule_tac x = "list" in mono_lookup)
+apply (metis mono_meet le_trans)
+apply (metis mono_meet mono_lookup mono_update le_trans)
+apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
+done
+
+lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'"
+apply(induction b arbitrary: r S S')
+apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits)
+apply(metis mono_aval' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
+done
+
+
+lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
+by (induction c c' rule: le_acom.induct) simp_all
+
+lemma mono_step: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
+apply(induction c c' arbitrary: S S' rule: le_acom.induct)
+apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
+  split: up.split)
+done
+
+
+subsubsection "Soundness"
+
+lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
+by(simp add: rep_st_def lookup_update)
+
+lemma While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
+by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
+
+lemma step_sound:
+  "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
+proof(induction c arbitrary: S s t)
+  case SKIP thus ?case
+    by simp (metis skipE up_fun_in_rep_le)
+next
+  case Assign thus ?case
+    apply (auto simp del: fun_upd_apply split: up.splits)
+    by (metis aval'_sound fun_in_rep_le in_rep_update rep_up.simps(2))
+next
+  case Semi thus ?case by simp blast
+next
+  case (If b c1 c2 S0)
+  show ?case
+  proof cases
+    assume "bval b s"
+    with If.prems have 1: "step (bfilter b True S) c1 \<sqsubseteq> c1"
+      and 2: "(strip c1, s) \<Rightarrow> t" and 3: "post c1 \<sqsubseteq> S0" by(auto simp: Let_def)
+    from If.IH(1)[OF 1 2 bfilter_sound[OF `s <:up S`]] `bval b s` 3
+    show ?thesis by simp (metis up_fun_in_rep_le)
+  next
+    assume "\<not> bval b s"
+    with If.prems have 1: "step (bfilter b False S) c2 \<sqsubseteq> c2"
+      and 2: "(strip c2, s) \<Rightarrow> t" and 3: "post c2 \<sqsubseteq> S0" by(auto simp: Let_def)
+    from If.IH(2)[OF 1 2 bfilter_sound[OF `s <:up S`]] `\<not> bval b s` 3
+    show ?thesis by simp (metis up_fun_in_rep_le)
+  qed
+next
+  case (While Inv b c P)
+  from While.prems have inv: "step (bfilter b True Inv) c \<sqsubseteq> c"
+    and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "bfilter b False Inv \<sqsubseteq> P"
+    by(auto simp: Let_def)
+  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
+    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
+      case WhileFalse thus ?case by simp
+    next
+      case (WhileTrue s1 s2 s3)
+      from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` bfilter_sound[OF `s1 <:up Inv`]] `post c \<sqsubseteq> Inv`]] `bval b s1`
+      show ?case by simp
+    qed
+  } note Inv = this
+  from  While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
+    by(auto dest: While_final_False)
+  from Inv[OF this(1) up_fun_in_rep_le[OF `s <:up S` `S \<sqsubseteq> Inv`]]
+  have "t <:up Inv" .
+  from up_fun_in_rep_le[OF bfilter_sound[OF this]  `bfilter b False Inv \<sqsubseteq> P`]
+  show ?case using `\<not> bval b t` by simp
+qed
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
+by(fastforce simp: AI_def strip_pfp mono_def in_rep_Top_up
+  intro: step_sound pfp  mono_step[OF le_refl])
+
+end
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int1_ivl.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,276 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int1_ivl
+imports Abs_Int1
+begin
+
+subsection "Interval Analysis"
+
+datatype ivl = I "int option" "int option"
+
+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
+
+fun plus_option where
+"Some x + Some y = Some(x+y)" |
+"_ + _ = None"
+
+instance proof qed
+
+end
+
+definition empty where "empty = I (Some 1) (Some 0)"
+
+fun is_empty where
+"is_empty(I (Some l) (Some h)) = (h<l)" |
+"is_empty _ = False"
+
+lemma [simp]: "is_empty(I l h) =
+  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
+by(auto split:option.split)
+
+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))"
+
+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\<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)"
+
+definition le_ivl where
+"i1 \<sqsubseteq> i2 =
+ (if is_empty i1 then True else
+  if is_empty i2 then False else le_aux i1 i2)"
+
+definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
+"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
+
+definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
+"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
+
+definition "i1 \<squnion> i2 =
+ (if is_empty i1 then i2 else if is_empty i2 then i1
+  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
+          I (min_option False l1 l2) (max_option True h1 h2))"
+
+definition "\<top> = I None None"
+
+instance
+proof
+  case goal1 thus ?case
+    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
+next
+  case goal2 thus ?case
+    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
+next
+  case goal3 thus ?case
+    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+next
+  case goal4 thus ?case
+    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+next
+  case goal5 thus ?case
+    by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
+next
+  case goal6 thus ?case
+    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
+qed
+
+end
+
+
+instantiation ivl :: L_top_bot
+begin
+
+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 "\<bottom> = empty"
+
+instance
+proof
+  case goal1 thus ?case
+    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+  case goal2 thus ?case
+    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+  case goal3 thus ?case
+    by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
+next
+  case goal4 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
+qed
+
+end
+
+instantiation option :: (minus)minus
+begin
+
+fun minus_option where
+"Some x - Some y = Some(x-y)" |
+"_ - _ = None"
+
+instance proof qed
+
+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))"
+
+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 "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
+  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
+
+fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
+"filter_less_ivl res (I l1 h1) (I l2 h2) =
+  (if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else
+   if res
+   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
+proof
+  case goal1 thus ?case
+    by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
+next
+  case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
+qed
+
+interpretation Val_abs rep_ivl num_ivl plus_ivl
+proof
+  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)
+next
+  case goal3 thus ?case
+    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
+qed
+
+interpretation Rep1 rep_ivl
+proof
+  case goal1 thus ?case
+    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
+next
+  case goal2 show ?case by(auto simp add: bot_ivl_def rep_ivl_def empty_def)
+qed
+
+lemma mono_minus_ivl:
+  "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> minus_ivl i1 i2 \<sqsubseteq> minus_ivl i1' i2'"
+apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits)
+  apply(simp split: option.splits)
+ apply(simp split: option.splits)
+apply(simp split: option.splits)
+done
+
+
+interpretation
+  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+proof
+  case goal1 thus ?case
+    by(auto simp add: filter_plus_ivl_def)
+      (metis rep_minus_ivl add_diff_cancel add_commute)+
+next
+  case goal2 thus ?case
+    by(cases a1, cases a2,
+      auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
+next
+  case goal3 thus ?case
+    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
+next
+  case goal4 thus ?case
+    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
+    by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+qed
+
+interpretation
+  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter 20)"
+defines afilter_ivl is afilter
+and bfilter_ivl is bfilter
+and step_ivl is step
+and AI_ivl is AI
+and aval_ivl is aval'
+proof qed (auto simp: iter_pfp strip_iter)
+
+definition "test1_ivl =
+ ''y'' ::= N 7;
+ IF Less (V ''x'') (V ''y'')
+ THEN ''y'' ::= Plus (V ''y'') (V ''x'')
+ ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
+
+translations
+"{i..j}" <= "CONST I (CONST Some i) (CONST Some j)"
+"{..j}" <= "CONST I (CONST None) (CONST Some j)"
+"{i..}" <= "CONST I (CONST Some i) (CONST None)"
+"CONST UNIV" <= "CONST I (CONST None) (CONST None)"
+
+value [code] "show_acom (AI_ivl test1_ivl)"
+
+value [code] "show_acom (AI_const test3_const)"
+value [code] "show_acom (AI_ivl test3_const)"
+
+value [code] "show_acom (AI_const test4_const)"
+value [code] "show_acom (AI_ivl test4_const)"
+
+value [code] "show_acom (AI_ivl test6_const)"
+
+definition "test2_ivl =
+ WHILE Less (V ''x'') (N 100)
+ DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+value [code] "show_acom (AI_ivl test2_ivl)"
+
+definition "test3_ivl =
+ ''x'' ::= N 7;
+ WHILE Less (V ''x'') (N 100)
+ DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+value [code] "show_acom (AI_ivl test3_ivl)"
+value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
+
+definition "test4_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] "show_acom(AI_ivl test4_ivl)"
+
+definition "test5_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] "show_acom(AI_ivl test5_ivl)"
+
+text{* Nontermination not detected: *}
+definition "test6_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+value [code] "show_acom(AI_ivl test6_ivl)"
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int2.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,216 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int2
+imports Abs_Int1_ivl
+begin
+
+
+subsection "Widening and Narrowing"
+
+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"
+
+
+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 l1)
+         (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
+
+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 st :: (WN)WN
+begin
+
+definition "widen_st F1 F2 =
+  FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
+
+definition "narrow_st 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_st_def le_st_def lookup_def widen)
+next
+  case goal2 thus ?case
+    by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
+next
+  case goal3 thus ?case
+    by(auto simp: narrow_st_def le_st_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
+
+fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
+"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
+"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" |
+"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
+  (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
+"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
+  ({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})"
+
+abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65)
+where "widen_acom == map2_acom (op \<nabla>)"
+
+abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65)
+where "narrow_acom == map2_acom (op \<triangle>)"
+
+lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
+by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
+
+lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
+by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
+
+fun iter_up :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"iter_up f 0 x = \<top>\<^sub>c (strip x)" |
+"iter_up f (Suc n) x =
+  (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla>\<^sub>c fx))"
+
+abbreviation
+  iter_down :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"iter_down f n x == ((\<lambda>x. x \<triangle>\<^sub>c f x)^^n) x"
+
+definition
+  iter' :: "nat \<Rightarrow> nat \<Rightarrow> (('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"iter' m n f x = iter_down f n (iter_up f m x)"
+
+lemma strip_map2_acom:
+ "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
+by(induct f c1 c2 rule: map2_acom.induct) simp_all
+
+lemma strip_iter_up: assumes "\<forall>c. strip(f c) = strip c"
+shows "strip(iter_up f n c) = strip c"
+apply (induction n arbitrary: c)
+ apply (metis iter_up.simps(1) strip_Top_acom snd_conv)
+apply (simp add:Let_def)
+by (metis assms strip_map2_acom)
+
+lemma iter_up_pfp: assumes "\<forall>c. strip(f c) = strip c"
+shows "f(iter_up f n c) \<sqsubseteq> iter_up f n c"
+apply (induction n arbitrary: c)
+ apply(simp add: assms)
+apply (simp add:Let_def)
+done
+
+lemma strip_iter_down: assumes "\<forall>c. strip(f c) = strip c"
+shows "strip(iter_down f n c) = strip c"
+apply (induction n arbitrary: c)
+ apply(simp)
+apply (simp add: strip_map2_acom assms)
+done
+
+lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
+defines "x n == iter_down f n x0"
+shows "f(x n) \<sqsubseteq> x n"
+proof (induction n)
+  case 0 show ?case by (simp add: x_def assms(2))
+next
+  case (Suc n)
+  have "f (x (Suc n)) = f(x n \<triangle>\<^sub>c f(x n))" by(simp add: x_def)
+  also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2_acom[OF Suc]])
+  also have "\<dots> \<sqsubseteq> x n \<triangle>\<^sub>c f(x n)" by(rule narrow1_acom[OF Suc])
+  also have "\<dots> = x(Suc n)" by(simp add: x_def)
+  finally show ?case .
+qed
+
+lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
+defines "x n == iter_down f n x0"
+shows "x n \<sqsubseteq> x0"
+proof (induction n)
+  case 0 show ?case by(simp add: x_def)
+next
+  case (Suc n)
+  have "x(Suc n) = x n \<triangle>\<^sub>c f(x n)" by(simp add: x_def)
+  also have "\<dots> \<sqsubseteq> x n" unfolding x_def
+    by(rule narrow2_acom[OF iter_down_pfp[OF assms(1), OF assms(2)]])
+  also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
+  finally show ?case .
+qed
+
+
+lemma iter'_pfp: assumes "\<forall>c. strip (f c) = strip c" and "mono f"
+shows "f (iter' m n f c) \<sqsubseteq> iter' m n f c"
+using iter_up_pfp[of f] iter_down_pfp[of f]
+by(auto simp add: iter'_def Let_def assms)
+
+lemma strip_iter': assumes "\<forall>c. strip(f c) = strip c"
+shows "strip(iter' m n f c) = strip c"
+by(simp add: iter'_def strip_iter_down strip_iter_up assms)
+
+
+interpretation
+  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 20 5)"
+defines afilter_ivl' is afilter
+and bfilter_ivl' is bfilter
+and step_ivl' is step
+and AI_ivl' is AI
+and aval_ivl' is aval'
+proof qed (auto simp: iter'_pfp strip_iter')
+
+value [code] "show_acom (AI_ivl test3_ivl)"
+value [code] "show_acom (AI_ivl' test3_ivl)"
+
+definition "step_up n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
+definition "step_down n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
+
+value [code] "show_acom (step_up 1 (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (step_up 2 (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (step_up 3 (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (step_up 4 (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (step_up 5 (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (step_down 1 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
+value [code] "show_acom (step_down 2 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
+value [code] "show_acom (step_down 3 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
+
+value [code] "show_acom (AI_ivl' test4_ivl)"
+value [code] "show_acom (AI_ivl' test5_ivl)"
+value [code] "show_acom (AI_ivl' test6_ivl)"
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy	Wed Sep 28 08:51:55 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Abs_Int0
-imports Abs_State
-begin
-
-subsection "Computable Abstract Interpretation"
-
-text{* Abstract interpretation over type @{text astate} instead of
-functions. *}
-
-locale Abs_Int = Val_abs +
-fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
-assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
-assumes above: "x0 \<sqsubseteq> pfp f x0"
-begin
-
-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)"
-
-abbreviation astate_in_rep (infix "<:" 50) where
-"s <: S == ALL x. s x <: lookup S x"
-
-lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
-by (metis in_mono le_astate_def le_rep lookup_def top)
-
-lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus')
-
-
-fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
-"AI SKIP S = S" |
-"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 = pfp (AI c) S"
-
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induction c arbitrary: s t S0)
-  case SKIP thus ?case by fastforce
-next
-  case Assign thus ?case
-    by (auto simp: lookup_update aval'_sound)
-next
-  case Semi thus ?case by auto
-next
-  case If thus ?case
-    by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
-next
-  case (While b c)
-  let ?P = "pfp (AI c) S0"
-  { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
-    proof(induction "WHILE b DO c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by simp
-    next
-      case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
-    qed
-  }
-  with astate_in_rep_le[OF `s <: S0` above]
-  show ?case by (metis While(2) AI.simps(5))
-qed
-
-end
-
-end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int0_const.thy	Wed Sep 28 08:51:55 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Abs_Int0_const
-imports Abs_Int0
-begin
-
-subsection "Constant Propagation"
-
-datatype cval = Const val | Any
-
-fun rep_cval where
-"rep_cval (Const n) = {n}" |
-"rep_cval (Any) = UNIV"
-
-fun plus_cval where
-"plus_cval (Const m) (Const n) = Const(m+n)" |
-"plus_cval _ _ = Any"
-
-instantiation cval :: SL_top
-begin
-
-fun le_cval where
-"_ \<sqsubseteq> Any = True" |
-"Const n \<sqsubseteq> Const m = (n=m)" |
-"Any \<sqsubseteq> Const _ = False"
-
-fun join_cval where
-"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
-"_ \<squnion> _ = Any"
-
-definition "Top = Any"
-
-instance
-proof
-  case goal1 thus ?case by (cases x) simp_all
-next
-  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
-next
-  case goal3 thus ?case by(cases x, cases y, simp_all)
-next
-  case goal4 thus ?case by(cases y, cases x, simp_all)
-next
-  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
-next
-  case goal6 thus ?case by(simp add: Top_cval_def)
-qed
-
-end
-
-interpretation Rep rep_cval
-proof
-  case goal1 thus ?case
-    by(cases a, cases b, simp, simp, cases b, simp, simp)
-qed
-
-interpretation Val_abs rep_cval Const plus_cval
-proof
-  case goal1 show ?case by simp
-next
-  case goal2 thus ?case
-    by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
-qed
-
-interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
-defines AI_const is AI
-and aval'_const is aval'
-proof qed (auto simp: iter'_pfp_above)
-
-text{* Straight line code: *}
-definition "test1_const =
- ''y'' ::= N 7;
- ''z'' ::= Plus (V ''y'') (N 2);
- ''y'' ::= Plus (V ''x'') (N 0)"
-
-text{* Conditional: *}
-definition "test2_const =
- IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
-
-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"
-
-text{* While: *}
-definition "test4_const =
- ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
-
-text{* While, test is ignored: *}
-definition "test5_const =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
-
-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'')"
-
-text{* More iteration would be needed: *}
-definition "test7_const =
-  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
-  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 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int0_fun.thy	Wed Sep 28 08:51:55 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-header "Denotational Abstract Interpretation"
-
-theory Abs_Int0_fun
-imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
-begin
-
-subsection "Orderings"
-
-class preord =
-fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
-assumes le_refl[simp]: "x \<sqsubseteq> x"
-and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-
-text{* Note: no antisymmetry. Allows implementations where some abstract
-element is implemented by two different values @{prop "x \<noteq> y"}
-such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
-needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
-*}
-
-class SL_top = preord +
-fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
-fixes Top :: "'a"
-assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
-and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
-and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<sqsubseteq> Top"
-begin
-
-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 :: "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 n f x) \<sqsubseteq> iter n f x"
-apply (induction n arbitrary: x)
- apply (simp)
-apply (simp)
-done
-
-abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
-
-lemma iter'_pfp_above:
-  "f(iter' n f x0) \<sqsubseteq> iter' n f x0"  "x0 \<sqsubseteq> iter' n f x0"
-using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
-
-text{* So much for soundness. But how good an approximation of the post-fixed
-point does @{const iter} yield? *}
-
-lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
-apply(induction n arbitrary: x)
- apply simp
-apply (auto)
- apply(metis funpow.simps(1) id_def)
-by (metis funpow.simps(2) funpow_swap1 o_apply)
-
-text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
-post-fixed point above @{text x0}, unless it yields @{text Top}. *}
-
-lemma iter_least_pfp:
-assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
-proof-
-  obtain k where "iter n f x0 = (f^^k) x0"
-    using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
-  moreover
-  { fix n have "(f^^n) x0 \<sqsubseteq> p"
-    proof(induction n)
-      case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
-    next
-      case (Suc n) thus ?case
-        by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
-    qed
-  } ultimately show ?thesis by simp
-qed
-
-end
-
-text{* The interface of abstract values: *}
-
-locale Rep =
-fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
-assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
-begin
-
-abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
-
-lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
-by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
-
-end
-
-locale Val_abs = Rep rep
-  for rep :: "'a::SL_top \<Rightarrow> val set" +
-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"
-
-
-instantiation "fun" :: (type, SL_top) SL_top
-begin
-
-definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
-definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
-definition "Top = (\<lambda>x. Top)"
-
-lemma join_apply[simp]:
-  "(f \<squnion> g) x = f x \<squnion> g x"
-by (simp add: join_fun_def)
-
-instance
-proof
-  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
-qed (simp_all add: le_fun_def Top_fun_def)
-
-end
-
-subsection "Abstract Interpretation Abstractly"
-
-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 +
-fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
-assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
-assumes above: "x \<sqsubseteq> pfp f x"
-begin
-
-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)"
-
-abbreviation fun_in_rep (infix "<:" 50) where
-"f <: F == \<forall>x. f x <: F x"
-
-lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
-by (metis le_fun_def le_rep subsetD)
-
-lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus')
-
-fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
-"AI SKIP S = S" |
-"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 = pfp (AI c) S"
-
-lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induction c arbitrary: s t S0)
-  case SKIP thus ?case by fastforce
-next
-  case Assign thus ?case by (auto simp: aval'_sound)
-next
-  case Semi thus ?case by auto
-next
-  case If thus ?case by(auto simp: in_rep_join)
-next
-  case (While b c)
-  let ?P = "pfp (AI c) S0"
-  { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
-    proof(induction "WHILE b DO c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by simp
-    next
-      case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
-    qed
-  }
-  with fun_in_rep_le[OF `s <: S0` above]
-  show ?case by (metis While(2) AI.simps(5))
-qed
-
-end
-
-
-text{* Problem: not executable because of the comparison of abstract states,
-i.e. functions, in the post-fixedpoint computation. Need to implement
-abstract states concretely. *}
-
-end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int1.thy	Wed Sep 28 08:51:55 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,214 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Abs_Int1
-imports Abs_Int0_const
-begin
-
-subsection "Backward Analysis of Expressions"
-
-class L_top_bot = SL_top +
-fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
-and Bot :: "'a"
-assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
-and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
-and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
-assumes bot[simp]: "Bot \<sqsubseteq> x"
-
-locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
-assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
-and rep_Bot: "rep Bot = {}"
-begin
-
-lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
-by (metis IntI inter_rep_subset_rep_meet set_mp)
-
-lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
-by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
-
-end
-
-
-locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
-  for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
-fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
-  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
-  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-
-datatype 'a up = bot | Up 'a
-
-instantiation up :: (SL_top)SL_top
-begin
-
-fun le_up where
-"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
-"bot \<sqsubseteq> y = True" |
-"Up _ \<sqsubseteq> bot = False"
-
-lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
-by (cases x) simp_all
-
-lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
-by (cases u) auto
-
-fun join_up where
-"Up x \<squnion> Up y = Up(x \<squnion> y)" |
-"bot \<squnion> y = y" |
-"x \<squnion> bot = x"
-
-lemma [simp]: "x \<squnion> bot = x"
-by (cases x) simp_all
-
-
-definition "Top = Up Top"
-
-instance proof
-  case goal1 show ?case by(cases x, simp_all)
-next
-  case goal2 thus ?case
-    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
-next
-  case goal3 thus ?case by(cases x, simp, cases y, simp_all)
-next
-  case goal4 thus ?case by(cases y, simp, cases x, simp_all)
-next
-  case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
-next
-  case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
-qed
-
-end
-
-
-locale Abs_Int1 = Val_abs1 +
-fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
-assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
-assumes above: "x0 \<sqsubseteq> pfp f x0"
-begin
-
-(* FIXME avoid duplicating this defn *)
-abbreviation astate_in_rep (infix "<:" 50) where
-"s <: S == ALL x. s x <: lookup S x"
-
-abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool"  (infix "<::" 50) where
-"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
-
-lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
-apply auto
-by (metis in_mono le_astate_def le_rep lookup_def top)
-
-lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
-by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
-
-fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
-"aval' _ bot = Bot" |
-"aval' (N n) _ = num' n" |
-"aval' (V x) (Up S) = lookup S x" |
-"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-
-lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus')
-
-fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
-"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'))" |
-"afilter (Plus e1 e2) a S =
- (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
-  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 collapse 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" |
-"bfilter (And b1 b2) res S =
-  (if res then bfilter b1 True (bfilter b2 True S)
-   else bfilter b1 False S \<squnion> bfilter b2 False S)" |
-"bfilter (Less e1 e2) res S =
-  (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
-   in afilter e1 res1 (afilter e2 res2 S))"
-
-lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
-proof(induction e arbitrary: a S)
-  case N thus ?case by simp
-next
-  case (V x)
-  obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
-  moreover hence "s x <: lookup S' x" by(simp)
-  moreover have "s x <: a" using V by simp
-  ultimately show ?case using V(1)
-    by(simp add: lookup_update Let_def)
-       (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
-next
-  case (Plus e1 e2) thus ?case
-    using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
-    by (auto split: prod.split)
-qed
-
-lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
-proof(induction b arbitrary: S bv)
-  case B thus ?case by simp
-next
-  case (Not b) thus ?case by simp
-next
-  case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
-next
-  case (Less e1 e2) thus ?case
-    by (auto split: prod.split)
-       (metis afilter_sound filter_less' aval'_sound Less)
-qed
-
-fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
-"AI SKIP S = S" |
-"AI (x ::= a) S =
-  (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
-"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 (pfp (\<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(induction c arbitrary: s t S)
-  case SKIP thus ?case by fastforce
-next
-  case Assign thus ?case
-    by (auto simp: lookup_update aval'_sound)
-next
-  case Semi thus ?case by fastforce
-next
-  case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
-next
-  case (While b c)
-  let ?P = "pfp (\<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"
-    proof(induction "WHILE b DO c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by(metis bfilter_sound)
-    next
-      case WhileTrue show ?case
-        by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
-           rule While.IH[OF WhileTrue(2)],
-           rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
-    qed
-  }
-  with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
-  show ?case by simp
-qed
-
-end
-
-end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int1_ivl.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int1_ivl.thy	Wed Sep 28 08:51:55 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,260 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Abs_Int1_ivl
-imports Abs_Int1
-begin
-
-subsection "Interval Analysis"
-
-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
-
-fun plus_option where
-"Some x + Some y = Some(x+y)" |
-"_ + _ = None"
-
-instance proof qed
-
-end
-
-definition empty where "empty = I (Some 1) (Some 0)"
-
-fun is_empty where
-"is_empty(I (Some l) (Some h)) = (h<l)" |
-"is_empty _ = False"
-
-lemma [simp]: "is_empty(I l h) =
-  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
-by(auto split:option.split)
-
-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))"
-
-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\<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)"
-
-definition le_ivl where
-"i1 \<sqsubseteq> i2 =
- (if is_empty i1 then True else
-  if is_empty i2 then False else le_aux i1 i2)"
-
-definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
-"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
-
-definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
-"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
-
-definition "i1 \<squnion> i2 =
- (if is_empty i1 then i2 else if is_empty i2 then i1
-  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
-          I (min_option False l1 l2) (max_option True h1 h2))"
-
-definition "Top = I None None"
-
-instance
-proof
-  case goal1 thus ?case
-    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
-next
-  case goal2 thus ?case
-    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
-next
-  case goal3 thus ?case
-    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
-next
-  case goal4 thus ?case
-    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
-next
-  case goal5 thus ?case
-    by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
-next
-  case goal6 thus ?case
-    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
-qed
-
-end
-
-
-instantiation ivl :: L_top_bot
-begin
-
-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"
-
-instance
-proof
-  case goal1 thus ?case
-    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
-next
-  case goal2 thus ?case
-    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
-next
-  case goal3 thus ?case
-    by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
-next
-  case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
-qed
-
-end
-
-instantiation option :: (minus)minus
-begin
-
-fun minus_option where
-"Some x - Some y = Some(x-y)" |
-"_ - _ = None"
-
-instance proof qed
-
-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))"
-
-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 "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
-  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
-
-fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
-"filter_less_ivl res (I l1 h1) (I l2 h2) =
-  ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
-   if res
-   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
-proof
-  case goal1 thus ?case
-    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 num_ivl plus_ivl
-proof
-  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)
-qed
-
-interpretation Rep1 rep_ivl
-proof
-  case goal1 thus ?case
-    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
-next
-  case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
-qed
-
-interpretation
-  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
-proof
-  case goal1 thus ?case
-    by(auto simp add: filter_plus_ivl_def)
-      (metis rep_minus_ivl add_diff_cancel add_commute)+
-next
-  case goal2 thus ?case
-    by(cases a1, cases a2,
-      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 num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 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'_pfp_above)
-
-
-fun list_up where
-"list_up bot = bot" |
-"list_up (Up x) = Up(list x)"
-
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
- (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
- (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
-  (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
-  (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
-  (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
-  (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
-  (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
-
-definition "test_ivl1 =
- ''y'' ::= N 7;
- IF Less (V ''x'') (V ''y'')
- THEN ''y'' ::= Plus (V ''y'') (V ''x'')
- ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
-value [code] "list_up(AI_ivl test_ivl1 Top)"
-
-value "list_up (AI_ivl test3_const Top)"
-
-value "list_up (AI_ivl test5_const Top)"
-
-value "list_up (AI_ivl test6_const Top)"
-
-definition "test2_ivl =
- ''y'' ::= N 7;
- 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)"
-
-text{* Nontermination not detected: *}
-definition "test5_ivl =
- ''x'' ::= N 0;
- WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
-value [code] "list_up(AI_ivl test5_ivl Top)"
-
-end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int2.thy	Wed Sep 28 08:51:55 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,207 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Abs_Int2
-imports Abs_Int1_ivl
-begin
-
-context preord
-begin
-
-definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
-
-lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
-
-lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
-by(simp add: mono_def)
-
-declare le_trans[trans]
-
-end
-
-
-subsection "Widening and Narrowing"
-
-text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
-rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
-a trivial widening step. We generalise this idea and complement it with
-narrowing, a process to regain precision.
-
-Class @{text WN} makes some assumptions about the widening and narrowing
-operators. The assumptions serve two purposes. Together with a further
-assumption that certain chains become stationary, they permit to prove
-termination of the fixed point iteration, which we do not --- we limit the
-number of iterations as before. The second purpose of the narrowing
-assumptions is to prove that the narrowing iteration keeps on producing
-post-fixed points and that it goes down. However, this requires the function
-being iterated to be monotone. Unfortunately, abstract interpretation with
-widening is not monotone. Hence the (recursive) abstract interpretation of a
-loop body that again contains a loop may result in a non-monotone
-function. Therefore our narrowing iteration needs to check at every step
-that a post-fixed point is maintained, and we cannot prove that the precision
-increases. *}
-
-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 (induction 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 (induction n arbitrary: x)
- apply (simp)
-apply (simp add: Let_def)
-done
-
-definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter' m n f x =
-  (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
-
-lemma iter'_pfp_above:
-shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
-and "x0 \<sqsubseteq> iter' 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'_def Let_def)
-
-text{* This is how narrowing works on monotone functions: you just iterate. *}
-
-abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
-
-text{* Narrowing always yields a post-fixed point: *}
-
-lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
-defines "x n == iter_down_mono f n x0"
-shows "f(x n) \<sqsubseteq> x n"
-proof (induction n)
-  case 0 show ?case by (simp add: x_def assms(2))
-next
-  case (Suc n)
-  have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
-  also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
-  also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
-  also have "\<dots> = x(Suc n)" by(simp add: x_def)
-  finally show ?case .
-qed
-
-text{* Narrowing can only increase precision: *}
-
-lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
-defines "x n == iter_down_mono f n x0"
-shows "x n \<sqsubseteq> x0"
-proof (induction n)
-  case 0 show ?case by(simp add: x_def)
-next
-  case (Suc n)
-  have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
-  also have "\<dots> \<sqsubseteq> x n" unfolding x_def
-    by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
-  also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
-  finally show ?case .
-qed
-
-
-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 filter_plus_ivl filter_less_ivl "(iter' 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'_pfp_above)
-
-value [code] "list_up(AI_ivl' test3_ivl Top)"
-value [code] "list_up(AI_ivl' test4_ivl Top)"
-value [code] "list_up(AI_ivl' test5_ivl Top)"
-
-end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,67 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int_den0
+imports Abs_State_den
+begin
+
+subsection "Computable Abstract Interpretation"
+
+text{* Abstract interpretation over type @{text astate} instead of
+functions. *}
+
+locale Abs_Int = Val_abs +
+fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> pfp f x0"
+begin
+
+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)"
+
+abbreviation astate_in_rep (infix "<:" 50) where
+"s <: S == ALL x. s x <: lookup S x"
+
+lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
+by (metis in_mono le_astate_def le_rep lookup_def top)
+
+lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus')
+
+
+fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
+"AI SKIP S = S" |
+"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 = pfp (AI c) S"
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
+proof(induction c arbitrary: s t S0)
+  case SKIP thus ?case by fastforce
+next
+  case Assign thus ?case
+    by (auto simp: lookup_update aval'_sound)
+next
+  case Semi thus ?case by auto
+next
+  case If thus ?case
+    by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
+next
+  case (While b c)
+  let ?P = "pfp (AI c) S0"
+  { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
+    proof(induction "WHILE b DO c" s t rule: big_step_induct)
+      case WhileFalse thus ?case by simp
+    next
+      case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
+    qed
+  }
+  with astate_in_rep_le[OF `s <: S0` above]
+  show ?case by (metis While(2) AI.simps(5))
+qed
+
+end
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,111 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int_den0_const
+imports Abs_Int_den0
+begin
+
+subsection "Constant Propagation"
+
+datatype cval = Const val | Any
+
+fun rep_cval where
+"rep_cval (Const n) = {n}" |
+"rep_cval (Any) = UNIV"
+
+fun plus_cval where
+"plus_cval (Const m) (Const n) = Const(m+n)" |
+"plus_cval _ _ = Any"
+
+instantiation cval :: SL_top
+begin
+
+fun le_cval where
+"_ \<sqsubseteq> Any = True" |
+"Const n \<sqsubseteq> Const m = (n=m)" |
+"Any \<sqsubseteq> Const _ = False"
+
+fun join_cval where
+"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
+"_ \<squnion> _ = Any"
+
+definition "Top = Any"
+
+instance
+proof
+  case goal1 thus ?case by (cases x) simp_all
+next
+  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
+next
+  case goal3 thus ?case by(cases x, cases y, simp_all)
+next
+  case goal4 thus ?case by(cases y, cases x, simp_all)
+next
+  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
+next
+  case goal6 thus ?case by(simp add: Top_cval_def)
+qed
+
+end
+
+interpretation Rep rep_cval
+proof
+  case goal1 thus ?case
+    by(cases a, cases b, simp, simp, cases b, simp, simp)
+qed
+
+interpretation Val_abs rep_cval Const plus_cval
+proof
+  case goal1 show ?case by simp
+next
+  case goal2 thus ?case
+    by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
+qed
+
+interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
+defines AI_const is AI
+and aval'_const is aval'
+proof qed (auto simp: iter'_pfp_above)
+
+text{* Straight line code: *}
+definition "test1_const =
+ ''y'' ::= N 7;
+ ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= Plus (V ''x'') (N 0)"
+
+text{* Conditional: *}
+definition "test2_const =
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
+
+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"
+
+text{* While: *}
+definition "test4_const =
+ ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
+
+text{* While, test is ignored: *}
+definition "test5_const =
+ ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+
+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'')"
+
+text{* More iteration would be needed: *}
+definition "test7_const =
+  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
+  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 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,187 @@
+(* Author: Tobias Nipkow *)
+
+header "Denotational Abstract Interpretation"
+
+theory Abs_Int_den0_fun
+imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+begin
+
+subsection "Orderings"
+
+class preord =
+fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
+assumes le_refl[simp]: "x \<sqsubseteq> x"
+and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+
+text{* Note: no antisymmetry. Allows implementations where some abstract
+element is implemented by two different values @{prop "x \<noteq> y"}
+such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
+needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
+*}
+
+class SL_top = preord +
+fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+fixes Top :: "'a"
+assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
+and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
+and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
+and top[simp]: "x \<sqsubseteq> Top"
+begin
+
+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 :: "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 n f x) \<sqsubseteq> iter n f x"
+apply (induction n arbitrary: x)
+ apply (simp)
+apply (simp)
+done
+
+abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
+
+lemma iter'_pfp_above:
+  "f(iter' n f x0) \<sqsubseteq> iter' n f x0"  "x0 \<sqsubseteq> iter' n f x0"
+using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
+
+text{* So much for soundness. But how good an approximation of the post-fixed
+point does @{const iter} yield? *}
+
+lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
+apply(induction n arbitrary: x)
+ apply simp
+apply (auto)
+ apply(metis funpow.simps(1) id_def)
+by (metis funpow.simps(2) funpow_swap1 o_apply)
+
+text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
+post-fixed point above @{text x0}, unless it yields @{text Top}. *}
+
+lemma iter_least_pfp:
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
+proof-
+  obtain k where "iter n f x0 = (f^^k) x0"
+    using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
+  moreover
+  { fix n have "(f^^n) x0 \<sqsubseteq> p"
+    proof(induction n)
+      case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
+    next
+      case (Suc n) thus ?case
+        by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
+    qed
+  } ultimately show ?thesis by simp
+qed
+
+end
+
+text{* The interface of abstract values: *}
+
+locale Rep =
+fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
+assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
+begin
+
+abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
+
+lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
+by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
+
+end
+
+locale Val_abs = Rep rep
+  for rep :: "'a::SL_top \<Rightarrow> val set" +
+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"
+
+
+instantiation "fun" :: (type, SL_top) SL_top
+begin
+
+definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
+definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+definition "Top = (\<lambda>x. Top)"
+
+lemma join_apply[simp]:
+  "(f \<squnion> g) x = f x \<squnion> g x"
+by (simp add: join_fun_def)
+
+instance
+proof
+  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
+qed (simp_all add: le_fun_def Top_fun_def)
+
+end
+
+subsection "Abstract Interpretation Abstractly"
+
+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 +
+fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
+assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
+assumes above: "x \<sqsubseteq> pfp f x"
+begin
+
+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)"
+
+abbreviation fun_in_rep (infix "<:" 50) where
+"f <: F == \<forall>x. f x <: F x"
+
+lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
+by (metis le_fun_def le_rep subsetD)
+
+lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus')
+
+fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
+"AI SKIP S = S" |
+"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 = pfp (AI c) S"
+
+lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
+proof(induction c arbitrary: s t S0)
+  case SKIP thus ?case by fastforce
+next
+  case Assign thus ?case by (auto simp: aval'_sound)
+next
+  case Semi thus ?case by auto
+next
+  case If thus ?case by(auto simp: in_rep_join)
+next
+  case (While b c)
+  let ?P = "pfp (AI c) S0"
+  { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
+    proof(induction "WHILE b DO c" s t rule: big_step_induct)
+      case WhileFalse thus ?case by simp
+    next
+      case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
+    qed
+  }
+  with fun_in_rep_le[OF `s <: S0` above]
+  show ?case by (metis While(2) AI.simps(5))
+qed
+
+end
+
+
+text{* Problem: not executable because of the comparison of abstract states,
+i.e. functions, in the post-fixedpoint computation. Need to implement
+abstract states concretely. *}
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,214 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int_den1
+imports Abs_Int_den0_const
+begin
+
+subsection "Backward Analysis of Expressions"
+
+class L_top_bot = SL_top +
+fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
+and Bot :: "'a"
+assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
+and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
+and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+assumes bot[simp]: "Bot \<sqsubseteq> x"
+
+locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
+assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
+and rep_Bot: "rep Bot = {}"
+begin
+
+lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
+by (metis IntI inter_rep_subset_rep_meet set_mp)
+
+lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
+by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
+
+end
+
+
+locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
+  for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
+fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
+  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
+  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+
+datatype 'a up = bot | Up 'a
+
+instantiation up :: (SL_top)SL_top
+begin
+
+fun le_up where
+"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
+"bot \<sqsubseteq> y = True" |
+"Up _ \<sqsubseteq> bot = False"
+
+lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
+by (cases x) simp_all
+
+lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
+by (cases u) auto
+
+fun join_up where
+"Up x \<squnion> Up y = Up(x \<squnion> y)" |
+"bot \<squnion> y = y" |
+"x \<squnion> bot = x"
+
+lemma [simp]: "x \<squnion> bot = x"
+by (cases x) simp_all
+
+
+definition "Top = Up Top"
+
+instance proof
+  case goal1 show ?case by(cases x, simp_all)
+next
+  case goal2 thus ?case
+    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
+next
+  case goal3 thus ?case by(cases x, simp, cases y, simp_all)
+next
+  case goal4 thus ?case by(cases y, simp, cases x, simp_all)
+next
+  case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+next
+  case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
+qed
+
+end
+
+
+locale Abs_Int1 = Val_abs1 +
+fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
+assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
+assumes above: "x0 \<sqsubseteq> pfp f x0"
+begin
+
+(* FIXME avoid duplicating this defn *)
+abbreviation astate_in_rep (infix "<:" 50) where
+"s <: S == ALL x. s x <: lookup S x"
+
+abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool"  (infix "<::" 50) where
+"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
+
+lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
+apply auto
+by (metis in_mono le_astate_def le_rep lookup_def top)
+
+lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
+by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
+
+fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
+"aval' _ bot = Bot" |
+"aval' (N n) _ = num' n" |
+"aval' (V x) (Up S) = lookup S x" |
+"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+
+lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
+by (induct a) (auto simp: rep_num' rep_plus')
+
+fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
+"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'))" |
+"afilter (Plus e1 e2) a S =
+ (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
+  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 collapse 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" |
+"bfilter (And b1 b2) res S =
+  (if res then bfilter b1 True (bfilter b2 True S)
+   else bfilter b1 False S \<squnion> bfilter b2 False S)" |
+"bfilter (Less e1 e2) res S =
+  (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
+   in afilter e1 res1 (afilter e2 res2 S))"
+
+lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
+proof(induction e arbitrary: a S)
+  case N thus ?case by simp
+next
+  case (V x)
+  obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
+  moreover hence "s x <: lookup S' x" by(simp)
+  moreover have "s x <: a" using V by simp
+  ultimately show ?case using V(1)
+    by(simp add: lookup_update Let_def)
+       (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
+next
+  case (Plus e1 e2) thus ?case
+    using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+    by (auto split: prod.split)
+qed
+
+lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
+proof(induction b arbitrary: S bv)
+  case B thus ?case by simp
+next
+  case (Not b) thus ?case by simp
+next
+  case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
+next
+  case (Less e1 e2) thus ?case
+    by (auto split: prod.split)
+       (metis afilter_sound filter_less' aval'_sound Less)
+qed
+
+fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
+"AI SKIP S = S" |
+"AI (x ::= a) S =
+  (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
+"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"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 (pfp (\<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(induction c arbitrary: s t S)
+  case SKIP thus ?case by fastforce
+next
+  case Assign thus ?case
+    by (auto simp: lookup_update aval'_sound)
+next
+  case Semi thus ?case by fastforce
+next
+  case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
+next
+  case (While b c)
+  let ?P = "pfp (\<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"
+    proof(induction "WHILE b DO c" s t rule: big_step_induct)
+      case WhileFalse thus ?case by(metis bfilter_sound)
+    next
+      case WhileTrue show ?case
+        by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
+           rule While.IH[OF WhileTrue(2)],
+           rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
+    qed
+  }
+  with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
+  show ?case by simp
+qed
+
+end
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,260 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int_den1_ivl
+imports Abs_Int_den1
+begin
+
+subsection "Interval Analysis"
+
+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
+
+fun plus_option where
+"Some x + Some y = Some(x+y)" |
+"_ + _ = None"
+
+instance proof qed
+
+end
+
+definition empty where "empty = I (Some 1) (Some 0)"
+
+fun is_empty where
+"is_empty(I (Some l) (Some h)) = (h<l)" |
+"is_empty _ = False"
+
+lemma [simp]: "is_empty(I l h) =
+  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
+by(auto split:option.split)
+
+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))"
+
+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\<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)"
+
+definition le_ivl where
+"i1 \<sqsubseteq> i2 =
+ (if is_empty i1 then True else
+  if is_empty i2 then False else le_aux i1 i2)"
+
+definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
+"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
+
+definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
+"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
+
+definition "i1 \<squnion> i2 =
+ (if is_empty i1 then i2 else if is_empty i2 then i1
+  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
+          I (min_option False l1 l2) (max_option True h1 h2))"
+
+definition "Top = I None None"
+
+instance
+proof
+  case goal1 thus ?case
+    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
+next
+  case goal2 thus ?case
+    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
+next
+  case goal3 thus ?case
+    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+next
+  case goal4 thus ?case
+    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+next
+  case goal5 thus ?case
+    by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
+next
+  case goal6 thus ?case
+    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
+qed
+
+end
+
+
+instantiation ivl :: L_top_bot
+begin
+
+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"
+
+instance
+proof
+  case goal1 thus ?case
+    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+  case goal2 thus ?case
+    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+  case goal3 thus ?case
+    by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
+next
+  case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
+qed
+
+end
+
+instantiation option :: (minus)minus
+begin
+
+fun minus_option where
+"Some x - Some y = Some(x-y)" |
+"_ - _ = None"
+
+instance proof qed
+
+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))"
+
+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 "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
+  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
+
+fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
+"filter_less_ivl res (I l1 h1) (I l2 h2) =
+  ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
+   if res
+   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
+proof
+  case goal1 thus ?case
+    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 num_ivl plus_ivl
+proof
+  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)
+qed
+
+interpretation Rep1 rep_ivl
+proof
+  case goal1 thus ?case
+    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
+next
+  case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
+qed
+
+interpretation
+  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+proof
+  case goal1 thus ?case
+    by(auto simp add: filter_plus_ivl_def)
+      (metis rep_minus_ivl add_diff_cancel add_commute)+
+next
+  case goal2 thus ?case
+    by(cases a1, cases a2,
+      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 num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 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'_pfp_above)
+
+
+fun list_up where
+"list_up bot = bot" |
+"list_up (Up x) = Up(list x)"
+
+value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
+value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
+value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
+ (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
+value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
+ (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
+value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
+  (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
+value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
+  (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
+
+value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+  (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
+value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+  (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
+value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
+  (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
+
+definition "test_ivl1 =
+ ''y'' ::= N 7;
+ IF Less (V ''x'') (V ''y'')
+ THEN ''y'' ::= Plus (V ''y'') (V ''x'')
+ ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
+value [code] "list_up(AI_ivl test_ivl1 Top)"
+
+value "list_up (AI_ivl test3_const Top)"
+
+value "list_up (AI_ivl test5_const Top)"
+
+value "list_up (AI_ivl test6_const Top)"
+
+definition "test2_ivl =
+ ''y'' ::= N 7;
+ 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)"
+
+text{* Nontermination not detected: *}
+definition "test5_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+value [code] "list_up(AI_ivl test5_ivl Top)"
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,207 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int_den2
+imports Abs_Int_den1_ivl
+begin
+
+context preord
+begin
+
+definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+
+lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
+
+lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
+by(simp add: mono_def)
+
+declare le_trans[trans]
+
+end
+
+
+subsection "Widening and Narrowing"
+
+text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
+rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
+a trivial widening step. We generalise this idea and complement it with
+narrowing, a process to regain precision.
+
+Class @{text WN} makes some assumptions about the widening and narrowing
+operators. The assumptions serve two purposes. Together with a further
+assumption that certain chains become stationary, they permit to prove
+termination of the fixed point iteration, which we do not --- we limit the
+number of iterations as before. The second purpose of the narrowing
+assumptions is to prove that the narrowing iteration keeps on producing
+post-fixed points and that it goes down. However, this requires the function
+being iterated to be monotone. Unfortunately, abstract interpretation with
+widening is not monotone. Hence the (recursive) abstract interpretation of a
+loop body that again contains a loop may result in a non-monotone
+function. Therefore our narrowing iteration needs to check at every step
+that a post-fixed point is maintained, and we cannot prove that the precision
+increases. *}
+
+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 (induction 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 (induction n arbitrary: x)
+ apply (simp)
+apply (simp add: Let_def)
+done
+
+definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter' m n f x =
+  (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
+
+lemma iter'_pfp_above:
+shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
+and "x0 \<sqsubseteq> iter' 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'_def Let_def)
+
+text{* This is how narrowing works on monotone functions: you just iterate. *}
+
+abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
+
+text{* Narrowing always yields a post-fixed point: *}
+
+lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
+defines "x n == iter_down_mono f n x0"
+shows "f(x n) \<sqsubseteq> x n"
+proof (induction n)
+  case 0 show ?case by (simp add: x_def assms(2))
+next
+  case (Suc n)
+  have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
+  also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
+  also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
+  also have "\<dots> = x(Suc n)" by(simp add: x_def)
+  finally show ?case .
+qed
+
+text{* Narrowing can only increase precision: *}
+
+lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
+defines "x n == iter_down_mono f n x0"
+shows "x n \<sqsubseteq> x0"
+proof (induction n)
+  case 0 show ?case by(simp add: x_def)
+next
+  case (Suc n)
+  have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
+  also have "\<dots> \<sqsubseteq> x n" unfolding x_def
+    by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
+  also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
+  finally show ?case .
+qed
+
+
+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 filter_plus_ivl filter_less_ivl "(iter' 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'_pfp_above)
+
+value [code] "list_up(AI_ivl' test3_ivl Top)"
+value [code] "list_up(AI_ivl' test4_ivl Top)"
+value [code] "list_up(AI_ivl' test5_ivl Top)"
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_State.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_State.thy	Wed Sep 28 08:51:55 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Abs_State
-imports Abs_Int0_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"
-
-text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
-
-datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
-
-fun "fun" where "fun (FunDom f _) = f"
-fun dom where "dom (FunDom _ A) = A"
-
-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 \<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)
-
-instantiation astate :: (SL_top) SL_top
-begin
-
-definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
-
-definition
-"join_astate F G =
- FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
-
-definition "Top = FunDom (\<lambda>x. Top) []"
-
-instance
-proof
-  case goal2 thus ?case
-    apply(auto simp: le_astate_def)
-    by (metis lookup_def preord_class.le_trans top)
-qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
-
-end
-
-end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,50 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_State_den
+imports Abs_Int_den0_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"
+
+text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
+
+datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
+
+fun "fun" where "fun (FunDom f _) = f"
+fun dom where "dom (FunDom _ A) = A"
+
+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 \<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)
+
+instantiation astate :: (SL_top) SL_top
+begin
+
+definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
+
+definition
+"join_astate F G =
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
+
+definition "Top = FunDom (\<lambda>x. Top) []"
+
+instance
+proof
+  case goal2 thus ?case
+    apply(auto simp: le_astate_def)
+    by (metis lookup_def preord_class.le_trans top)
+qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
+
+end
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/Abs_State.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_State.thy	Wed Sep 28 09:55:11 2011 +0200
@@ -0,0 +1,95 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_State
+imports Abs_Int0_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"
+
+text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
+
+datatype 'a st = FunDom "name \<Rightarrow> 'a" "name list"
+
+fun "fun" where "fun (FunDom f _) = f"
+fun dom where "dom (FunDom _ A) = A"
+
+definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
+
+definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
+
+fun show_st_up where
+"show_st_up Bot = Bot" |
+"show_st_up (Up S) = Up(show_st S)"
+
+definition "show_acom = map_acom show_st_up"
+
+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 \<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)
+
+definition "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}"
+
+instantiation st :: (SL_top) SL_top
+begin
+
+definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
+
+definition
+"join_st F G =
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
+
+definition "\<top> = FunDom (\<lambda>x. \<top>) []"
+
+instance
+proof
+  case goal2 thus ?case
+    apply(auto simp: le_st_def)
+    by (metis lookup_def preord_class.le_trans top)
+qed (auto simp: le_st_def lookup_def join_st_def Top_st_def)
+
+end
+
+lemma mono_lookup: "F \<sqsubseteq> F' \<Longrightarrow> lookup F x \<sqsubseteq> lookup F' x"
+by(auto simp add: lookup_def le_st_def)
+
+lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
+by(auto simp add: le_st_def lookup_def update_def)
+
+context Rep
+begin
+
+abbreviation fun_in_rep :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
+"s <:f S == s \<in> rep_st rep S"
+
+notation fun_in_rep (infix "<:\<^sub>f" 50)
+
+lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
+apply(auto simp add: rep_st_def le_st_def dest: le_rep)
+by (metis in_rep_Top le_rep lookup_def subsetD)
+
+abbreviation in_rep_up :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50)
+where "s <:up S == s : rep_up (rep_st rep) S"
+
+notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)
+
+lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
+by (cases S) (auto intro:fun_in_rep_le)
+
+lemma in_rep_up_iff: "x <:up u \<longleftrightarrow> (\<exists>u'. u = Up u' \<and> x <:f u')"
+by (cases u) auto
+
+lemma in_rep_Top_fun: "s <:f \<top>"
+by(simp add: rep_st_def lookup_def Top_st_def)
+
+lemma in_rep_Top_up: "s <:up \<top>"
+by(simp add: Top_up_def in_rep_Top_fun)
+
+end
+
+end
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Wed Sep 28 08:51:55 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML	Wed Sep 28 09:55:11 2011 +0200
@@ -18,7 +18,8 @@
  "Hoare_Examples",
  "VC",
  "HoareT",
- "Abs_Int_Den/Abs_Int2",
+ "Abs_Int2",
+ "Abs_Int_Den/Abs_Int_den2",
  "Procs_Dyn_Vars_Dyn",
  "Procs_Stat_Vars_Dyn",
  "Procs_Stat_Vars_Stat",
diff -r 305f83b6da54 -r 054a9ac0d7ef src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Sep 28 08:51:55 2011 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 28 09:55:11 2011 +0200
@@ -515,10 +515,10 @@
 
 HOL-IMP: HOL $(OUT)/HOL-IMP
 
-$(OUT)/HOL-IMP: $(OUT)/HOL IMP/Abs_Int_Den/Abs_Int0_fun.thy \
-  IMP/Abs_Int_Den/Abs_State.thy  IMP/Abs_Int_Den/Abs_Int0.thy \
-  IMP/Abs_Int_Den/Abs_Int0_const.thy IMP/Abs_Int_Den/Abs_Int1.thy \
-  IMP/Abs_Int_Den/Abs_Int1_ivl.thy IMP/Abs_Int_Den/Abs_Int2.thy \
+$(OUT)/HOL-IMP: $(OUT)/HOL IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \
+  IMP/Abs_Int_Den/Abs_State_den.thy  IMP/Abs_Int_Den/Abs_Int_den0.thy \
+  IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \
+  IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \
   IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
   IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
   IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \