--- a/src/HOL/IMP/Abs_Int0.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Sat Dec 31 17:53:50 2011 +0100
@@ -12,7 +12,7 @@
context Val_abs
begin
-fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
+fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
"aval' (N n) S = num' n" |
"aval' (V x) S = lookup S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
@@ -22,10 +22,14 @@
end
-locale Abs_Int = Val_abs
+text{* The for-clause (here and elsewhere) only serves the purpose of fixing
+the name of the type parameter @{typ 'av} which would otherwise be renamed to
+@{typ 'a}. *}
+
+locale Abs_Int = Val_abs \<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
begin
-fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where
+fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" where
"step' S (SKIP {P}) = (SKIP {S})" |
"step' S (x ::= e {P}) =
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
@@ -36,7 +40,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 option acom option" where
+definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI = lpfp\<^isub>c (step' \<top>)"
--- a/src/HOL/IMP/Abs_Int0_const.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy Sat Dec 31 17:53:50 2011 +0100
@@ -52,7 +52,8 @@
end
-interpretation Val_abs \<gamma>_cval Const plus_cval
+interpretation Val_abs
+where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
defines aval'_const is aval'
proof
case goal1 thus ?case
@@ -66,7 +67,8 @@
by(auto simp: plus_cval_cases split: cval.split)
qed
-interpretation Abs_Int \<gamma>_cval Const plus_cval
+interpretation Abs_Int
+where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
defines AI_const is AI
and step_const is step'
proof qed
@@ -74,7 +76,8 @@
text{* Monotonicity: *}
-interpretation Abs_Int_mono \<gamma>_cval Const plus_cval
+interpretation Abs_Int_mono
+where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
proof
case goal1 thus ?case
by(auto simp: plus_cval_cases split: cval.split)
--- a/src/HOL/IMP/Abs_Int0_fun.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Sat Dec 31 17:53:50 2011 +0100
@@ -234,26 +234,26 @@
text{* The interface for abstract values: *}
locale Val_abs =
-fixes \<gamma> :: "'a::SL_top \<Rightarrow> val set"
+fixes \<gamma> :: "'av::SL_top \<Rightarrow> val set"
assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
-fixes num' :: "val \<Rightarrow> 'a"
-and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+fixes num' :: "val \<Rightarrow> 'av"
+and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
assumes gamma_num': "n : \<gamma>(num' n)"
and gamma_plus':
"n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
-type_synonym 'a st = "(vname \<Rightarrow> 'a)"
+type_synonym 'av st = "(vname \<Rightarrow> 'av)"
-locale Abs_Int_Fun = Val_abs
+locale Abs_Int_Fun = Val_abs \<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
begin
-fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
+fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
"aval' (N n) S = num' n" |
"aval' (V x) S = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
-fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
+fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom"
where
"step' S (SKIP {P}) = (SKIP {S})" |
"step' S (x ::= e {P}) =
@@ -264,7 +264,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 option acom option" where
+definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI = lpfp\<^isub>c (step' \<top>)"
@@ -272,13 +272,13 @@
by(induct c arbitrary: S) (simp_all add: Let_def)
-abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
where "\<gamma>\<^isub>f == \<gamma>_fun \<gamma>"
-abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
-abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"
--- a/src/HOL/IMP/Abs_Int1.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Sat Dec 31 17:53:50 2011 +0100
@@ -38,8 +38,7 @@
end
locale Val_abs1_gamma =
- Val_abs \<gamma> num' plus'
- for \<gamma> :: "'a::L_top_bot \<Rightarrow> val set" and num' plus' +
+ Val_abs where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
assumes inter_gamma_subset_gamma_meet:
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
and gamma_Bot[simp]: "\<gamma> \<bottom> = {}"
@@ -54,22 +53,25 @@
end
-locale Val_abs1 = Val_abs1_gamma +
-fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+locale Val_abs1 =
+ Val_abs1_gamma where \<gamma> = \<gamma>
+ for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
+fixes filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
+and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
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 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
-locale Abs_Int1 = Val_abs1
+locale Abs_Int1 =
+ Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set"
begin
lemma in_gamma_join_UpI: "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp)
-fun aval'' :: "aexp \<Rightarrow> 'a st option \<Rightarrow> 'a" where
+fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
"aval'' e None = \<bottom>" |
"aval'' e (Some sa) = aval' e sa"
@@ -78,7 +80,7 @@
subsubsection "Backward analysis"
-fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st option \<Rightarrow> 'a st option" where
+fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av 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
@@ -97,7 +99,7 @@
making the analysis less precise. *}
-fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st option \<Rightarrow> 'a st option" where
+fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
"bfilter (Bc v) res S = (if v=res then S else None)" |
"bfilter (Not b) res S = bfilter b (\<not> res) S" |
"bfilter (And b1 b2) res S =
@@ -139,7 +141,7 @@
qed
-fun step' :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom"
+fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom"
where
"step' S (SKIP {P}) = (SKIP {S})" |
"step' S (x ::= e {P}) =
@@ -153,7 +155,7 @@
WHILE b DO step' (bfilter b True Inv) c
{bfilter b False Inv}"
-definition AI :: "com \<Rightarrow> 'a st option acom option" where
+definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI = lpfp\<^isub>c (step' \<top>)"
lemma strip_step'[simp]: "strip(step' S c) = strip c"
--- a/src/HOL/IMP/Abs_Int1_ivl.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Sat Dec 31 17:53:50 2011 +0100
@@ -170,7 +170,8 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-interpretation Val_abs \<gamma>_ivl num_ivl plus_ivl
+interpretation Val_abs
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
defines aval_ivl is aval'
proof
case goal1 thus ?case
@@ -184,7 +185,8 @@
by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-interpretation Val_abs1_gamma \<gamma>_ivl num_ivl plus_ivl
+interpretation Val_abs1_gamma
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
proof
case goal1 thus ?case
by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -201,8 +203,9 @@
done
-interpretation
- Val_abs1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Val_abs1
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
proof
case goal1 thus ?case
by(auto simp add: filter_plus_ivl_def)
@@ -213,8 +216,9 @@
auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed
-interpretation
- Abs_Int1 \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Abs_Int1
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
defines afilter_ivl is afilter
and bfilter_ivl is bfilter
and step_ivl is step'
@@ -225,8 +229,9 @@
text{* Monotonicity: *}
-interpretation
- Abs_Int1_mono \<gamma>_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+interpretation Abs_Int1_mono
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
proof
case goal1 thus ?case
by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
--- a/src/HOL/IMP/Abs_Int2.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Sat Dec 31 17:53:50 2011 +0100
@@ -180,10 +180,11 @@
apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
by (metis (no_types) strip_lpfpc strip_map2_acom strip_while)
-locale Abs_Int2 = Abs_Int1_mono \<gamma> for \<gamma> :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
+locale Abs_Int2 = Abs_Int1_mono
+where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"
begin
-definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where
+definition AI_WN :: "com \<Rightarrow> 'av st option acom option" where
"AI_WN = pfp_WN (step' \<top>)"
lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'"
@@ -206,8 +207,9 @@
end
-interpretation
- Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl \<gamma>_ivl
+interpretation Abs_Int2
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
defines AI_ivl' is AI_WN
proof qed
--- a/src/HOL/IMP/Abs_State.thy Sat Dec 31 10:15:53 2011 +0100
+++ b/src/HOL/IMP/Abs_State.thy Sat Dec 31 17:53:50 2011 +0100
@@ -61,13 +61,13 @@
context Val_abs
begin
-abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>"
-abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set"
+abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
-abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom"
+abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV"