# HG changeset patch
# User haftmann
# Date 1282555033 -7200
# Node ID 8fa437809c67ee9f75da2dc9af12fe3eb2d8e5af
# Parent  9cde57cdd0e379f346d4e37a444fbaedf846edc2
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates

diff -r 9cde57cdd0e3 -r 8fa437809c67 NEWS
--- a/NEWS	Sun Aug 22 14:27:30 2010 +0200
+++ b/NEWS	Mon Aug 23 11:17:13 2010 +0200
@@ -35,6 +35,8 @@
 
 *** HOL ***
 
+* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
+
 * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
 canonical names for instance definitions for functions; various improvements.
 INCOMPATIBILITY.
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Library/Convex.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -244,7 +244,7 @@
   shows "convex_on s (\<lambda>x. c * f x)"
 proof-
   have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
-  show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
+  show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto
 qed
 
 lemma convex_lower:
@@ -253,7 +253,7 @@
 proof-
   let ?m = "max (f x) (f y)"
   have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
-    using assms(4,5) by(auto simp add: mult_mono1 add_mono)
+    using assms(4,5) by (auto simp add: mult_left_mono add_mono)
   also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
   finally show ?thesis
     using assms unfolding convex_on_def by fastsimp
@@ -481,8 +481,8 @@
   hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
   have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
             \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
-    using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
-      mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
+    using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
+      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
   hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
     by (auto simp add:field_simps)
   thus "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Library/Function_Algebras.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -105,12 +105,6 @@
 instance "fun" :: (type, mult_zero) mult_zero proof
 qed (simp_all add: zero_fun_def times_fun_def)
 
-instance "fun" :: (type, mult_mono) mult_mono proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
-
-instance "fun" :: (type, mult_mono1) mult_mono1 proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
-
 instance "fun" :: (type, zero_neq_one) zero_neq_one proof
 qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
 
@@ -186,9 +180,11 @@
 
 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
 
-instance "fun" :: (type, ordered_semiring) ordered_semiring ..
+instance "fun" :: (type, ordered_semiring) ordered_semiring proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
 
-instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
+qed (fact mult_left_mono)
 
 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
 
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -2507,7 +2507,7 @@
     fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
       unfolding dist_norm  by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
   next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using  `e>0`
-      unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
+      unfolding dist_norm by(auto intro!: mult_strict_left_mono)
     have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
       unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
     hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -220,7 +220,7 @@
   fixes x :: "'a::real_normed_vector"
   shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
   unfolding norm_scaleR
-  apply (erule mult_mono1)
+  apply (erule mult_left_mono)
   apply simp
   done
 
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -107,7 +107,7 @@
   apply (subst mult_assoc)
   apply (rule order_trans)
   apply (rule onorm(1)[OF lf])
-  apply (rule mult_mono1)
+  apply (rule mult_left_mono)
   apply (rule onorm(1)[OF lg])
   apply (rule onorm_pos_le[OF lf])
   done
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -5678,7 +5678,7 @@
     next
       case (Suc m)
       hence "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
-        using `0 \<le> c` using mult_mono1_class.mult_mono1[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
+        using `0 \<le> c` using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
       thus ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
         unfolding fzn and mult_le_cancel_left by auto
     qed
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -925,12 +925,12 @@
 done
 
 instance star :: (ordered_comm_semiring) ordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.mult_mono1)
+by (intro_classes, transfer, rule mult_left_mono)
 
 instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
 
 instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
-by (intro_classes, transfer, rule mult_strict_left_mono_comm)
+by (intro_classes, transfer, rule mult_strict_left_mono)
 
 instance star :: (ordered_ring) ordered_ring ..
 instance star :: (ordered_ring_abs) ordered_ring_abs
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Probability/Lebesgue.thy
--- a/src/HOL/Probability/Lebesgue.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -700,7 +700,7 @@
     using `a \<in> nnfis f` unfolding nnfis_def by auto
   with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
     by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
-      LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
+      LIMSEQ_mult LIMSEQ_const psfis_mult mult_left_mono)
 qed
 
 lemma nnfis_add:
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Rings.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -628,10 +628,6 @@
 
 end
 
-class mult_mono = times + zero + ord +
-  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
-  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
-
 text {*
   The theory of partially ordered rings is taken from the books:
   \begin{itemize}
@@ -645,31 +641,29 @@
   \end{itemize}
 *}
 
-class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
+class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
+  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
+  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
 begin
 
 lemma mult_mono:
-  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
-     \<Longrightarrow> a * c \<le> b * d"
+  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
 apply (erule mult_right_mono [THEN order_trans], assumption)
 apply (erule mult_left_mono, assumption)
 done
 
 lemma mult_mono':
-  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
-     \<Longrightarrow> a * c \<le> b * d"
+  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
 apply (rule mult_mono)
 apply (fast intro: order_trans)+
 done
 
 end
 
-class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
-  + semiring + cancel_comm_monoid_add
+class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
 begin
 
 subclass semiring_0_cancel ..
-subclass ordered_semiring ..
 
 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
 using mult_left_mono [of 0 b a] by simp
@@ -689,7 +683,7 @@
 
 end
 
-class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
+class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
 begin
 
 subclass ordered_cancel_semiring ..
@@ -854,41 +848,38 @@
 
 end
 
-class mult_mono1 = times + zero + ord +
-  assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
-
-class ordered_comm_semiring = comm_semiring_0
-  + ordered_ab_semigroup_add + mult_mono1
+class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
+  assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
 begin
 
 subclass ordered_semiring
 proof
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
-  thus "c * a \<le> c * b" by (rule mult_mono1)
+  thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
   thus "a * c \<le> b * c" by (simp only: mult_commute)
 qed
 
 end
 
-class ordered_cancel_comm_semiring = comm_semiring_0_cancel
-  + ordered_ab_semigroup_add + mult_mono1
+class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
 begin
 
+subclass comm_semiring_0_cancel ..
 subclass ordered_comm_semiring ..
 subclass ordered_cancel_semiring ..
 
 end
 
 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
-  assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
+  assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
 begin
 
 subclass linordered_semiring_strict
 proof
   fix a b c :: 'a
   assume "a < b" "0 < c"
-  thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
+  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
   thus "a * c < b * c" by (simp only: mult_commute)
 qed
 
diff -r 9cde57cdd0e3 -r 8fa437809c67 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Transcendental.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -2790,7 +2790,7 @@
 
 lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1"
 proof -
-  from mult_mono1[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
+  from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
   have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
   thus ?thesis using zero_le_power2 by auto
 qed