# HG changeset patch
# User nipkow
# Date 1327680128 -3600
# Node ID 10c18630612a71a0f2a96e116438366449f97016
# Parent  202f8b8086a3a79e7658cc2206c1c56a241b3b5b
removed duplicate definitions that made locale inconsistent

diff -r 202f8b8086a3 -r 10c18630612a src/HOL/IMP/Abs_Int0.thy
--- 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
diff -r 202f8b8086a3 -r 10c18630612a src/HOL/IMP/Abs_Int0_const.thy
--- 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
 
 
diff -r 202f8b8086a3 -r 10c18630612a src/HOL/IMP/Abs_Int0_parity.thy
--- 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
 
 
diff -r 202f8b8086a3 -r 10c18630612a src/HOL/IMP/Abs_Int1.thy
--- 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> = {}"
diff -r 202f8b8086a3 -r 10c18630612a src/HOL/IMP/Abs_Int1_ivl.thy
--- 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)
diff -r 202f8b8086a3 -r 10c18630612a src/HOL/IMP/Abs_State.thy
--- 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"