(* Title: HOL/Analysis/Norm_Arith.thy
Author: Amine Chaieb, University of Cambridge
*)
section \<open>Linear Decision Procedure for Normed Spaces\<close>
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 *)
lemma norm_add_rule_thm:
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
add_numeral_special
add_neg_numeral_special
mult_1_left
mult_1_right
ML_file \<open>normarith.ML\<close>
method_setup\<^marker>\<open>tag important\<close> norm = \<open>
Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
\<close> "prove simple linear statements about vector norms"
text \<open>Hence more metric properties.\<close>
text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
proposition dist_triangle_add:
fixes x y x' y' :: "'a::real_normed_vector"
shows "dist (x + y) (x' + y') \ dist x x' + dist y y'"
by norm
lemma dist_triangle_add_half:
fixes x x' y y' :: "'a::real_normed_vector"
shows "dist x x' < e / 2 \ dist y y' < e / 2 \ dist(x + y) (x' + y') < e"
by norm
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
