src/HOL/Multivariate_Analysis/Norm_Arith.thy
 changeset 63627 6ddb43c6b711 parent 63626 44ce6b524ff3 child 63631 2edc8da89edc child 63633 2accfb71e33b
```     1.1 --- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Fri Aug 05 18:34:57 2016 +0200
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,146 +0,0 @@
1.4 -(*  Title:      HOL/Multivariate_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.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.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 -