# HG changeset patch
# User haftmann
# Date 1232114336 -3600
# Node ID 7071b017cb3519456575f68a1c2a3192535a9711
# Parent  6fe4200532b7a4ed8a465b56db1897186137aa4d
migrated class package to new locale implementation

diff -r 6fe4200532b7 -r 7071b017cb35 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOL/Library/Countable.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Countable.thy
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 *)
 
diff -r 6fe4200532b7 -r 7071b017cb35 src/HOL/MetisExamples/BT.thy
--- a/src/HOL/MetisExamples/BT.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOL/MetisExamples/BT.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -84,7 +84,7 @@
 lemma depth_reflect: "depth (reflect t) = depth t"
   apply (induct t)
   apply (metis depth.simps(1) reflect.simps(1))
-  apply (metis depth.simps(2) min_max.less_eq_less_sup.sup_commute reflect.simps(2))
+  apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2))
   done
 
 text {*
diff -r 6fe4200532b7 -r 7071b017cb35 src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MetisExamples/BigO.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method
@@ -13,9 +12,7 @@
 
 subsection {* Definitions *}
 
-constdefs 
-
-  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
+definition bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where
   "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
 
 ML_command{*AtpWrapper.problem_name := "BigO__bigo_pos_const"*}
@@ -362,7 +359,7 @@
   apply (rule add_mono)
 ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq_simpler"*} 
 (*Found by SPASS; SLOW*)
-apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right order_trans)
+apply (metis le_maxI2 linorder_linear linorder_not_le min_max.sup_absorb1 mult_le_cancel_right order_trans)
 apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
 done
 
@@ -1164,7 +1161,7 @@
 (*sledgehammer*);  
   apply (case_tac "0 <= k x - g x")
   prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*)
-   apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.less_eq_less_sup.sup_absorb1 min_max.less_eq_less_sup.sup_commute)
+   apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.sup_absorb1 min_max.sup_commute)
 proof (neg_clausify)
 fix x
 assume 0: "\<And>A. k A \<le> f A"
@@ -1174,16 +1171,16 @@
 have 3: "\<not> k x - g x < (0\<Colon>'b)"
   by (metis 2 linorder_not_less)
 have 4: "\<And>X1 X2. min X1 (k X2) \<le> f X2"
-  by (metis min_max.less_eq_less_inf.inf_le2 min_max.less_eq_less_inf.le_inf_iff min_max.less_eq_less_inf.le_iff_inf 0)
+  by (metis min_max.inf_le2 min_max.le_inf_iff min_max.le_iff_inf 0)
 have 5: "\<bar>g x - f x\<bar> = f x - g x"
-  by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.less_eq_less_inf.inf_commute 4 linorder_not_le min_max.less_eq_less_inf.le_iff_inf 3 diff_less_0_iff_less linorder_not_less)
+  by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.inf_commute 4 linorder_not_le min_max.le_iff_inf 3 diff_less_0_iff_less linorder_not_less)
 have 6: "max (0\<Colon>'b) (k x - g x) = k x - g x"
-  by (metis min_max.less_eq_less_sup.le_iff_sup 2)
+  by (metis min_max.le_iff_sup 2)
 assume 7: "\<not> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
 have 8: "\<not> k x - g x \<le> f x - g x"
-  by (metis 5 abs_minus_commute 7 min_max.less_eq_less_sup.sup_commute 6)
+  by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)
 show "False"
-  by (metis min_max.less_eq_less_sup.sup_commute min_max.less_eq_less_inf.inf_commute min_max.less_eq_less_inf_sup.sup_inf_absorb min_max.less_eq_less_inf.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
+  by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
 qed
 
 ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3"*}
@@ -1206,7 +1203,7 @@
 ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3_simpler"*}
 apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
 apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
-apply (metis abs_ge_zero linorder_linear min_max.less_eq_less_sup.sup_absorb1 min_max.less_eq_less_sup.sup_commute)
+apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
 done
 
 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
diff -r 6fe4200532b7 -r 7071b017cb35 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOLCF/CompactBasis.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -244,7 +244,7 @@
   assumes "ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
-  class_interpret ab_semigroup_idem_mult [f] by fact
+  interpret ab_semigroup_idem_mult f by fact
   show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 qed
 
diff -r 6fe4200532b7 -r 7071b017cb35 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -296,9 +296,8 @@
 apply (simp add: PDPlus_absorb)
 done
 
-class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
-  by unfold_locales
-    (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
+interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
+  proof qed (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
 
 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
 by (rule aci_convex_plus.mult_left_commute)
diff -r 6fe4200532b7 -r 7071b017cb35 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOLCF/HOLCF.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -16,7 +16,6 @@
   "Tools/domain/domain_theorems.ML"
   "Tools/domain/domain_extender.ML"
   "Tools/adm_tac.ML"
-
 begin
 
 defaultsort pcpo
diff -r 6fe4200532b7 -r 7071b017cb35 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOLCF/LowerPD.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -250,9 +250,8 @@
 apply (simp add: PDPlus_absorb)
 done
 
-class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
-  by unfold_locales
-    (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
+interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
+  proof qed (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
 
 lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
 by (rule aci_lower_plus.mult_left_commute)
diff -r 6fe4200532b7 -r 7071b017cb35 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOLCF/UpperPD.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -248,9 +248,8 @@
 apply (simp add: PDPlus_absorb)
 done
 
-class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
-  by unfold_locales
-    (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
+interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
+  proof qed (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
 
 lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
 by (rule aci_upper_plus.mult_left_commute)