src/HOL/Rings.thy
changeset 38642 8fa437809c67
parent 37767 a2b7a20d6ea3
child 44064 5bce8ff0d9ae
     1.1 --- a/src/HOL/Rings.thy	Sun Aug 22 14:27:30 2010 +0200
     1.2 +++ b/src/HOL/Rings.thy	Mon Aug 23 11:17:13 2010 +0200
     1.3 @@ -628,10 +628,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class mult_mono = times + zero + ord +
     1.8 -  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
     1.9 -  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
    1.10 -
    1.11  text {*
    1.12    The theory of partially ordered rings is taken from the books:
    1.13    \begin{itemize}
    1.14 @@ -645,31 +641,29 @@
    1.15    \end{itemize}
    1.16  *}
    1.17  
    1.18 -class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
    1.19 +class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
    1.20 +  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    1.21 +  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
    1.22  begin
    1.23  
    1.24  lemma mult_mono:
    1.25 -  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
    1.26 -     \<Longrightarrow> a * c \<le> b * d"
    1.27 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
    1.28  apply (erule mult_right_mono [THEN order_trans], assumption)
    1.29  apply (erule mult_left_mono, assumption)
    1.30  done
    1.31  
    1.32  lemma mult_mono':
    1.33 -  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
    1.34 -     \<Longrightarrow> a * c \<le> b * d"
    1.35 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
    1.36  apply (rule mult_mono)
    1.37  apply (fast intro: order_trans)+
    1.38  done
    1.39  
    1.40  end
    1.41  
    1.42 -class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
    1.43 -  + semiring + cancel_comm_monoid_add
    1.44 +class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
    1.45  begin
    1.46  
    1.47  subclass semiring_0_cancel ..
    1.48 -subclass ordered_semiring ..
    1.49  
    1.50  lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
    1.51  using mult_left_mono [of 0 b a] by simp
    1.52 @@ -689,7 +683,7 @@
    1.53  
    1.54  end
    1.55  
    1.56 -class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
    1.57 +class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
    1.58  begin
    1.59  
    1.60  subclass ordered_cancel_semiring ..
    1.61 @@ -854,41 +848,38 @@
    1.62  
    1.63  end
    1.64  
    1.65 -class mult_mono1 = times + zero + ord +
    1.66 -  assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    1.67 -
    1.68 -class ordered_comm_semiring = comm_semiring_0
    1.69 -  + ordered_ab_semigroup_add + mult_mono1
    1.70 +class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
    1.71 +  assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    1.72  begin
    1.73  
    1.74  subclass ordered_semiring
    1.75  proof
    1.76    fix a b c :: 'a
    1.77    assume "a \<le> b" "0 \<le> c"
    1.78 -  thus "c * a \<le> c * b" by (rule mult_mono1)
    1.79 +  thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
    1.80    thus "a * c \<le> b * c" by (simp only: mult_commute)
    1.81  qed
    1.82  
    1.83  end
    1.84  
    1.85 -class ordered_cancel_comm_semiring = comm_semiring_0_cancel
    1.86 -  + ordered_ab_semigroup_add + mult_mono1
    1.87 +class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
    1.88  begin
    1.89  
    1.90 +subclass comm_semiring_0_cancel ..
    1.91  subclass ordered_comm_semiring ..
    1.92  subclass ordered_cancel_semiring ..
    1.93  
    1.94  end
    1.95  
    1.96  class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
    1.97 -  assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
    1.98 +  assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
    1.99  begin
   1.100  
   1.101  subclass linordered_semiring_strict
   1.102  proof
   1.103    fix a b c :: 'a
   1.104    assume "a < b" "0 < c"
   1.105 -  thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
   1.106 +  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
   1.107    thus "a * c < b * c" by (simp only: mult_commute)
   1.108  qed
   1.109