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