1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Mon Feb 11 11:38:16 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Tue Feb 12 11:54:29 2013 +0100
     1.3 @@ -242,9 +242,8 @@
     1.4    and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
     1.5  fixes num' :: "val \<Rightarrow> 'av"
     1.6  and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
     1.7 -  assumes gamma_num': "i : \<gamma>(num' i)"
     1.8 -  and gamma_plus':
     1.9 - "i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma>(plus' a1 a2)"
    1.10 +  assumes gamma_num': "i \<in> \<gamma>(num' i)"
    1.11 +  and gamma_plus': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1+i2 \<in> \<gamma>(plus' a1 a2)"
    1.12  
    1.13  type_synonym 'av st = "(vname \<Rightarrow> 'av)"
    1.14  
    1.15 @@ -263,7 +262,8 @@
    1.16    x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" |
    1.17  "step' S (C1; C2) = step' S C1; step' (post C1) C2" |
    1.18  "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
    1.19 -   IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2}" |
    1.20 +   IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
    1.21 +   {post C1 \<squnion> post C2}" |
    1.22  "step' S ({I} WHILE b DO {P} C {Q}) =
    1.23    {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
    1.24  
    1.25 @@ -290,8 +290,6 @@
    1.26  lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
    1.27  by (simp add: Top_option_def)
    1.28  
    1.29 -(* FIXME (maybe also le \<rightarrow> sqle?) *)
    1.30 -
    1.31  lemma mono_gamma_s: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
    1.32  by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
    1.33  

     2.1 --- a/src/HOL/IMP/Abs_Int1.thy	Mon Feb 11 11:38:16 2013 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Tue Feb 12 11:54:29 2013 +0100
     2.3 @@ -71,7 +71,7 @@
     2.4     {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
     2.5  
     2.6  definition AI :: "com \<Rightarrow> 'av st option acom option" where
     2.7 -"AI c = pfp (step' (top c)) (bot c)"
     2.8 +"AI c = pfp (step' (top(vars c))) (bot c)"
     2.9  
    2.10  
    2.11  lemma strip_step'[simp]: "strip(step' S C) = strip C"
    2.12 @@ -110,21 +110,21 @@
    2.13  
    2.14  lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    2.15  proof(simp add: CS_def AI_def)
    2.16 -  assume 1: "pfp (step' (top c)) (bot c) = Some C"
    2.17 +  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
    2.18    have "C \<in> L(vars c)"
    2.19      by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
    2.20        (erule step'_in_L[OF _ top_in_L])
    2.21 -  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    2.22 -  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    2.23 +  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    2.24 +  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    2.25    proof(rule order_trans)
    2.26 -    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
    2.27 +    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
    2.28        by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
    2.29 -    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
    2.30 +    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
    2.31        by(rule mono_gamma_c[OF pfp'])
    2.32    qed
    2.33    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
    2.34 -  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
    2.35 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
    2.36 +  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
    2.37 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
    2.38    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    2.39  qed
    2.40  
    2.41 @@ -153,8 +153,8 @@
    2.42              split: option.split)
    2.43  done
    2.44  
    2.45 -lemma mono_step'_top: "C \<in> L(vars c) \<Longrightarrow> C' \<in> L(vars c) \<Longrightarrow>
    2.46 -  C \<sqsubseteq> C' \<Longrightarrow> step' (top c) C \<sqsubseteq> step' (top c) C'"
    2.47 +lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
    2.48 +  C \<sqsubseteq> C' \<Longrightarrow> step' (top X) C \<sqsubseteq> step' (top X) C'"
    2.49  by (metis top_in_L mono_step' preord_class.le_refl)
    2.50  
    2.51  lemma pfp_bot_least:
    2.52 @@ -167,7 +167,7 @@
    2.53  by (simp_all add: assms(4,5) bot_least)
    2.54  
    2.55  lemma AI_least_pfp: assumes "AI c = Some C"
    2.56 -and "step' (top c) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
    2.57 +and "step' (top(vars c)) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
    2.58  shows "C \<sqsubseteq> C'"
    2.59  apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
    2.60  by (simp_all add: mono_step'_top)

     3.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Feb 11 11:38:16 2013 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Feb 12 11:54:29 2013 +0100
     3.3 @@ -74,7 +74,7 @@
     3.4  
     3.5  subsubsection "Tests"
     3.6  
     3.7 -definition "steps c i = (step_const(top c) ^^ i) (bot c)"
     3.8 +definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)"
     3.9  
    3.10  value "show_acom (steps test1_const 0)"
    3.11  value "show_acom (steps test1_const 1)"

     4.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Mon Feb 11 11:38:16 2013 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Tue Feb 12 11:54:29 2013 +0100
     4.3 @@ -127,7 +127,7 @@
     4.4    ''x'' ::= N 1;
     4.5    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
     4.6  
     4.7 -definition "steps c i = (step_parity(top c) ^^ i) (bot c)"
     4.8 +definition "steps c i = (step_parity(top(vars c)) ^^ i) (bot c)"
     4.9  
    4.10  value "show_acom (steps test2_parity 0)"
    4.11  value "show_acom (steps test2_parity 1)"

     5.1 --- a/src/HOL/IMP/Abs_Int2.thy	Mon Feb 11 11:38:16 2013 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Tue Feb 12 11:54:29 2013 +0100
     5.3 @@ -55,11 +55,11 @@
     5.4  fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
     5.5  and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
     5.6  and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
     5.7 -assumes test_num': "test_num' i a = (i : \<gamma> a)"
     5.8 +assumes test_num': "test_num' n a = (n : \<gamma> a)"
     5.9  and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
    5.10 -  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma> a \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
    5.11 -and filter_less': "filter_less' (i1<i2) a1 a2 = (b1,b2) \<Longrightarrow>
    5.12 -  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
    5.13 +  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
    5.14 +and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
    5.15 +  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
    5.16  
    5.17  
    5.18  locale Abs_Int1 =
    5.19 @@ -80,13 +80,13 @@
    5.20  subsubsection "Backward analysis"
    5.21  
    5.22  fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
    5.23 -"afilter (N i) a S = (if test_num' i a then S else None)" |
    5.24 +"afilter (N n) a S = (if test_num' n a then S else None)" |
    5.25  "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
    5.26    let a' = fun S x \<sqinter> a in
    5.27    if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
    5.28  "afilter (Plus e1 e2) a S =
    5.29 - (let (a\<^isub>1',a\<^isub>2') = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    5.30 -  in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
    5.31 + (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    5.32 +  in afilter e1 a1 (afilter e2 a2 S))"
    5.33  
    5.34  text{* The test for @{const bot} in the @{const V}-case is important: @{const
    5.35  bot} indicates that a variable has no possible values, i.e.\ that the current
    5.36 @@ -105,8 +105,8 @@
    5.37    (if res then bfilter b1 True (bfilter b2 True S)
    5.38     else bfilter b1 False S \<squnion> bfilter b2 False S)" |
    5.39  "bfilter (Less e1 e2) res S =
    5.40 -  (let (a\<^isub>1',a\<^isub>2') = filter_less' res (aval'' e1 S) (aval'' e2 S)
    5.41 -   in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
    5.42 +  (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
    5.43 +   in afilter e1 res1 (afilter e2 res2 S))"
    5.44  
    5.45  lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
    5.46  by(induction e arbitrary: a S)
    5.47 @@ -167,7 +167,7 @@
    5.48     {bfilter b False I}"
    5.49  
    5.50  definition AI :: "com \<Rightarrow> 'av st option acom option" where
    5.51 -"AI c = pfp (step' \<top>\<^bsub>c\<^esub>) (bot c)"
    5.52 +"AI c = pfp (step' \<top>\<^bsub>vars c\<^esub>) (bot c)"
    5.53  
    5.54  lemma strip_step'[simp]: "strip(step' S c) = strip c"
    5.55  by(induct c arbitrary: S) (simp_all add: Let_def)
    5.56 @@ -209,21 +209,21 @@
    5.57  
    5.58  lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    5.59  proof(simp add: CS_def AI_def)
    5.60 -  assume 1: "pfp (step' (top c)) (bot c) = Some C"
    5.61 +  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
    5.62    have "C \<in> L(vars c)"
    5.63      by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
    5.64        (erule step'_in_L[OF _ top_in_L])
    5.65 -  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    5.66 -  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    5.67 +  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    5.68 +  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    5.69    proof(rule order_trans)
    5.70 -    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
    5.71 +    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
    5.72        by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
    5.73 -    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
    5.74 +    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
    5.75        by(rule mono_gamma_c[OF pfp'])
    5.76    qed
    5.77    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
    5.78 -  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
    5.79 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
    5.80 +  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
    5.81 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
    5.82    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    5.83  qed
    5.84  
    5.85 @@ -281,8 +281,8 @@
    5.86              split: option.split)
    5.87  done
    5.88  
    5.89 -lemma mono_step'_top: "C1 \<in> L(vars c) \<Longrightarrow> C2 \<in> L(vars c) \<Longrightarrow>
    5.90 -  C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top c) C1 \<sqsubseteq> step' (top c) C2"
    5.91 +lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
    5.92 +  C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"
    5.93  by (metis top_in_L mono_step' preord_class.le_refl)
    5.94  
    5.95  end

     6.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Feb 11 11:38:16 2013 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Tue Feb 12 11:54:29 2013 +0100
     6.3 @@ -248,27 +248,25 @@
     6.4  
     6.5  subsubsection "Tests"
     6.6  
     6.7 -value "show_acom (the(AI_ivl test1_ivl))"
     6.8 +value "show_acom_opt (AI_ivl test1_ivl)"
     6.9  
    6.10  text{* Better than @{text AI_const}: *}
    6.11 -value "show_acom (the(AI_ivl test3_const))"
    6.12 -value "show_acom (the(AI_ivl test4_const))"
    6.13 -value "show_acom (the(AI_ivl test6_const))"
    6.14 +value "show_acom_opt (AI_ivl test3_const)"
    6.15 +value "show_acom_opt (AI_ivl test4_const)"
    6.16 +value "show_acom_opt (AI_ivl test6_const)"
    6.17  
    6.18 -definition "steps c i = (step_ivl(top c) ^^ i) (bot c)"
    6.19 +definition "steps c i = (step_ivl(top(vars c)) ^^ i) (bot c)"
    6.20  
    6.21 -value "test2_ivl"
    6.22 -value "show_acom (the(AI_ivl test2_ivl))"
    6.23 +value "show_acom_opt (AI_ivl test2_ivl)"
    6.24  value "show_acom (steps test2_ivl 0)"
    6.25  value "show_acom (steps test2_ivl 1)"
    6.26  value "show_acom (steps test2_ivl 2)"
    6.27  value "show_acom (steps test2_ivl 3)"
    6.28  
    6.29 -text{* Fixed point reached in 3 steps.
    6.30 +text{* Fixed point reached in 2 steps.
    6.31   Not so if the start value of x is known: *}
    6.32  
    6.33 -value "test3_ivl"
    6.34 -value "show_acom (the(AI_ivl test3_ivl))"
    6.35 +value "show_acom_opt (AI_ivl test3_ivl)"
    6.36  value "show_acom (steps test3_ivl 0)"
    6.37  value "show_acom (steps test3_ivl 1)"
    6.38  value "show_acom (steps test3_ivl 2)"
    6.39 @@ -281,15 +279,12 @@
    6.40  the actual execution terminates, the analysis may not. The value of y keeps
    6.41  decreasing as the analysis is iterated, no matter how long: *}
    6.42  
    6.43 -value "test4_ivl"
    6.44  value "show_acom (steps test4_ivl 50)"
    6.45  
    6.46  text{* Relationships between variables are NOT captured: *}
    6.47 -value "test5_ivl"
    6.48 -value "show_acom (the(AI_ivl test5_ivl))"
    6.49 +value "show_acom_opt (AI_ivl test5_ivl)"
    6.50  
    6.51  text{* Again, the analysis would not terminate: *}
    6.52 -value "test6_ivl"
    6.53  value "show_acom (steps test6_ivl 50)"
    6.54  
    6.55  end

     7.1 --- a/src/HOL/IMP/Abs_Int3.thy	Mon Feb 11 11:38:16 2013 +0100
     7.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Tue Feb 12 11:54:29 2013 +0100
     7.3 @@ -358,24 +358,24 @@
     7.4  begin
     7.5  
     7.6  definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
     7.7 -"AI_wn c = pfp_wn (step' (top c)) (bot c)"
     7.8 +"AI_wn c = pfp_wn (step' (top(vars c))) (bot c)"
     7.9  
    7.10  lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    7.11  proof(simp add: CS_def AI_wn_def)
    7.12 -  assume 1: "pfp_wn (step' (top c)) (bot c) = Some C"
    7.13 -  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
    7.14 +  assume 1: "pfp_wn (step' (top(vars c))) (bot c) = Some C"
    7.15 +  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<sqsubseteq> C"
    7.16      by(rule pfp_wn_pfp[where x="bot c"])
    7.17        (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
    7.18 -  have pfp: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    7.19 +  have pfp: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    7.20    proof(rule order_trans)
    7.21 -    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
    7.22 +    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
    7.23        by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
    7.24      show "... \<le> \<gamma>\<^isub>c C"
    7.25        by(rule mono_gamma_c[OF conjunct2[OF 2]])
    7.26    qed
    7.27    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
    7.28 -  have "lfp c (step (\<gamma>\<^isub>o (top c))) \<le> \<gamma>\<^isub>c C"
    7.29 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 pfp])
    7.30 +  have "lfp c (step (\<gamma>\<^isub>o (top(vars c)))) \<le> \<gamma>\<^isub>c C"
    7.31 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 pfp])
    7.32    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    7.33  qed
    7.34  
    7.35 @@ -396,9 +396,9 @@
    7.36  by(rule refl)
    7.37  
    7.38  definition "step_up_ivl n =
    7.39 -  ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)"
    7.40 +  ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
    7.41  definition "step_down_ivl n =
    7.42 -  ((\<lambda>C. C \<triangle> step_ivl (top (strip C)) C)^^n)"
    7.43 +  ((\<lambda>C. C \<triangle> step_ivl (top(vars(strip C))) C)^^n)"
    7.44  
    7.45  text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
    7.46  the loop took to execute. In contrast, @{const AI_ivl'} converges in a
    7.47 @@ -416,14 +416,14 @@
    7.48  value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
    7.49  value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
    7.50  value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
    7.51 -value "show_acom (the(AI_ivl' test3_ivl))"
    7.52 +value "show_acom_opt (AI_ivl' test3_ivl)"
    7.53  
    7.54  
    7.55  text{* Now all the analyses terminate: *}
    7.56  
    7.57 -value "show_acom (the(AI_ivl' test4_ivl))"
    7.58 -value "show_acom (the(AI_ivl' test5_ivl))"
    7.59 -value "show_acom (the(AI_ivl' test6_ivl))"
    7.60 +value "show_acom_opt (AI_ivl' test4_ivl)"
    7.61 +value "show_acom_opt (AI_ivl' test5_ivl)"
    7.62 +value "show_acom_opt (AI_ivl' test6_ivl)"
    7.63  
    7.64  
    7.65  subsubsection "Generic Termination Proof"
    7.66 @@ -629,14 +629,14 @@
    7.67  
    7.68  
    7.69  lemma iter_winden_step_ivl_termination:
    7.70 -  "\<exists>C. iter_widen (step_ivl (top c)) (bot c) = Some C"
    7.71 +  "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
    7.72  apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
    7.73  apply (simp_all add: step'_in_Lc m_c_widen)
    7.74  done
    7.75  
    7.76  lemma iter_narrow_step_ivl_termination:
    7.77 -  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top c) C0 \<sqsubseteq> C0 \<Longrightarrow>
    7.78 -  \<exists>C. iter_narrow (step_ivl (top c)) C0 = Some C"
    7.79 +  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
    7.80 +  \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
    7.81  apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
    7.82  apply (simp add: step'_in_Lc)
    7.83  apply (simp)
    7.84 @@ -654,7 +654,7 @@
    7.85  apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
    7.86             split: option.split)
    7.87  apply(rule iter_narrow_step_ivl_termination)
    7.88 -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])
    7.89 +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])
    7.90  apply(erule iter_widen_pfp)
    7.91  done
    7.92  

     8.1 --- a/src/HOL/IMP/Abs_State.thy	Mon Feb 11 11:38:16 2013 +0100
     8.2 +++ b/src/HOL/IMP/Abs_State.thy	Tue Feb 12 11:54:29 2013 +0100
     8.3 @@ -60,12 +60,12 @@
     8.4  end
     8.5  
     8.6  class semilatticeL = join + L +
     8.7 -fixes top :: "com \<Rightarrow> 'a"
     8.8 +fixes top :: "vname set \<Rightarrow> 'a"
     8.9  assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
    8.10  and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
    8.11  and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
    8.12 -and top[simp]: "x \<in> L(vars c) \<Longrightarrow> x \<sqsubseteq> top c"
    8.13 -and top_in_L[simp]: "top c \<in> L(vars c)"
    8.14 +and top[simp]: "x \<in> L X \<Longrightarrow> x \<sqsubseteq> top X"
    8.15 +and top_in_L[simp]: "top X \<in> L X"
    8.16  and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
    8.17  
    8.18  notation (input) top ("\<top>\<^bsub>_\<^esub>")
    8.19 @@ -109,6 +109,7 @@
    8.20  value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
    8.21  
    8.22  definition "show_acom = map_acom (Option.map show_st)"
    8.23 +definition "show_acom_opt = Option.map show_acom"
    8.24  
    8.25  definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
    8.26  
    8.27 @@ -157,7 +158,7 @@
    8.28  instantiation st :: (semilattice) semilatticeL
    8.29  begin
    8.30  
    8.31 -definition top_st where "top c = FunDom (\<lambda>x. \<top>) (vars c)"
    8.32 +definition top_st where "top X = FunDom (\<lambda>x. \<top>) X"
    8.33  
    8.34  instance
    8.35  proof
    8.36 @@ -200,8 +201,6 @@
    8.37  lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
    8.38  by (simp add: top_option_def)
    8.39  
    8.40 -(* FIXME (maybe also le \<rightarrow> sqle?) *)
    8.41 -
    8.42  lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
    8.43  apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
    8.44  by (metis mono_gamma subsetD)