# HG changeset patch
# User nipkow
# Date 1360666469 -3600
# Node ID e7b54119c436cb3aa07e0976fa20dc87031e7a74
# Parent  36aee533d7a772fcda4a83916f5a8c60dad754b5
tuned top

diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -242,9 +242,8 @@
   and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
 fixes num' :: "val \<Rightarrow> 'av"
 and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
-  assumes gamma_num': "i : \<gamma>(num' i)"
-  and gamma_plus':
- "i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma>(plus' a1 a2)"
+  assumes gamma_num': "i \<in> \<gamma>(num' i)"
+  and gamma_plus': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1+i2 \<in> \<gamma>(plus' a1 a2)"
 
 type_synonym 'av st = "(vname \<Rightarrow> 'av)"
 
@@ -263,7 +262,8 @@
   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 {P1} C1 ELSE {P2} C2 {Q}) =
-   IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2}" |
+   IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
+   {post C1 \<squnion> post C2}" |
 "step' S ({I} WHILE b DO {P} C {Q}) =
   {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
 
@@ -290,8 +290,6 @@
 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_s: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
 by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
 
diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -71,7 +71,7 @@
    {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' (top c)) (bot c)"
+"AI c = pfp (step' (top(vars c))) (bot c)"
 
 
 lemma strip_step'[simp]: "strip(step' S C) = strip C"
@@ -110,21 +110,21 @@
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
-  assume 1: "pfp (step' (top c)) (bot c) = Some C"
+  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
   have "C \<in> L(vars c)"
     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
       (erule step'_in_L[OF _ top_in_L])
-  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
-  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   proof(rule order_trans)
-    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
+    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
       by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
-    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
+    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
       by(rule mono_gamma_c[OF pfp'])
   qed
   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
-  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
-    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
+  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
@@ -153,8 +153,8 @@
             split: option.split)
 done
 
-lemma mono_step'_top: "C \<in> L(vars c) \<Longrightarrow> C' \<in> L(vars c) \<Longrightarrow>
-  C \<sqsubseteq> C' \<Longrightarrow> step' (top c) C \<sqsubseteq> step' (top c) C'"
+lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
+  C \<sqsubseteq> C' \<Longrightarrow> step' (top X) C \<sqsubseteq> step' (top X) C'"
 by (metis top_in_L mono_step' preord_class.le_refl)
 
 lemma pfp_bot_least:
@@ -167,7 +167,7 @@
 by (simp_all add: assms(4,5) bot_least)
 
 lemma AI_least_pfp: assumes "AI c = Some C"
-and "step' (top c) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
+and "step' (top(vars c)) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
 shows "C \<sqsubseteq> C'"
 apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
 by (simp_all add: mono_step'_top)
diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -74,7 +74,7 @@
 
 subsubsection "Tests"
 
-definition "steps c i = (step_const(top c) ^^ i) (bot c)"
+definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)"
 
 value "show_acom (steps test1_const 0)"
 value "show_acom (steps test1_const 1)"
diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -127,7 +127,7 @@
   ''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)"
+definition "steps c i = (step_parity(top(vars c)) ^^ i) (bot c)"
 
 value "show_acom (steps test2_parity 0)"
 value "show_acom (steps test2_parity 1)"
diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -55,11 +55,11 @@
 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' i a = (i : \<gamma> a)"
+assumes test_num': "test_num' n a = (n : \<gamma> a)"
 and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
-  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma> a \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
-and filter_less': "filter_less' (i1<i2) a1 a2 = (b1,b2) \<Longrightarrow>
-  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
+  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 =
@@ -80,13 +80,13 @@
 subsubsection "Backward analysis"
 
 fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
-"afilter (N i) a S = (if test_num' i a then S else None)" |
+"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 (a\<^isub>1',a\<^isub>2') = filter_plus' a (aval'' e1 S) (aval'' e2 S)
-  in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' 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
@@ -105,8 +105,8 @@
   (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 (a\<^isub>1',a\<^isub>2') = filter_less' res (aval'' e1 S) (aval'' e2 S)
-   in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
+  (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
+   in afilter e1 res1 (afilter e2 res2 S))"
 
 lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
 by(induction e arbitrary: a S)
@@ -167,7 +167,7 @@
    {bfilter b False I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' \<top>\<^bsub>c\<^esub>) (bot c)"
+"AI c = pfp (step' \<top>\<^bsub>vars c\<^esub>) (bot c)"
 
 lemma strip_step'[simp]: "strip(step' S c) = strip c"
 by(induct c arbitrary: S) (simp_all add: Let_def)
@@ -209,21 +209,21 @@
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
-  assume 1: "pfp (step' (top c)) (bot c) = Some C"
+  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
   have "C \<in> L(vars c)"
     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
       (erule step'_in_L[OF _ top_in_L])
-  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
-  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   proof(rule order_trans)
-    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
+    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
       by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
-    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
+    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
       by(rule mono_gamma_c[OF pfp'])
   qed
   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
-  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
-    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
+  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
@@ -281,8 +281,8 @@
             split: option.split)
 done
 
-lemma mono_step'_top: "C1 \<in> L(vars c) \<Longrightarrow> C2 \<in> L(vars c) \<Longrightarrow>
-  C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top c) C1 \<sqsubseteq> step' (top c) C2"
+lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
+  C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"
 by (metis top_in_L mono_step' preord_class.le_refl)
 
 end
diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -248,27 +248,25 @@
 
 subsubsection "Tests"
 
-value "show_acom (the(AI_ivl test1_ivl))"
+value "show_acom_opt (AI_ivl test1_ivl)"
 
 text{* Better than @{text AI_const}: *}
-value "show_acom (the(AI_ivl test3_const))"
-value "show_acom (the(AI_ivl test4_const))"
-value "show_acom (the(AI_ivl test6_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)"
+definition "steps c i = (step_ivl(top(vars c)) ^^ i) (bot c)"
 
-value "test2_ivl"
-value "show_acom (the(AI_ivl test2_ivl))"
+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)"
 value "show_acom (steps test2_ivl 3)"
 
-text{* Fixed point reached in 3 steps.
+text{* Fixed point reached in 2 steps.
  Not so if the start value of x is known: *}
 
-value "test3_ivl"
-value "show_acom (the(AI_ivl test3_ivl))"
+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)"
@@ -281,15 +279,12 @@
 the actual execution terminates, the analysis may not. The value of y keeps
 decreasing as the analysis is iterated, no matter how long: *}
 
-value "test4_ivl"
 value "show_acom (steps test4_ivl 50)"
 
 text{* Relationships between variables are NOT captured: *}
-value "test5_ivl"
-value "show_acom (the(AI_ivl test5_ivl))"
+value "show_acom_opt (AI_ivl test5_ivl)"
 
 text{* Again, the analysis would not terminate: *}
-value "test6_ivl"
 value "show_acom (steps test6_ivl 50)"
 
 end
diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -358,24 +358,24 @@
 begin
 
 definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
-"AI_wn c = pfp_wn (step' (top c)) (bot c)"
+"AI_wn c = pfp_wn (step' (top(vars c))) (bot 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)) (bot c) = Some C"
-  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
+  assume 1: "pfp_wn (step' (top(vars c))) (bot c) = Some C"
+  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<sqsubseteq> C"
     by(rule pfp_wn_pfp[where x="bot c"])
       (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
-  have pfp: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+  have pfp: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   proof(rule order_trans)
-    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
+    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
       by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
     show "... \<le> \<gamma>\<^isub>c C"
       by(rule mono_gamma_c[OF conjunct2[OF 2]])
   qed
   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
-  have "lfp c (step (\<gamma>\<^isub>o (top c))) \<le> \<gamma>\<^isub>c C"
-    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 pfp])
+  have "lfp c (step (\<gamma>\<^isub>o (top(vars c)))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 pfp])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
@@ -396,9 +396,9 @@
 by(rule refl)
 
 definition "step_up_ivl n =
-  ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)"
+  ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
 definition "step_down_ivl n =
-  ((\<lambda>C. C \<triangle> step_ivl (top (strip C)) C)^^n)"
+  ((\<lambda>C. C \<triangle> step_ivl (top(vars(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
@@ -416,14 +416,14 @@
 value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
 value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
 value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
-value "show_acom (the(AI_ivl' test3_ivl))"
+value "show_acom_opt (AI_ivl' test3_ivl)"
 
 
 text{* Now all the analyses terminate: *}
 
-value "show_acom (the(AI_ivl' test4_ivl))"
-value "show_acom (the(AI_ivl' test5_ivl))"
-value "show_acom (the(AI_ivl' test6_ivl))"
+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"
@@ -629,14 +629,14 @@
 
 
 lemma iter_winden_step_ivl_termination:
-  "\<exists>C. iter_widen (step_ivl (top c)) (bot c) = Some C"
+  "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
 apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
 apply (simp_all add: step'_in_Lc m_c_widen)
 done
 
 lemma iter_narrow_step_ivl_termination:
-  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top c) C0 \<sqsubseteq> C0 \<Longrightarrow>
-  \<exists>C. iter_narrow (step_ivl (top c)) C0 = Some C"
+  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
+  \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
 apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
 apply (simp add: step'_in_Lc)
 apply (simp)
@@ -654,7 +654,7 @@
 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. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>c\<^esub>" and c=c, simplified])
+apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>vars c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>vars c\<^esub>" and c=c, simplified])
 apply(erule iter_widen_pfp)
 done
 
diff -r 36aee533d7a7 -r e7b54119c436 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Mon Feb 11 11:38:16 2013 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Tue Feb 12 11:54:29 2013 +0100
@@ -60,12 +60,12 @@
 end
 
 class semilatticeL = join + L +
-fixes top :: "com \<Rightarrow> 'a"
+fixes top :: "vname set \<Rightarrow> 'a"
 assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
 and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
 and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<in> L(vars c) \<Longrightarrow> x \<sqsubseteq> top c"
-and top_in_L[simp]: "top c \<in> L(vars c)"
+and top[simp]: "x \<in> L X \<Longrightarrow> x \<sqsubseteq> top X"
+and top_in_L[simp]: "top X \<in> L X"
 and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
 
 notation (input) top ("\<top>\<^bsub>_\<^esub>")
@@ -109,6 +109,7 @@
 value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
 
 definition "show_acom = map_acom (Option.map show_st)"
+definition "show_acom_opt = Option.map show_acom"
 
 definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
 
@@ -157,7 +158,7 @@
 instantiation st :: (semilattice) semilatticeL
 begin
 
-definition top_st where "top c = FunDom (\<lambda>x. \<top>) (vars c)"
+definition top_st where "top X = FunDom (\<lambda>x. \<top>) X"
 
 instance
 proof
@@ -200,8 +201,6 @@
 lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
 by (simp add: top_option_def)
 
-(* FIXME (maybe also le \<rightarrow> sqle?) *)
-
 lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
 apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
 by (metis mono_gamma subsetD)