dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
authorhaftmann
Mon Aug 23 11:17:13 2010 +0200 (2010-08-23)
changeset 386428fa437809c67
parent 38632 9cde57cdd0e3
child 38643 8782e4f0cdc8
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
NEWS
src/HOL/Library/Convex.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Operator_Norm.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/StarDef.thy
src/HOL/Probability/Lebesgue.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Sun Aug 22 14:27:30 2010 +0200
     1.2 +++ b/NEWS	Mon Aug 23 11:17:13 2010 +0200
     1.3 @@ -35,6 +35,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
     1.8 +
     1.9  * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
    1.10  canonical names for instance definitions for functions; various improvements.
    1.11  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Library/Convex.thy	Sun Aug 22 14:27:30 2010 +0200
     2.2 +++ b/src/HOL/Library/Convex.thy	Mon Aug 23 11:17:13 2010 +0200
     2.3 @@ -244,7 +244,7 @@
     2.4    shows "convex_on s (\<lambda>x. c * f x)"
     2.5  proof-
     2.6    have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
     2.7 -  show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
     2.8 +  show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto
     2.9  qed
    2.10  
    2.11  lemma convex_lower:
    2.12 @@ -253,7 +253,7 @@
    2.13  proof-
    2.14    let ?m = "max (f x) (f y)"
    2.15    have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
    2.16 -    using assms(4,5) by(auto simp add: mult_mono1 add_mono)
    2.17 +    using assms(4,5) by (auto simp add: mult_left_mono add_mono)
    2.18    also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
    2.19    finally show ?thesis
    2.20      using assms unfolding convex_on_def by fastsimp
    2.21 @@ -481,8 +481,8 @@
    2.22    hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
    2.23    have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
    2.24              \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
    2.25 -    using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
    2.26 -      mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
    2.27 +    using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
    2.28 +      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
    2.29    hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
    2.30      by (auto simp add:field_simps)
    2.31    thus "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
     3.1 --- a/src/HOL/Library/Function_Algebras.thy	Sun Aug 22 14:27:30 2010 +0200
     3.2 +++ b/src/HOL/Library/Function_Algebras.thy	Mon Aug 23 11:17:13 2010 +0200
     3.3 @@ -105,12 +105,6 @@
     3.4  instance "fun" :: (type, mult_zero) mult_zero proof
     3.5  qed (simp_all add: zero_fun_def times_fun_def)
     3.6  
     3.7 -instance "fun" :: (type, mult_mono) mult_mono proof
     3.8 -qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
     3.9 -
    3.10 -instance "fun" :: (type, mult_mono1) mult_mono1 proof
    3.11 -qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
    3.12 -
    3.13  instance "fun" :: (type, zero_neq_one) zero_neq_one proof
    3.14  qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
    3.15  
    3.16 @@ -186,9 +180,11 @@
    3.17  
    3.18  instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
    3.19  
    3.20 -instance "fun" :: (type, ordered_semiring) ordered_semiring ..
    3.21 +instance "fun" :: (type, ordered_semiring) ordered_semiring proof
    3.22 +qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
    3.23  
    3.24 -instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
    3.25 +instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
    3.26 +qed (fact mult_left_mono)
    3.27  
    3.28  instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
    3.29  
     4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
     4.3 @@ -2507,7 +2507,7 @@
     4.4      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`
     4.5        unfolding dist_norm  by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
     4.6    next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using  `e>0`
     4.7 -      unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
     4.8 +      unfolding dist_norm by(auto intro!: mult_strict_left_mono)
     4.9      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)"
    4.10        unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
    4.11      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)}"
     5.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
     5.3 @@ -220,7 +220,7 @@
     5.4    fixes x :: "'a::real_normed_vector"
     5.5    shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
     5.6    unfolding norm_scaleR
     5.7 -  apply (erule mult_mono1)
     5.8 +  apply (erule mult_left_mono)
     5.9    apply simp
    5.10    done
    5.11  
     6.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Aug 22 14:27:30 2010 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Mon Aug 23 11:17:13 2010 +0200
     6.3 @@ -107,7 +107,7 @@
     6.4    apply (subst mult_assoc)
     6.5    apply (rule order_trans)
     6.6    apply (rule onorm(1)[OF lf])
     6.7 -  apply (rule mult_mono1)
     6.8 +  apply (rule mult_left_mono)
     6.9    apply (rule onorm(1)[OF lg])
    6.10    apply (rule onorm_pos_le[OF lf])
    6.11    done
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
     7.3 @@ -5678,7 +5678,7 @@
     7.4      next
     7.5        case (Suc m)
     7.6        hence "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
     7.7 -        using `0 \<le> c` using mult_mono1_class.mult_mono1[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
     7.8 +        using `0 \<le> c` using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
     7.9        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]
    7.10          unfolding fzn and mult_le_cancel_left by auto
    7.11      qed
     8.1 --- a/src/HOL/NSA/StarDef.thy	Sun Aug 22 14:27:30 2010 +0200
     8.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Aug 23 11:17:13 2010 +0200
     8.3 @@ -925,12 +925,12 @@
     8.4  done
     8.5  
     8.6  instance star :: (ordered_comm_semiring) ordered_comm_semiring
     8.7 -by (intro_classes, transfer, rule mult_mono1_class.mult_mono1)
     8.8 +by (intro_classes, transfer, rule mult_left_mono)
     8.9  
    8.10  instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
    8.11  
    8.12  instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
    8.13 -by (intro_classes, transfer, rule mult_strict_left_mono_comm)
    8.14 +by (intro_classes, transfer, rule mult_strict_left_mono)
    8.15  
    8.16  instance star :: (ordered_ring) ordered_ring ..
    8.17  instance star :: (ordered_ring_abs) ordered_ring_abs
     9.1 --- a/src/HOL/Probability/Lebesgue.thy	Sun Aug 22 14:27:30 2010 +0200
     9.2 +++ b/src/HOL/Probability/Lebesgue.thy	Mon Aug 23 11:17:13 2010 +0200
     9.3 @@ -700,7 +700,7 @@
     9.4      using `a \<in> nnfis f` unfolding nnfis_def by auto
     9.5    with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
     9.6      by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
     9.7 -      LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
     9.8 +      LIMSEQ_mult LIMSEQ_const psfis_mult mult_left_mono)
     9.9  qed
    9.10  
    9.11  lemma nnfis_add:
    10.1 --- a/src/HOL/Rings.thy	Sun Aug 22 14:27:30 2010 +0200
    10.2 +++ b/src/HOL/Rings.thy	Mon Aug 23 11:17:13 2010 +0200
    10.3 @@ -628,10 +628,6 @@
    10.4  
    10.5  end
    10.6  
    10.7 -class mult_mono = times + zero + ord +
    10.8 -  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    10.9 -  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   10.10 -
   10.11  text {*
   10.12    The theory of partially ordered rings is taken from the books:
   10.13    \begin{itemize}
   10.14 @@ -645,31 +641,29 @@
   10.15    \end{itemize}
   10.16  *}
   10.17  
   10.18 -class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
   10.19 +class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   10.20 +  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   10.21 +  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   10.22  begin
   10.23  
   10.24  lemma mult_mono:
   10.25 -  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
   10.26 -     \<Longrightarrow> a * c \<le> b * d"
   10.27 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
   10.28  apply (erule mult_right_mono [THEN order_trans], assumption)
   10.29  apply (erule mult_left_mono, assumption)
   10.30  done
   10.31  
   10.32  lemma mult_mono':
   10.33 -  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
   10.34 -     \<Longrightarrow> a * c \<le> b * d"
   10.35 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
   10.36  apply (rule mult_mono)
   10.37  apply (fast intro: order_trans)+
   10.38  done
   10.39  
   10.40  end
   10.41  
   10.42 -class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
   10.43 -  + semiring + cancel_comm_monoid_add
   10.44 +class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
   10.45  begin
   10.46  
   10.47  subclass semiring_0_cancel ..
   10.48 -subclass ordered_semiring ..
   10.49  
   10.50  lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   10.51  using mult_left_mono [of 0 b a] by simp
   10.52 @@ -689,7 +683,7 @@
   10.53  
   10.54  end
   10.55  
   10.56 -class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
   10.57 +class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
   10.58  begin
   10.59  
   10.60  subclass ordered_cancel_semiring ..
   10.61 @@ -854,41 +848,38 @@
   10.62  
   10.63  end
   10.64  
   10.65 -class mult_mono1 = times + zero + ord +
   10.66 -  assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   10.67 -
   10.68 -class ordered_comm_semiring = comm_semiring_0
   10.69 -  + ordered_ab_semigroup_add + mult_mono1
   10.70 +class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
   10.71 +  assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   10.72  begin
   10.73  
   10.74  subclass ordered_semiring
   10.75  proof
   10.76    fix a b c :: 'a
   10.77    assume "a \<le> b" "0 \<le> c"
   10.78 -  thus "c * a \<le> c * b" by (rule mult_mono1)
   10.79 +  thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
   10.80    thus "a * c \<le> b * c" by (simp only: mult_commute)
   10.81  qed
   10.82  
   10.83  end
   10.84  
   10.85 -class ordered_cancel_comm_semiring = comm_semiring_0_cancel
   10.86 -  + ordered_ab_semigroup_add + mult_mono1
   10.87 +class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
   10.88  begin
   10.89  
   10.90 +subclass comm_semiring_0_cancel ..
   10.91  subclass ordered_comm_semiring ..
   10.92  subclass ordered_cancel_semiring ..
   10.93  
   10.94  end
   10.95  
   10.96  class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
   10.97 -  assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   10.98 +  assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   10.99  begin
  10.100  
  10.101  subclass linordered_semiring_strict
  10.102  proof
  10.103    fix a b c :: 'a
  10.104    assume "a < b" "0 < c"
  10.105 -  thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
  10.106 +  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
  10.107    thus "a * c < b * c" by (simp only: mult_commute)
  10.108  qed
  10.109  
    11.1 --- a/src/HOL/Transcendental.thy	Sun Aug 22 14:27:30 2010 +0200
    11.2 +++ b/src/HOL/Transcendental.thy	Mon Aug 23 11:17:13 2010 +0200
    11.3 @@ -2790,7 +2790,7 @@
    11.4  
    11.5  lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1"
    11.6  proof -
    11.7 -  from mult_mono1[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
    11.8 +  from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
    11.9    have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
   11.10    thus ?thesis using zero_le_power2 by auto
   11.11  qed