src/HOL/Real_Vector_Spaces.thy
changeset 54778 13f08c876899
parent 54703 499f92dc6e45
child 54785 4876fb408c0d
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -431,6 +431,121 @@
     1.4    "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
     1.5    by (rule Reals_cases) auto
     1.6  
     1.7 +subsection {* Ordered real vector spaces *}
     1.8 +
     1.9 +class ordered_real_vector = real_vector + ordered_ab_group_add +
    1.10 +  assumes scaleR_left_mono: "x \<le> y \<Longrightarrow> 0 \<le> a \<Longrightarrow> a *\<^sub>R x \<le> a *\<^sub>R y"
    1.11 +  assumes scaleR_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>R x \<le> b *\<^sub>R x"
    1.12 +begin
    1.13 +
    1.14 +lemma scaleR_mono:
    1.15 +  "a \<le> b \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>R x \<le> b *\<^sub>R y"
    1.16 +apply (erule scaleR_right_mono [THEN order_trans], assumption)
    1.17 +apply (erule scaleR_left_mono, assumption)
    1.18 +done
    1.19 +
    1.20 +lemma scaleR_mono':
    1.21 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R d"
    1.22 +  by (rule scaleR_mono) (auto intro: order.trans)
    1.23 +
    1.24 +end
    1.25 +
    1.26 +lemma scaleR_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> (x::'a::ordered_real_vector) \<Longrightarrow> 0 \<le> a *\<^sub>R x"
    1.27 +  using scaleR_left_mono [of 0 x a]
    1.28 +  by simp
    1.29 +
    1.30 +lemma scaleR_nonneg_nonpos: "0 \<le> a \<Longrightarrow> (x::'a::ordered_real_vector) \<le> 0 \<Longrightarrow> a *\<^sub>R x \<le> 0"
    1.31 +  using scaleR_left_mono [of x 0 a] by simp
    1.32 +
    1.33 +lemma scaleR_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> (x::'a::ordered_real_vector) \<Longrightarrow> a *\<^sub>R x \<le> 0"
    1.34 +  using scaleR_right_mono [of a 0 x] by simp
    1.35 +
    1.36 +lemma split_scaleR_neg_le: "(0 \<le> a & x \<le> 0) | (a \<le> 0 & 0 \<le> x) \<Longrightarrow>
    1.37 +  a *\<^sub>R (x::'a::ordered_real_vector) \<le> 0"
    1.38 +  by (auto simp add: scaleR_nonneg_nonpos scaleR_nonpos_nonneg)
    1.39 +
    1.40 +lemma le_add_iff1:
    1.41 +  fixes c d e::"'a::ordered_real_vector"
    1.42 +  shows "a *\<^sub>R e + c \<le> b *\<^sub>R e + d \<longleftrightarrow> (a - b) *\<^sub>R e + c \<le> d"
    1.43 +  by (simp add: algebra_simps)
    1.44 +
    1.45 +lemma le_add_iff2:
    1.46 +  fixes c d e::"'a::ordered_real_vector"
    1.47 +  shows "a *\<^sub>R e + c \<le> b *\<^sub>R e + d \<longleftrightarrow> c \<le> (b - a) *\<^sub>R e + d"
    1.48 +  by (simp add: algebra_simps)
    1.49 +
    1.50 +lemma scaleR_left_mono_neg:
    1.51 +  fixes a b::"'a::ordered_real_vector"
    1.52 +  shows "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b"
    1.53 +  apply (drule scaleR_left_mono [of _ _ "- c"])
    1.54 +  apply simp_all
    1.55 +  done
    1.56 +
    1.57 +lemma scaleR_right_mono_neg:
    1.58 +  fixes c::"'a::ordered_real_vector"
    1.59 +  shows "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R c"
    1.60 +  apply (drule scaleR_right_mono [of _ _ "- c"])
    1.61 +  apply simp_all
    1.62 +  done
    1.63 +
    1.64 +lemma scaleR_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> (b::'a::ordered_real_vector) \<le> 0 \<Longrightarrow> 0 \<le> a *\<^sub>R b"
    1.65 +using scaleR_right_mono_neg [of a 0 b] by simp
    1.66 +
    1.67 +lemma split_scaleR_pos_le:
    1.68 +  fixes b::"'a::ordered_real_vector"
    1.69 +  shows "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a *\<^sub>R b"
    1.70 +  by (auto simp add: scaleR_nonneg_nonneg scaleR_nonpos_nonpos)
    1.71 +
    1.72 +lemma zero_le_scaleR_iff:
    1.73 +  fixes b::"'a::ordered_real_vector"
    1.74 +  shows "0 \<le> a *\<^sub>R b \<longleftrightarrow> 0 < a \<and> 0 \<le> b \<or> a < 0 \<and> b \<le> 0 \<or> a = 0" (is "?lhs = ?rhs")
    1.75 +proof cases
    1.76 +  assume "a \<noteq> 0"
    1.77 +  show ?thesis
    1.78 +  proof
    1.79 +    assume lhs: ?lhs
    1.80 +    {
    1.81 +      assume "0 < a"
    1.82 +      with lhs have "inverse a *\<^sub>R 0 \<le> inverse a *\<^sub>R (a *\<^sub>R b)"
    1.83 +        by (intro scaleR_mono) auto
    1.84 +      hence ?rhs using `0 < a`
    1.85 +        by simp
    1.86 +    } moreover {
    1.87 +      assume "0 > a"
    1.88 +      with lhs have "- inverse a *\<^sub>R 0 \<le> - inverse a *\<^sub>R (a *\<^sub>R b)"
    1.89 +        by (intro scaleR_mono) auto
    1.90 +      hence ?rhs using `0 > a`
    1.91 +        by simp
    1.92 +    } ultimately show ?rhs using `a \<noteq> 0` by arith
    1.93 +  qed (auto simp: not_le `a \<noteq> 0` intro!: split_scaleR_pos_le)
    1.94 +qed simp
    1.95 +
    1.96 +lemma scaleR_le_0_iff:
    1.97 +  fixes b::"'a::ordered_real_vector"
    1.98 +  shows "a *\<^sub>R b \<le> 0 \<longleftrightarrow> 0 < a \<and> b \<le> 0 \<or> a < 0 \<and> 0 \<le> b \<or> a = 0"
    1.99 +  by (insert zero_le_scaleR_iff [of "-a" b]) force
   1.100 +
   1.101 +lemma scaleR_le_cancel_left:
   1.102 +  fixes b::"'a::ordered_real_vector"
   1.103 +  shows "c *\<^sub>R a \<le> c *\<^sub>R b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   1.104 +  by (auto simp add: neq_iff scaleR_left_mono scaleR_left_mono_neg
   1.105 +    dest: scaleR_left_mono[where a="inverse c"] scaleR_left_mono_neg[where c="inverse c"])
   1.106 +
   1.107 +lemma scaleR_le_cancel_left_pos:
   1.108 +  fixes b::"'a::ordered_real_vector"
   1.109 +  shows "0 < c \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b \<longleftrightarrow> a \<le> b"
   1.110 +  by (auto simp: scaleR_le_cancel_left)
   1.111 +
   1.112 +lemma scaleR_le_cancel_left_neg:
   1.113 +  fixes b::"'a::ordered_real_vector"
   1.114 +  shows "c < 0 \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b \<longleftrightarrow> b \<le> a"
   1.115 +  by (auto simp: scaleR_le_cancel_left)
   1.116 +
   1.117 +lemma scaleR_left_le_one_le:
   1.118 +  fixes x::"'a::ordered_real_vector" and a::real
   1.119 +  shows "0 \<le> x \<Longrightarrow> a \<le> 1 \<Longrightarrow> a *\<^sub>R x \<le> x"
   1.120 +  using scaleR_right_mono[of a 1 x] by simp
   1.121 +
   1.122  
   1.123  subsection {* Real normed vector spaces *}
   1.124