Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
authorhoelzl
Tue Apr 20 17:58:34 2010 +0200 (2010-04-20)
changeset 36622e393a91f86df
parent 36609 6ed6112f0a95
child 36623 d26348b667f2
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
src/HOL/Big_Operators.thy
src/HOL/List.thy
src/HOL/Log.thy
src/HOL/Product_Type.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Apr 20 17:58:34 2010 +0200
     1.3 @@ -554,6 +554,26 @@
     1.4    case False thus ?thesis by (simp add: setsum_def)
     1.5  qed
     1.6  
     1.7 +lemma setsum_nonneg_leq_bound:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
     1.9 +  assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
    1.10 +  shows "f i \<le> B"
    1.11 +proof -
    1.12 +  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
    1.13 +    using assms by (auto intro!: setsum_nonneg)
    1.14 +  moreover
    1.15 +  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
    1.16 +    using assms by (simp add: setsum_diff1)
    1.17 +  ultimately show ?thesis by auto
    1.18 +qed
    1.19 +
    1.20 +lemma setsum_nonneg_0:
    1.21 +  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
    1.22 +  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
    1.23 +  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
    1.24 +  shows "f i = 0"
    1.25 +  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
    1.26 +
    1.27  lemma setsum_mono2:
    1.28  fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
    1.29  assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
     2.1 --- a/src/HOL/List.thy	Mon May 03 07:59:51 2010 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Apr 20 17:58:34 2010 +0200
     2.3 @@ -3039,6 +3039,9 @@
     2.4  lemma length_replicate [simp]: "length (replicate n x) = n"
     2.5  by (induct n) auto
     2.6  
     2.7 +lemma Ex_list_of_length: "\<exists>xs. length xs = n"
     2.8 +by (rule exI[of _ "replicate n undefined"]) simp
     2.9 +
    2.10  lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
    2.11  by (induct n) auto
    2.12  
     3.1 --- a/src/HOL/Log.thy	Mon May 03 07:59:51 2010 +0200
     3.2 +++ b/src/HOL/Log.thy	Tue Apr 20 17:58:34 2010 +0200
     3.3 @@ -145,6 +145,21 @@
     3.4  apply (drule_tac a = "log a x" in powr_less_mono, auto)
     3.5  done
     3.6  
     3.7 +lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}"
     3.8 +proof (rule inj_onI, simp)
     3.9 +  fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
    3.10 +  show "x = y"
    3.11 +  proof (cases rule: linorder_cases)
    3.12 +    assume "x < y" hence "log b x < log b y"
    3.13 +      using log_less_cancel_iff[OF `1 < b`] pos by simp
    3.14 +    thus ?thesis using * by simp
    3.15 +  next
    3.16 +    assume "y < x" hence "log b y < log b x"
    3.17 +      using log_less_cancel_iff[OF `1 < b`] pos by simp
    3.18 +    thus ?thesis using * by simp
    3.19 +  qed simp
    3.20 +qed
    3.21 +
    3.22  lemma log_le_cancel_iff [simp]:
    3.23       "[| 1 < a; 0 < x; 0 < y |] ==> (log a x \<le> log a y) = (x \<le> y)"
    3.24  by (simp add: linorder_not_less [symmetric])
     4.1 --- a/src/HOL/Product_Type.thy	Mon May 03 07:59:51 2010 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Tue Apr 20 17:58:34 2010 +0200
     4.3 @@ -990,6 +990,15 @@
     4.4  lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
     4.5  by blast
     4.6  
     4.7 +lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
     4.8 +  by auto
     4.9 +
    4.10 +lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
    4.11 +  by (auto intro!: image_eqI)
    4.12 +
    4.13 +lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
    4.14 +  by (auto intro!: image_eqI)
    4.15 +
    4.16  lemma insert_times_insert[simp]:
    4.17    "insert a A \<times> insert b B =
    4.18     insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
    4.19 @@ -999,13 +1008,20 @@
    4.20    by (auto, rule_tac p = "f x" in PairE, auto)
    4.21  
    4.22  lemma swap_inj_on:
    4.23 -  "inj_on (%(i, j). (j, i)) (A \<times> B)"
    4.24 -  by (unfold inj_on_def) fast
    4.25 +  "inj_on (\<lambda>(i, j). (j, i)) A"
    4.26 +  by (auto intro!: inj_onI)
    4.27  
    4.28  lemma swap_product:
    4.29    "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
    4.30    by (simp add: split_def image_def) blast
    4.31  
    4.32 +lemma image_split_eq_Sigma:
    4.33 +  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
    4.34 +proof (safe intro!: imageI vimageI)
    4.35 +  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
    4.36 +  show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
    4.37 +    using * eq[symmetric] by auto
    4.38 +qed simp_all
    4.39  
    4.40  subsubsection {* Code generator setup *}
    4.41  
     5.1 --- a/src/HOL/Rings.thy	Mon May 03 07:59:51 2010 +0200
     5.2 +++ b/src/HOL/Rings.thy	Tue Apr 20 17:58:34 2010 +0200
     5.3 @@ -684,6 +684,18 @@
     5.4  end
     5.5  
     5.6  class linordered_semiring_1 = linordered_semiring + semiring_1
     5.7 +begin
     5.8 +
     5.9 +lemma convex_bound_le:
    5.10 +  assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
    5.11 +  shows "u * x + v * y \<le> a"
    5.12 +proof-
    5.13 +  from assms have "u * x + v * y \<le> u * a + v * a"
    5.14 +    by (simp add: add_mono mult_left_mono)
    5.15 +  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
    5.16 +qed
    5.17 +
    5.18 +end
    5.19  
    5.20  class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
    5.21    assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
    5.22 @@ -803,6 +815,21 @@
    5.23  end
    5.24  
    5.25  class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
    5.26 +begin
    5.27 +
    5.28 +subclass linordered_semiring_1 ..
    5.29 +
    5.30 +lemma convex_bound_lt:
    5.31 +  assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
    5.32 +  shows "u * x + v * y < a"
    5.33 +proof -
    5.34 +  from assms have "u * x + v * y < u * a + v * a"
    5.35 +    by (cases "u = 0")
    5.36 +       (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
    5.37 +  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
    5.38 +qed
    5.39 +
    5.40 +end
    5.41  
    5.42  class mult_mono1 = times + zero + ord +
    5.43    assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    5.44 @@ -1108,6 +1135,7 @@
    5.45    (*previously linordered_ring*)
    5.46  begin
    5.47  
    5.48 +subclass linordered_semiring_1_strict ..
    5.49  subclass linordered_ring_strict ..
    5.50  subclass ordered_comm_ring ..
    5.51  subclass idom ..