# Theory Norm_Arith

```(*  Title:      HOL/Analysis/Norm_Arith.thy
Author:     Amine Chaieb, University of Cambridge
*)

section ‹Linear Decision Procedure for Normed Spaces›

theory Norm_Arith
imports "HOL-Library.Sum_of_Squares"
begin

(* FIXME: move elsewhere *)
lemma sum_sqs_eq:
fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) ⟹ y = x"
by algebra

lemma norm_cmul_rule_thm:
fixes x :: "'a::real_normed_vector"
shows "b ≥ norm x ⟹ ¦c¦ * b ≥ norm (scaleR c x)"
unfolding norm_scaleR
apply (erule mult_left_mono)
apply simp
done

(* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
fixes x1 x2 :: "'a::real_normed_vector"
shows "norm x1 ≤ b1 ⟹ norm x2 ≤ b2 ⟹ norm (x1 + x2) ≤ b1 + b2"
by (rule order_trans [OF norm_triangle_ineq add_mono])

lemma ge_iff_diff_ge_0:
fixes a :: "'a::linordered_ring"
shows "a ≥ b ≡ a - b ≥ 0"
by (simp add: field_simps)

lemma pth_1:
fixes x :: "'a::real_normed_vector"
shows "x ≡ scaleR 1 x" by simp

lemma pth_2:
fixes x :: "'a::real_normed_vector"
shows "x - y ≡ x + -y"
by (atomize (full)) simp

lemma pth_3:
fixes x :: "'a::real_normed_vector"
shows "- x ≡ scaleR (-1) x"
by simp

lemma pth_4:
fixes x :: "'a::real_normed_vector"
shows "scaleR 0 x ≡ 0"
and "scaleR c 0 = (0::'a)"
by simp_all

lemma pth_5:
fixes x :: "'a::real_normed_vector"
shows "scaleR c (scaleR d x) ≡ scaleR (c * d) x"
by simp

lemma pth_6:
fixes x :: "'a::real_normed_vector"
shows "scaleR c (x + y) ≡ scaleR c x + scaleR c y"
by (simp add: scaleR_right_distrib)

lemma pth_7:
fixes x :: "'a::real_normed_vector"
shows "0 + x ≡ x"
and "x + 0 ≡ x"
by simp_all

lemma pth_8:
fixes x :: "'a::real_normed_vector"
shows "scaleR c x + scaleR d x ≡ scaleR (c + d) x"
by (simp add: scaleR_left_distrib)

lemma pth_9:
fixes x :: "'a::real_normed_vector"
shows "(scaleR c x + z) + scaleR d x ≡ scaleR (c + d) x + z"
and "scaleR c x + (scaleR d x + z) ≡ scaleR (c + d) x + z"
and "(scaleR c x + w) + (scaleR d x + z) ≡ scaleR (c + d) x + (w + z)"
by (simp_all add: algebra_simps)

lemma pth_a:
fixes x :: "'a::real_normed_vector"
shows "scaleR 0 x + y ≡ y"
by simp

lemma pth_b:
fixes x :: "'a::real_normed_vector"
shows "scaleR c x + scaleR d y ≡ scaleR c x + scaleR d y"
and "(scaleR c x + z) + scaleR d y ≡ scaleR c x + (z + scaleR d y)"
and "scaleR c x + (scaleR d y + z) ≡ scaleR c x + (scaleR d y + z)"
and "(scaleR c x + w) + (scaleR d y + z) ≡ scaleR c x + (w + (scaleR d y + z))"
by (simp_all add: algebra_simps)

lemma pth_c:
fixes x :: "'a::real_normed_vector"
shows "scaleR c x + scaleR d y ≡ scaleR d y + scaleR c x"
and "(scaleR c x + z) + scaleR d y ≡ scaleR d y + (scaleR c x + z)"
and "scaleR c x + (scaleR d y + z) ≡ scaleR d y + (scaleR c x + z)"
and "(scaleR c x + w) + (scaleR d y + z) ≡ scaleR d y + ((scaleR c x + w) + z)"
by (simp_all add: algebra_simps)

lemma pth_d:
fixes x :: "'a::real_normed_vector"
shows "x + 0 ≡ x"
by simp

lemma norm_imp_pos_and_ge:
fixes x :: "'a::real_normed_vector"
shows "norm x ≡ n ⟹ norm x ≥ 0 ∧ n ≥ norm x"
by atomize auto

lemma real_eq_0_iff_le_ge_0:
fixes x :: real
shows "x = 0 ≡ x ≥ 0 ∧ - x ≥ 0"
by arith

lemma norm_pths:
fixes x :: "'a::real_normed_vector"
shows "x = y ⟷ norm (x - y) ≤ 0"
and "x ≠ y ⟷ ¬ (norm (x - y) ≤ 0)"
using norm_ge_zero[of "x - y"] by auto

lemmas arithmetic_simps =
arith_simps
mult_1_left
mult_1_right

ML_file ‹normarith.ML›

method_setup✐‹tag important› norm = ‹
Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
› "prove simple linear statements about vector norms"

text ‹Hence more metric properties.›
text✐‹tag important› ‹%whitespace›