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