src/HOL/Analysis/Norm_Arith.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69517 dc20f278e8f3
child 69565 1daf07b65385
permissions -rw-r--r--
capitalize proper names in lemma names
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 \<open>Linear Decision Procedure for Normed Spaces\<close>
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) \<Longrightarrow> 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 \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> 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 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> 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 \<ge> b \<equiv> a - b \<ge> 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 \<equiv> 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 \<equiv> 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 \<equiv> 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 \<equiv> 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) \<equiv> 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) \<equiv> 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 \<equiv> x"
wenzelm@53717
    68
    and "x + 0 \<equiv> 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 \<equiv> 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 \<equiv> scaleR (c + d) x + z"
wenzelm@53717
    79
    and "scaleR c x + (scaleR d x + z) \<equiv> scaleR (c + d) x + z"
wenzelm@53717
    80
    and "(scaleR c x + w) + (scaleR d x + z) \<equiv> 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 \<equiv> 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 \<equiv> scaleR c x + scaleR d y"
wenzelm@53717
    91
    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR c x + (z + scaleR d y)"
wenzelm@53717
    92
    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR c x + (scaleR d y + z)"
wenzelm@53717
    93
    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> 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 \<equiv> scaleR d y + scaleR c x"
wenzelm@53717
    99
    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR d y + (scaleR c x + z)"
wenzelm@53717
   100
    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR d y + (scaleR c x + z)"
wenzelm@53717
   101
    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> 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 \<equiv> 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 \<equiv> n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> 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 \<equiv> x \<ge> 0 \<and> - x \<ge> 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 \<longleftrightarrow> norm (x - y) \<le> 0"
wenzelm@53717
   122
    and "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 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 = \<open>
wenzelm@53717
   135
  Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
wenzelm@60420
   136
\<close> "prove simple linear statements about vector norms"
huffman@44516
   137
wenzelm@53717
   138
wenzelm@60420
   139
text \<open>Hence more metric properties.\<close>
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') \<le> 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 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
huffman@44516
   149
  by norm
huffman@44516
   150
huffman@44516
   151
end