Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.

--- a/src/HOL/Big_Operators.thy	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Big_Operators.thy	Tue Apr 20 17:58:34 2010 +0200
@@ -554,6 +554,26 @@
   case False thus ?thesis by (simp add: setsum_def)
 qed
 
+lemma setsum_nonneg_leq_bound:
+  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
+  assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
+  shows "f i \<le> B"
+proof -
+  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
+    using assms by (auto intro!: setsum_nonneg)
+  moreover
+  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
+    using assms by (simp add: setsum_diff1)
+  ultimately show ?thesis by auto
+qed
+
+lemma setsum_nonneg_0:
+  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
+  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
+  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
+  shows "f i = 0"
+  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
+
 lemma setsum_mono2:
 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"

--- a/src/HOL/List.thy	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/List.thy	Tue Apr 20 17:58:34 2010 +0200
@@ -3039,6 +3039,9 @@
 lemma length_replicate [simp]: "length (replicate n x) = n"
 by (induct n) auto
 
+lemma Ex_list_of_length: "\<exists>xs. length xs = n"
+by (rule exI[of _ "replicate n undefined"]) simp
+
 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
 by (induct n) auto
 

--- a/src/HOL/Log.thy	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Log.thy	Tue Apr 20 17:58:34 2010 +0200
@@ -145,6 +145,21 @@
 apply (drule_tac a = "log a x" in powr_less_mono, auto)
 done
 
+lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}"
+proof (rule inj_onI, simp)
+  fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
+  show "x = y"
+  proof (cases rule: linorder_cases)
+    assume "x < y" hence "log b x < log b y"
+      using log_less_cancel_iff[OF `1 < b`] pos by simp
+    thus ?thesis using * by simp
+  next
+    assume "y < x" hence "log b y < log b x"
+      using log_less_cancel_iff[OF `1 < b`] pos by simp
+    thus ?thesis using * by simp
+  qed simp
+qed
+
 lemma log_le_cancel_iff [simp]:
      "[| 1 < a; 0 < x; 0 < y |] ==> (log a x \<le> log a y) = (x \<le> y)"
 by (simp add: linorder_not_less [symmetric])

--- a/src/HOL/Product_Type.thy	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Product_Type.thy	Tue Apr 20 17:58:34 2010 +0200
@@ -990,6 +990,15 @@
 lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
 by blast
 
+lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
+  by auto
+
+lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
+  by (auto intro!: image_eqI)
+
+lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
+  by (auto intro!: image_eqI)
+
 lemma insert_times_insert[simp]:
   "insert a A \<times> insert b B =
    insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
@@ -999,13 +1008,20 @@
   by (auto, rule_tac p = "f x" in PairE, auto)
 
 lemma swap_inj_on:
-  "inj_on (%(i, j). (j, i)) (A \<times> B)"
-  by (unfold inj_on_def) fast
+  "inj_on (\<lambda>(i, j). (j, i)) A"
+  by (auto intro!: inj_onI)
 
 lemma swap_product:
   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
   by (simp add: split_def image_def) blast
 
+lemma image_split_eq_Sigma:
+  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
+proof (safe intro!: imageI vimageI)
+  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
+  show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
+    using * eq[symmetric] by auto
+qed simp_all
 
 subsubsection {* Code generator setup *}
 

--- a/src/HOL/Rings.thy	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Rings.thy	Tue Apr 20 17:58:34 2010 +0200
@@ -684,6 +684,18 @@
 end
 
 class linordered_semiring_1 = linordered_semiring + semiring_1
+begin
+
+lemma convex_bound_le:
+  assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
+  shows "u * x + v * y \<le> a"
+proof-
+  from assms have "u * x + v * y \<le> u * a + v * a"
+    by (simp add: add_mono mult_left_mono)
+  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+qed
+
+end
 
 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
@@ -803,6 +815,21 @@
 end
 
 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
+begin
+
+subclass linordered_semiring_1 ..
+
+lemma convex_bound_lt:
+  assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
+  shows "u * x + v * y < a"
+proof -
+  from assms have "u * x + v * y < u * a + v * a"
+    by (cases "u = 0")
+       (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
+  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+qed
+
+end
 
 class mult_mono1 = times + zero + ord +
   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
@@ -1108,6 +1135,7 @@
   (*previously linordered_ring*)
 begin
 
+subclass linordered_semiring_1_strict ..
 subclass linordered_ring_strict ..
 subclass ordered_comm_ring ..
 subclass idom ..