src/HOL/Analysis/Norm_Arith.thy
 author nipkow Fri Dec 28 10:29:59 2018 +0100 (7 months ago) changeset 69517 dc20f278e8f3 parent 68607 67bb59e49834 child 69565 1daf07b65385 permissions -rw-r--r--
 hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/Norm_Arith.thy ``` huffman@44516 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` huffman@44516 ` 3` ```*) ``` huffman@44516 ` 4` nipkow@69517 ` 5` ```section \Linear Decision Procedure for Normed Spaces\ ``` huffman@44516 ` 6` huffman@44516 ` 7` ```theory Norm_Arith ``` wenzelm@66453 ` 8` ```imports "HOL-Library.Sum_of_Squares" ``` huffman@44516 ` 9` ```begin ``` huffman@44516 ` 10` lp15@63928 ` 11` ```(* FIXME: move elsewhere *) ``` lp15@63928 ` 12` ```lemma sum_sqs_eq: ``` lp15@63928 ` 13` ``` fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \ y = x" ``` lp15@63928 ` 14` ``` by algebra ``` lp15@63928 ` 15` huffman@44516 ` 16` ```lemma norm_cmul_rule_thm: ``` huffman@44516 ` 17` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 18` ``` shows "b \ norm x \ \c\ * b \ norm (scaleR c x)" ``` huffman@44516 ` 19` ``` unfolding norm_scaleR ``` huffman@44516 ` 20` ``` apply (erule mult_left_mono) ``` huffman@44516 ` 21` ``` apply simp ``` huffman@44516 ` 22` ``` done ``` huffman@44516 ` 23` wenzelm@53717 ` 24` ```(* FIXME: Move all these theorems into the ML code using lemma antiquotation *) ``` huffman@44516 ` 25` ```lemma norm_add_rule_thm: ``` huffman@44516 ` 26` ``` fixes x1 x2 :: "'a::real_normed_vector" ``` huffman@44516 ` 27` ``` shows "norm x1 \ b1 \ norm x2 \ b2 \ norm (x1 + x2) \ b1 + b2" ``` huffman@44516 ` 28` ``` by (rule order_trans [OF norm_triangle_ineq add_mono]) ``` huffman@44516 ` 29` wenzelm@53717 ` 30` ```lemma ge_iff_diff_ge_0: ``` wenzelm@53717 ` 31` ``` fixes a :: "'a::linordered_ring" ``` wenzelm@53717 ` 32` ``` shows "a \ b \ a - b \ 0" ``` huffman@44516 ` 33` ``` by (simp add: field_simps) ``` huffman@44516 ` 34` huffman@44516 ` 35` ```lemma pth_1: ``` huffman@44516 ` 36` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 37` ``` shows "x \ scaleR 1 x" by simp ``` huffman@44516 ` 38` huffman@44516 ` 39` ```lemma pth_2: ``` huffman@44516 ` 40` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 41` ``` shows "x - y \ x + -y" ``` wenzelm@53717 ` 42` ``` by (atomize (full)) simp ``` huffman@44516 ` 43` huffman@44516 ` 44` ```lemma pth_3: ``` huffman@44516 ` 45` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 46` ``` shows "- x \ scaleR (-1) x" ``` wenzelm@53717 ` 47` ``` by simp ``` huffman@44516 ` 48` huffman@44516 ` 49` ```lemma pth_4: ``` huffman@44516 ` 50` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 51` ``` shows "scaleR 0 x \ 0" ``` wenzelm@53717 ` 52` ``` and "scaleR c 0 = (0::'a)" ``` wenzelm@53717 ` 53` ``` by simp_all ``` huffman@44516 ` 54` huffman@44516 ` 55` ```lemma pth_5: ``` huffman@44516 ` 56` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 57` ``` shows "scaleR c (scaleR d x) \ scaleR (c * d) x" ``` wenzelm@53717 ` 58` ``` by simp ``` huffman@44516 ` 59` huffman@44516 ` 60` ```lemma pth_6: ``` huffman@44516 ` 61` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 62` ``` shows "scaleR c (x + y) \ scaleR c x + scaleR c y" ``` huffman@44516 ` 63` ``` by (simp add: scaleR_right_distrib) ``` huffman@44516 ` 64` huffman@44516 ` 65` ```lemma pth_7: ``` huffman@44516 ` 66` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 67` ``` shows "0 + x \ x" ``` wenzelm@53717 ` 68` ``` and "x + 0 \ x" ``` wenzelm@53717 ` 69` ``` by simp_all ``` huffman@44516 ` 70` huffman@44516 ` 71` ```lemma pth_8: ``` huffman@44516 ` 72` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 73` ``` shows "scaleR c x + scaleR d x \ scaleR (c + d) x" ``` huffman@44516 ` 74` ``` by (simp add: scaleR_left_distrib) ``` huffman@44516 ` 75` huffman@44516 ` 76` ```lemma pth_9: ``` wenzelm@53717 ` 77` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 78` ``` shows "(scaleR c x + z) + scaleR d x \ scaleR (c + d) x + z" ``` wenzelm@53717 ` 79` ``` and "scaleR c x + (scaleR d x + z) \ scaleR (c + d) x + z" ``` wenzelm@53717 ` 80` ``` and "(scaleR c x + w) + (scaleR d x + z) \ scaleR (c + d) x + (w + z)" ``` huffman@44516 ` 81` ``` by (simp_all add: algebra_simps) ``` huffman@44516 ` 82` huffman@44516 ` 83` ```lemma pth_a: ``` huffman@44516 ` 84` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 85` ``` shows "scaleR 0 x + y \ y" ``` wenzelm@53717 ` 86` ``` by simp ``` huffman@44516 ` 87` huffman@44516 ` 88` ```lemma pth_b: ``` wenzelm@53717 ` 89` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 90` ``` shows "scaleR c x + scaleR d y \ scaleR c x + scaleR d y" ``` wenzelm@53717 ` 91` ``` and "(scaleR c x + z) + scaleR d y \ scaleR c x + (z + scaleR d y)" ``` wenzelm@53717 ` 92` ``` and "scaleR c x + (scaleR d y + z) \ scaleR c x + (scaleR d y + z)" ``` wenzelm@53717 ` 93` ``` and "(scaleR c x + w) + (scaleR d y + z) \ scaleR c x + (w + (scaleR d y + z))" ``` huffman@44516 ` 94` ``` by (simp_all add: algebra_simps) ``` huffman@44516 ` 95` huffman@44516 ` 96` ```lemma pth_c: ``` wenzelm@53717 ` 97` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 98` ``` shows "scaleR c x + scaleR d y \ scaleR d y + scaleR c x" ``` wenzelm@53717 ` 99` ``` and "(scaleR c x + z) + scaleR d y \ scaleR d y + (scaleR c x + z)" ``` wenzelm@53717 ` 100` ``` and "scaleR c x + (scaleR d y + z) \ scaleR d y + (scaleR c x + z)" ``` wenzelm@53717 ` 101` ``` and "(scaleR c x + w) + (scaleR d y + z) \ scaleR d y + ((scaleR c x + w) + z)" ``` huffman@44516 ` 102` ``` by (simp_all add: algebra_simps) ``` huffman@44516 ` 103` huffman@44516 ` 104` ```lemma pth_d: ``` huffman@44516 ` 105` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 106` ``` shows "x + 0 \ x" ``` wenzelm@53717 ` 107` ``` by simp ``` huffman@44516 ` 108` huffman@44516 ` 109` ```lemma norm_imp_pos_and_ge: ``` huffman@44516 ` 110` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 111` ``` shows "norm x \ n \ norm x \ 0 \ n \ norm x" ``` huffman@44516 ` 112` ``` by atomize auto ``` huffman@44516 ` 113` wenzelm@53717 ` 114` ```lemma real_eq_0_iff_le_ge_0: ``` wenzelm@53717 ` 115` ``` fixes x :: real ``` wenzelm@53717 ` 116` ``` shows "x = 0 \ x \ 0 \ - x \ 0" ``` wenzelm@53717 ` 117` ``` by arith ``` huffman@44516 ` 118` huffman@44516 ` 119` ```lemma norm_pths: ``` wenzelm@53717 ` 120` ``` fixes x :: "'a::real_normed_vector" ``` wenzelm@53717 ` 121` ``` shows "x = y \ norm (x - y) \ 0" ``` wenzelm@53717 ` 122` ``` and "x \ y \ \ (norm (x - y) \ 0)" ``` huffman@44516 ` 123` ``` using norm_ge_zero[of "x - y"] by auto ``` huffman@44516 ` 124` huffman@47108 ` 125` ```lemmas arithmetic_simps = ``` huffman@47108 ` 126` ``` arith_simps ``` huffman@47108 ` 127` ``` add_numeral_special ``` huffman@47108 ` 128` ``` add_neg_numeral_special ``` huffman@47108 ` 129` ``` mult_1_left ``` huffman@47108 ` 130` ``` mult_1_right ``` huffman@47108 ` 131` wenzelm@48891 ` 132` ```ML_file "normarith.ML" ``` huffman@44516 ` 133` immler@67962 ` 134` ```method_setup%important norm = \ ``` wenzelm@53717 ` 135` ``` Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) ``` wenzelm@60420 ` 136` ```\ "prove simple linear statements about vector norms" ``` huffman@44516 ` 137` wenzelm@53717 ` 138` wenzelm@60420 ` 139` ```text \Hence more metric properties.\ ``` huffman@44516 ` 140` immler@68607 ` 141` ```proposition dist_triangle_add: ``` huffman@44516 ` 142` ``` fixes x y x' y' :: "'a::real_normed_vector" ``` wenzelm@53717 ` 143` ``` shows "dist (x + y) (x' + y') \ dist x x' + dist y y'" ``` huffman@44516 ` 144` ``` by norm ``` huffman@44516 ` 145` huffman@44516 ` 146` ```lemma dist_triangle_add_half: ``` huffman@44516 ` 147` ``` fixes x x' y y' :: "'a::real_normed_vector" ``` huffman@44516 ` 148` ``` shows "dist x x' < e / 2 \ dist y y' < e / 2 \ dist(x + y) (x' + y') < e" ``` huffman@44516 ` 149` ``` by norm ``` huffman@44516 ` 150` huffman@44516 ` 151` ```end ```