# HG changeset patch
# User haftmann
# Date 1172846595 -3600
# Node ID 33a46e6c7f048e70149d44b248bf03163da1c097
# Parent  01e90256550d562337661bbfcba8fd06385a55be
prefix of class interpretation not mandatory any longer

diff -r 01e90256550d -r 33a46e6c7f04 NEWS
--- a/NEWS	Fri Mar 02 12:38:58 2007 +0100
+++ b/NEWS	Fri Mar 02 15:43:15 2007 +0100
@@ -505,6 +505,10 @@
 
 *** HOL ***
 
+* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
+"cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
+avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
+
 * Addes class (axclass + locale) "preorder" as superclass of "order";
 potential INCOMPATIBILITY: order of proof goals in order/linorder instance
 proofs changed.
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -256,7 +256,7 @@
 proof (induct n)
   case 0 show ?case by simp
 next
-  case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) 
+  case Suc thus ?case by (simp add: add_assoc) 
 qed
 
 lemma natsum_cong [cong]:
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -21,7 +21,7 @@
    apply (induct_tac m)
     apply simp
    apply force
-  apply (simp add: ab_semigroup_add_class.add_commute [of m]) 
+  apply (simp add: add_commute [of m]) 
   done
 
 lemma SUM_extend_below: 
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -318,7 +318,7 @@
 by (intro_classes, transfer, rule mult_commute)
 
 instance star :: (comm_monoid_add) comm_monoid_add
-by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
+by (intro_classes, transfer, rule comm_monoid_add_class.zero_plus.add_0)
 
 instance star :: (monoid_mult) monoid_mult
 apply (intro_classes)
@@ -427,12 +427,12 @@
 done
 
 instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.mult_mono)
+by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
 
 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
 
 instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict
-by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.mult_strict_mono)
+by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
 
 instance star :: (pordered_ring) pordered_ring ..
 instance star :: (lordered_ring) lordered_ring ..
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Lattices.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -37,13 +37,13 @@
 
 lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
 apply simp
 done
 
 lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
 apply simp
 done
 
@@ -51,7 +51,7 @@
 by(blast intro: inf_greatest)
 
 lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
-by(blast intro: trans)
+by(blast intro: order_trans)
 
 lemma le_inf_iff [simp]:
  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
@@ -70,13 +70,13 @@
 
 lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
 apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
 apply simp
 done
 
 lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
 apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
 apply simp
 done
 
@@ -84,7 +84,7 @@
 by(blast intro: sup_least)
 
 lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
-by(blast intro: trans)
+by(blast intro: order_trans)
 
 lemma ge_sup_conv[simp]:
  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -96,7 +96,7 @@
   unfolding Fract_of_int_eq rat_number_of_def by simp
 
 lemma rat_minus [code func]:
-  "(a\<Colon>rat) - b = a + (- b)" unfolding ab_group_add_class.diff_minus ..
+  "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
 
 lemma rat_divide [code func]:
   "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -73,15 +73,15 @@
 
 class preorder = ord +
   assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
-  and refl [iff]: "x \<sqsubseteq> x"
-  and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+  and order_refl [iff]: "x \<sqsubseteq> x"
+  and order_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
 begin
 
 text {* Reflexivity. *}
 
 lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y"
     -- {* This form is useful with the classical reasoner. *}
-  by (erule ssubst) (rule refl)
+  by (erule ssubst) (rule order_refl)
 
 lemma less_irrefl [iff]: "\<not> x \<sqsubset> x"
   by (simp add: less_le)
@@ -119,7 +119,6 @@
 
 end
 
-
 subsection {* Partial orderings *}
 
 class order = preorder + 
@@ -147,13 +146,13 @@
 text {* Transitivity. *}
 
 lemma less_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
-  by (simp add: less_le) (blast intro: trans antisym)
+  by (simp add: less_le) (blast intro: order_trans antisym)
 
 lemma le_less_trans: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
-  by (simp add: less_le) (blast intro: trans antisym)
+  by (simp add: less_le) (blast intro: order_trans antisym)
 
 lemma less_le_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
-  by (simp add: less_le) (blast intro: trans antisym)
+  by (simp add: less_le) (blast intro: order_trans antisym)
 
 
 text {* Useful for simplification, but too risky to include by default. *}
@@ -189,7 +188,7 @@
   "\<lbrakk> x \<sqsubseteq> y \<Longrightarrow> P; y \<sqsubseteq> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   using linear by blast
 
-lemma cases [case_names less equal greater]:
+lemma linorder_cases [case_names less equal greater]:
     "\<lbrakk> x \<sqsubset> y \<Longrightarrow> P; x = y \<Longrightarrow> P; y \<sqsubset> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   using less_linear by blast
 
@@ -239,13 +238,18 @@
   max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "max a b = (if a \<sqsubseteq> b then b else a)"
 
+end
+
+context linorder
+begin
+
 lemma min_le_iff_disj:
   "min x y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
-  unfolding min_def using linear by (auto intro: trans)
+  unfolding min_def using linear by (auto intro: order_trans)
 
 lemma le_max_iff_disj:
   "z \<sqsubseteq> max x y \<longleftrightarrow> z \<sqsubseteq> x \<or> z \<sqsubseteq> y"
-  unfolding max_def using linear by (auto intro: trans)
+  unfolding max_def using linear by (auto intro: order_trans)
 
 lemma min_less_iff_disj:
   "min x y \<sqsubset> z \<longleftrightarrow> x \<sqsubset> z \<or> y \<sqsubset> z"
@@ -276,9 +280,9 @@
 
 subsection {* Name duplicates *}
 
-lemmas order_refl [iff] = preorder_class.refl
-lemmas order_trans = preorder_class.trans
-lemmas order_less_le = preorder_class.less_le
+(*lemmas order_refl [iff] = preorder_class.order_refl
+lemmas order_trans = preorder_class.order_trans*)
+lemmas order_less_le = less_le
 lemmas order_eq_refl = preorder_class.eq_refl
 lemmas order_less_irrefl = preorder_class.less_irrefl
 lemmas order_le_less = preorder_class.le_less
@@ -289,7 +293,7 @@
 lemmas order_neq_le_trans = preorder_class.neq_le_trans
 lemmas order_le_neq_trans = preorder_class.le_neq_trans
 
-lemmas order_antisym = order_class.antisym
+lemmas order_antisym = antisym
 lemmas order_less_not_sym = order_class.less_not_sym
 lemmas order_less_asym = order_class.less_asym
 lemmas order_eq_iff = order_class.eq_iff
@@ -302,11 +306,11 @@
 lemmas order_less_imp_triv = order_class.less_imp_triv
 lemmas order_less_asym' = order_class.less_asym'
 
-lemmas linorder_linear = linorder_class.linear
+lemmas linorder_linear = linear
 lemmas linorder_less_linear = linorder_class.less_linear
 lemmas linorder_le_less_linear = linorder_class.le_less_linear
 lemmas linorder_le_cases = linorder_class.le_cases
-lemmas linorder_cases = linorder_class.cases
+(*lemmas linorder_cases = linorder_class.linorder_cases*)
 lemmas linorder_not_less = linorder_class.not_less
 lemmas linorder_not_le = linorder_class.not_le
 lemmas linorder_neq_iff = linorder_class.neq_iff
@@ -896,7 +900,6 @@
     "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   by (simp add: max_def)
 
-
 subsection {* Basic ML bindings *}
 
 ML {*
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -103,6 +103,11 @@
   units :: "'a set" where
   "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
 
+end
+
+context monoid
+begin
+
 lemma inv_obtain:
   assumes "x \<in> units"
   obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
@@ -150,6 +155,11 @@
   npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
 
+end
+
+context monoid
+begin
+
 abbreviation
   npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
   "x \<^loc>\<up> n \<equiv> npow n x"
@@ -299,24 +309,24 @@
 instance * :: (semigroup, semigroup) semigroup
   mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
               (x1 \<otimes> y1, x2 \<otimes> y2)"
-by default (simp_all add: split_paired_all mult_prod_def semigroup_class.assoc)
+by default (simp_all add: split_paired_all mult_prod_def assoc)
 
 instance * :: (monoidl, monoidl) monoidl
   one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoidl_class.neutl)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
 
 instance * :: (monoid, monoid) monoid
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.neutr)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr)
 
 instance * :: (monoid_comm, monoid_comm) monoid_comm
-by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
+by default (simp_all add: split_paired_all mult_prod_def comm)
 
 instance * :: (group, group) group
   inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def group_class.invl)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
 
 instance * :: (group_comm, group_comm) group_comm
-by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
+by default (simp_all add: split_paired_all mult_prod_def comm)
 
 definition
   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
diff -r 01e90256550d -r 33a46e6c7f04 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Fri Mar 02 15:43:15 2007 +0100
@@ -17,9 +17,6 @@
 abbreviation (in ord)
   "sorted \<equiv> abs_sorted less_eq"
 
-abbreviation
-  "sorted \<equiv> abs_sorted less_eq"
-
 lemma (in order) sorted_weakening:
   assumes "sorted (x # xs)"
   shows "sorted xs"
@@ -138,7 +135,7 @@
 apply (simp_all add: "fin_*_def")
 apply (unfold split_paired_all)
 apply (rule product_all)
-apply (rule finite_class.member_fin)+
+apply (rule member_fin)+
 done
 
 instance option :: (finite) finite
@@ -149,7 +146,7 @@
   proof (cases x)
     case None then show ?thesis by auto
   next
-    case (Some x) then show ?thesis by (auto intro: finite_class.member_fin)
+    case (Some x) then show ?thesis by (auto intro: member_fin)
   qed
 qed