src/HOL/Rings.thy
changeset 36622 e393a91f86df
parent 36348 89c54f51f55a
child 36719 d396f6f63d94
     1.1 --- a/src/HOL/Rings.thy	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Rings.thy	Tue Apr 20 17:58:34 2010 +0200
     1.3 @@ -684,6 +684,18 @@
     1.4  end
     1.5  
     1.6  class linordered_semiring_1 = linordered_semiring + semiring_1
     1.7 +begin
     1.8 +
     1.9 +lemma convex_bound_le:
    1.10 +  assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
    1.11 +  shows "u * x + v * y \<le> a"
    1.12 +proof-
    1.13 +  from assms have "u * x + v * y \<le> u * a + v * a"
    1.14 +    by (simp add: add_mono mult_left_mono)
    1.15 +  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
    1.16 +qed
    1.17 +
    1.18 +end
    1.19  
    1.20  class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
    1.21    assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
    1.22 @@ -803,6 +815,21 @@
    1.23  end
    1.24  
    1.25  class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
    1.26 +begin
    1.27 +
    1.28 +subclass linordered_semiring_1 ..
    1.29 +
    1.30 +lemma convex_bound_lt:
    1.31 +  assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
    1.32 +  shows "u * x + v * y < a"
    1.33 +proof -
    1.34 +  from assms have "u * x + v * y < u * a + v * a"
    1.35 +    by (cases "u = 0")
    1.36 +       (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
    1.37 +  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
    1.38 +qed
    1.39 +
    1.40 +end
    1.41  
    1.42  class mult_mono1 = times + zero + ord +
    1.43    assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    1.44 @@ -1108,6 +1135,7 @@
    1.45    (*previously linordered_ring*)
    1.46  begin
    1.47  
    1.48 +subclass linordered_semiring_1_strict ..
    1.49  subclass linordered_ring_strict ..
    1.50  subclass ordered_comm_ring ..
    1.51  subclass idom ..