--- a/src/HOL/IMP/Abs_Int0.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Tue Apr 30 03:18:07 2013 +0200
@@ -10,10 +10,10 @@
defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
If you view this theory with jedit, just click on the names to get there. *}
-class semilattice = semilattice_sup + top
+class semilattice_sup_top = semilattice_sup + top
-instance "fun" :: (type, semilattice) semilattice ..
+instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top ..
instantiation option :: (order)order
begin
@@ -58,7 +58,7 @@
end
-instantiation option :: (semilattice)semilattice
+instantiation option :: (semilattice_sup_top)semilattice_sup_top
begin
definition top_option where "\<top> = Some \<top>"
@@ -149,7 +149,7 @@
text{* The interface for abstract values: *}
locale Val_abs =
-fixes \<gamma> :: "'av::semilattice \<Rightarrow> val set"
+fixes \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'av"
@@ -159,7 +159,12 @@
type_synonym 'av st = "(vname \<Rightarrow> 'av)"
-locale Abs_Int_fun = Val_abs \<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
+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_fun = Val_abs where \<gamma>=\<gamma>
+ for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
@@ -349,7 +354,8 @@
by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
-locale Measure_fun = Measure1_fun where m=m for m :: "'av::semilattice \<Rightarrow> nat" +
+locale Measure_fun = Measure1_fun where m=m
+ for m :: "'av::semilattice_sup_top \<Rightarrow> nat" +
assumes m2: "x < y \<Longrightarrow> m x > m y"
begin
@@ -465,7 +471,7 @@
locale Abs_Int_fun_measure =
Abs_Int_fun_mono where \<gamma>=\<gamma> + Measure_fun where m=m
- for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
+ for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
begin
lemma top_on_step': "top_on_acom C (-vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
--- a/src/HOL/IMP/Abs_Int1.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Tue Apr 30 03:18:07 2013 +0200
@@ -32,11 +32,8 @@
end
-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 = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
+locale Abs_Int = Gamma where \<gamma>=\<gamma>
+ for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
definition "step' = Step
@@ -172,7 +169,7 @@
apply(auto)
by transfer simp
-lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
+lemma top_on_Step: fixes C :: "('a::semilattice_sup_top)st option acom"
assumes "!!x e S. \<lbrakk>top_on_opt S X; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (f x e S) X"
"!!b S. top_on_opt S X \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt (g b S) X"
shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt S X; top_on_acom C X \<rbrakk> \<Longrightarrow> top_on_acom (Step f g S C) X"
@@ -250,7 +247,7 @@
locale Abs_Int_measure =
Abs_Int_mono where \<gamma>=\<gamma> + Measure where m=m
- for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
+ for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
begin
lemma top_on_step': "\<lbrakk> top_on_acom C (-vars C) \<rbrakk> \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
--- a/src/HOL/IMP/Abs_Int1_const.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Tue Apr 30 03:18:07 2013 +0200
@@ -20,7 +20,7 @@
(case (a1,a2) of (Const i, Const j) \<Rightarrow> Const(i+j) | _ \<Rightarrow> Any)"
by(auto split: prod.split const.split)
-instantiation const :: semilattice
+instantiation const :: semilattice_sup_top
begin
fun less_eq_const where "x \<le> y = (y = Any | x=y)"
--- a/src/HOL/IMP/Abs_Int1_parity.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Tue Apr 30 03:18:07 2013 +0200
@@ -47,9 +47,9 @@
end
-text{* Instantiation of class @{class semilattice} with type @{typ parity}: *}
+text{* Instantiation of class @{class semilattice_sup_top} with type @{typ parity}: *}
-instantiation parity :: semilattice
+instantiation parity :: semilattice_sup_top
begin
definition sup_parity where
--- a/src/HOL/IMP/Abs_Int2.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Tue Apr 30 03:18:07 2013 +0200
@@ -26,10 +26,10 @@
subsection "Backward Analysis of Expressions"
-subclass (in bounded_lattice) semilattice ..
+subclass (in bounded_lattice) semilattice_sup_top ..
-locale Val_abs1_gamma =
- Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
+locale Val_abs1_gamma = Gamma where \<gamma> = \<gamma>
+ for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
assumes inter_gamma_subset_gamma_inf:
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
and gamma_bot[simp]: "\<gamma> \<bottom> = {}"
@@ -45,8 +45,7 @@
end
-locale Val_abs1 =
- Val_abs1_gamma where \<gamma> = \<gamma>
+locale Val_abs1 = Val_abs1_gamma where \<gamma> = \<gamma>
for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
@@ -58,8 +57,8 @@
n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
-locale Abs_Int1 =
- Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
+locale Abs_Int1 = Val_abs1 where \<gamma> = \<gamma>
+ for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
begin
lemma in_gamma_sup_UpI:
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Tue Apr 30 03:18:07 2013 +0200
@@ -65,7 +65,7 @@
declare is_empty_rep_iff[THEN iffD1, simp]
-instantiation ivl :: semilattice
+instantiation ivl :: semilattice_sup_top
begin
definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
--- a/src/HOL/IMP/Abs_Int3.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Tue Apr 30 03:18:07 2013 +0200
@@ -241,8 +241,8 @@
(metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
-locale Abs_Int2 = Abs_Int1_mono
-where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set"
+locale Abs_Int2 = Abs_Int1_mono where \<gamma>=\<gamma>
+ for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set"
begin
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
@@ -337,7 +337,8 @@
that not yet @{prop"y \<le> x"}. This complicates the termination proof for
widening. *}
-locale Measure_WN = Measure1 where m=m for m :: "'av::{top,WN} \<Rightarrow> nat" +
+locale Measure_WN = Measure1 where m=m
+ for m :: "'av::{top,WN} \<Rightarrow> nat" +
fixes n :: "'av \<Rightarrow> nat"
assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
@@ -503,8 +504,7 @@
by blast
qed
-locale Abs_Int2_measure =
- Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m
+locale Abs_Int2_measure = Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m
for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
--- a/src/HOL/IMP/Abs_State.thy Mon Apr 29 18:52:35 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy Tue Apr 30 03:18:07 2013 +0200
@@ -96,7 +96,7 @@
apply(fastforce simp: fun_rep_map_of fun_eq_iff split:option.splits)
done
-instantiation st :: (semilattice) semilattice
+instantiation st :: (semilattice_sup_top) semilattice_sup_top
begin
lift_definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<squnion>)"
@@ -129,7 +129,8 @@
lemma mono_fun: "S1 \<le> S2 \<Longrightarrow> fun S1 x \<le> fun S2 x"
by transfer (simp add: less_eq_st_rep_iff)
-locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
+locale Gamma = Val_abs where \<gamma>=\<gamma>
+ for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"