# HG changeset patch
# User nipkow
# Date 1334859564 -7200
# Node ID 540a5af9a01c41c899d8493cfdf8977b283ebd35
# Parent  bc9c7b5c26fd1572ecbb38666ec66410120c7615# Parent  e72e44cee6f2f726ce21e2c53a2b575faf718864
merged

diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Thu Apr 19 19:36:09 2012 +0200
+++ b/src/HOL/IMP/ACom.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -41,6 +41,13 @@
 "anno a (WHILE b DO c) =
   ({a} WHILE b DO anno a c {a})"
 
+fun annos :: "'a acom \<Rightarrow> 'a list" where
+"annos (SKIP {a}) = [a]" |
+"annos (x::=e {a}) = [a]" |
+"annos (C1;C2) = annos C1 @ annos C2" |
+"annos (IF b THEN C1 ELSE C2 {a}) = a #  annos C1 @ annos C2" |
+"annos ({i} WHILE b DO C {a}) = i # a # annos C"
+
 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
 "map_acom f (SKIP {P}) = SKIP {f P}" |
 "map_acom f (x ::= e {P}) = (x ::= e {f P})" |
@@ -106,4 +113,16 @@
   (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)"
 by (cases c) simp_all
 
+
+lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}"
+by(induction C)(auto)
+
+lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
+apply(induct C2 arbitrary: C1)
+apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Semi strip_eq_If strip_eq_While)
+done
+
+lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
+
+
 end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,407 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int0
+imports Abs_Int_init
+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"
+begin
+
+definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+
+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 join = preord +
+fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+
+class SL_top = join +
+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, preord) preord
+begin
+
+definition "f \<sqsubseteq> g = (\<forall>x. f x \<sqsubseteq> g x)"
+
+instance
+proof
+  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
+qed (simp_all add: le_fun_def)
+
+end
+
+
+instantiation "fun" :: (type, SL_top) SL_top
+begin
+
+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
+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) (D1;D2) = (C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)" |
+"le_acom (IF b THEN C1 ELSE C2 {S}) (IF b' THEN D1 ELSE D2 {S'}) =
+  (b=b' \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" |
+"le_acom ({I} WHILE b DO C {P}) ({I'} WHILE b' DO C' {P'}) =
+  (b=b' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<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>D1 D2. C = D1;D2 \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)"
+by (cases C) auto
+
+lemma [simp]: "IF b THEN C1 ELSE C2 {S} \<sqsubseteq> C \<longleftrightarrow>
+  (\<exists>D1 D2 S'. C = IF b THEN D1 ELSE D2 {S'} \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')"
+by (cases C) auto
+
+lemma [simp]: "{I} WHILE b DO C {P} \<sqsubseteq> W \<longleftrightarrow>
+  (\<exists>I' C' P'. W = {I'} WHILE b DO C' {P'} \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<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
+
+
+instantiation option :: (preord)preord
+begin
+
+fun le_option where
+"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" |
+"None \<sqsubseteq> y = True" |
+"Some _ \<sqsubseteq> None = False"
+
+lemma [simp]: "(x \<sqsubseteq> None) = (x = None)"
+by (cases x) simp_all
+
+lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y \<and> x \<sqsubseteq> y)"
+by (cases u) auto
+
+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)
+qed
+
+end
+
+instantiation option :: (join)join
+begin
+
+fun join_option where
+"Some x \<squnion> Some y = Some(x \<squnion> y)" |
+"None \<squnion> y = y" |
+"x \<squnion> None = x"
+
+lemma join_None2[simp]: "x \<squnion> None = x"
+by (cases x) simp_all
+
+instance ..
+
+end
+
+instantiation option :: (SL_top)SL_top
+begin
+
+definition "\<top> = Some \<top>"
+
+instance proof
+  case goal1 thus ?case by(cases x, simp, cases y, simp_all)
+next
+  case goal2 thus ?case by(cases y, simp, cases x, simp_all)
+next
+  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+next
+  case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
+qed
+
+end
+
+class Bot = preord +
+fixes Bot :: "'a" ("\<bottom>")
+assumes Bot[simp]: "\<bottom> \<sqsubseteq> x"
+
+instantiation option :: (preord)Bot
+begin
+
+definition Bot_option :: "'a option" where
+"\<bottom> = None"
+
+instance
+proof
+  case goal1 thus ?case by(auto simp: Bot_option_def)
+qed
+
+end
+
+
+definition bot :: "com \<Rightarrow> 'a option acom" where
+"bot c = anno None c"
+
+lemma bot_least: "strip C = c \<Longrightarrow> bot c \<sqsubseteq> C"
+by(induct C arbitrary: c)(auto simp: bot_def)
+
+lemma strip_bot[simp]: "strip(bot c) = c"
+by(simp add: bot_def)
+
+
+subsubsection "Post-fixed point iteration"
+
+definition
+  pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
+"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f"
+
+lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x"
+using while_option_stop[OF assms[simplified pfp_def]] by simp
+
+lemma pfp_least:
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" and "pfp f x0 = Some x" shows "x \<sqsubseteq> p"
+proof-
+  { fix x assume "x \<sqsubseteq> p"
+    hence  "f x \<sqsubseteq> f p" by(rule mono)
+    from this `f p \<sqsubseteq> p` have "f x \<sqsubseteq> p" by(rule le_trans)
+  }
+  thus "x \<sqsubseteq> p" using assms(2-) while_option_rule[where P = "%x. x \<sqsubseteq> p"]
+    unfolding pfp_def by blast
+qed
+
+definition
+ lpfp :: "('a::preord option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
+where "lpfp f c = pfp f (bot c)"
+
+lemma lpfpc_pfp: "lpfp f c = Some p \<Longrightarrow> f p \<sqsubseteq> p"
+by(simp add: pfp_pfp lpfp_def)
+
+lemma strip_pfp:
+assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
+using assms while_option_rule[where P = "%x. g x = g x0" and c = f]
+unfolding pfp_def by metis
+
+lemma strip_lpfp: assumes "\<And>C. strip(f C) = strip C" and "lpfp f c = Some C"
+shows "strip C = c"
+using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp_def]]
+by(metis strip_bot)
+
+
+subsection "Abstract Interpretation"
+
+definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
+"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"
+
+fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
+"\<gamma>_option \<gamma> None = {}" |
+"\<gamma>_option \<gamma> (Some a) = \<gamma> a"
+
+text{* The interface for abstract values: *}
+
+locale Val_abs =
+fixes \<gamma> :: "'av::SL_top \<Rightarrow> val set"
+  assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
+  and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
+fixes num' :: "val \<Rightarrow> 'av"
+and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
+  assumes gamma_num': "n : \<gamma>(num' n)"
+  and gamma_plus':
+ "n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
+
+type_synonym 'av st = "(vname \<Rightarrow> 'av)"
+
+locale Abs_Int_Fun = Val_abs \<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
+begin
+
+fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
+"aval' (N n) S = num' n" |
+"aval' (V x) S = S x" |
+"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+
+fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom"
+ where
+"step' S (SKIP {P}) = (SKIP {S})" |
+"step' S (x ::= e {P}) =
+  x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(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}) =
+   IF b THEN step' S C1 ELSE step' S 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}"
+
+definition AI :: "com \<Rightarrow> 'av st option acom option" where
+"AI = lpfp (step' \<top>)"
+
+
+lemma strip_step'[simp]: "strip(step' S C) = strip C"
+by(induct C arbitrary: S) (simp_all add: Let_def)
+
+
+abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
+where "\<gamma>\<^isub>f == \<gamma>_fun \<gamma>"
+
+abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
+
+abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
+
+lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
+by(simp add: Top_fun_def \<gamma>_fun_def)
+
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
+by (simp add: Top_option_def)
+
+(* FIXME (maybe also le \<rightarrow> sqle?) *)
+
+lemma mono_gamma_f: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>f f1 \<subseteq> \<gamma>\<^isub>f f2"
+by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
+
+lemma mono_gamma_o:
+  "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
+by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_f)
+
+lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
+by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
+
+text{* Soundness: *}
+
+lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
+by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
+
+lemma in_gamma_update:
+  "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(S(x := a))"
+by(simp add: \<gamma>_fun_def)
+
+lemma step_preserves_le:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; C \<le> \<gamma>\<^isub>c C' \<rbrakk> \<Longrightarrow> step S C \<le> \<gamma>\<^isub>c (step' S' C')"
+proof(induction C arbitrary: C' S S')
+  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
+next
+  case Assign thus ?case
+    by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
+      split: option.splits del:subsetD)
+next
+  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+    by (metis le_post post_map_acom)
+next
+  case (If b C1 C2 P)
+  then obtain D1 D2 P' where
+      "C' = IF b THEN D1 ELSE D2 {P'}"
+      "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1" "C2 \<le> \<gamma>\<^isub>c D2"
+    by (fastforce simp: If_le map_acom_If)
+  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)"
+    by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c D1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)"
+    by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c D2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
+  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` by (simp add: If.IH subset_iff)
+next
+  case (While I b C1 P)
+  then obtain D1 I' P' where
+    "C' = {I'} WHILE b DO D1 {P'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1"
+    by (fastforce simp: map_acom_While While_le)
+  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post D1)"
+    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c D1`, simplified]
+    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
+  ultimately show ?case by (simp add: While.IH subset_iff)
+qed
+
+lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
+proof(simp add: CS_def AI_def)
+  assume 1: "lpfp (step' \<top>) c = Some C"
+  have 2: "step' \<top> C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
+  have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c"
+    by(simp add: strip_lpfp[OF _ 1])
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> C)"
+  proof(rule lfp_lowerbound[simplified,OF 3])
+    show "step UNIV (\<gamma>\<^isub>c (step' \<top> C)) \<le> \<gamma>\<^isub>c (step' \<top> C)"
+    proof(rule step_preserves_le[OF _ _])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
+      show "\<gamma>\<^isub>c (step' \<top> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
+    qed
+  qed
+  with 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+    by (blast intro: mono_gamma_c order_trans)
+qed
+
+end
+
+
+subsubsection "Monotonicity"
+
+lemma mono_post: "C1 \<sqsubseteq> C2 \<Longrightarrow> post C1 \<sqsubseteq> post C2"
+by(induction C1 C2 rule: le_acom.induct) (auto)
+
+locale Abs_Int_Fun_mono = Abs_Int_Fun +
+assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+begin
+
+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 mono_step': "S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
+            split: option.split)
+done
+
+end
+
+text{* Problem: not executable because of the comparison of abstract states,
+i.e. functions, in the post-fixedpoint computation. *}
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,313 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int1
+imports Abs_State
+begin
+
+lemma le_iff_le_annos_zip: "C1 \<sqsubseteq> C2 \<longleftrightarrow>
+ (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<sqsubseteq> a2) \<and> strip C1 = strip C2"
+by(induct C1 C2 rule: le_acom.induct) (auto simp: size_annos_same2)
+
+lemma le_iff_le_annos: "C1 \<sqsubseteq> C2 \<longleftrightarrow>
+  strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<sqsubseteq> annos C2 ! i)"
+by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
+
+
+lemma mono_fun_wt[simp]: "wt F X \<Longrightarrow> F \<sqsubseteq> G \<Longrightarrow> x : X \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
+by(simp add: mono_fun wt_st_def)
+
+lemma wt_bot[simp]: "wt (bot c) (vars c)"
+by(simp add: wt_acom_def bot_def)
+
+lemma wt_acom_simps[simp]: "wt (SKIP {P}) X \<longleftrightarrow> wt P X"
+  "wt (x ::= e {P}) X \<longleftrightarrow> x : X \<and> vars e \<subseteq> X \<and> wt P X"
+  "wt (C1;C2) X \<longleftrightarrow> wt C1 X \<and> wt C2 X"
+  "wt (IF b THEN C1 ELSE C2 {P}) X \<longleftrightarrow>
+   vars b \<subseteq> X \<and> wt C1 X \<and> wt C2 X \<and> wt P X"
+  "wt ({I} WHILE b DO C {P}) X \<longleftrightarrow>
+   wt I X \<and> vars b \<subseteq> X \<and> wt C X \<and> wt P X"
+by(auto simp add: wt_acom_def)
+
+lemma wt_post[simp]: "wt c  X \<Longrightarrow> wt (post c) X"
+by(induction c)(auto simp: wt_acom_def)
+
+lemma lpfp_inv:
+assumes "lpfp f x0 = Some x" and "\<And>x. P x \<Longrightarrow> P(f x)" and "P(bot x0)"
+shows "P x"
+using assms unfolding lpfp_def pfp_def
+by (metis (lifting) while_option_rule)
+
+
+subsection "Computable Abstract Interpretation"
+
+text{* Abstract interpretation over type @{text st} instead of
+functions. *}
+
+context Gamma
+begin
+
+fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
+"aval' (N n) S = num' n" |
+"aval' (V x) S = fun S x" |
+"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+
+lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> vars a \<subseteq> dom S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
+by (induction a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def)
+
+end
+
+text{* The for-clause (here and elsewhere) only serves the purpose of fixing
+the name of the type parameter @{typ 'av} which would otherwise be renamed to
+@{typ 'a}. *}
+
+locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
+begin
+
+fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" where
+"step' S (SKIP {P}) = (SKIP {S})" |
+"step' S (x ::= e {P}) =
+  x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(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}) =
+  (IF b THEN step' S C1 ELSE step' S 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}"
+
+definition AI :: "com \<Rightarrow> 'av st option acom option" where
+"AI c = lpfp (step' (top c)) c"
+
+
+lemma strip_step'[simp]: "strip(step' S C) = strip C"
+by(induct C arbitrary: S) (simp_all add: Let_def)
+
+
+text{* Soundness: *}
+
+lemma in_gamma_update:
+  "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)"
+by(simp add: \<gamma>_st_def)
+
+theorem step_preserves_le:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; C \<le> \<gamma>\<^isub>c C';  wt C' X; wt S' X \<rbrakk> \<Longrightarrow> step S C \<le> \<gamma>\<^isub>c (step' S' C')"
+proof(induction C arbitrary: C' S S')
+  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
+next
+  case Assign thus ?case
+    by(fastforce simp: Assign_le map_acom_Assign wt_st_def
+        intro: aval'_sound in_gamma_update split: option.splits)
+next
+  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+    by (metis le_post post_map_acom wt_post)
+next
+  case (If b C1 C2 P)
+  then obtain C1' C2' P' where
+      "C' = IF b THEN C1' ELSE C2' {P'}"
+      "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'"
+    by (fastforce simp: If_le map_acom_If)
+  moreover from this(1) `wt C' X` have wt: "wt C1' X" "wt C2' X"
+    by simp_all
+  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
+    by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c C1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom wt wt_post)
+  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
+    by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c C2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom wt wt_post)
+  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` `wt S' X`
+    by (simp add: If.IH subset_iff)
+next
+  case (While I b C1 P)
+  then obtain C1' I' P' where
+    "C' = {I'} WHILE b DO C1' {P'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'"
+    by (fastforce simp: map_acom_While While_le)
+  moreover from this(1) `wt C' X`
+  have wt: "wt C1' X" "wt I' X" by simp_all
+  moreover note compat = `wt S' X` wt_post[OF wt(1)]
+  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
+    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c C1'`, simplified]
+    by (metis (no_types) join_ge1[OF compat] join_ge2[OF compat] le_sup_iff mono_gamma_o order_trans)
+  ultimately show ?case by (simp add: While.IH subset_iff)
+qed
+
+lemma wt_step'[simp]:
+  "\<lbrakk> wt C X; wt S X \<rbrakk> \<Longrightarrow> wt (step' S C) X"
+proof(induction C arbitrary: S)
+  case Assign thus ?case
+    by(auto simp: wt_st_def update_def split: option.splits)
+qed auto
+
+theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
+proof(simp add: CS_def AI_def)
+  assume 1: "lpfp (step' (top c)) c = Some C"
+  have "wt C (vars c)"
+    by(rule lpfp_inv[where P = "%C. wt C (vars c)", OF 1 _ wt_bot])
+      (erule wt_step'[OF _ wt_top])
+  have 2: "step' (top c) C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
+  have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
+    by(simp add: strip_lpfp[OF _ 1])
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' (top c) C)"
+  proof(rule lfp_lowerbound[simplified,OF 3])
+    show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
+    proof(rule step_preserves_le[OF _ _ `wt C (vars c)` wt_top])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o (top c)" by simp
+      show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
+    qed
+  qed
+  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+    by (blast intro: mono_gamma_c order_trans)
+qed
+
+end
+
+
+subsubsection "Monotonicity"
+
+lemma le_join_disj: "wt y X \<Longrightarrow> wt (z::_::SL_top_wt) X \<Longrightarrow> x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
+by (metis join_ge1 join_ge2 preord_class.le_trans)
+
+locale Abs_Int_mono = Abs_Int +
+assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+begin
+
+lemma mono_aval': "S1 \<sqsubseteq> S2 \<Longrightarrow> wt S1 X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
+by(induction e) (auto simp: le_st_def mono_plus' wt_st_def)
+
+theorem mono_step': "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> wt C1 X \<Longrightarrow> wt C2 X \<Longrightarrow>
+  S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+apply (auto simp: Let_def mono_aval' mono_post
+  le_join_disj le_join_disj[OF  wt_post wt_post]
+            split: option.split)
+done
+
+lemma mono_step'_top: "wt c (vars c0) \<Longrightarrow> wt c' (vars c0) \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' (top c0) c \<sqsubseteq> step' (top c0) c'"
+by (metis wt_top mono_step' preord_class.le_refl)
+
+end
+
+
+subsubsection "Termination"
+
+abbreviation sqless (infix "\<sqsubset>" 50) where
+"x \<sqsubset> y == x \<sqsubseteq> y \<and> \<not> y \<sqsubseteq> x"
+
+lemma pfp_termination:
+fixes x0 :: "'a::preord" and m :: "'a \<Rightarrow> nat"
+assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> m x > m y"
+and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<sqsubseteq> f x0"
+shows "EX x. pfp f x0 = Some x"
+proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<sqsubseteq> f x"])
+  show "wf {(y,x). ((I x \<and> x \<sqsubseteq> f x) \<and> \<not> f x \<sqsubseteq> x) \<and> y = f x}"
+    by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
+next
+  show "I x0 \<and> x0 \<sqsubseteq> f x0" using `I x0` `x0 \<sqsubseteq> f x0` by blast
+next
+  fix x assume "I x \<and> x \<sqsubseteq> f x" thus "I(f x) \<and> f x \<sqsubseteq> f(f x)"
+    by (blast intro: I mono)
+qed
+
+lemma lpfp_termination:
+fixes f :: "'a::preord option acom \<Rightarrow> 'a option acom"
+and m :: "'a option acom \<Rightarrow> nat" and I :: "'a option acom \<Rightarrow> bool"
+assumes "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> m x > m y"
+and "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+and "\<And>x y. I x \<Longrightarrow> I(f x)" and "I(bot c)"
+and "\<And>C. strip (f C) = strip C"
+shows "\<exists>c'. lpfp f c = Some c'"
+unfolding lpfp_def
+by(fastforce intro: pfp_termination[where I=I and m=m] assms bot_least
+   simp: assms(5))
+
+
+locale Abs_Int_measure =
+  Abs_Int_mono where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set" +
+fixes m :: "'av \<Rightarrow> nat"
+fixes h :: "nat"
+assumes m1: "x \<sqsubseteq> y \<Longrightarrow> m x \<ge> m y"
+assumes m2: "x \<sqsubset> y \<Longrightarrow> m x > m y"
+assumes h: "m x \<le> h"
+begin
+
+definition "m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
+
+lemma m_st1: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st S1 \<ge> m_st S2"
+proof(auto simp add: le_st_def m_st_def)
+  assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
+  hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
+  thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
+    by (metis setsum_mono)
+qed
+
+lemma m_st2: "finite(dom S1) \<Longrightarrow> S1 \<sqsubset> S2 \<Longrightarrow> m_st S1 > m_st S2"
+proof(auto simp add: le_st_def m_st_def)
+  assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
+  hence 1: "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
+  fix x assume "x \<in> dom S2" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
+  hence 2: "\<exists>x\<in>dom S2. m(fun S1 x) > m(fun S2 x)" using 0 m2 by blast
+  from setsum_strict_mono_ex1[OF `finite(dom S2)` 1 2]
+  show "(\<Sum>x\<in>dom S2. m (fun S2 x)) < (\<Sum>x\<in>dom S2. m (fun S1 x))" .
+qed
+
+
+definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" where
+"m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_st S)"
+
+definition m_c :: "'av st option acom \<Rightarrow> nat" where
+"m_c c = (\<Sum>i<size(annos c). m_o (card(vars(strip c))) (annos c ! i))"
+
+lemma m_st_h: "wt x X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
+by(simp add: wt_st_def m_st_def)
+  (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
+
+lemma m_o1: "finite X \<Longrightarrow> wt o1 X \<Longrightarrow> wt o2 X \<Longrightarrow>
+  o1 \<sqsubseteq> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
+proof(induction o1 o2 rule: le_option.induct)
+  case 1 thus ?case by (simp add: m_o_def)(metis m_st1)
+next
+  case 2 thus ?case
+    by(simp add: wt_option_def m_o_def le_SucI m_st_h split: option.splits)
+next
+  case 3 thus ?case by simp
+qed
+
+lemma m_o2: "finite X \<Longrightarrow> wt o1 X \<Longrightarrow> wt o2 X \<Longrightarrow>
+  o1 \<sqsubset> o2 \<Longrightarrow> m_o (card X) o1 > m_o (card X) o2"
+proof(induction o1 o2 rule: le_option.induct)
+  case 1 thus ?case by (simp add: m_o_def wt_st_def m_st2)
+next
+  case 2 thus ?case
+    by(auto simp add: m_o_def le_imp_less_Suc m_st_h)
+next
+  case 3 thus ?case by simp
+qed
+
+lemma m_c2: "wt c1 (vars(strip c1)) \<Longrightarrow> wt c2 (vars(strip c2)) \<Longrightarrow>
+  c1 \<sqsubset> c2 \<Longrightarrow> m_c c1 > m_c c2"
+proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of c1 c2] wt_acom_def)
+  let ?X = "vars(strip c2)"
+  let ?n = "card ?X"
+  assume V1: "\<forall>a\<in>set(annos c1). wt a ?X"
+    and V2: "\<forall>a\<in>set(annos c2). wt a ?X"
+    and strip_eq: "strip c1 = strip c2"
+    and 0: "\<forall>i<size(annos c2). annos c1 ! i \<sqsubseteq> annos c2 ! i"
+  hence 1: "\<forall>i<size(annos c2). m_o ?n (annos c1 ! i) \<ge> m_o ?n (annos c2 ! i)"
+    by (auto simp: all_set_conv_all_nth)
+       (metis finite_cvars m_o1 size_annos_same2)
+  fix i assume "i < size(annos c2)" "\<not> annos c2 ! i \<sqsubseteq> annos c1 ! i"
+  hence "m_o ?n (annos c1 ! i) > m_o ?n (annos c2 ! i)" (is "?P i")
+    by(metis m_o2[OF finite_cvars] V1 V2 strip_eq nth_mem size_annos_same 0)
+  hence 2: "\<exists>i < size(annos c2). ?P i" using `i < size(annos c2)` by blast
+  show "(\<Sum>i<size(annos c2). m_o ?n (annos c2 ! i))
+         < (\<Sum>i<size(annos c2). m_o ?n (annos c1 ! i))"
+    apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
+qed
+
+lemma AI_Some_measure: "\<exists>C. AI c = Some C"
+unfolding AI_def
+apply(rule lpfp_termination[where I = "%C. strip C = c \<and> wt C (vars c)"
+  and m="m_c"])
+apply(simp_all add: m_c2 mono_step'_top)
+done
+
+end
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int1_const.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,143 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int1_const
+imports Abs_Int1
+begin
+
+subsection "Constant Propagation"
+
+datatype const = Const val | Any
+
+fun \<gamma>_const where
+"\<gamma>_const (Const n) = {n}" |
+"\<gamma>_const (Any) = UNIV"
+
+fun plus_const where
+"plus_const (Const m) (Const n) = Const(m+n)" |
+"plus_const _ _ = Any"
+
+lemma plus_const_cases: "plus_const a1 a2 =
+  (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
+by(auto split: prod.split const.split)
+
+instantiation const :: SL_top
+begin
+
+fun le_const where
+"_ \<sqsubseteq> Any = True" |
+"Const n \<sqsubseteq> Const m = (n=m)" |
+"Any \<sqsubseteq> Const _ = False"
+
+fun join_const 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_const_def)
+qed
+
+end
+
+
+interpretation Val_abs
+where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
+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_const_def)
+next
+  case goal3 show ?case by simp
+next
+  case goal4 thus ?case
+    by(auto simp: plus_const_cases split: const.split)
+qed
+
+interpretation Abs_Int
+where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
+defines AI_const is AI and step_const is step' and aval'_const is aval'
+..
+
+
+subsubsection "Tests"
+
+definition "steps c i = (step_const(top c) ^^ i) (bot c)"
+
+value "show_acom (steps test1_const 0)"
+value "show_acom (steps test1_const 1)"
+value "show_acom (steps test1_const 2)"
+value "show_acom (steps test1_const 3)"
+value "show_acom_opt (AI_const test1_const)"
+
+value "show_acom_opt (AI_const test2_const)"
+value "show_acom_opt (AI_const test3_const)"
+
+value "show_acom (steps test4_const 0)"
+value "show_acom (steps test4_const 1)"
+value "show_acom (steps test4_const 2)"
+value "show_acom (steps test4_const 3)"
+value "show_acom_opt (AI_const test4_const)"
+
+value "show_acom (steps test5_const 0)"
+value "show_acom (steps test5_const 1)"
+value "show_acom (steps test5_const 2)"
+value "show_acom (steps test5_const 3)"
+value "show_acom (steps test5_const 4)"
+value "show_acom (steps test5_const 5)"
+value "show_acom_opt (AI_const test5_const)"
+
+value "show_acom (steps test6_const 0)"
+value "show_acom (steps test6_const 1)"
+value "show_acom (steps test6_const 2)"
+value "show_acom (steps test6_const 3)"
+value "show_acom (steps test6_const 4)"
+value "show_acom (steps test6_const 5)"
+value "show_acom (steps test6_const 6)"
+value "show_acom (steps test6_const 7)"
+value "show_acom (steps test6_const 8)"
+value "show_acom (steps test6_const 9)"
+value "show_acom (steps test6_const 10)"
+value "show_acom (steps test6_const 11)"
+value "show_acom_opt (AI_const test6_const)"
+
+
+text{* Monotonicity: *}
+
+interpretation Abs_Int_mono
+where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
+proof
+  case goal1 thus ?case
+    by(auto simp: plus_const_cases split: const.split)
+qed
+
+text{* Termination: *}
+
+definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
+
+interpretation Abs_Int_measure
+where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
+and m = m_const and h = "2"
+proof
+  case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
+next
+  case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
+next
+  case goal3 thus ?case by(auto simp: m_const_def split: const.splits)
+qed
+
+thm AI_Some_measure
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int1_parity.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,169 @@
+theory Abs_Int1_parity
+imports Abs_Int1
+begin
+
+subsection "Parity Analysis"
+
+datatype parity = Even | Odd | Either
+
+text{* Instantiation of class @{class preord} with type @{typ parity}: *}
+
+instantiation parity :: preord
+begin
+
+text{* First the definition of the interface function @{text"\<sqsubseteq>"}. Note that
+the header of the definition must refer to the ascii name @{const le} of the
+constants as @{text le_parity} and the definition is named @{text
+le_parity_def}.  Inside the definition the symbolic names can be used. *}
+
+definition le_parity where
+"x \<sqsubseteq> y = (y = Either \<or> x=y)"
+
+text{* Now the instance proof, i.e.\ the proof that the definition fulfills
+the axioms (assumptions) of the class. The initial proof-step generates the
+necessary proof obligations. *}
+
+instance
+proof
+  fix x::parity show "x \<sqsubseteq> x" by(auto simp: le_parity_def)
+next
+  fix x y z :: parity assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+    by(auto simp: le_parity_def)
+qed
+
+end
+
+text{* Instantiation of class @{class SL_top} with type @{typ parity}: *}
+
+instantiation parity :: SL_top
+begin
+
+definition join_parity where
+"x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)"
+
+definition Top_parity where
+"\<top> = Either"
+
+text{* Now the instance proof. This time we take a lazy shortcut: we do not
+write out the proof obligations but use the @{text goali} primitive to refer
+to the assumptions of subgoal i and @{text "case?"} to refer to the
+conclusion of subgoal i. The class axioms are presented in the same order as
+in the class definition. *}
+
+instance
+proof
+  case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def)
+next
+  case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def)
+next
+  case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def)
+next
+  case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def)
+qed
+
+end
+
+
+text{* Now we define the functions used for instantiating the abstract
+interpretation locales. Note that the Isabelle terminology is
+\emph{interpretation}, not \emph{instantiation} of locales, but we use
+instantiation to avoid confusion with abstract interpretation.  *}
+
+fun \<gamma>_parity :: "parity \<Rightarrow> val set" where
+"\<gamma>_parity Even = {i. i mod 2 = 0}" |
+"\<gamma>_parity Odd  = {i. i mod 2 = 1}" |
+"\<gamma>_parity Either = UNIV"
+
+fun num_parity :: "val \<Rightarrow> parity" where
+"num_parity i = (if i mod 2 = 0 then Even else Odd)"
+
+fun plus_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where
+"plus_parity Even Even = Even" |
+"plus_parity Odd  Odd  = Even" |
+"plus_parity Even Odd  = Odd" |
+"plus_parity Odd  Even = Odd" |
+"plus_parity Either y  = Either" |
+"plus_parity x Either  = Either"
+
+text{* First we instantiate the abstract value interface and prove that the
+functions on type @{typ parity} have all the necessary properties: *}
+
+interpretation Val_abs
+where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
+proof txt{* of the locale axioms *}
+  fix a b :: parity
+  assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
+    by(auto simp: le_parity_def)
+next txt{* The rest in the lazy, implicit way *}
+  case goal2 show ?case by(auto simp: Top_parity_def)
+next
+  case goal3 show ?case by auto
+next
+  txt{* Warning: this subproof refers to the names @{text a1} and @{text a2}
+  from the statement of the axiom. *}
+  case goal4 thus ?case
+  proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust])
+  qed (auto simp add:mod_add_eq)
+qed
+
+text{* Instantiating the abstract interpretation locale requires no more
+proofs (they happened in the instatiation above) but delivers the
+instantiated abstract interpreter which we call AI: *}
+
+interpretation Abs_Int
+where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
+defines aval_parity is aval' and step_parity is step' and AI_parity is AI
+..
+
+
+subsubsection "Tests"
+
+definition "test1_parity =
+  ''x'' ::= N 1;
+  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
+
+value "show_acom_opt (AI_parity test1_parity)"
+
+definition "test2_parity =
+  ''x'' ::= N 1;
+  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
+
+definition "steps c i = (step_parity(top c) ^^ i) (bot c)"
+
+value "show_acom (steps test2_parity 0)"
+value "show_acom (steps test2_parity 1)"
+value "show_acom (steps test2_parity 2)"
+value "show_acom (steps test2_parity 3)"
+value "show_acom (steps test2_parity 4)"
+value "show_acom (steps test2_parity 5)"
+value "show_acom_opt (AI_parity test2_parity)"
+
+
+subsubsection "Termination"
+
+interpretation Abs_Int_mono
+where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
+proof
+  case goal1 thus ?case
+  proof(cases a1 a2 b1 b2
+   rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
+  qed (auto simp add:le_parity_def)
+qed
+
+definition m_parity :: "parity \<Rightarrow> nat" where
+"m_parity x = (if x=Either then 0 else 1)"
+
+interpretation Abs_Int_measure
+where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
+and m = m_parity and h = "2"
+proof
+  case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
+next
+  case goal2 thus ?case by(auto simp add: m_parity_def le_parity_def)
+next
+  case goal3 thus ?case by(auto simp add: m_parity_def le_parity_def)
+qed
+
+thm AI_Some_measure
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,312 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int2
+imports Abs_Int1
+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"
+
+class L_top_bot = SL_top + Bot +
+fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
+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"
+begin
+
+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_gamma =
+  Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
+assumes inter_gamma_subset_gamma_meet:
+  "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
+and gamma_Bot[simp]: "\<gamma> \<bottom> = {}"
+begin
+
+lemma in_gamma_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
+by (metis IntI inter_gamma_subset_gamma_meet set_mp)
+
+lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2)
+
+end
+
+
+locale Val_abs1 =
+  Val_abs1_gamma where \<gamma> = \<gamma>
+   for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
+fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
+and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
+and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
+assumes test_num': "test_num' n a = (n : \<gamma> a)"
+and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
+  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
+and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
+  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
+
+
+locale Abs_Int1 =
+  Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set"
+begin
+
+lemma in_gamma_join_UpI:
+  "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
+by (metis (hide_lams, no_types) SL_top_wt_class.join_ge1 SL_top_wt_class.join_ge2 mono_gamma_o subsetD)
+
+fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
+"aval'' e None = \<bottom>" |
+"aval'' e (Some sa) = aval' e sa"
+
+lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> wt S X \<Longrightarrow> vars a \<subseteq> X \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
+by(simp add: wt_option_def wt_st_def aval'_sound split: option.splits)
+
+subsubsection "Backward analysis"
+
+fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
+"afilter (N n) a S = (if test_num' n a then S else None)" |
+"afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
+  let a' = fun S x \<sqinter> a in
+  if a' \<sqsubseteq> \<bottom> then None else Some(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 None}. Put differently, we maintain the invariant that in an abstract
+state of the form @{term"Some s"}, 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> 'av st option \<Rightarrow> 'av st option" where
+"bfilter (Bc v) res S = (if v=res then S else None)" |
+"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 wt_afilter: "wt S X \<Longrightarrow> vars e \<subseteq> X ==> wt (afilter e a S) X"
+by(induction e arbitrary: a S)
+  (auto simp: Let_def update_def wt_st_def
+           split: option.splits prod.split)
+
+lemma afilter_sound: "wt S X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
+  s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
+proof(induction e arbitrary: a S)
+  case N thus ?case by simp (metis test_num')
+next
+  case (V x)
+  obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>o S`
+    by(auto simp: in_gamma_option_iff)
+  moreover hence "s x : \<gamma> (fun S' x)"
+    using V(1,2) by(simp add: \<gamma>_st_def wt_st_def)
+  moreover have "s x : \<gamma> a" using V by simp
+  ultimately show ?case using V(3)
+    by(simp add: Let_def \<gamma>_st_def)
+      (metis mono_gamma emptyE in_gamma_meet gamma_Bot subset_empty)
+next
+  case (Plus e1 e2) thus ?case
+    using filter_plus'[OF _ aval''_sound[OF Plus.prems(3)] aval''_sound[OF Plus.prems(3)]]
+    by (auto simp: wt_afilter split: prod.split)
+qed
+
+lemma wt_bfilter: "wt S X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> wt (bfilter b bv S) X"
+by(induction b arbitrary: bv S)
+  (auto simp: wt_afilter split: prod.split)
+
+lemma bfilter_sound: "wt S X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
+  s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)"
+proof(induction b arbitrary: S bv)
+  case Bc thus ?case by simp
+next
+  case (Not b) thus ?case by simp
+next
+  case (And b1 b2) thus ?case
+    by simp (metis And(1) And(2) wt_bfilter in_gamma_join_UpI)
+next
+  case (Less e1 e2) thus ?case
+    by(auto split: prod.split)
+      (metis (lifting) wt_afilter afilter_sound aval''_sound filter_less')
+qed
+
+
+fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom"
+ where
+"step' S (SKIP {P}) = (SKIP {S})" |
+"step' S (x ::= e {P}) =
+  x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(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 D1 = step' (bfilter b True S) C1; D2 = step' (bfilter b False S) C2
+   in IF b THEN D1 ELSE D2 {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}"
+
+definition AI :: "com \<Rightarrow> 'av st option acom option" where
+"AI c = lpfp (step' \<top>\<^bsub>c\<^esub>) c"
+
+lemma strip_step'[simp]: "strip(step' S c) = strip c"
+by(induct c arbitrary: S) (simp_all add: Let_def)
+
+
+subsubsection "Soundness"
+
+lemma in_gamma_update:
+  "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)"
+by(simp add: \<gamma>_st_def)
+
+theorem step_preserves_le:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; C \<le> \<gamma>\<^isub>c C'; wt C' X; wt S' X \<rbrakk> \<Longrightarrow> step S C \<le> \<gamma>\<^isub>c (step' S' C')"
+proof(induction C arbitrary: C' S S')
+  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
+next
+  case Assign thus ?case
+    by (fastforce simp: Assign_le map_acom_Assign wt_option_def wt_st_def
+        intro: aval'_sound in_gamma_update  split: option.splits del:subsetD)
+next
+  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+    by (metis le_post post_map_acom wt_post)
+next
+  case (If b C1 C2 P)
+  then obtain C1' C2' P' where
+      "C' = IF b THEN C1' ELSE C2' {P'}"
+      "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'"
+    by (fastforce simp: If_le map_acom_If)
+  moreover from this(1) `wt C' X` have wt: "wt C1' X" "wt C2' X"
+    and "vars b \<subseteq> X" by simp_all
+  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
+    by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c C1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom wt_post wt)
+  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
+    by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c C2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom wt_post wt)
+  moreover note vars = `wt S' X` `vars b \<subseteq> X`
+  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'`
+    by (simp add: If.IH subset_iff bfilter_sound[OF vars] wt_bfilter[OF vars])
+next
+  case (While I b C1 P)
+  then obtain C1' I' P' where
+    "C' = {I'} WHILE b DO C1' {P'}"
+    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c C1'"
+    by (fastforce simp: map_acom_While While_le)
+  moreover from this(1) `wt C' X`
+  have wt: "wt C1' X" "wt I' X" and "vars b \<subseteq> X" by simp_all
+  moreover note compat = `wt S' X` wt_post[OF wt(1)]
+  moreover note vars = `wt I' X` `vars b \<subseteq> X`
+  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
+    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c C1'`, simplified]
+    by (metis (no_types) join_ge1[OF compat] join_ge2[OF compat] le_sup_iff mono_gamma_o order_trans)
+  ultimately show ?case
+    by (simp add: While.IH subset_iff bfilter_sound[OF vars] wt_bfilter[OF vars])
+qed
+
+lemma wt_step'[simp]:
+  "\<lbrakk> wt C X; wt S X \<rbrakk> \<Longrightarrow> wt (step' S C) X"
+proof(induction C arbitrary: S)
+  case Assign thus ?case by(simp add: wt_option_def wt_st_def update_def split: option.splits)
+qed (auto simp add: wt_bfilter)
+
+theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
+proof(simp add: CS_def AI_def)
+  assume 1: "lpfp (step' (top c)) c = Some C"
+  have "wt C (vars c)"
+    by(rule lpfp_inv[where P = "%C. wt C (vars c)", OF 1 _ wt_bot])
+      (erule wt_step'[OF _ wt_top])
+  have 2: "step' (top c) C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
+  have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
+    by(simp add: strip_lpfp[OF _ 1])
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' (top c) C)"
+  proof(rule lfp_lowerbound[simplified,OF 3])
+    show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
+    proof(rule step_preserves_le[OF _ _ `wt C (vars c)` wt_top])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o (top c)" by simp
+      show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
+    qed
+  qed
+  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+    by (blast intro: mono_gamma_c order_trans)
+qed
+
+end
+
+
+subsubsection "Monotonicity"
+
+locale Abs_Int1_mono = Abs_Int1 +
+assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+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"
+begin
+
+lemma mono_aval':
+  "S1 \<sqsubseteq> S2 \<Longrightarrow> wt S1 X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
+by(induction e) (auto simp: le_st_def mono_plus' wt_st_def)
+
+lemma mono_aval'':
+  "S1 \<sqsubseteq> S2 \<Longrightarrow> wt S1 X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<sqsubseteq> aval'' e S2"
+apply(cases S1)
+ apply simp
+apply(cases S2)
+ apply simp
+by (simp add: mono_aval')
+
+lemma mono_afilter: "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
+  r1 \<sqsubseteq> r2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> afilter e r1 S1 \<sqsubseteq> afilter e r2 S2"
+apply(induction e arbitrary: r1 r2 S1 S2)
+apply(auto simp: test_num' Let_def mono_meet split: option.splits prod.splits)
+apply (metis mono_gamma subsetD)
+apply(drule (2) mono_fun_wt)
+apply (metis mono_meet le_trans)
+apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv wt_afilter)
+done
+
+lemma mono_bfilter: "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
+  S1 \<sqsubseteq> S2 \<Longrightarrow> bfilter b bv S1 \<sqsubseteq> bfilter b bv S2"
+apply(induction b arbitrary: bv S1 S2)
+apply(simp)
+apply(simp)
+apply simp
+apply(metis join_least le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] wt_bfilter)
+apply (simp split: prod.splits)
+apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv wt_afilter)
+done
+
+theorem mono_step': "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> wt C1 X \<Longrightarrow> wt C2 X \<Longrightarrow>
+  S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
+  le_join_disj le_join_disj[OF  wt_post wt_post] wt_bfilter
+            split: option.split)
+done
+
+lemma mono_step'_top: "wt C1 (vars c) \<Longrightarrow> wt C2 (vars c) \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top c) C1 \<sqsubseteq> step' (top c) C2"
+by (metis wt_top mono_step' preord_class.le_refl)
+
+end
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int2_ivl.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,288 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int2_ivl
+imports Abs_Int2
+begin
+
+subsection "Interval Analysis"
+
+datatype ivl = I "int option" "int option"
+
+definition "\<gamma>_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)"
+
+abbreviation I_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
+"{lo\<dots>hi} == I (Some lo) (Some hi)"
+abbreviation I_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
+"{lo\<dots>} == I (Some lo) None"
+abbreviation I_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
+"{\<dots>hi} == I None (Some hi)"
+abbreviation I_None_None :: "ivl"  ("{\<dots>}") where
+"{\<dots>} == I None None"
+
+definition "num_ivl n = {n\<dots>n}"
+
+fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
+"in_ivl k (I (Some l) (Some h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
+"in_ivl k (I (Some l) None) \<longleftrightarrow> l \<le> k" |
+"in_ivl k (I None (Some h)) \<longleftrightarrow> k \<le> h" |
+"in_ivl k (I None None) \<longleftrightarrow> True"
+
+instantiation option :: (plus)plus
+begin
+
+fun plus_option where
+"Some x + Some y = Some(x+y)" |
+"_ + _ = None"
+
+instance ..
+
+end
+
+definition empty where "empty = {1\<dots>0}"
+
+fun is_empty where
+"is_empty {l\<dots>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> \<gamma>_ivl i = {}"
+by(auto simp add: \<gamma>_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> = {\<dots>}"
+
+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 goal2 thus ?case
+    by (simp add:meet_ivl_def empty_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+  case goal3 thus ?case
+    by (simp add: empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+next
+  case goal4 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 goal1 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 ..
+
+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 gamma_minus_ivl:
+  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
+by(auto simp add: minus_ivl_def \<gamma>_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 Val_abs
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+proof
+  case goal1 thus ?case
+    by(auto simp: \<gamma>_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
+next
+  case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
+next
+  case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
+next
+  case goal4 thus ?case
+    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
+qed
+
+interpretation Val_abs1_gamma
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+defines aval_ivl is aval'
+proof
+  case goal1 thus ?case
+    by(auto simp add: \<gamma>_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 \<gamma>_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
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = in_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
+proof
+  case goal1 thus ?case
+    by (simp add: \<gamma>_ivl_def split: ivl.split option.split)
+next
+  case goal2 thus ?case
+    by(auto simp add: filter_plus_ivl_def)
+      (metis gamma_minus_ivl add_diff_cancel add_commute)+
+next
+  case goal3 thus ?case
+    by(cases a1, cases a2,
+      auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
+qed
+
+interpretation Abs_Int1
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = in_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
+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''
+..
+
+
+text{* Monotonicity: *}
+
+interpretation Abs_Int1_mono
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = in_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
+proof
+  case goal1 thus ?case
+    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
+next
+  case goal2 thus ?case
+    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
+next
+  case goal3 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
+
+
+subsubsection "Tests"
+
+value "show_acom_opt (AI_ivl test1_ivl)"
+
+text{* Better than @{text AI_const}: *}
+value "show_acom_opt (AI_ivl test3_const)"
+value "show_acom_opt (AI_ivl test4_const)"
+value "show_acom_opt (AI_ivl test6_const)"
+
+definition "steps c i = (step_ivl(top c) ^^ i) (bot c)"
+
+value "show_acom_opt (AI_ivl test2_ivl)"
+value "show_acom (steps test2_ivl 0)"
+value "show_acom (steps test2_ivl 1)"
+value "show_acom (steps test2_ivl 2)"
+
+text{* Fixed point reached in 2 steps.
+ Not so if the start value of x is known: *}
+
+value "show_acom_opt (AI_ivl test3_ivl)"
+value "show_acom (steps test3_ivl 0)"
+value "show_acom (steps test3_ivl 1)"
+value "show_acom (steps test3_ivl 2)"
+value "show_acom (steps test3_ivl 3)"
+value "show_acom (steps test3_ivl 4)"
+
+text{* Takes as many iterations as the actual execution. Would diverge if
+loop did not terminate. Worse still, as the following example shows: even if
+the actual execution terminates, the analysis may not. The value of y keeps
+decreasing as the analysis is iterated, no matter how long: *}
+
+value "show_acom (steps test4_ivl 50)"
+
+text{* Relationships between variables are NOT captured: *}
+value "show_acom_opt (AI_ivl test5_ivl)"
+
+text{* Again, the analysis would not terminate: *}
+value "show_acom (steps test6_ivl 50)"
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int3.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,683 @@
+(* Author: Tobias Nipkow *)
+
+theory Abs_Int3
+imports Abs_Int2_ivl
+begin
+
+subsubsection "Welltypedness"
+
+class Wt =
+fixes Wt :: "'a \<Rightarrow> com \<Rightarrow> bool"
+
+instantiation st :: (type)Wt
+begin
+
+definition Wt_st :: "'a st \<Rightarrow> com \<Rightarrow> bool" where
+"Wt_st S c = wt S (vars c)"
+
+instance ..
+
+end
+
+instantiation acom :: (Wt)Wt
+begin
+
+definition Wt_acom :: "'a acom \<Rightarrow> com \<Rightarrow> bool" where
+"Wt C c = (strip C = c \<and> (\<forall>a\<in>set(annos C). Wt a c))"
+
+instance ..
+
+end
+
+instantiation option :: (Wt)Wt
+begin
+
+fun Wt_option :: "'a option \<Rightarrow> com \<Rightarrow> bool" where
+"Wt None c = True" |
+"Wt (Some x) c = Wt x c"
+
+instance ..
+
+end
+
+lemma Wt_option_iff_wt[simp]: fixes a :: "_ st option"
+shows "Wt a c = wt a (vars c)"
+by(auto simp add: wt_option_def Wt_st_def split: option.splits)
+
+
+context Abs_Int1
+begin
+
+lemma Wt_step': "Wt C c \<Longrightarrow> Wt S c \<Longrightarrow> Wt (step' S C) c"
+apply(auto simp add: Wt_acom_def)
+by (metis wt_acom_def wt_step' order_refl)
+
+end
+
+
+subsection "Widening and Narrowing"
+
+class widen =
+fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
+
+class narrow =
+fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
+
+class WN = widen + narrow + preord +
+assumes widen1: "x \<sqsubseteq> x \<nabla> y"
+assumes widen2: "y \<sqsubseteq> x \<nabla> y"
+assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
+assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+
+class WN_Wt = widen + narrow + preord + Wt +
+assumes widen1: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
+assumes widen2: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
+assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
+assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+assumes Wt_widen[simp]: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> Wt (x \<nabla> y) c"
+assumes Wt_narrow[simp]: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> Wt (x \<triangle> y) c"
+
+
+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_Wt
+begin
+
+definition "widen_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
+
+definition "narrow_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
+
+instance
+proof
+  case goal1 thus ?case
+    by(simp add: widen_st_def le_st_def WN_class.widen1)
+next
+  case goal2 thus ?case
+    by(simp add: widen_st_def le_st_def WN_class.widen2 Wt_st_def wt_st_def)
+next
+  case goal3 thus ?case
+    by(auto simp: narrow_st_def le_st_def WN_class.narrow1)
+next
+  case goal4 thus ?case
+    by(auto simp: narrow_st_def le_st_def WN_class.narrow2)
+next
+  case goal5 thus ?case by(auto simp: widen_st_def Wt_st_def wt_st_def)
+next
+  case goal6 thus ?case by(auto simp: narrow_st_def Wt_st_def wt_st_def)
+qed
+
+end
+
+
+instantiation option :: (WN_Wt)WN_Wt
+begin
+
+fun widen_option where
+"None \<nabla> x = x" |
+"x \<nabla> None = x" |
+"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
+
+fun narrow_option where
+"None \<triangle> x = None" |
+"x \<triangle> None = None" |
+"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
+
+instance
+proof
+  case goal1 thus ?case
+    by(induct x y rule: widen_option.induct)(simp_all add: widen1)
+next
+  case goal2 thus ?case
+    by(induct x y rule: widen_option.induct)(simp_all add: widen2)
+next
+  case goal3 thus ?case
+    by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
+next
+  case goal4 thus ?case
+    by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
+next
+  case goal5 thus ?case
+    by(induction x y rule: widen_option.induct)(auto simp: Wt_st_def)
+next
+  case goal6 thus ?case
+    by(induction x y rule: narrow_option.induct)(auto simp: Wt_st_def)
+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) (D1;D2) = (map2_acom f C1 D1; map2_acom f C2 D2)" |
+"map2_acom f (IF b THEN C1 ELSE C2 {a1}) (IF b' THEN D1 ELSE D2 {a2}) =
+  (IF b THEN map2_acom f C1 D1 ELSE map2_acom f C2 D2 {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})"
+
+instantiation acom :: (WN_Wt)WN_Wt
+begin
+
+definition "widen_acom = map2_acom (op \<nabla>)"
+
+definition "narrow_acom = map2_acom (op \<triangle>)"
+
+lemma widen_acom1:
+  "\<lbrakk>\<forall>a\<in>set(annos x). Wt a c; \<forall>a\<in>set (annos y). Wt a c; strip x = strip y\<rbrakk>
+   \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
+by(induct x y rule: le_acom.induct)
+  (auto simp: widen_acom_def widen1 Wt_acom_def)
+
+lemma widen_acom2:
+  "\<lbrakk>\<forall>a\<in>set(annos x). Wt a c; \<forall>a\<in>set (annos y). Wt a c; strip x = strip y\<rbrakk>
+   \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
+by(induct x y rule: le_acom.induct)
+  (auto simp: widen_acom_def widen2 Wt_acom_def)
+
+lemma strip_map2_acom[simp]:
+ "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_widen_acom[simp]:
+  "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1"
+by(simp add: widen_acom_def strip_map2_acom)
+
+lemma strip_narrow_acom[simp]:
+  "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1"
+by(simp add: narrow_acom_def strip_map2_acom)
+
+lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
+  annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
+by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2)
+
+instance
+proof
+  case goal1 thus ?case by(auto simp: Wt_acom_def widen_acom1)
+next
+  case goal2 thus ?case by(auto simp: Wt_acom_def widen_acom2)
+next
+  case goal3 thus ?case
+    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow1)
+next
+  case goal4 thus ?case
+    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow2)
+next
+  case goal5 thus ?case
+    by(auto simp: Wt_acom_def widen_acom_def split_conv elim!: in_set_zipE)
+next
+  case goal6 thus ?case
+    by(auto simp: Wt_acom_def narrow_acom_def split_conv elim!: in_set_zipE)
+qed
+
+end
+
+lemma wt_widen_o[simp]: fixes x1 x2 :: "_ st option"
+shows "wt x1 X \<Longrightarrow> wt x2 X \<Longrightarrow> wt (x1 \<nabla> x2) X"
+by(induction x1 x2 rule: widen_option.induct)
+  (simp_all add: widen_st_def wt_st_def)
+
+lemma wt_narrow_o[simp]: fixes x1 x2 :: "_ st option"
+shows "wt x1 X \<Longrightarrow> wt x2 X \<Longrightarrow> wt (x1 \<triangle> x2) X"
+by(induction x1 x2 rule: narrow_option.induct)
+  (simp_all add: narrow_st_def wt_st_def)
+
+lemma wt_widen_c: fixes C1 C2 :: "_ st option acom"
+shows "strip C1 = strip C2 \<Longrightarrow> wt C1 X \<Longrightarrow> wt C2 X \<Longrightarrow> wt (C1 \<nabla> C2) X"
+by(induction C1 C2 rule: le_acom.induct)
+  (auto simp: widen_acom_def)
+
+lemma wt_narrow_c: fixes C1 C2 :: "_ st option acom"
+shows "strip C1 = strip C2 \<Longrightarrow> wt C1 X \<Longrightarrow> wt C2 X \<Longrightarrow> wt (C1 \<triangle> C2) X"
+by(induction C1 C2 rule: le_acom.induct)
+  (auto simp: narrow_acom_def)
+
+lemma Wt_bot[simp]: "Wt (bot c) c"
+by(simp add: Wt_acom_def bot_def)
+
+
+subsubsection "Post-fixed point computation"
+
+definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,widen})option"
+where "iter_widen f = while_option (\<lambda>c. \<not> f c \<sqsubseteq> c) (\<lambda>c. c \<nabla> f c)"
+
+definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,narrow})option"
+where "iter_narrow f = while_option (\<lambda>c. \<not> c \<sqsubseteq> c \<triangle> f c) (\<lambda>c. c \<triangle> f c)"
+
+definition pfp_wn :: "(('a::WN_Wt option acom) \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
+where "pfp_wn f c =
+  (case iter_widen f (bot c) of None \<Rightarrow> None | Some c' \<Rightarrow> iter_narrow f c')"
+
+
+lemma iter_widen_pfp: "iter_widen f c = Some c' \<Longrightarrow> f c' \<sqsubseteq> c'"
+by(auto simp add: iter_widen_def dest: while_option_stop)
+
+lemma iter_widen_inv:
+assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x"
+and "iter_widen f x = Some y" shows "P y"
+using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]]
+by (blast intro: assms(1-3))
+
+lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
+assumes "\<forall>C. strip (f C) = strip C" and "while_option P f C = Some C'"
+shows "strip C' = strip C"
+using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
+by (metis assms(1))
+
+lemma strip_iter_widen: fixes f :: "'a::WN_Wt acom \<Rightarrow> 'a acom"
+assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
+shows "strip C' = strip C"
+proof-
+  have "\<forall>C. strip(C \<nabla> f C) = strip C"
+    by (metis assms(1) strip_map2_acom widen_acom_def)
+  from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
+qed
+
+lemma iter_narrow_pfp:
+assumes mono: "!!c1 c2::_::WN_Wt. P c1 \<Longrightarrow>  P c2 \<Longrightarrow> c1 \<sqsubseteq> c2 \<Longrightarrow> f c1 \<sqsubseteq> f c2"
+and Pinv: "!!c. P c \<Longrightarrow> P(f c)" "!!c1 c2. P c1 \<Longrightarrow> P c2 \<Longrightarrow> P(c1 \<triangle> c2)" and "P c0"
+and "f c0 \<sqsubseteq> c0" and "iter_narrow f c0 = Some c"
+shows "P c \<and> f c \<sqsubseteq> c"
+proof-
+  let ?Q = "%c. P c \<and> f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0"
+  { fix c assume "?Q c"
+    note P = conjunct1[OF this] and 12 = conjunct2[OF this]
+    note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
+    let ?c' = "c \<triangle> f c"
+    have "?Q ?c'"
+    proof auto
+      show "P ?c'" by (blast intro: P Pinv)
+      have "f ?c' \<sqsubseteq> f c" by(rule mono[OF `P (c \<triangle> f c)`  P narrow2[OF 1]])
+      also have "\<dots> \<sqsubseteq> ?c'" by(rule narrow1[OF 1])
+      finally show "f ?c' \<sqsubseteq> ?c'" .
+      have "?c' \<sqsubseteq> c" by (rule narrow2[OF 1])
+      also have "c \<sqsubseteq> c0" by(rule 2)
+      finally show "?c' \<sqsubseteq> c0" .
+    qed
+  }
+  thus ?thesis
+    using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
+    by (blast intro: assms(4,5) le_refl)
+qed
+
+lemma pfp_wn_pfp:
+assumes mono: "!!c1 c2::_::WN_Wt option acom. P c1 \<Longrightarrow>  P c2 \<Longrightarrow> c1 \<sqsubseteq> c2 \<Longrightarrow> f c1 \<sqsubseteq> f c2"
+and Pinv: "P (bot c)"  "!!c. P c \<Longrightarrow> P(f c)"
+  "!!c1 c2. P c1 \<Longrightarrow> P c2 \<Longrightarrow> P(c1 \<nabla> c2)"
+  "!!c1 c2. P c1 \<Longrightarrow> P c2 \<Longrightarrow> P(c1 \<triangle> c2)"
+and pfp_wn: "pfp_wn f c = Some c'" shows "P c' \<and> f c' \<sqsubseteq> c'"
+proof-
+  from pfp_wn obtain p
+    where its: "iter_widen f (bot c) = Some p" "iter_narrow f p = Some c'"
+    by(auto simp: pfp_wn_def split: option.splits)
+  have "P p" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
+  thus ?thesis
+    by - (assumption |
+          rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+
+qed
+
+lemma strip_pfp_wn:
+  "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
+by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
+  (metis (no_types) narrow_acom_def strip_bot strip_iter_widen strip_map2_acom strip_while)
+
+
+locale Abs_Int2 = Abs_Int1_mono
+where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"
+begin
+
+definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
+"AI_wn c = pfp_wn (step' (top c)) c"
+
+lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
+proof(simp add: CS_def AI_wn_def)
+  assume 1: "pfp_wn (step' (top c)) c = Some C"
+  have 2: "(strip C = c & wt C (vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
+    by(rule pfp_wn_pfp[where c=c])
+      (simp_all add: 1 mono_step'_top wt_widen_c wt_narrow_c)
+  have 3: "strip (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) = c" by(simp add: strip_pfp_wn[OF _ 1])
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
+  proof(rule lfp_lowerbound[simplified,OF 3])
+    show "step UNIV (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
+    proof(rule step_preserves_le[OF _ _ _ wt_top])
+      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>\<^bsub>c\<^esub>" by simp
+      show "\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF conjunct2[OF 2]])
+      show "wt C (vars c)" using 2 by blast
+    qed
+  qed
+  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+    by (blast intro: mono_gamma_c order_trans)
+qed
+
+end
+
+interpretation Abs_Int2
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = in_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
+defines AI_ivl' is AI_wn
+..
+
+
+subsubsection "Tests"
+
+definition "step_up_ivl n =
+  ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)"
+definition "step_down_ivl n =
+  ((\<lambda>C. C \<triangle> step_ivl (top (strip C)) C)^^n)"
+
+text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
+the loop took to execute. In contrast, @{const AI_ivl'} converges in a
+constant number of steps: *}
+
+value "show_acom (step_up_ivl 1 (bot test3_ivl))"
+value "show_acom (step_up_ivl 2 (bot test3_ivl))"
+value "show_acom (step_up_ivl 3 (bot test3_ivl))"
+value "show_acom (step_up_ivl 4 (bot test3_ivl))"
+value "show_acom (step_up_ivl 5 (bot test3_ivl))"
+value "show_acom (step_down_ivl 1 (step_up_ivl 5 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 2 (step_up_ivl 5 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 3 (step_up_ivl 5 (bot test3_ivl)))"
+value "show_acom_opt (AI_ivl' test3_ivl)"
+
+
+text{* Now all the analyses terminate: *}
+
+value "show_acom_opt (AI_ivl' test4_ivl)"
+value "show_acom_opt (AI_ivl' test5_ivl)"
+value "show_acom_opt (AI_ivl' test6_ivl)"
+
+
+subsubsection "Generic Termination Proof"
+
+locale Abs_Int2_measure = Abs_Int2
+  where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set" +
+fixes m :: "'av \<Rightarrow> nat"
+fixes n :: "'av \<Rightarrow> nat"
+fixes h :: "nat"
+assumes m_anti_mono: "x \<sqsubseteq> y \<Longrightarrow> m x \<ge> m y"
+assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
+assumes m_height: "m x \<le> h"
+assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
+assumes n_narrow: "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
+
+begin
+
+definition "m_st S = (SUM x:dom S. m(fun S x))"
+
+lemma h_st: assumes "finite X" and "dom S \<subseteq> X"
+shows "m_st S \<le> h * card X"
+proof(auto simp: m_st_def)
+  have "(\<Sum>x\<in>dom S. m (fun S x)) \<le> (\<Sum>x\<in>dom S. h)" (is "?L \<le> _")
+    by(rule setsum_mono)(simp add: m_height)
+  also have "\<dots> \<le> (\<Sum>x\<in>X. h)"
+    by(rule setsum_mono3[OF assms]) simp
+  also have "\<dots> = h * card X" by simp
+  finally show "?L \<le> \<dots>" .
+qed
+
+
+(* FIXME identical *)
+lemma m_st_anti_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st S1 \<ge> m_st S2"
+proof(auto simp add: le_st_def m_st_def)
+  assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
+  hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m_anti_mono)
+  thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
+    by (metis setsum_mono)
+qed
+
+lemma m_st_widen: "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> finite X \<Longrightarrow>
+  ~ S2 \<sqsubseteq> S1 \<Longrightarrow> m_st(S1 \<nabla> S2) < m_st S1"
+proof(auto simp add: le_st_def m_st_def wt_st_def widen_st_def)
+  assume "finite(dom S1)"
+  have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
+    by (metis m_anti_mono WN_class.widen1)
+  fix x assume "x \<in> dom S1" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
+  hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
+    using m_widen by blast
+  from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2]
+  show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
+qed
+
+definition "n_st S = (\<Sum>x\<in>dom S. n(fun S x))"
+
+lemma n_st_mono: assumes "S1 \<sqsubseteq> S2" shows "n_st S1 \<le> n_st S2"
+proof-
+  from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
+    by(simp_all add: le_st_def)
+  have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))"
+    by(rule setsum_mono)(simp add: le_st_def n_mono)
+  thus ?thesis by(simp add: n_st_def)
+qed
+
+lemma n_st_narrow:
+assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
+shows "n_st (S1 \<triangle> S2) < n_st S1"
+proof-
+  from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
+    by(simp_all add: le_st_def)
+  have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
+    by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
+  have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<sqsubseteq> S1 \<triangle> S2`
+    by(auto simp: le_st_def narrow_st_def intro: n_narrow)
+  have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
+    apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
+  moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
+  ultimately show ?thesis by(simp add: n_st_def)
+qed
+
+
+definition "m_o k opt = (case opt of None \<Rightarrow> k+1 | Some x \<Rightarrow> m_st x)"
+
+lemma m_o_anti_mono: "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> finite X \<Longrightarrow>
+  S1 \<sqsubseteq> S2 \<Longrightarrow> m_o (h * card X) S2 \<le> m_o (h * card X) S1"
+apply(induction S1 S2 rule: le_option.induct)
+apply(auto simp: m_o_def m_st_anti_mono le_SucI h_st wt_st_def
+           split: option.splits)
+done
+
+lemma m_o_widen: "\<lbrakk> wt S1 X; wt S2 X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
+  m_o (h * card X) (S1 \<nabla> S2) < m_o (h * card X) S1"
+by(auto simp: m_o_def wt_st_def h_st less_Suc_eq_le m_st_widen
+        split: option.split)
+
+definition "n_o opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n_st x + 1)"
+
+lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n_o S1 \<le> n_o S2"
+by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_st_mono)
+
+lemma n_o_narrow:
+  "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> finite X
+  \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n_o (S1 \<triangle> S2) < n_o S1"
+apply(induction S1 S2 rule: narrow_option.induct)
+apply(auto simp: n_o_def wt_st_def n_st_narrow)
+done
+
+
+lemma annos_narrow_acom[simp]: "strip C2 = strip (C1::'a::WN_Wt acom) \<Longrightarrow>
+  annos(C1 \<triangle> C2) = map (%(x,y).x\<triangle>y) (zip (annos C1) (annos C2))"
+by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" C1 C2 rule: map2_acom.induct)
+  (simp_all add: narrow_acom_def size_annos_same2)
+
+
+definition "m_c C = (let as = annos C in
+  \<Sum>i=0..<size as. m_o (h * card(vars(strip C))) (as!i))"
+
+lemma m_c_widen:
+  "Wt C1 c \<Longrightarrow> Wt C2 c \<Longrightarrow> \<not> C2 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
+apply(auto simp: Wt_acom_def m_c_def Let_def widen_acom_def)
+apply(subgoal_tac "length(annos C2) = length(annos C1)")
+prefer 2 apply (simp add: size_annos_same2)
+apply (auto)
+apply(rule setsum_strict_mono_ex1)
+apply simp
+apply (clarsimp)
+apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
+apply(auto simp: le_iff_le_annos listrel_iff_nth)
+apply(rule_tac x=i in bexI)
+prefer 2 apply simp
+apply(rule m_o_widen)
+apply (simp add: finite_cvars)+(*FIXME [simp]*)
+done
+
+definition "n_c C = (let as = annos C in \<Sum>i=0..<size as. n_o (as!i))"
+
+lemma n_c_narrow:
+  "Wt C1 c \<Longrightarrow> Wt C2 c \<Longrightarrow> C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n_c (C1 \<triangle> C2) < n_c C1"
+apply(auto simp: n_c_def Let_def Wt_acom_def narrow_acom_def)
+apply(subgoal_tac "length(annos C2) = length(annos C1)")
+prefer 2 apply (simp add: size_annos_same2)
+apply (auto)
+apply(rule setsum_strict_mono_ex1)
+apply simp
+apply (clarsimp)
+apply(rule n_o_mono)
+apply(rule narrow2)
+apply(fastforce simp: le_iff_le_annos listrel_iff_nth)
+apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom)
+apply(rule_tac x=i in bexI)
+prefer 2 apply simp
+apply(rule n_o_narrow[where X = "vars(strip C1)"])
+apply (simp add: finite_cvars)+
+done
+
+end
+
+
+lemma iter_widen_termination:
+fixes m :: "'a::WN_Wt \<Rightarrow> nat"
+assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
+and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
+and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<sqsubseteq> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
+and "P C" shows "EX C'. iter_widen f C = Some C'"
+proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = P])
+  show "wf {(cc, c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc = c \<nabla> f c}"
+    by(rule wf_subset[OF wf_measure[of "m"]])(auto simp: m_widen P_f)
+next
+  show "P C" by(rule `P C`)
+next
+  fix C assume "P C" thus "P (C \<nabla> f C)" by(simp add: P_f P_widen)
+qed
+thm mono_step'(*FIXME does not need wt assms*)
+lemma iter_narrow_termination:
+fixes n :: "'a::WN_Wt \<Rightarrow> nat"
+assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
+and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
+and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"
+and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<sqsubseteq> C1 \<Longrightarrow> ~ C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
+and init: "P C" "f C \<sqsubseteq> C" shows "EX C'. iter_narrow f C = Some C'"
+proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "%C. P C \<and> f C \<sqsubseteq> C"])
+  show "wf {(c', c). ((P c \<and> f c \<sqsubseteq> c) \<and> \<not> c \<sqsubseteq> c \<triangle> f c) \<and> c' = c \<triangle> f c}"
+    by(rule wf_subset[OF wf_measure[of "n"]])(auto simp: n_narrow P_f)
+next
+  show "P C \<and> f C \<sqsubseteq> C" using init by blast
+next
+  fix C assume 1: "P C \<and> f C \<sqsubseteq> C"
+  hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
+  moreover then have "f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C"
+    by (metis narrow1 narrow2 1 mono preord_class.le_trans)
+  ultimately show "P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C" ..
+qed
+
+
+subsubsection "Termination: Intervals"
+
+definition m_ivl :: "ivl \<Rightarrow> nat" where
+"m_ivl ivl = (case ivl of I l h \<Rightarrow>
+     (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))"
+
+lemma m_ivl_height: "m_ivl ivl \<le> 2"
+by(simp add: m_ivl_def split: ivl.split option.split)
+
+lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
+by(auto simp: m_ivl_def le_option_def le_ivl_def
+        split: ivl.split option.split if_splits)
+
+lemma m_ivl_widen:
+  "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
+by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def
+        split: ivl.splits option.splits if_splits)
+
+definition n_ivl :: "ivl \<Rightarrow> nat" where
+"n_ivl ivl = 2 - m_ivl ivl"
+
+lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
+unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
+
+lemma n_ivl_narrow:
+  "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
+by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def
+        split: ivl.splits option.splits if_splits)
+
+
+interpretation Abs_Int2_measure
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = in_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
+and m = m_ivl and n = n_ivl and h = 2
+proof
+  case goal1 thus ?case by(rule m_ivl_anti_mono)
+next
+  case goal2 thus ?case by(rule m_ivl_widen)
+next
+  case goal3 thus ?case by(rule m_ivl_height)
+next
+  case goal4 thus ?case by(rule n_ivl_mono)
+next
+  case goal5 thus ?case by(rule n_ivl_narrow)
+qed
+
+
+lemma iter_winden_step_ivl_termination:
+  "\<exists>C. iter_widen (step_ivl (top c)) (bot c) = Some C"
+apply(rule iter_widen_termination[where m = "m_c" and P = "%C. Wt C c"])
+apply (simp_all add: Wt_step' m_c_widen)
+done
+
+lemma iter_narrow_step_ivl_termination:
+  "Wt C0 c \<Longrightarrow> step_ivl (top c) C0 \<sqsubseteq> C0 \<Longrightarrow>
+  \<exists>C. iter_narrow (step_ivl (top c)) C0 = Some C"
+apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. Wt C c"])
+apply (simp add: Wt_step')
+apply (simp)
+apply(rule mono_step'_top)
+apply(simp add: Wt_acom_def wt_acom_def)
+apply(simp add: Wt_acom_def wt_acom_def)
+apply assumption
+apply(erule (3) n_c_narrow)
+apply assumption
+apply assumption
+done
+
+theorem AI_ivl'_termination:
+  "\<exists>C. AI_ivl' c = Some C"
+apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
+           split: option.split)
+apply(rule iter_narrow_step_ivl_termination)
+apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>c\<^esub>" and P = "%C. Wt C c"] Wt_bot Wt_widen Wt_step'[where S = "\<top>\<^bsub>c\<^esub>" and c=c, simplified])
+apply(erule iter_widen_pfp)
+done
+
+(*unused_thms Abs_Int_init -*)
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Thu Apr 19 19:36:09 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -1,5 +1,7 @@
 (* Author: Tobias Nipkow *)
 
+header "Abstract Interpretation (ITP)"
+
 theory Abs_Int0_ITP
 imports "~~/src/HOL/ex/Interpretation_with_Defs"
         "~~/src/HOL/Library/While_Combinator"
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Thu Apr 19 19:36:09 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -329,23 +329,6 @@
 qed
 
 
-fun annos :: "'a acom \<Rightarrow> 'a list" where
-"annos (SKIP {a}) = [a]" |
-"annos (x::=e {a}) = [a]" |
-"annos (c1;c2) = annos c1 @ annos c2" |
-"annos (IF b THEN c1 ELSE c2 {a}) = a #  annos c1 @ annos c2" |
-"annos ({i} WHILE b DO c {a}) = i # a # annos c"
-
-lemma size_annos_same: "strip c1 = strip c2 \<Longrightarrow> size(annos c1) = size(annos c2)"
-apply(induct c2 arbitrary: c1)
-apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Semi strip_eq_If strip_eq_While)
-done
-
-lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
-
-lemma set_annos_anno: "set (annos (anno a c)) = {a}"
-by(induction c)(auto)
-
 lemma le_iff_le_annos: "c1 \<sqsubseteq> c2 \<longleftrightarrow>
  (annos c1, annos c2) : listrel{(x,y). x \<sqsubseteq> y} \<and> strip c1 = strip c2"
 apply(induct c1 c2 rule: le_acom.induct)
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/Abs_Int_init.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_init.thy	Thu Apr 19 20:19:24 2012 +0200
@@ -0,0 +1,9 @@
+theory Abs_Int_init
+imports "~~/src/HOL/ex/Interpretation_with_Defs"
+        "~~/src/HOL/Library/While_Combinator"
+        Vars Collecting Abs_Int_Tests
+begin
+
+hide_const (open) top bot dom --"to avoid qualified names"
+
+end
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Thu Apr 19 19:36:09 2012 +0200
+++ b/src/HOL/IMP/ROOT.ML	Thu Apr 19 20:19:24 2012 +0200
@@ -23,6 +23,9 @@
  "Collecting1",
  "Collecting_list",
  "Abs_Int_Tests",
+ "Abs_Int1_parity",
+ "Abs_Int1_const",
+ "Abs_Int3",
  "Abs_Int_ITP/Abs_Int1_parity_ITP",
  "Abs_Int_ITP/Abs_Int1_const_ITP",
  "Abs_Int_ITP/Abs_Int3_ITP",
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Thu Apr 19 19:36:09 2012 +0200
+++ b/src/HOL/IMP/document/root.tex	Thu Apr 19 20:19:24 2012 +0200
@@ -4,6 +4,8 @@
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
+\usepackage{latexsym}
+
 %\usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
@@ -35,14 +37,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
-\newcommand{\isasymSKIP}{\CMD{skip}}
-\newcommand{\isasymIF}{\CMD{if}}
-\newcommand{\isasymTHEN}{\CMD{then}}
-\newcommand{\isasymELSE}{\CMD{else}}
-\newcommand{\isasymWHILE}{\CMD{while}}
-\newcommand{\isasymDO}{\CMD{do}}
-
 % for uniform font size
 \renewcommand{\isastyle}{\isastyleminor}
 
diff -r bc9c7b5c26fd -r 540a5af9a01c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Apr 19 19:36:09 2012 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 19 20:19:24 2012 +0200
@@ -526,6 +526,9 @@
 
 $(OUT)/HOL-IMP: $(OUT)/HOL \
   IMP/ACom.thy \
+  IMP/Abs_Int0.thy IMP/Abs_State.thy IMP/Abs_Int1.thy \
+  IMP/Abs_Int1_const.thy IMP/Abs_Int1_parity.thy \
+  IMP/Abs_Int2.thy IMP/Abs_Int2_ivl.thy IMP/Abs_Int3.thy \
   IMP/Abs_Int_ITP/Abs_Int0_ITP.thy IMP/Abs_Int_ITP/Abs_State_ITP.thy \
   IMP/Abs_Int_ITP/Abs_Int1_ITP.thy IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy \
   IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy IMP/Abs_Int_ITP/Abs_Int2_ITP.thy \