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.15 +  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
1.16 +qed
1.17 +
1.18 +end
1.19
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 ..
```