--- a/NEWS Mon Aug 23 11:18:38 2010 +0200
+++ b/NEWS Mon Aug 23 11:56:12 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.
--- a/src/HOL/Library/Convex.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Library/Convex.thy Mon Aug 23 11:56:12 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"
--- a/src/HOL/Library/Function_Algebras.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Mon Aug 23 11:56:12 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 ..
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 23 11:56:12 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)}"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 23 11:56:12 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
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Mon Aug 23 11:56:12 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
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 23 11:56:12 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
--- a/src/HOL/NSA/StarDef.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Aug 23 11:56:12 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
--- a/src/HOL/Probability/Lebesgue.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Mon Aug 23 11:56:12 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:
--- a/src/HOL/Rings.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Rings.thy Mon Aug 23 11:56:12 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
--- a/src/HOL/Transcendental.thy Mon Aug 23 11:18:38 2010 +0200
+++ b/src/HOL/Transcendental.thy Mon Aug 23 11:56:12 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