src/HOL/Analysis/Norm_Arith.thy
changeset 63627 6ddb43c6b711
parent 60420 884f54e01427
child 63928 d81fb5b46a5c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Mon Aug 08 14:13:14 2016 +0200
     1.3 @@ -0,0 +1,146 @@
     1.4 +(*  Title:      HOL/Analysis/Norm_Arith.thy
     1.5 +    Author:     Amine Chaieb, University of Cambridge
     1.6 +*)
     1.7 +
     1.8 +section \<open>General linear decision procedure for normed spaces\<close>
     1.9 +
    1.10 +theory Norm_Arith
    1.11 +imports "~~/src/HOL/Library/Sum_of_Squares"
    1.12 +begin
    1.13 +
    1.14 +lemma norm_cmul_rule_thm:
    1.15 +  fixes x :: "'a::real_normed_vector"
    1.16 +  shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)"
    1.17 +  unfolding norm_scaleR
    1.18 +  apply (erule mult_left_mono)
    1.19 +  apply simp
    1.20 +  done
    1.21 +
    1.22 +(* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
    1.23 +lemma norm_add_rule_thm:
    1.24 +  fixes x1 x2 :: "'a::real_normed_vector"
    1.25 +  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
    1.26 +  by (rule order_trans [OF norm_triangle_ineq add_mono])
    1.27 +
    1.28 +lemma ge_iff_diff_ge_0:
    1.29 +  fixes a :: "'a::linordered_ring"
    1.30 +  shows "a \<ge> b \<equiv> a - b \<ge> 0"
    1.31 +  by (simp add: field_simps)
    1.32 +
    1.33 +lemma pth_1:
    1.34 +  fixes x :: "'a::real_normed_vector"
    1.35 +  shows "x \<equiv> scaleR 1 x" by simp
    1.36 +
    1.37 +lemma pth_2:
    1.38 +  fixes x :: "'a::real_normed_vector"
    1.39 +  shows "x - y \<equiv> x + -y"
    1.40 +  by (atomize (full)) simp
    1.41 +
    1.42 +lemma pth_3:
    1.43 +  fixes x :: "'a::real_normed_vector"
    1.44 +  shows "- x \<equiv> scaleR (-1) x"
    1.45 +  by simp
    1.46 +
    1.47 +lemma pth_4:
    1.48 +  fixes x :: "'a::real_normed_vector"
    1.49 +  shows "scaleR 0 x \<equiv> 0"
    1.50 +    and "scaleR c 0 = (0::'a)"
    1.51 +  by simp_all
    1.52 +
    1.53 +lemma pth_5:
    1.54 +  fixes x :: "'a::real_normed_vector"
    1.55 +  shows "scaleR c (scaleR d x) \<equiv> scaleR (c * d) x"
    1.56 +  by simp
    1.57 +
    1.58 +lemma pth_6:
    1.59 +  fixes x :: "'a::real_normed_vector"
    1.60 +  shows "scaleR c (x + y) \<equiv> scaleR c x + scaleR c y"
    1.61 +  by (simp add: scaleR_right_distrib)
    1.62 +
    1.63 +lemma pth_7:
    1.64 +  fixes x :: "'a::real_normed_vector"
    1.65 +  shows "0 + x \<equiv> x"
    1.66 +    and "x + 0 \<equiv> x"
    1.67 +  by simp_all
    1.68 +
    1.69 +lemma pth_8:
    1.70 +  fixes x :: "'a::real_normed_vector"
    1.71 +  shows "scaleR c x + scaleR d x \<equiv> scaleR (c + d) x"
    1.72 +  by (simp add: scaleR_left_distrib)
    1.73 +
    1.74 +lemma pth_9:
    1.75 +  fixes x :: "'a::real_normed_vector"
    1.76 +  shows "(scaleR c x + z) + scaleR d x \<equiv> scaleR (c + d) x + z"
    1.77 +    and "scaleR c x + (scaleR d x + z) \<equiv> scaleR (c + d) x + z"
    1.78 +    and "(scaleR c x + w) + (scaleR d x + z) \<equiv> scaleR (c + d) x + (w + z)"
    1.79 +  by (simp_all add: algebra_simps)
    1.80 +
    1.81 +lemma pth_a:
    1.82 +  fixes x :: "'a::real_normed_vector"
    1.83 +  shows "scaleR 0 x + y \<equiv> y"
    1.84 +  by simp
    1.85 +
    1.86 +lemma pth_b:
    1.87 +  fixes x :: "'a::real_normed_vector"
    1.88 +  shows "scaleR c x + scaleR d y \<equiv> scaleR c x + scaleR d y"
    1.89 +    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR c x + (z + scaleR d y)"
    1.90 +    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR c x + (scaleR d y + z)"
    1.91 +    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR c x + (w + (scaleR d y + z))"
    1.92 +  by (simp_all add: algebra_simps)
    1.93 +
    1.94 +lemma pth_c:
    1.95 +  fixes x :: "'a::real_normed_vector"
    1.96 +  shows "scaleR c x + scaleR d y \<equiv> scaleR d y + scaleR c x"
    1.97 +    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR d y + (scaleR c x + z)"
    1.98 +    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR d y + (scaleR c x + z)"
    1.99 +    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR d y + ((scaleR c x + w) + z)"
   1.100 +  by (simp_all add: algebra_simps)
   1.101 +
   1.102 +lemma pth_d:
   1.103 +  fixes x :: "'a::real_normed_vector"
   1.104 +  shows "x + 0 \<equiv> x"
   1.105 +  by simp
   1.106 +
   1.107 +lemma norm_imp_pos_and_ge:
   1.108 +  fixes x :: "'a::real_normed_vector"
   1.109 +  shows "norm x \<equiv> n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
   1.110 +  by atomize auto
   1.111 +
   1.112 +lemma real_eq_0_iff_le_ge_0:
   1.113 +  fixes x :: real
   1.114 +  shows "x = 0 \<equiv> x \<ge> 0 \<and> - x \<ge> 0"
   1.115 +  by arith
   1.116 +
   1.117 +lemma norm_pths:
   1.118 +  fixes x :: "'a::real_normed_vector"
   1.119 +  shows "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
   1.120 +    and "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   1.121 +  using norm_ge_zero[of "x - y"] by auto
   1.122 +
   1.123 +lemmas arithmetic_simps =
   1.124 +  arith_simps
   1.125 +  add_numeral_special
   1.126 +  add_neg_numeral_special
   1.127 +  mult_1_left
   1.128 +  mult_1_right
   1.129 +
   1.130 +ML_file "normarith.ML"
   1.131 +
   1.132 +method_setup norm = \<open>
   1.133 +  Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   1.134 +\<close> "prove simple linear statements about vector norms"
   1.135 +
   1.136 +
   1.137 +text \<open>Hence more metric properties.\<close>
   1.138 +
   1.139 +lemma dist_triangle_add:
   1.140 +  fixes x y x' y' :: "'a::real_normed_vector"
   1.141 +  shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
   1.142 +  by norm
   1.143 +
   1.144 +lemma dist_triangle_add_half:
   1.145 +  fixes x x' y y' :: "'a::real_normed_vector"
   1.146 +  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
   1.147 +  by norm
   1.148 +
   1.149 +end