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