src/HOL/Multivariate_Analysis/Norm_Arith.thy
author blanchet
Fri, 01 Aug 2014 14:43:57 +0200
changeset 57743 0af2d5dfb0ac
parent 53717 6eb85a1cb406
child 58877 262572d90bc6
permissions -rw-r--r--
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
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
begin
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    10
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    11
lemma norm_cmul_rule_thm:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    12
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    13
  shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    14
  unfolding norm_scaleR
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    15
  apply (erule mult_left_mono)
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    16
  apply simp
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    17
  done
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    18
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    19
(* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    20
lemma norm_add_rule_thm:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    21
  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
    22
  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
    23
  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
    24
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    25
lemma ge_iff_diff_ge_0:
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    26
  fixes a :: "'a::linordered_ring"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    27
  shows "a \<ge> b \<equiv> a - b \<ge> 0"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    28
  by (simp add: field_simps)
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    29
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    30
lemma pth_1:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    31
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    32
  shows "x \<equiv> scaleR 1 x" by simp
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    33
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    34
lemma pth_2:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    35
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    36
  shows "x - y \<equiv> x + -y"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    37
  by (atomize (full)) simp
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    38
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    39
lemma pth_3:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    40
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    41
  shows "- x \<equiv> scaleR (-1) x"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    42
  by simp
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    43
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    44
lemma pth_4:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    45
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    46
  shows "scaleR 0 x \<equiv> 0"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    47
    and "scaleR c 0 = (0::'a)"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    48
  by simp_all
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    49
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    50
lemma pth_5:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    51
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    52
  shows "scaleR c (scaleR d x) \<equiv> scaleR (c * d) x"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    53
  by simp
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    54
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    55
lemma pth_6:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    56
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    57
  shows "scaleR c (x + y) \<equiv> scaleR c x + scaleR c y"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    58
  by (simp add: scaleR_right_distrib)
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    59
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    60
lemma pth_7:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    61
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    62
  shows "0 + x \<equiv> x"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    63
    and "x + 0 \<equiv> x"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    64
  by simp_all
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    65
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    66
lemma pth_8:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    67
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    68
  shows "scaleR c x + scaleR d x \<equiv> scaleR (c + d) x"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    69
  by (simp add: scaleR_left_distrib)
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    70
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    71
lemma pth_9:
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    72
  fixes x :: "'a::real_normed_vector"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    73
  shows "(scaleR c x + z) + scaleR d x \<equiv> scaleR (c + d) x + z"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    74
    and "scaleR c x + (scaleR d x + z) \<equiv> scaleR (c + d) x + z"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    75
    and "(scaleR c x + w) + (scaleR d x + z) \<equiv> scaleR (c + d) x + (w + z)"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    76
  by (simp_all add: algebra_simps)
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    77
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    78
lemma pth_a:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    79
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    80
  shows "scaleR 0 x + y \<equiv> y"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    81
  by simp
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    82
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    83
lemma pth_b:
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    84
  fixes x :: "'a::real_normed_vector"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    85
  shows "scaleR c x + scaleR d y \<equiv> scaleR c x + scaleR d y"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    86
    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR c x + (z + scaleR d y)"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    87
    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR c x + (scaleR d y + z)"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    88
    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR c x + (w + (scaleR d y + z))"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    89
  by (simp_all add: algebra_simps)
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    90
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    91
lemma pth_c:
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    92
  fixes x :: "'a::real_normed_vector"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    93
  shows "scaleR c x + scaleR d y \<equiv> scaleR d y + scaleR c x"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    94
    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR d y + (scaleR c x + z)"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    95
    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR d y + (scaleR c x + z)"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
    96
    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR d y + ((scaleR c x + w) + z)"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
    97
  by (simp_all add: algebra_simps)
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 pth_d:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   100
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   101
  shows "x + 0 \<equiv> x"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   102
  by simp
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   103
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   104
lemma norm_imp_pos_and_ge:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   105
  fixes x :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   106
  shows "norm x \<equiv> n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   107
  by atomize auto
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   108
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   109
lemma real_eq_0_iff_le_ge_0:
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   110
  fixes x :: real
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   111
  shows "x = 0 \<equiv> x \<ge> 0 \<and> - x \<ge> 0"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   112
  by arith
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   113
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   114
lemma norm_pths:
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   115
  fixes x :: "'a::real_normed_vector"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   116
  shows "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   117
    and "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   118
  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
   119
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44516
diff changeset
   120
lemmas arithmetic_simps =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44516
diff changeset
   121
  arith_simps
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44516
diff changeset
   122
  add_numeral_special
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44516
diff changeset
   123
  add_neg_numeral_special
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44516
diff changeset
   124
  mult_1_left
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44516
diff changeset
   125
  mult_1_right
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 44516
diff changeset
   126
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48112
diff changeset
   127
ML_file "normarith.ML"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   128
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   129
method_setup norm = {*
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   130
  Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   131
*} "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
   132
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   133
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   134
text {* Hence more metric properties. *}
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   135
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   136
lemma dist_triangle_add:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   137
  fixes x y x' y' :: "'a::real_normed_vector"
53717
6eb85a1cb406 tuned proofs;
wenzelm
parents: 48891
diff changeset
   138
  shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   139
  by norm
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   140
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   141
lemma dist_triangle_add_half:
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   142
  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
   143
  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
   144
  by norm
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   145
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff changeset
   146
end