--- 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)
--- 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)
--- 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)"
--- 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)"
--- 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
--- 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
--- 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
--- 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)