# HG changeset patch
# User nipkow
# Date 1322161117 -3600
# Node ID f682f3f7b726eec557e3c2eaf5a57ddf2d408dee
# Parent  4334c91b7405f2bb66a0e666facf7da84b999eed
Abstract interpretation is now based uniformly on annotated programs,
including a collecting and a small step semantics

diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/ACom.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/ACom.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,84 @@
+(* Author: Tobias Nipkow *)
+
+theory ACom
+imports Com
+begin
+
+(* is there a better place? *)
+definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
+
+section "Annotated Commands"
+
+datatype 'a acom =
+  SKIP   'a                           ("SKIP {_}") |
+  Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
+  Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
+  If     bexp "('a acom)" "('a acom)" 'a
+    ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
+  While  'a bexp "('a acom)" 'a
+    ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
+
+fun post :: "'a acom \<Rightarrow>'a" where
+"post (SKIP {P}) = P" |
+"post (x ::= e {P}) = P" |
+"post (c1; c2) = post c2" |
+"post (IF b THEN c1 ELSE c2 {P}) = P" |
+"post ({Inv} WHILE b DO c {P}) = P"
+
+fun strip :: "'a acom \<Rightarrow> com" where
+"strip (SKIP {a}) = com.SKIP" |
+"strip (x ::= e {a}) = (x ::= e)" |
+"strip (c1;c2) = (strip c1; strip c2)" |
+"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
+"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
+
+fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
+"anno a com.SKIP = SKIP {a}" |
+"anno a (x ::= e) = (x ::= e {a})" |
+"anno a (c1;c2) = (anno a c1; anno a c2)" |
+"anno a (IF b THEN c1 ELSE c2) =
+  (IF b THEN anno a c1 ELSE anno a c2 {a})" |
+"anno a (WHILE b DO c) =
+  ({a} WHILE b DO anno a c {a})"
+
+fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
+"map_acom f (SKIP {a}) = SKIP {f a}" |
+"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
+"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
+"map_acom f (IF b THEN c1 ELSE c2 {a}) =
+  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
+"map_acom f ({a1} WHILE b DO c {a2}) =
+  ({f a1} WHILE b DO map_acom f c {f a2})"
+
+
+lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
+by (induction c) simp_all
+
+lemma strip_acom[simp]: "strip (map_acom f c) = strip c"
+by (induction c) auto
+
+
+lemma strip_anno[simp]: "strip (anno a c) = c"
+by(induct c) simp_all
+
+lemma strip_eq_SKIP: "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Assign: "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Semi:
+  "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
+by (cases c) simp_all
+
+lemma strip_eq_If:
+  "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow>
+  (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)"
+by (cases c) simp_all
+
+lemma strip_eq_While:
+  "strip c = WHILE b DO c1 \<longleftrightarrow>
+  (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)"
+by (cases c) simp_all
+
+end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -6,10 +6,10 @@
 
 subsection "Computable Abstract Interpretation"
 
-text{* Abstract interpretation over type @{text astate} instead of
+text{* Abstract interpretation over type @{text st} instead of
 functions. *}
 
-locale Abs_Int = Val_abs
+context Val_abs
 begin
 
 fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
@@ -17,10 +17,18 @@
 "aval' (V x) S = lookup S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
+lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
+by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
+
+end
+
+locale Abs_Int = Val_abs
+begin
+
+fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
 "step S (SKIP {P}) = (SKIP {S})" |
 "step S (x ::= e {P}) =
-  x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(update S x (aval' e S))}" |
+  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 c1' = step S c1; c2' = step S c2
@@ -28,7 +36,7 @@
 "step S ({Inv} WHILE b DO c {P}) =
    {S \<squnion> post c} WHILE b DO step Inv c {Inv}"
 
-definition AI :: "com \<Rightarrow> 'a st up acom option" where
+definition AI :: "com \<Rightarrow> 'a st option acom option" where
 "AI = lpfp\<^isub>c (step \<top>)"
 
 
@@ -38,47 +46,73 @@
 
 text{* Soundness: *}
 
-lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
-by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
-
-lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
+lemma in_rep_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: rep_st_def lookup_update)
 
-lemma step_sound:
-  "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
-proof(induction c arbitrary: S s t)
+text{* The soundness proofs are textually identical to the ones for the step
+function operating on states as functions. *}
+
+lemma step_preserves_le2:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
+proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
-    by simp (metis skipE up_fun_in_rep_le)
+    by(auto simp:strip_eq_SKIP)
 next
   case Assign thus ?case
-    apply (auto simp del: fun_upd_apply simp: split: up.splits)
-    by (metis aval'_sound fun_in_rep_le in_rep_update)
-next
-  case Semi thus ?case by simp blast
+    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+      split: option.splits del:subsetD)
 next
-  case (If b c1 c2 S0) thus ?case
-    apply(auto simp: Let_def)
-    apply (metis up_fun_in_rep_le)+
-    done
+  case Semi thus ?case apply (auto simp: strip_eq_Semi)
+    by (metis le_post post_map_acom)
 next
-  case (While Inv b c P)
-  from While.prems have inv: "step Inv c \<sqsubseteq> c"
-    and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
-  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
-    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by simp
-    next
-      case (WhileTrue s1 s2 s3)
-      from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
-      show ?case .
-    qed
-  }
-  thus ?case using While.prems(2)
-    by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
+  case (If b c1 c2)
+  then obtain cs1 cs2 ca1 ca2 P Pa where
+      "cs = IF b THEN cs1 ELSE cs2 {P}" "ca = IF b THEN ca1 ELSE ca2 {Pa}"
+      "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+      "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
+    by (fastforce simp: strip_eq_If)
+  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
+  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
+  ultimately show ?case using If.prems(1) by (simp add: If.IH subset_iff)
+next
+  case (While b c1)
+  then obtain cs1 ca1 I P Ia Pa where
+    "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
+    "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+    "strip cs1 = c1" "strip ca1 = c1"
+    by (fastforce simp: strip_eq_While)
+  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
+    using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+  ultimately show ?case by (simp add: While.IH subset_iff)
 qed
 
-lemma AI_sound: "\<lbrakk> AI c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
-by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
+lemma step_preserves_le:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
+by (metis le_strip step_preserves_le2 strip_acom)
+
+lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+proof(simp add: CS_def AI_def)
+  assume 1: "lpfp\<^isub>c (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_lpfpc[OF _ 1])
+  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  proof(rule lfp_lowerbound[OF 3])
+    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    proof(rule step_preserves_le[OF _ _ 3])
+      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
+      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+    qed
+  qed
+  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+    by (blast intro: mono_rep_c order_trans)
+qed
 
 end
 
@@ -97,7 +131,7 @@
 
 lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
 apply(induction c arbitrary: S S')
-apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
+apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
 done
 
 end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -1,7 +1,7 @@
 (* Author: Tobias Nipkow *)
 
 theory Abs_Int0_const
-imports Abs_Int0
+imports Abs_Int0 Abs_Int_Tests
 begin
 
 subsection "Constant Propagation"
@@ -53,6 +53,7 @@
 
 
 interpretation Val_abs rep_cval Const plus_cval
+defines aval'_const is aval'
 proof
   case goal1 thus ?case
     by(cases a, cases b, simp, simp, cases b, simp, simp)
@@ -67,43 +68,20 @@
 
 interpretation Abs_Int rep_cval Const plus_cval
 defines AI_const is AI
-and aval'_const is aval'
 and step_const is step
 proof qed
 
-text{* Straight line code: *}
-definition "test1_const =
- ''y'' ::= N 7;
- ''z'' ::= Plus (V ''y'') (N 2);
- ''y'' ::= Plus (V ''x'') (N 0)"
 
-text{* Conditional: *}
-definition "test2_const =
- IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
-
-text{* Conditional, test is ignored: *}
-definition "test3_const =
- ''x'' ::= N 42;
- IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
+text{* Monotonicity: *}
 
-text{* While: *}
-definition "test4_const =
- ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
-
-text{* While, test is ignored: *}
-definition "test5_const =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+interpretation Abs_Int_mono rep_cval Const plus_cval
+proof
+  case goal1 thus ?case
+    by(auto simp: plus_cval_cases split: cval.split)
+qed
 
-text{* Iteration is needed: *}
-definition "test6_const =
-  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
-  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
 
-text{* More iteration would be needed: *}
-definition "test7_const =
-  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
-  WHILE Less (V ''x'') (N 1)
-  DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+subsubsection "Tests"
 
 value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
 value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
@@ -129,14 +107,5 @@
 value [code] "show_acom_opt (AI_const test5_const)"
 
 value [code] "show_acom_opt (AI_const test6_const)"
-value [code] "show_acom_opt (AI_const test7_const)"
-
-text{* Monotonicity: *}
-
-interpretation Abs_Int_mono rep_cval Const plus_cval
-proof
-  case goal1 thus ?case
-    by(auto simp: plus_cval_cases split: cval.split)
-qed
 
 end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -3,57 +3,11 @@
 header "Abstract Interpretation"
 
 theory Abs_Int0_fun
-imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+imports "~~/src/HOL/ex/Interpretation_with_Defs"
         "~~/src/HOL/Library/While_Combinator"
+        Collecting
 begin
 
-subsection "Annotated Commands"
-
-datatype 'a acom =
-  SKIP   'a                           ("SKIP {_}") |
-  Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
-  Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
-  If     bexp "('a acom)" "('a acom)" 'a
-    ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
-  While  'a bexp "('a acom)" 'a
-    ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
-
-fun post :: "'a acom \<Rightarrow>'a" where
-"post (SKIP {P}) = P" |
-"post (x ::= e {P}) = P" |
-"post (c1; c2) = post c2" |
-"post (IF b THEN c1 ELSE c2 {P}) = P" |
-"post ({Inv} WHILE b DO c {P}) = P"
-
-fun strip :: "'a acom \<Rightarrow> com" where
-"strip (SKIP {a}) = com.SKIP" |
-"strip (x ::= e {a}) = (x ::= e)" |
-"strip (c1;c2) = (strip c1; strip c2)" |
-"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
-"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
-
-fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
-"anno a com.SKIP = SKIP {a}" |
-"anno a (x ::= e) = (x ::= e {a})" |
-"anno a (c1;c2) = (anno a c1; anno a c2)" |
-"anno a (IF b THEN c1 ELSE c2) =
-  (IF b THEN anno a c1 ELSE anno a c2 {a})" |
-"anno a (WHILE b DO c) =
-  ({a} WHILE b DO anno a c {a})"
-
-lemma strip_anno[simp]: "strip (anno a c) = c"
-by(induct c) simp_all
-
-fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
-"map_acom f (SKIP {a}) = SKIP {f a}" |
-"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
-"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
-"map_acom f (IF b THEN c1 ELSE c2 {a}) =
-  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
-"map_acom f ({a1} WHILE b DO c {a2}) =
-  ({f a1} WHILE b DO map_acom f c {f a2})"
-
-
 subsection "Orderings"
 
 class preord =
@@ -159,31 +113,29 @@
 
 subsubsection "Lifting"
 
-datatype 'a up = Bot | Up 'a
-
-instantiation up :: (SL_top)SL_top
+instantiation option :: (SL_top)SL_top
 begin
 
-fun le_up where
-"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
-"Bot \<sqsubseteq> y = True" |
-"Up _ \<sqsubseteq> Bot = False"
+fun le_option where
+"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" |
+"None \<sqsubseteq> y = True" |
+"Some _ \<sqsubseteq> None = False"
 
-lemma [simp]: "(x \<sqsubseteq> Bot) = (x = Bot)"
+lemma [simp]: "(x \<sqsubseteq> None) = (x = None)"
 by (cases x) simp_all
 
-lemma [simp]: "(Up x \<sqsubseteq> u) = (\<exists>y. u = Up y & x \<sqsubseteq> y)"
+lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y & x \<sqsubseteq> y)"
 by (cases u) auto
 
-fun join_up where
-"Up x \<squnion> Up y = Up(x \<squnion> y)" |
-"Bot \<squnion> y = y" |
-"x \<squnion> Bot = x"
+fun join_option where
+"Some x \<squnion> Some y = Some(x \<squnion> y)" |
+"None \<squnion> y = y" |
+"x \<squnion> None = x"
 
-lemma [simp]: "x \<squnion> Bot = x"
+lemma [simp]: "x \<squnion> None = x"
 by (cases x) simp_all
 
-definition "\<top> = Up \<top>"
+definition "\<top> = Some \<top>"
 
 instance proof
   case goal1 show ?case by(cases x, simp_all)
@@ -197,13 +149,13 @@
 next
   case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
 next
-  case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
+  case goal6 thus ?case by(cases x, simp_all add: Top_option_def)
 qed
 
 end
 
-definition bot_acom :: "com \<Rightarrow> ('a::SL_top)up acom" ("\<bottom>\<^sub>c") where
-"\<bottom>\<^sub>c = anno Bot"
+definition bot_acom :: "com \<Rightarrow> ('a::SL_top)option acom" ("\<bottom>\<^sub>c") where
+"\<bottom>\<^sub>c = anno None"
 
 lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c"
 by(simp add: bot_acom_def)
@@ -246,7 +198,7 @@
 qed
 
 definition
- lpfp\<^isub>c :: "(('a::SL_top)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option" where
+ lpfp\<^isub>c :: "(('a::SL_top)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" where
 "lpfp\<^isub>c f c = pfp f (\<bottom>\<^sub>c c)"
 
 lemma lpfpc_pfp: "lpfp\<^isub>c f c0 = Some c \<Longrightarrow> f c \<sqsubseteq> c"
@@ -275,30 +227,21 @@
 definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
 "rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
 
-fun rep_up :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a up \<Rightarrow> 'b set" where
-"rep_up rep Bot = {}" |
-"rep_up rep (Up a) = rep a"
+fun rep_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
+"rep_option rep None = {}" |
+"rep_option rep (Some a) = rep a"
 
 text{* The interface for abstract values: *}
 
 locale Val_abs =
-fixes rep :: "'a::SL_top \<Rightarrow> val set"
-  assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
-  and rep_Top: "rep \<top> = UNIV"
+fixes rep :: "'a::SL_top \<Rightarrow> val set" ("\<gamma>")
+  assumes mono_rep: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
+  and rep_Top[simp]: "\<gamma> \<top> = UNIV"
 fixes num' :: "val \<Rightarrow> 'a"
 and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-  assumes rep_num': "n : rep(num' n)"
+  assumes rep_num': "n : \<gamma>(num' n)"
   and rep_plus':
- "n1 : rep a1 \<Longrightarrow> n2 : rep a2 \<Longrightarrow> n1+n2 : rep(plus' a1 a2)"
-begin
-
-abbreviation in_rep (infix "<:" 50)
- where "x <: a == x : rep a"
-
-lemma in_rep_Top[simp]: "x <: \<top>"
-by(simp add: rep_Top)
-
-end
+ "n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
 
 type_synonym 'a st = "(vname \<Rightarrow> 'a)"
 
@@ -310,18 +253,18 @@
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
+fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
  where
 "step S (SKIP {P}) = (SKIP {S})" |
 "step S (x ::= e {P}) =
-  x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(S(x := aval' e S))}" |
+  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> 'a st up acom option" where
+definition AI :: "com \<Rightarrow> 'a st option acom option" where
 "AI = lpfp\<^isub>c (step \<top>)"
 
 
@@ -329,76 +272,102 @@
 by(induct c arbitrary: S) (simp_all add: Let_def)
 
 
-text{*Lifting @{text "<:"} to other types: *}
-
-abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
-"s <:f S == s \<in> rep_fun rep S"
-
-notation fun_in_rep (infix "<:\<^sub>f" 50)
-
-lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
-by(auto simp add: rep_fun_def le_fun_def dest: le_rep)
+abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
+where "\<gamma>\<^isub>f == rep_fun \<gamma>"
 
-abbreviation up_in_rep :: "state \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50) where
-"s <:up S == s : rep_up (rep_fun rep) S"
-
-notation (output) up_in_rep (infix "<:\<^sub>u\<^sub>p" 50)
+abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
+where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
 
-lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
-by (cases S) (auto intro:fun_in_rep_le)
+abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
 
-lemma in_rep_Top_fun: "s <:f Top"
+lemma rep_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
 by(simp add: Top_fun_def rep_fun_def)
 
-lemma in_rep_Top_up: "s <:up Top"
-by(simp add: Top_up_def in_rep_Top_fun)
+lemma rep_u_Top[simp]: "\<gamma>\<^isub>u Top = UNIV"
+by (simp add: Top_option_def)
+
+(* FIXME (maybe also le \<rightarrow> sqle?) *)
 
+lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+by(auto simp: le_fun_def rep_fun_def dest: mono_rep)
+
+lemma mono_rep_u:
+  "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
+
+lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
 
 text{* Soundness: *}
 
-lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
+lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
 by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def)
 
-lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f S(x := a)"
+lemma in_rep_update:
+  "\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(S(x := a))"
 by(simp add: rep_fun_def)
 
-lemma step_sound:
-  "\<lbrakk> step S c \<sqsubseteq> c; (strip c,s) \<Rightarrow> t; s <:up S \<rbrakk>
-   \<Longrightarrow> t <:up post c"
-proof(induction c arbitrary: S s t)
+lemma step_preserves_le2:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
+proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
-    by simp (metis skipE up_fun_in_rep_le)
+    by(auto simp:strip_eq_SKIP)
 next
   case Assign thus ?case
-    apply (auto simp del: fun_upd_apply split: up.splits)
-    by (metis aval'_sound fun_in_rep_le in_rep_update)
-next
-  case Semi thus ?case by simp blast
+    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+      split: option.splits del:subsetD)
 next
-  case (If b c1 c2 S0) thus ?case
-    apply(auto simp: Let_def)
-    apply (metis up_fun_in_rep_le)+
-    done
+  case Semi thus ?case apply (auto simp: strip_eq_Semi)
+    by (metis le_post post_map_acom)
 next
-  case (While Inv b c P)
-  from While.prems have inv: "step Inv c \<sqsubseteq> c"
-    and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
-  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
-    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by simp
-    next
-      case (WhileTrue s1 s2 s3)
-      from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
-      show ?case .
-    qed
-  }
-  thus ?case using While.prems(2)
-    by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
+  case (If b c1 c2)
+  then obtain cs1 cs2 ca1 ca2 P Pa where
+      "cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}"
+      "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+      "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
+    by (fastforce simp: strip_eq_If)
+  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
+  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
+  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>u sa` by (simp add: If.IH subset_iff)
+next
+  case (While b c1)
+  then obtain cs1 ca1 I P Ia Pa where
+    "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
+    "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+    "strip cs1 = c1" "strip ca1 = c1"
+    by (fastforce simp: strip_eq_While)
+  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
+    using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+  ultimately show ?case by (simp add: While.IH subset_iff)
 qed
 
-lemma AI_sound:
- "\<lbrakk> AI c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
-by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
+lemma step_preserves_le:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
+by (metis le_strip step_preserves_le2 strip_acom)
+
+lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+proof(simp add: CS_def AI_def)
+  assume 1: "lpfp\<^isub>c (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_lpfpc[OF _ 1])
+  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  proof(rule lfp_lowerbound[OF 3])
+    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    proof(rule step_preserves_le[OF _ _ 3])
+      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
+      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+    qed
+  qed
+  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+    by (blast intro: mono_rep_c order_trans)
+qed
 
 end
 
@@ -417,7 +386,7 @@
 
 lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
 apply(induction c arbitrary: S S')
-apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
+apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
 done
 
 end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -1,7 +1,7 @@
 (* Author: Tobias Nipkow *)
 
 theory Abs_Int1
-imports Abs_Int0_const
+imports Abs_Int0
 begin
 
 instantiation prod :: (preord,preord) preord
@@ -37,20 +37,19 @@
 
 end
 
-
 locale Val_abs1_rep =
   Val_abs rep num' plus'
-  for rep :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
+  for rep :: "'a::L_top_bot \<Rightarrow> val set" ("\<gamma>") and num' plus' +
 assumes inter_rep_subset_rep_meet:
   "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
-and rep_Bot: "rep \<bottom> = {}"
+and rep_Bot[simp]: "rep \<bottom> = {}"
 begin
 
-lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
+lemma in_rep_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
 by (metis IntI inter_rep_subset_rep_meet set_mp)
 
-lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
-by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
+lemma rep_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+by (metis equalityI inter_rep_subset_rep_meet le_inf_iff mono_rep meet_le1 meet_le2)
 
 end
 
@@ -59,76 +58,74 @@
 fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
 and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
 assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
-  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
 and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
-  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
+  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
 
 
 locale Abs_Int1 = Val_abs1
 begin
 
-lemma in_rep_join_UpI: "s <:up S1 | s <:up S2 \<Longrightarrow> s <:up S1 \<squnion> S2"
-by (metis join_ge1 join_ge2 up_fun_in_rep_le)
+lemma in_rep_join_UpI: "s : \<gamma>\<^isub>u S1 | s : \<gamma>\<^isub>u S2 \<Longrightarrow> s : \<gamma>\<^isub>u(S1 \<squnion> S2)"
+by (metis (no_types) join_ge1 join_ge2 mono_rep_u set_rev_mp)
 
-fun aval' :: "aexp \<Rightarrow> 'a st up \<Rightarrow> 'a" where
-"aval' _ Bot = \<bottom>" |
-"aval' (N n) _ = num' n" |
-"aval' (V x) (Up S) = lookup S x" |
-"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
+fun aval'' :: "aexp \<Rightarrow> 'a st option \<Rightarrow> 'a" where
+"aval'' e None = \<bottom>" |
+"aval'' e (Some sa) = aval' e sa"
 
-lemma aval'_sound: "s <:up S \<Longrightarrow> aval a s <: aval' a S"
-by(induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def)
+lemma aval''_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
+by(cases S)(simp add: aval'_sound)+
 
 subsubsection "Backward analysis"
 
-fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
-"afilter (N n) a S = (if n <: a then S else Bot)" |
-"afilter (V x) a S = (case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow>
+fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st option \<Rightarrow> 'a st option" where
+"afilter (N n) a S = (if n : \<gamma> a then S else None)" |
+"afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
   let a' = lookup S x \<sqinter> a in
-  if a' \<sqsubseteq> \<bottom> then Bot else Up(update S x a'))" |
+  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)
+ (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
+text{* The test for @{const bot} in the @{const V}-case is important: @{const
+bot} indicates that a variable has no possible values, i.e.\ that the current
 program point is unreachable. But then the abstract state should collapse to
-@{const bot}. Put differently, we maintain the invariant that in an abstract
-state all variables are mapped to non-@{const Bot} values. Otherwise the
-(pointwise) join of two abstract states, one of which contains @{const Bot}
-values, may produce too large a result, thus making the analysis less
-precise. *}
+@{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> 'a st up \<Rightarrow> 'a st up" where
-"bfilter (Bc v) res S = (if v=res then S else Bot)" |
+fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st option \<Rightarrow> 'a 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)
+  (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
    in afilter e1 res1 (afilter e2 res2 S))"
 
-lemma afilter_sound: "s <:up S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:up afilter e a S"
+lemma afilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>u (afilter e a S)"
 proof(induction e arbitrary: a S)
   case N thus ?case by simp
 next
   case (V x)
-  obtain S' where "S = Up S'" and "s <:f S'" using `s <:up S`
+  obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>u S`
     by(auto simp: in_rep_up_iff)
-  moreover hence "s x <: lookup S' x" by(simp add: rep_st_def)
-  moreover have "s x <: a" using V by simp
+  moreover hence "s x : \<gamma> (lookup S' x)" by(simp add: rep_st_def)
+  moreover have "s x : \<gamma> a" using V by simp
   ultimately show ?case using V(1)
     by(simp add: lookup_update Let_def rep_st_def)
-      (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
+      (metis mono_rep emptyE in_rep_meet rep_Bot subset_empty)
 next
   case (Plus e1 e2) thus ?case
-    using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+    using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]]
     by (auto split: prod.split)
 qed
 
-lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S"
+lemma bfilter_sound: "s : \<gamma>\<^isub>u S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>u(bfilter b bv S)"
 proof(induction b arbitrary: S bv)
   case Bc thus ?case by simp
 next
@@ -138,16 +135,15 @@
 next
   case (Less e1 e2) thus ?case
     by (auto split: prod.split)
-       (metis afilter_sound filter_less' aval'_sound Less)
+       (metis afilter_sound filter_less' aval''_sound Less)
 qed
 
 
-fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
+fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
  where
 "step S (SKIP {P}) = (SKIP {S})" |
 "step S (x ::= e {P}) =
-  x ::= e {case S of Bot \<Rightarrow> Bot
-           | Up S \<Rightarrow> Up(update S x (aval' e (Up S)))}" |
+  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 c1' = step (bfilter b True S) c1; c2' = step (bfilter b False S) c2
@@ -157,7 +153,7 @@
    WHILE b DO step (bfilter b True Inv) c
    {bfilter b False Inv}"
 
-definition AI :: "com \<Rightarrow> 'a st up acom option" where
+definition AI :: "com \<Rightarrow> 'a st option acom option" where
 "AI = lpfp\<^isub>c (step \<top>)"
 
 lemma strip_step[simp]: "strip(step S c) = strip c"
@@ -166,68 +162,73 @@
 
 subsubsection "Soundness"
 
-lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
+lemma in_rep_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: rep_st_def lookup_update)
 
-lemma While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
-by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
 
-lemma step_sound:
-  "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
-proof(induction c arbitrary: S s t)
+lemma step_preserves_le2:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk>
+   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)"
+proof(induction c arbitrary: cs ca S sa)
   case SKIP thus ?case
-    by simp (metis skipE up_fun_in_rep_le)
+    by(auto simp:strip_eq_SKIP)
 next
   case Assign thus ?case
-    apply (auto simp del: fun_upd_apply split: up.splits)
-    by (metis aval'_sound fun_in_rep_le in_rep_update rep_up.simps(2))
+    by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update
+      split: option.splits del:subsetD)
 next
-  case Semi thus ?case by simp blast
+  case Semi thus ?case apply (auto simp: strip_eq_Semi)
+    by (metis le_post post_map_acom)
 next
-  case (If b c1 c2 S0)
-  show ?case
-  proof cases
-    assume "bval b s"
-    with If.prems have 1: "step (bfilter b True S) c1 \<sqsubseteq> c1"
-      and 2: "(strip c1, s) \<Rightarrow> t" and 3: "post c1 \<sqsubseteq> S0" by(auto simp: Let_def)
-    from If.IH(1)[OF 1 2 bfilter_sound[OF `s <:up S`]] `bval b s` 3
-    show ?thesis by simp (metis up_fun_in_rep_le)
-  next
-    assume "\<not> bval b s"
-    with If.prems have 1: "step (bfilter b False S) c2 \<sqsubseteq> c2"
-      and 2: "(strip c2, s) \<Rightarrow> t" and 3: "post c2 \<sqsubseteq> S0" by(auto simp: Let_def)
-    from If.IH(2)[OF 1 2 bfilter_sound[OF `s <:up S`]] `\<not> bval b s` 3
-    show ?thesis by simp (metis up_fun_in_rep_le)
-  qed
+  case (If b c1 c2)
+  then obtain cs1 cs2 ca1 ca2 P Pa where
+      "cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}"
+      "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+      "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2"
+    by (fastforce simp: strip_eq_If)
+  moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom)
+  moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)"
+    by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom)
+  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>u sa`
+    by (simp add: If.IH subset_iff bfilter_sound)
 next
-  case (While Inv b c P)
-  from While.prems have inv: "step (bfilter b True Inv) c \<sqsubseteq> c"
-    and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "bfilter b False Inv \<sqsubseteq> P"
-    by(auto simp: Let_def)
-  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
-    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by simp
-    next
-      case (WhileTrue s1 s2 s3)
-      from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` bfilter_sound[OF `s1 <:up Inv`]] `post c \<sqsubseteq> Inv`]] `bval b s1`
-      show ?case by simp
-    qed
-  } note Inv = this
-  from  While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
-    by(auto dest: While_final_False)
-  from Inv[OF this(1) up_fun_in_rep_le[OF `s <:up S` `S \<sqsubseteq> Inv`]]
-  have "t <:up Inv" .
-  from up_fun_in_rep_le[OF bfilter_sound[OF this]  `bfilter b False Inv \<sqsubseteq> P`]
-  show ?case using `\<not> bval b t` by simp
+  case (While b c1)
+  then obtain cs1 ca1 I P Ia Pa where
+    "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}"
+    "I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+    "strip cs1 = c1" "strip ca1 = c1"
+    by (fastforce simp: strip_eq_While)
+  moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)"
+    using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans)
+  ultimately show ?case by (simp add: While.IH subset_iff bfilter_sound)
 qed
 
-lemma AI_sound: "\<lbrakk> AI c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
-unfolding AI_def
-by (metis in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
-(*
-by(metis step_sound[of "\<top>" c' s t] strip_lpfp strip_step
-  lpfp_pfp mono_def mono_step[OF le_refl] in_rep_Top_up)
-*)
+lemma step_preserves_le:
+  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk>
+   \<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)"
+by (metis le_strip step_preserves_le2 strip_acom)
+
+lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+proof(simp add: CS_def AI_def)
+  assume 1: "lpfp\<^isub>c (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_lpfpc[OF _ 1])
+  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  proof(rule lfp_lowerbound[OF 3])
+    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    proof(rule step_preserves_le[OF _ _ 3])
+      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
+      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+    qed
+  qed
+  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+    by (blast intro: mono_rep_c order_trans)
+qed
+
 end
 
 
@@ -242,39 +243,44 @@
 begin
 
 lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+by(induction e) (auto simp: le_st_def lookup_def mono_plus')
+
+lemma mono_aval'': "S \<sqsubseteq> S' \<Longrightarrow> aval'' e S \<sqsubseteq> aval'' e S'"
 apply(cases S)
  apply simp
 apply(cases S')
  apply simp
-apply simp
-by(induction e) (auto simp: le_st_def lookup_def mono_plus')
+by (simp add: mono_aval')
 
 lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
 apply(induction e arbitrary: r r' S S')
-apply(auto simp: Let_def split: up.splits prod.splits)
-apply (metis le_rep subsetD)
+apply(auto simp: Let_def split: option.splits prod.splits)
+apply (metis mono_rep subsetD)
 apply(drule_tac x = "list" in mono_lookup)
 apply (metis mono_meet le_trans)
-apply (metis mono_meet mono_lookup mono_update le_trans)
-apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
+apply (metis mono_meet mono_lookup mono_update)
+apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
 done
 
 lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'"
 apply(induction b arbitrary: r S S')
 apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits)
-apply(metis mono_aval' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
+apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
 done
 
 
 lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
 by (induction c c' rule: le_acom.induct) simp_all
 
-lemma mono_step: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
+lemma mono_step_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
 apply(induction c c' arbitrary: S S' rule: le_acom.induct)
 apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
-  split: up.split)
+  split: option.split)
 done
 
+lemma mono_step: "mono (step S)"
+by(simp add: mono_def mono_step_aux[OF le_refl])
+
 end
 
 end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_Int1_ivl.thy
--- a/src/HOL/IMP/Abs_Int1_ivl.thy	Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -1,7 +1,7 @@
 (* Author: Tobias Nipkow *)
 
 theory Abs_Int1_ivl
-imports Abs_Int1
+imports Abs_Int1 Abs_Int_Tests
 begin
 
 subsection "Interval Analysis"
@@ -117,10 +117,10 @@
 instance
 proof
   case goal1 thus ?case
-    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+    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 goal2 thus ?case
-    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+    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 goal3 thus ?case
     by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
@@ -161,6 +161,7 @@
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
 interpretation Val_abs rep_ivl num_ivl plus_ivl
+defines aval_ivl is aval'
 proof
   case goal1 thus ?case
     by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
@@ -208,72 +209,9 @@
 and bfilter_ivl is bfilter
 and step_ivl is step
 and AI_ivl is AI
-and aval_ivl is aval'
+and aval_ivl' is aval''
 proof qed
 
-definition "test1_ivl =
- ''y'' ::= N 7;
- IF Less (V ''x'') (V ''y'')
- THEN ''y'' ::= Plus (V ''y'') (V ''x'')
- ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
-
-value [code] "show_acom_opt (AI_ivl test1_ivl)"
-
-value [code] "show_acom_opt (AI_const test3_const)"
-value [code] "show_acom_opt (AI_ivl test3_const)"
-
-value [code] "show_acom_opt (AI_const test4_const)"
-value [code] "show_acom_opt (AI_ivl test4_const)"
-
-value [code] "show_acom_opt (AI_ivl test6_const)"
-
-definition "test2_ivl =
- WHILE Less (V ''x'') (N 100)
- DO ''x'' ::= Plus (V ''x'') (N 1)"
-
-value [code] "show_acom_opt (AI_ivl test2_ivl)"
-value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
-
-text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
-
-definition "test3_ivl =
- ''x'' ::= N 7;
- WHILE Less (V ''x'') (N 100)
- DO ''x'' ::= Plus (V ''x'') (N 1)"
-
-value [code] "show_acom_opt (AI_ivl test3_ivl)"
-value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
-
-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: *}
-
-definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
- WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
-
-text{* The value of y keeps decreasing as the analysis is iterated, no matter
-how long: *}
-
-value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
-
-definition "test5_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
- WHILE Less (V ''x'') (N 1000)
- DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
-value [code] "show_acom_opt (AI_ivl test5_ivl)"
-
-text{* Again, the analysis would not terminate: *}
-definition "test6_ivl =
- ''x'' ::= N 0;
- WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
 
 text{* Monotonicity: *}
 
@@ -291,4 +229,41 @@
     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 [code] "show_acom_opt (AI_ivl test1_ivl)"
+
+text{* Better than @{text AI_const}: *}
+value [code] "show_acom_opt (AI_ivl test3_const)"
+value [code] "show_acom_opt (AI_ivl test4_const)"
+value [code] "show_acom_opt (AI_ivl test6_const)"
+
+value [code] "show_acom_opt (AI_ivl test2_ivl)"
+value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
+
+text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
+
+value [code] "show_acom_opt (AI_ivl test3_ivl)"
+value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
+value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
+
+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 [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
+
+text{* Relationships between variables are NOT captured: *}
+value [code] "show_acom_opt (AI_ivl test5_ivl)"
+
+text{* Again, the analysis would not terminate: *}
+value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test6_ivl))"
+
 end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -64,32 +64,32 @@
 
 end
 
-instantiation up :: (WN)WN
+instantiation option :: (WN)WN
 begin
 
-fun widen_up where
-"widen_up Bot x = x" |
-"widen_up x Bot = x" |
-"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
+fun widen_option where
+"None \<nabla> x = x" |
+"x \<nabla> None = x" |
+"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
 
-fun narrow_up where
-"narrow_up Bot x = Bot" |
-"narrow_up x Bot = Bot" |
-"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
+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 show ?case
-    by(induct x y rule: widen_up.induct) (simp_all add: widen1)
+    by(induct x y rule: widen_option.induct) (simp_all add: widen1)
 next
   case goal2 show ?case
-    by(induct x y rule: widen_up.induct) (simp_all add: widen2)
+    by(induct x y rule: widen_option.induct) (simp_all add: widen2)
 next
   case goal3 thus ?case
-    by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
+    by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
 next
   case goal4 thus ?case
-    by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
+    by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
 qed
 
 end
@@ -129,7 +129,7 @@
 "prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f"
 
 definition
-  pfp_WN :: "(('a::WN)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option"
+  pfp_WN :: "(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
 where "pfp_WN f c = (case lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c of None \<Rightarrow> None
                      | Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')"
 
@@ -183,13 +183,26 @@
 locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
 begin
 
-definition AI_WN :: "com \<Rightarrow> 'a st up acom option" where
+definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
 "AI_WN = pfp_WN (step \<top>)"
 
-lemma AI_sound: "\<lbrakk> AI_WN c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
-unfolding AI_WN_def
-by(metis step_sound[of "\<top>" c' s t] strip_pfp_WN strip_step
-  pfp_WN_pfp mono_def mono_step[OF le_refl] in_rep_Top_up)
+lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
+proof(simp add: CS_def AI_WN_def)
+  assume 1: "pfp_WN (step \<top>) c = Some c'"
+  from pfp_WN_pfp[OF allI[OF strip_step] mono_step 1]
+  have 2: "step \<top> c' \<sqsubseteq> c'" .
+  have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
+  have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')"
+  proof(rule lfp_lowerbound[OF 3])
+    show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')"
+    proof(rule step_preserves_le[OF _ _ 3])
+      show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
+      show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
+    qed
+  qed
+  from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'"
+    by (blast intro: mono_rep_c order_trans)
+qed
 
 end
 
@@ -198,12 +211,16 @@
 defines AI_ivl' is AI_WN
 proof qed
 
-value [code] "show_acom_opt (AI_ivl test3_ivl)"
-value [code] "show_acom_opt (AI_ivl' test3_ivl)"
+
+subsubsection "Tests"
 
 definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
 definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> 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 [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))"
 value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))"
 value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))"
@@ -213,6 +230,8 @@
 value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
 value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
 
+text{* Now all the analyses terminate: *}
+
 value [code] "show_acom_opt (AI_ivl' test4_ivl)"
 value [code] "show_acom_opt (AI_ivl' test5_ivl)"
 value [code] "show_acom_opt (AI_ivl' test6_ivl)"
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_Int_Tests.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,68 @@
+theory Abs_Int_Tests
+imports ACom
+begin
+
+subsection "Test Programs"
+
+text{* For constant propagation: *}
+
+text{* Straight line code: *}
+definition "test1_const =
+ ''y'' ::= N 7;
+ ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= Plus (V ''x'') (N 0)"
+
+text{* Conditional: *}
+definition "test2_const =
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
+
+text{* Conditional, test is relevant: *}
+definition "test3_const =
+ ''x'' ::= N 42;
+ IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
+
+text{* While: *}
+definition "test4_const =
+ ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
+
+text{* While, test is relevant: *}
+definition "test5_const =
+ ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+
+text{* Iteration is needed: *}
+definition "test6_const =
+  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
+  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
+
+text{* For intervals: *}
+
+definition "test1_ivl =
+ ''y'' ::= N 7;
+ IF Less (V ''x'') (V ''y'')
+ THEN ''y'' ::= Plus (V ''y'') (V ''x'')
+ ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
+
+definition "test2_ivl =
+ WHILE Less (V ''x'') (N 100)
+ DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+definition "test3_ivl =
+ ''x'' ::= N 7;
+ WHILE Less (V ''x'') (N 100)
+ DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+definition "test4_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ WHILE Less (V ''x'') (N 11)
+ DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
+
+definition "test5_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 0;
+ WHILE Less (V ''x'') (N 1000)
+ DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+
+definition "test6_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+
+end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed Nov 23 23:31:32 2011 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -19,11 +19,7 @@
 
 definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
 
-fun show_st_up where
-"show_st_up Bot = Bot" |
-"show_st_up (Up S) = Up(show_st S)"
-
-definition "show_acom = map_acom show_st_up"
+definition "show_acom = map_acom (Option.map show_st)"
 definition "show_acom_opt = Option.map show_acom"
 
 definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
@@ -65,32 +61,37 @@
 context Val_abs
 begin
 
-abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
-"s <:f S == s \<in> rep_st rep S"
+abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f")
+where "\<gamma>\<^isub>f == rep_st rep"
 
-notation fun_in_rep (infix "<:\<^sub>f" 50)
+abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u")
+where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f"
 
-lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
-apply(auto simp add: rep_st_def le_st_def dest: le_rep)
-by (metis in_rep_Top le_rep lookup_def subsetD)
+abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c")
+where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u"
 
-abbreviation in_rep_up :: "state \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50)
-where "s <:up S == s : rep_up (rep_st rep) S"
+lemma rep_f_Top[simp]: "rep_f Top = UNIV"
+by(auto simp: Top_st_def rep_st_def lookup_def)
+
+lemma rep_u_Top[simp]: "rep_u Top = UNIV"
+by (simp add: Top_option_def)
 
-notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)
+(* FIXME (maybe also le \<rightarrow> sqle?) *)
+
+lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+apply(simp add:rep_st_def subset_iff lookup_def le_st_def split: if_splits)
+by (metis UNIV_I mono_rep rep_Top subsetD)
 
-lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
-by (cases S) (auto intro:fun_in_rep_le)
+lemma mono_rep_u:
+  "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'"
+by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f)
 
-lemma in_rep_up_iff: "x <:up u \<longleftrightarrow> (\<exists>u'. u = Up u' \<and> x <:f u')"
+lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'"
+by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u)
+
+lemma in_rep_up_iff: "x : rep_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
 by (cases u) auto
 
-lemma in_rep_Top_fun: "s <:f \<top>"
-by(simp add: rep_st_def lookup_def Top_st_def)
-
-lemma in_rep_Top_up: "s <:up \<top>"
-by(simp add: Top_up_def in_rep_Top_fun)
-
 end
 
 end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Collecting.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Collecting.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,180 @@
+theory Collecting
+imports Complete_Lattice_ix ACom
+begin
+
+subsection "Collecting Semantics of Commands"
+
+subsubsection "Annotated commands as a complete lattice"
+
+(* Orderings could also be lifted generically (thus subsuming the
+instantiation for preord and order), but then less_eq_acom would need to
+become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would
+need to unfold this defn first. *)
+
+instantiation acom :: (order) order
+begin
+
+fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"less_eq_acom (SKIP {S}) (SKIP {S'}) = (S \<le> S')" |
+"less_eq_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
+"less_eq_acom (c1;c2) (c1';c2') = (less_eq_acom c1 c1' \<and> less_eq_acom c2 c2')" |
+"less_eq_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
+  (b=b' \<and> less_eq_acom c1 c1' \<and> less_eq_acom c2 c2' \<and> S \<le> S')" |
+"less_eq_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
+  (b=b' \<and> less_eq_acom c c' \<and> Inv \<le> Inv' \<and> P \<le> P')" |
+"less_eq_acom _ _ = False"
+
+lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
+by (cases c) auto
+
+lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
+by (cases c) auto
+
+lemma Semi_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
+by (cases c) auto
+
+lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
+  (\<exists>c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')"
+by (cases c) auto
+
+lemma While_le: "{Inv} WHILE b DO c {P} \<le> w \<longleftrightarrow>
+  (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')"
+by (cases w) auto
+
+definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
+
+instance
+proof
+  case goal1 show ?case by(simp add: less_acom_def)
+next
+  case goal2 thus ?case by (induct x) auto
+next
+  case goal3 thus ?case
+  apply(induct x y arbitrary: z rule: less_eq_acom.induct)
+  apply (auto intro: le_trans simp: SKIP_le Assign_le Semi_le If_le While_le)
+  done
+next
+  case goal4 thus ?case
+  apply(induct x y rule: less_eq_acom.induct)
+  apply (auto intro: le_antisym)
+  done
+qed
+
+end
+
+fun lift :: "('a set set \<Rightarrow> 'a set) \<Rightarrow> com \<Rightarrow> 'a set acom set \<Rightarrow> 'a set acom"
+where
+"lift F com.SKIP M = (SKIP {F {P. SKIP {P} : M}})" |
+"lift F (x ::= a) M = (x ::= a {F {P. x::=a {P} : M}})" |
+"lift F (c1;c2) M =
+  (lift F c1 {c1. \<exists>c2. c1;c2 : M}); (lift F c2 {c2. \<exists>c1. c1;c2 : M})" |
+"lift F (IF b THEN c1 ELSE c2) M =
+  IF b THEN lift F c1 {c1. \<exists>c2 P. IF b THEN c1 ELSE c2 {P} : M}
+       ELSE lift F c2 {c2. \<exists>c1 P. IF b THEN c1 ELSE c2 {P} : M}
+  {F {P. \<exists>c1 c2. IF b THEN c1 ELSE c2 {P} : M}}" |
+"lift F (WHILE b DO c) M =
+ {F {I. \<exists>c P. {I} WHILE b DO c {P} : M}}
+ WHILE b DO lift F c {c. \<exists>I P. {I} WHILE b DO c {P} : M}
+ {F {P. \<exists>I c. {I} WHILE b DO c {P} : M}}"
+
+interpretation Complete_Lattice_ix strip "lift Inter"
+proof
+  case goal1
+  have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
+  proof(induction a arbitrary: A)
+    case Semi from Semi.prems show ?case by(fastforce intro!: Semi.IH)
+  next
+    case If from If.prems show ?case by(fastforce intro!: If.IH)
+  next
+    case While from While.prems show ?case by(fastforce intro!: While.IH)
+  qed auto
+  with goal1 show ?case by auto
+next
+  case goal2
+  thus ?case
+  proof(induction b arbitrary: i A)
+    case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
+  next
+    case If from If.prems show ?case by (fastforce intro!: If.IH)
+  next
+    case While from While.prems show ?case by(fastforce intro: While.IH)
+  qed fastforce+
+next
+  case goal3
+  thus ?case
+  proof(induction i arbitrary: A)
+    case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
+  next
+    case If from If.prems show ?case by (fastforce intro!: If.IH)
+  next
+    case While from While.prems show ?case by(fastforce intro: While.IH)
+  qed auto
+qed
+
+lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
+by(induction c d rule: less_eq_acom.induct) auto
+
+lemma le_strip: "c \<le> d \<Longrightarrow> strip c = strip d"
+by(induction c d rule: less_eq_acom.induct) auto
+
+lemma le_SKIP_iff: "c \<le> SKIP {P'} \<longleftrightarrow> (EX P. c = SKIP {P} \<and> P \<le> P')"
+by (cases c) simp_all
+
+lemma le_Assign_iff: "c \<le> x::=e {P'} \<longleftrightarrow> (EX P. c = x::=e {P} \<and> P \<le> P')"
+by (cases c) simp_all
+
+lemma le_Semi_iff: "c \<le> d1;d2 \<longleftrightarrow> (EX c1 c2. c = c1;c2 \<and> c1 \<le> d1 \<and> c2 \<le> d2)"
+by (cases c) simp_all
+
+lemma le_If_iff: "c \<le> IF b THEN d1 ELSE d2 {P'} \<longleftrightarrow>
+  (EX c1 c2 P. c = IF b THEN c1 ELSE c2 {P} \<and> c1 \<le> d1 \<and> c2 \<le> d2 \<and> P \<le> P')"
+by (cases c) simp_all
+
+lemma le_While_iff: "c \<le> {I'} WHILE b DO d {P'} \<longleftrightarrow>
+  (EX I c' P. c = {I} WHILE b DO c' {P} \<and> I \<le> I' \<and> c' \<le> d \<and> P \<le> P')"
+by (cases c) auto
+
+
+subsubsection "Collecting semantics"
+
+fun step_cs :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
+"step_cs S (SKIP {P}) = (SKIP {S})" |
+"step_cs S (x ::= e {P}) =
+  (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
+"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
+"step_cs S (IF b THEN c1 ELSE c2 {P}) =
+   IF b THEN step_cs {s:S. bval b s} c1 ELSE step_cs {s:S. \<not> bval b s} c2
+   {post c1 \<union> post c2}" |
+"step_cs S ({Inv} WHILE b DO c {P}) =
+  {S \<union> post c} WHILE b DO (step_cs {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
+
+definition CS :: "state set \<Rightarrow> com \<Rightarrow> state set acom" where
+"CS S c = lfp c (step_cs S)"
+
+lemma mono_step_cs_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step_cs S x \<le> step_cs T y"
+proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
+  case 2 thus ?case by fastforce
+next
+  case 3 thus ?case by(simp add: le_post)
+next
+  case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+
+next
+  case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
+qed auto
+
+lemma mono_step_cs: "mono (step_cs S)"
+by(blast intro: monoI mono_step_cs_aux)
+
+lemma strip_step_cs: "strip(step_cs S c) = strip c"
+by (induction c arbitrary: S) auto
+
+lemmas lfp_cs_unfold = lfp_unfold[OF strip_step_cs mono_step_cs]
+
+lemma CS_unfold: "CS S c = step_cs S (CS S c)"
+by (metis CS_def lfp_cs_unfold)
+
+lemma strip_CS[simp]: "strip(CS S c) = c"
+by(simp add: CS_def)
+
+end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Collecting1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Collecting1.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,225 @@
+theory Collecting1
+imports Collecting
+begin
+
+subsection "A small step semantics on annotated commands"
+
+text{* The idea: the state is propagated through the annotated command as an
+annotation @{term "Some s"}, all other annotations are @{const None}. *}
+
+fun join :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" where
+"join None x = x" |
+"join x None = x"
+
+definition bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> state option \<Rightarrow> state option" where
+"bfilter b r so =
+  (case so of None \<Rightarrow> None | Some s \<Rightarrow> if bval b s = r then Some s else None)"
+
+lemma bfilter_None[simp]: "bfilter b r None = None"
+by(simp add: bfilter_def split: option.split)
+
+fun step1 :: "state option \<Rightarrow> state option acom \<Rightarrow> state option acom" where
+"step1 so (SKIP {P}) = SKIP {so}" |
+"step1 so (x::=e {P}) =
+  x ::= e {case so of None \<Rightarrow> None | Some s \<Rightarrow> Some(s(x := aval e s))}" |
+"step1 so (c1;c2) = step1 so c1; step1 (post c1) c2" |
+"step1 so (IF b THEN c1 ELSE c2 {P}) =
+  IF b THEN step1 (bfilter b True so) c1
+  ELSE step1 (bfilter b False so) c2
+  {join (post c1) (post c2)}" |
+"step1 so ({I} WHILE b DO c {P}) =
+  {join so (post c)}
+  WHILE b DO step1 (bfilter b True I) c
+  {bfilter b False I}"
+
+definition "show_acom xs = map_acom (Option.map (show_state xs))"
+
+definition
+ "p1 = ''x'' ::= N 2; IF Less (V ''x'') (N 3) THEN ''x'' ::= N 1 ELSE com.SKIP"
+
+definition "p2 =
+ ''x'' ::= N 0; WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+value "show_acom [''x'']
+ (((step1 None)^^6) (step1 (Some <>) (anno None p2)))"
+
+subsubsection "Relating the small step and the collecting semantics"
+
+hide_const (open) set
+
+abbreviation set :: "'a option acom \<Rightarrow> 'a set acom" where
+"set == map_acom Option.set"
+
+definition some :: "'a option \<Rightarrow> nat" where
+"some opt = (case opt of Some x \<Rightarrow> 1 | None \<Rightarrow> 0)"
+
+lemma some[simp]: "some None = 0 \<and> some (Some x) = 1"
+by(simp add: some_def split:option.split)
+
+fun somes :: "'a option acom \<Rightarrow> nat" where
+"somes(SKIP {p}) = some p" |
+"somes(x::=e {p}) = some p" |
+"somes(c1;c2) = somes c1 + somes c2" |
+"somes(IF b THEN c1 ELSE c2 {p}) = somes c1 + somes c2 + some p" |
+"somes({i} WHILE b DO c {p}) = some i + somes c + some p"
+
+lemma some_anno_None: "somes(anno None c) = 0"
+by(induction c) auto
+
+lemma some_post: "some(post co) \<le> somes co"
+by(induction co) auto
+
+lemma some_join:
+  "some so1 + some so2 \<le> 1 \<Longrightarrow> some(join so1 so2) = some so1 + some so2"
+by(simp add: some_def split: option.splits)
+
+lemma somes_step1: "some so + somes co \<le> 1 \<Longrightarrow>
+ somes(step1 so co) + some(post co) = some so + somes co"
+proof(induction co arbitrary: so)
+  case SKIP thus ?case by simp
+next
+  case Assign thus ?case by (simp split:option.split)
+next
+  case (Semi co1 _)
+  from Semi.prems Semi.IH(1)[of so] Semi.IH(2)[of "post co1"]
+  show ?case by simp
+next
+  case (If b)
+  from If.prems If.IH(1)[of "bfilter b True so"]
+       If.prems If.IH(2)[of "bfilter b False so"]
+  show ?case
+    by (auto simp: bfilter_def some_join split:option.split)
+next
+  case (While i b c p)
+  from While.prems While.IH[of "bfilter b True i"]
+  show ?case
+    by(auto simp: bfilter_def some_join split:option.split)
+qed
+
+lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
+by(induction c) auto
+
+lemma join_eq_Some: "some so1 + some so2 \<le> 1 \<Longrightarrow>
+  join so1 so2 = Some s =
+ (so1 = Some s & so2 = None | so1 = None & so2 = Some s)"
+apply(cases so1) apply simp
+apply(cases so2) apply auto
+done
+
+lemma set_bfilter:
+  "Option.set (bfilter b r so) = {s : Option.set so. bval b s = r}"
+by(auto simp: bfilter_def split: option.splits)
+
+lemma set_join:  "some so1 + some so2 \<le> 1 \<Longrightarrow>
+  Option.set (join so1 so2) = Option.set so1 \<union> Option.set so2"
+apply(cases so1) apply simp
+apply(cases so2) apply auto
+done
+
+lemma add_le1_iff: "m + n \<le> (Suc 0) \<longleftrightarrow> (m=0 \<and> n\<le>1 | m\<le>1 & n=0)"
+by arith
+
+lemma some_0_iff: "some opt = 0 \<longleftrightarrow> opt = None"
+by(auto simp add: some_def split: option.splits)
+
+lemma some_le1[simp]: "some x \<le> Suc 0"
+by(auto simp add: some_def split: option.splits)
+
+lemma step1_preserves_le:
+  "\<lbrakk> step_cs S cs = cs; Option.set so \<subseteq> S; set co \<le> cs;
+    somes co + some so \<le> 1 \<rbrakk> \<Longrightarrow>
+  set(step1 so co) \<le> cs"
+proof(induction co arbitrary: S cs so)
+  case SKIP thus ?case by (clarsimp simp: SKIP_le)
+next
+  case Assign thus ?case by (fastforce simp: Assign_le split: option.splits)
+next
+  case (Semi co1 co2)
+  from Semi.prems show ?case using some_post[of co1]
+    by (fastforce simp add: Semi_le add_le1_iff Semi.IH dest: le_post)
+next
+  case (If _ co1 co2)
+  from If.prems show ?case
+    using some_post[of co1] some_post[of co2]
+    by (fastforce simp: If_le add_le1_iff some_0_iff set_bfilter subset_iff
+      join_eq_Some If.IH dest: le_post)
+next
+  case (While _ _ co)
+  from While.prems show ?case
+    using some_post[of co]
+    by (fastforce simp: While_le set_bfilter subset_iff join_eq_Some
+      add_le1_iff some_0_iff While.IH dest: le_post)
+qed
+
+lemma step1_None_preserves_le:
+  "\<lbrakk> step_cs S cs = cs; set co \<le> cs; somes co \<le> 1 \<rbrakk> \<Longrightarrow>
+  set(step1 None co) \<le> cs"
+by(auto dest: step1_preserves_le[of _ _ None])
+
+lemma step1_Some_preserves_le:
+  "\<lbrakk> step_cs S cs = cs; s : S; set co \<le> cs; somes co = 0 \<rbrakk> \<Longrightarrow>
+  set(step1 (Some s) co) \<le> cs"
+by(auto dest: step1_preserves_le[of _ _ "Some s"])
+
+lemma steps_None_preserves_le: assumes "step_cs S cs = cs"
+shows "set co \<le> cs \<Longrightarrow> somes co \<le> 1 \<Longrightarrow> set ((step1 None ^^ n) co) \<le> cs"
+proof(induction n arbitrary: co)
+  case 0 thus ?case by simp
+next
+  case (Suc n) thus ?case
+    using somes_step1[of None co] step1_None_preserves_le[OF assms Suc.prems]
+    by(simp add:funpow_swap1 Suc.IH)
+qed
+
+
+definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state option acom" where
+"steps s c n = ((step1 None)^^n) (step1 (Some s) (anno None c))"
+
+lemma steps_approx_fix_step_cs: assumes "step_cs S cs = cs" and "s:S"
+shows "set (steps s (strip cs) n) \<le> cs"
+proof-
+  { fix c have "somes (anno None c) = 0" by(induction c) auto }
+  note somes_None = this
+  let ?cNone = "anno None (strip cs)"
+  have "set ?cNone \<le> cs" by(induction cs) auto
+  from step1_Some_preserves_le[OF assms this somes_None]
+  have 1: "set(step1 (Some s) ?cNone) \<le> cs" .
+  have 2: "somes (step1 (Some s) ?cNone) \<le> 1"
+    using some_post somes_step1[of "Some s" ?cNone]
+    by (simp add:some_anno_None[of "strip cs"])
+  from steps_None_preserves_le[OF assms(1) 1 2]
+  show ?thesis by(simp add: steps_def)
+qed
+
+theorem steps_approx_CS: "s:S \<Longrightarrow> set (steps s c n) \<le> CS S c"
+by (metis CS_unfold steps_approx_fix_step_cs strip_CS)
+
+lemma While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
+by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
+
+lemma step_cs_complete:
+  "\<lbrakk> step_cs S c = c; (strip c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post c"
+proof(induction c arbitrary: S s t)
+  case (While Inv b c P)
+  from While.prems have inv: "step_cs {s:Inv. bval b s} c = c"
+    and "post c \<subseteq> Inv" and "S \<subseteq> Inv" and "{s:Inv. \<not> bval b s} \<subseteq> P"  by(auto)
+  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s : Inv \<Longrightarrow> t : Inv"
+    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
+      case WhileFalse thus ?case by simp
+    next
+      case (WhileTrue s1 s2 s3)
+      from WhileTrue.hyps(5) While.IH[OF inv `(strip c, s1) \<Rightarrow> s2`]
+        `s1 : Inv` `post c \<subseteq> Inv` `bval b s1`
+      show ?case by auto
+    qed
+  } note Inv = this
+  from  While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
+    by(auto dest: While_final_False)
+  from Inv[OF this(1)] `s : S` `S \<subseteq> Inv` have "t : Inv" by blast
+  with `{s:Inv. \<not> bval b s} \<subseteq> P` show ?case using `\<not> bval b t` by auto
+qed auto
+
+theorem CS_complete: "\<lbrakk> (c,s) \<Rightarrow> t; s:S \<rbrakk> \<Longrightarrow> t : post(CS S c)"
+by (metis CS_unfold step_cs_complete strip_CS)
+
+end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Collecting_list.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Collecting_list.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,25 @@
+theory Collecting_list
+imports ACom
+begin
+
+subsection "Executable Collecting Semantics on lists"
+
+fun step_cs :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where
+"step_cs S (SKIP {P}) = (SKIP {S})" |
+"step_cs S (x ::= e {P}) =
+  (x ::= e {[s(x := aval e s). s \<leftarrow> S]})" |
+"step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" |
+"step_cs S (IF b THEN c1 ELSE c2 {P}) =
+   IF b THEN step_cs [s \<leftarrow> S. bval b s] c1 ELSE step_cs [s\<leftarrow>S. \<not> bval b s] c2
+   {post c1 @ post c2}" |
+"step_cs S ({Inv} WHILE b DO c {P}) =
+  {S @ post c} WHILE b DO (step_cs [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
+
+definition "c = WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
+definition "c0 = anno [] c"
+
+definition "show_acom xs = map_acom (map (show_state xs))"
+
+value "show_acom [''x''] (((step_cs [<>]) ^^ 6) c0)"
+
+end
diff -r 4334c91b7405 -r f682f3f7b726 src/HOL/IMP/Complete_Lattice_ix.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Complete_Lattice_ix.thy	Thu Nov 24 19:58:37 2011 +0100
@@ -0,0 +1,55 @@
+theory Complete_Lattice_ix
+imports Main
+begin
+
+text{* A complete lattice is an ordered type where every set of elements has
+a greatest lower (and thus also a leats upper) bound. Sets are the
+prototypical complete lattice where the greatest lower bound is
+intersection. Sometimes that set of all elements of a type is not a complete
+lattice although all elements of the same shape form a complete lattice, for
+example lists of the same length, where the list elements come from a
+complete lattice. We will have exactly this situation with annotated
+commands. This theory introduces a slightly generalised version of complete
+lattices where elements have an ``index'' and only the set of elements with
+the same index form a complete lattice; the type as a whole is a disjoint
+union of complete lattices. Because sets are not types, this requires a
+special treatment. *}
+
+locale Complete_Lattice_ix =
+fixes ix :: "'a::order \<Rightarrow> 'i"
+and Glb :: "'i \<Rightarrow> 'a set \<Rightarrow> 'a"
+assumes Glb_lower: "\<forall>a\<in>A. ix a = i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a"
+and Glb_greatest: "\<forall>a\<in>A. b \<le> a \<Longrightarrow> ix b = i \<Longrightarrow> b \<le> (Glb i A)"
+and ix_Glb: "\<forall>a\<in>A. ix a = i \<Longrightarrow> ix(Glb i A) = i"
+begin
+
+definition lfp :: "'i \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
+"lfp i f = Glb i {a. ix a = i \<and> f a \<le> a}"
+
+lemma index_lfp[simp]: "ix(lfp i f) = i"
+by(simp add: lfp_def ix_Glb)
+
+lemma lfp_lowerbound:
+  "\<lbrakk> ix a = i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp i f \<le> a"
+by (auto simp add: lfp_def intro: Glb_lower)
+
+lemma lfp_greatest:
+  "\<lbrakk> ix a = i;  \<And>u. \<lbrakk>ix u = i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp i f"
+by (auto simp add: lfp_def intro: Glb_greatest)
+
+lemma lfp_unfold: assumes "\<And>x. ix(f x) = ix x"
+and mono: "mono f" shows "lfp i f = f (lfp i f)"
+proof-
+  note assms(1)[simp]
+  have 1: "f (lfp i f) \<le> lfp i f"
+    apply(rule lfp_greatest)
+    apply(simp)
+    by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
+  have "lfp i f \<le> f (lfp i f)"
+    by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
+  with 1 show ?thesis by(blast intro: order_antisym)
+qed
+
+end
+
+end