introduced ordered real vector spaces
authorimmler
Mon Dec 16 17:08:22 2013 +0100 (2013-12-16)
changeset 5477813f08c876899
parent 54777 1a2da44c8e7d
child 54779 d9edb711ef31
introduced ordered real vector spaces
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Dec 16 17:08:22 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -3129,6 +3129,9 @@
     1.4  subclass ordered_ab_group_add_abs
     1.5    by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
     1.6  
     1.7 +subclass ordered_real_vector
     1.8 +  by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
     1.9 +
    1.10  subclass lattice
    1.11    by default (auto simp: eucl_inf eucl_sup eucl_le)
    1.12  
     2.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
     2.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Dec 16 17:08:22 2013 +0100
     2.3 @@ -431,6 +431,121 @@
     2.4    "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
     2.5    by (rule Reals_cases) auto
     2.6  
     2.7 +subsection {* Ordered real vector spaces *}
     2.8 +
     2.9 +class ordered_real_vector = real_vector + ordered_ab_group_add +
    2.10 +  assumes scaleR_left_mono: "x \<le> y \<Longrightarrow> 0 \<le> a \<Longrightarrow> a *\<^sub>R x \<le> a *\<^sub>R y"
    2.11 +  assumes scaleR_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>R x \<le> b *\<^sub>R x"
    2.12 +begin
    2.13 +
    2.14 +lemma scaleR_mono:
    2.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"
    2.16 +apply (erule scaleR_right_mono [THEN order_trans], assumption)
    2.17 +apply (erule scaleR_left_mono, assumption)
    2.18 +done
    2.19 +
    2.20 +lemma scaleR_mono':
    2.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"
    2.22 +  by (rule scaleR_mono) (auto intro: order.trans)
    2.23 +
    2.24 +end
    2.25 +
    2.26 +lemma scaleR_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> (x::'a::ordered_real_vector) \<Longrightarrow> 0 \<le> a *\<^sub>R x"
    2.27 +  using scaleR_left_mono [of 0 x a]
    2.28 +  by simp
    2.29 +
    2.30 +lemma scaleR_nonneg_nonpos: "0 \<le> a \<Longrightarrow> (x::'a::ordered_real_vector) \<le> 0 \<Longrightarrow> a *\<^sub>R x \<le> 0"
    2.31 +  using scaleR_left_mono [of x 0 a] by simp
    2.32 +
    2.33 +lemma scaleR_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> (x::'a::ordered_real_vector) \<Longrightarrow> a *\<^sub>R x \<le> 0"
    2.34 +  using scaleR_right_mono [of a 0 x] by simp
    2.35 +
    2.36 +lemma split_scaleR_neg_le: "(0 \<le> a & x \<le> 0) | (a \<le> 0 & 0 \<le> x) \<Longrightarrow>
    2.37 +  a *\<^sub>R (x::'a::ordered_real_vector) \<le> 0"
    2.38 +  by (auto simp add: scaleR_nonneg_nonpos scaleR_nonpos_nonneg)
    2.39 +
    2.40 +lemma le_add_iff1:
    2.41 +  fixes c d e::"'a::ordered_real_vector"
    2.42 +  shows "a *\<^sub>R e + c \<le> b *\<^sub>R e + d \<longleftrightarrow> (a - b) *\<^sub>R e + c \<le> d"
    2.43 +  by (simp add: algebra_simps)
    2.44 +
    2.45 +lemma le_add_iff2:
    2.46 +  fixes c d e::"'a::ordered_real_vector"
    2.47 +  shows "a *\<^sub>R e + c \<le> b *\<^sub>R e + d \<longleftrightarrow> c \<le> (b - a) *\<^sub>R e + d"
    2.48 +  by (simp add: algebra_simps)
    2.49 +
    2.50 +lemma scaleR_left_mono_neg:
    2.51 +  fixes a b::"'a::ordered_real_vector"
    2.52 +  shows "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b"
    2.53 +  apply (drule scaleR_left_mono [of _ _ "- c"])
    2.54 +  apply simp_all
    2.55 +  done
    2.56 +
    2.57 +lemma scaleR_right_mono_neg:
    2.58 +  fixes c::"'a::ordered_real_vector"
    2.59 +  shows "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R c"
    2.60 +  apply (drule scaleR_right_mono [of _ _ "- c"])
    2.61 +  apply simp_all
    2.62 +  done
    2.63 +
    2.64 +lemma scaleR_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> (b::'a::ordered_real_vector) \<le> 0 \<Longrightarrow> 0 \<le> a *\<^sub>R b"
    2.65 +using scaleR_right_mono_neg [of a 0 b] by simp
    2.66 +
    2.67 +lemma split_scaleR_pos_le:
    2.68 +  fixes b::"'a::ordered_real_vector"
    2.69 +  shows "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a *\<^sub>R b"
    2.70 +  by (auto simp add: scaleR_nonneg_nonneg scaleR_nonpos_nonpos)
    2.71 +
    2.72 +lemma zero_le_scaleR_iff:
    2.73 +  fixes b::"'a::ordered_real_vector"
    2.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")
    2.75 +proof cases
    2.76 +  assume "a \<noteq> 0"
    2.77 +  show ?thesis
    2.78 +  proof
    2.79 +    assume lhs: ?lhs
    2.80 +    {
    2.81 +      assume "0 < a"
    2.82 +      with lhs have "inverse a *\<^sub>R 0 \<le> inverse a *\<^sub>R (a *\<^sub>R b)"
    2.83 +        by (intro scaleR_mono) auto
    2.84 +      hence ?rhs using `0 < a`
    2.85 +        by simp
    2.86 +    } moreover {
    2.87 +      assume "0 > a"
    2.88 +      with lhs have "- inverse a *\<^sub>R 0 \<le> - inverse a *\<^sub>R (a *\<^sub>R b)"
    2.89 +        by (intro scaleR_mono) auto
    2.90 +      hence ?rhs using `0 > a`
    2.91 +        by simp
    2.92 +    } ultimately show ?rhs using `a \<noteq> 0` by arith
    2.93 +  qed (auto simp: not_le `a \<noteq> 0` intro!: split_scaleR_pos_le)
    2.94 +qed simp
    2.95 +
    2.96 +lemma scaleR_le_0_iff:
    2.97 +  fixes b::"'a::ordered_real_vector"
    2.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"
    2.99 +  by (insert zero_le_scaleR_iff [of "-a" b]) force
   2.100 +
   2.101 +lemma scaleR_le_cancel_left:
   2.102 +  fixes b::"'a::ordered_real_vector"
   2.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)"
   2.104 +  by (auto simp add: neq_iff scaleR_left_mono scaleR_left_mono_neg
   2.105 +    dest: scaleR_left_mono[where a="inverse c"] scaleR_left_mono_neg[where c="inverse c"])
   2.106 +
   2.107 +lemma scaleR_le_cancel_left_pos:
   2.108 +  fixes b::"'a::ordered_real_vector"
   2.109 +  shows "0 < c \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b \<longleftrightarrow> a \<le> b"
   2.110 +  by (auto simp: scaleR_le_cancel_left)
   2.111 +
   2.112 +lemma scaleR_le_cancel_left_neg:
   2.113 +  fixes b::"'a::ordered_real_vector"
   2.114 +  shows "c < 0 \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b \<longleftrightarrow> b \<le> a"
   2.115 +  by (auto simp: scaleR_le_cancel_left)
   2.116 +
   2.117 +lemma scaleR_left_le_one_le:
   2.118 +  fixes x::"'a::ordered_real_vector" and a::real
   2.119 +  shows "0 \<le> x \<Longrightarrow> a \<le> 1 \<Longrightarrow> a *\<^sub>R x \<le> x"
   2.120 +  using scaleR_right_mono[of a 1 x] by simp
   2.121 +
   2.122  
   2.123  subsection {* Real normed vector spaces *}
   2.124