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