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