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