Quelle Norm_Arith.thy Sprache: Isabelle

(*  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

quality60%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.