# HG changeset patch
# User nipkow
# Date 1367284687 -7200
# Node ID 054a4046144985df0e5402130e066ad2261176f6
# Parent  d4f1e439e1bdd3282e8ce4705e9f603d5912526e
canonical names of classes

diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_Int0.thy
--- 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)"
diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_Int1.thy
--- 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)"
diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_Int1_const.thy
--- 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)"
diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_Int1_parity.thy
--- 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
diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_Int2.thy
--- 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:
diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_Int2_ivl.thy
--- 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
diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_Int3.thy
--- 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"
 
 
diff -r d4f1e439e1bd -r 054a40461449 src/HOL/IMP/Abs_State.thy
--- 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"