--- a/src/HOL/IMP/Abs_Int0.thy Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Fri Jan 27 17:02:08 2012 +0100
@@ -9,7 +9,7 @@
text{* Abstract interpretation over type @{text st} instead of
functions. *}
-context Val_abs
+context Gamma
begin
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
@@ -26,7 +26,7 @@
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"
+locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
begin
fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" where
--- a/src/HOL/IMP/Abs_Int0_const.thy Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy Fri Jan 27 17:02:08 2012 +0100
@@ -54,7 +54,6 @@
interpretation Val_abs
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defines aval'_const is aval'
proof
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
@@ -69,8 +68,7 @@
interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defines AI_const is AI
-and step_const is step'
+defines AI_const is AI and step_const is step' and aval'_const is aval'
proof qed
--- a/src/HOL/IMP/Abs_Int0_parity.thy Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_parity.thy Fri Jan 27 17:02:08 2012 +0100
@@ -91,7 +91,6 @@
interpretation Val_abs
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defines aval_parity is aval'
proof txt{* of the locale axioms *}
fix a b :: parity
assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
@@ -114,7 +113,7 @@
interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defines step_parity is step' and AI_parity is AI
+defines aval_parity is aval' and step_parity is step' and AI_parity is AI
proof qed
--- a/src/HOL/IMP/Abs_Int1.thy Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Fri Jan 27 17:02:08 2012 +0100
@@ -61,7 +61,7 @@
end
locale Val_abs1_gamma =
- Val_abs where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
+ Gamma 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> = {}"
--- a/src/HOL/IMP/Abs_Int1_ivl.thy Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Fri Jan 27 17:02:08 2012 +0100
@@ -172,7 +172,6 @@
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
by(auto simp: \<gamma>_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
@@ -187,6 +186,7 @@
interpretation Val_abs1_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+defines aval_ivl is aval'
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)
--- a/src/HOL/IMP/Abs_State.thy Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_State.thy Fri Jan 27 17:02:08 2012 +0100
@@ -58,7 +58,7 @@
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
by(auto simp add: le_st_def lookup_def update_def)
-context Val_abs
+locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
begin
abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"