src/HOL/Multivariate_Analysis/Norm_Arith.thy
author huffman
Wed Aug 24 15:06:13 2011 -0700 (2011-08-24)
changeset 44516 d9a496ae5d9d
child 47108 2a1953f0d20d
permissions -rw-r--r--
move everything related to 'norm' method into new theory file Norm_Arith.thy
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
uses ("normarith.ML")
huffman@44516
    10
begin
huffman@44516
    11
huffman@44516
    12
lemma norm_cmul_rule_thm:
huffman@44516
    13
  fixes x :: "'a::real_normed_vector"
huffman@44516
    14
  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
huffman@44516
    15
  unfolding norm_scaleR
huffman@44516
    16
  apply (erule mult_left_mono)
huffman@44516
    17
  apply simp
huffman@44516
    18
  done
huffman@44516
    19
huffman@44516
    20
  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
huffman@44516
    21
lemma norm_add_rule_thm:
huffman@44516
    22
  fixes x1 x2 :: "'a::real_normed_vector"
huffman@44516
    23
  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
huffman@44516
    24
  by (rule order_trans [OF norm_triangle_ineq add_mono])
huffman@44516
    25
huffman@44516
    26
lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
huffman@44516
    27
  by (simp add: field_simps)
huffman@44516
    28
huffman@44516
    29
lemma pth_1:
huffman@44516
    30
  fixes x :: "'a::real_normed_vector"
huffman@44516
    31
  shows "x == scaleR 1 x" by simp
huffman@44516
    32
huffman@44516
    33
lemma pth_2:
huffman@44516
    34
  fixes x :: "'a::real_normed_vector"
huffman@44516
    35
  shows "x - y == x + -y" by (atomize (full)) simp
huffman@44516
    36
huffman@44516
    37
lemma pth_3:
huffman@44516
    38
  fixes x :: "'a::real_normed_vector"
huffman@44516
    39
  shows "- x == scaleR (-1) x" by simp
huffman@44516
    40
huffman@44516
    41
lemma pth_4:
huffman@44516
    42
  fixes x :: "'a::real_normed_vector"
huffman@44516
    43
  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
huffman@44516
    44
huffman@44516
    45
lemma pth_5:
huffman@44516
    46
  fixes x :: "'a::real_normed_vector"
huffman@44516
    47
  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
huffman@44516
    48
huffman@44516
    49
lemma pth_6:
huffman@44516
    50
  fixes x :: "'a::real_normed_vector"
huffman@44516
    51
  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
huffman@44516
    52
  by (simp add: scaleR_right_distrib)
huffman@44516
    53
huffman@44516
    54
lemma pth_7:
huffman@44516
    55
  fixes x :: "'a::real_normed_vector"
huffman@44516
    56
  shows "0 + x == x" and "x + 0 == x" by simp_all
huffman@44516
    57
huffman@44516
    58
lemma pth_8:
huffman@44516
    59
  fixes x :: "'a::real_normed_vector"
huffman@44516
    60
  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
huffman@44516
    61
  by (simp add: scaleR_left_distrib)
huffman@44516
    62
huffman@44516
    63
lemma pth_9:
huffman@44516
    64
  fixes x :: "'a::real_normed_vector" shows
huffman@44516
    65
  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
huffman@44516
    66
  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
huffman@44516
    67
  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
huffman@44516
    68
  by (simp_all add: algebra_simps)
huffman@44516
    69
huffman@44516
    70
lemma pth_a:
huffman@44516
    71
  fixes x :: "'a::real_normed_vector"
huffman@44516
    72
  shows "scaleR 0 x + y == y" by simp
huffman@44516
    73
huffman@44516
    74
lemma pth_b:
huffman@44516
    75
  fixes x :: "'a::real_normed_vector" shows
huffman@44516
    76
  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
huffman@44516
    77
  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
huffman@44516
    78
  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
huffman@44516
    79
  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
huffman@44516
    80
  by (simp_all add: algebra_simps)
huffman@44516
    81
huffman@44516
    82
lemma pth_c:
huffman@44516
    83
  fixes x :: "'a::real_normed_vector" shows
huffman@44516
    84
  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
huffman@44516
    85
  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
huffman@44516
    86
  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
huffman@44516
    87
  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
huffman@44516
    88
  by (simp_all add: algebra_simps)
huffman@44516
    89
huffman@44516
    90
lemma pth_d:
huffman@44516
    91
  fixes x :: "'a::real_normed_vector"
huffman@44516
    92
  shows "x + 0 == x" by simp
huffman@44516
    93
huffman@44516
    94
lemma norm_imp_pos_and_ge:
huffman@44516
    95
  fixes x :: "'a::real_normed_vector"
huffman@44516
    96
  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
huffman@44516
    97
  by atomize auto
huffman@44516
    98
huffman@44516
    99
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
huffman@44516
   100
huffman@44516
   101
lemma norm_pths:
huffman@44516
   102
  fixes x :: "'a::real_normed_vector" shows
huffman@44516
   103
  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
huffman@44516
   104
  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
huffman@44516
   105
  using norm_ge_zero[of "x - y"] by auto
huffman@44516
   106
huffman@44516
   107
use "normarith.ML"
huffman@44516
   108
huffman@44516
   109
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
huffman@44516
   110
*} "prove simple linear statements about vector norms"
huffman@44516
   111
huffman@44516
   112
text{* Hence more metric properties. *}
huffman@44516
   113
huffman@44516
   114
lemma dist_triangle_add:
huffman@44516
   115
  fixes x y x' y' :: "'a::real_normed_vector"
huffman@44516
   116
  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
huffman@44516
   117
  by norm
huffman@44516
   118
huffman@44516
   119
lemma dist_triangle_add_half:
huffman@44516
   120
  fixes x x' y y' :: "'a::real_normed_vector"
huffman@44516
   121
  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
huffman@44516
   122
  by norm
huffman@44516
   123
huffman@44516
   124
end