--- a/src/HOL/Library/Euclidean_Space.thy Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Mar 04 10:45:52 2009 +0100
@@ -8,6 +8,7 @@
theory Euclidean_Space
imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
+ Inner_Product
uses ("normarith.ML")
begin
@@ -84,7 +85,13 @@
instance by (intro_classes)
end
-text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
+instantiation "^" :: (scaleR, type) scaleR
+begin
+definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
+instance ..
+end
+
+text{* Also the scalar-vector multiplication. *}
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
where "c *s x = (\<chi> i. c * (x$i))"
@@ -118,6 +125,7 @@
[@{thm vector_add_def}, @{thm vector_mult_def},
@{thm vector_minus_def}, @{thm vector_uminus_def},
@{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},
+ @{thm vector_scaleR_def},
@{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}]
fun vector_arith_tac ths =
simp_tac ss1
@@ -166,9 +174,18 @@
shows "(- x)$i = - (x$i)"
using i by vector
+lemma vector_scaleR_component:
+ fixes x :: "'a::scaleR ^ 'n"
+ assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}"
+ shows "(scaleR r x)$i = scaleR r (x$i)"
+ using i by vector
+
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
-lemmas vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component cond_component
+lemmas vector_component =
+ vec_component vector_add_component vector_mult_component
+ vector_smult_component vector_minus_component vector_uminus_component
+ vector_scaleR_component cond_component
subsection {* Some frequently useful arithmetic lemmas over vectors. *}
@@ -199,6 +216,9 @@
apply (intro_classes)
by (vector Cart_eq)
+instance "^" :: (real_vector, type) real_vector
+ by default (vector scaleR_left_distrib scaleR_right_distrib)+
+
instance "^" :: (semigroup_mult,type) semigroup_mult
apply (intro_classes) by (vector mult_assoc)
@@ -242,6 +262,18 @@
instance "^" :: (ring,type) ring by (intro_classes)
instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes)
instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes)
+
+instance "^" :: (ring_1,type) ring_1 ..
+
+instance "^" :: (real_algebra,type) real_algebra
+ apply intro_classes
+ apply (simp_all add: vector_scaleR_def ring_simps)
+ apply vector
+ apply vector
+ done
+
+instance "^" :: (real_algebra_1,type) real_algebra_1 ..
+
lemma of_nat_index:
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
apply (induct n)
@@ -290,8 +322,7 @@
qed
instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes
- (* FIXME!!! Why does the axclass package complain here !!*)
-(* instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes *)
+instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
by (vector mult_assoc)
@@ -314,6 +345,241 @@
apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta )
using dimindex_ge_1 apply auto done
+subsection {* Square root of sum of squares *}
+
+definition
+ "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"
+
+lemma setL2_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
+ unfolding setL2_def by simp
+
+lemma strong_setL2_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
+ unfolding setL2_def simp_implies_def by simp
+
+lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_empty [simp]: "setL2 f {} = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_insert [simp]:
+ "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
+ setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"
+ unfolding setL2_def by (simp add: setsum_nonneg)
+
+lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
+ unfolding setL2_def by (simp add: setsum_nonneg)
+
+lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_mono:
+ assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
+ assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
+ shows "setL2 f K \<le> setL2 g K"
+ unfolding setL2_def
+ by (simp add: setsum_nonneg setsum_mono power_mono prems)
+
+lemma setL2_right_distrib:
+ "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
+ unfolding setL2_def
+ apply (simp add: power_mult_distrib)
+ apply (simp add: setsum_right_distrib [symmetric])
+ apply (simp add: real_sqrt_mult setsum_nonneg)
+ done
+
+lemma setL2_left_distrib:
+ "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
+ unfolding setL2_def
+ apply (simp add: power_mult_distrib)
+ apply (simp add: setsum_left_distrib [symmetric])
+ apply (simp add: real_sqrt_mult setsum_nonneg)
+ done
+
+lemma setsum_nonneg_eq_0_iff:
+ fixes f :: "'a \<Rightarrow> 'b::pordered_ab_group_add"
+ shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ apply (induct set: finite, simp)
+ apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
+ done
+
+lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ unfolding setL2_def
+ by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
+
+lemma setL2_triangle_ineq:
+ shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
+proof (cases "finite A")
+ case False
+ thus ?thesis by simp
+next
+ case True
+ thus ?thesis
+ proof (induct set: finite)
+ case empty
+ show ?case by simp
+ next
+ case (insert x F)
+ hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>
+ sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"
+ by (intro real_sqrt_le_mono add_left_mono power_mono insert
+ setL2_nonneg add_increasing zero_le_power2)
+ also have
+ "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"
+ by (rule real_sqrt_sum_squares_triangle_ineq)
+ finally show ?case
+ using insert by simp
+ qed
+qed
+
+lemma sqrt_sum_squares_le_sum:
+ "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply (simp add: mult_nonneg_nonneg)
+ apply (simp add: add_nonneg_nonneg)
+ done
+
+lemma setL2_le_setsum [rule_format]:
+ "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply clarsimp
+ apply (erule order_trans [OF sqrt_sum_squares_le_sum])
+ apply simp
+ apply simp
+ apply simp
+ done
+
+lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply (simp add: mult_nonneg_nonneg)
+ apply (simp add: add_nonneg_nonneg)
+ done
+
+lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply simp
+ apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
+ apply simp
+ apply simp
+ done
+
+lemma setL2_mult_ineq_lemma:
+ fixes a b c d :: real
+ shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+proof -
+ have "0 \<le> (a * d - b * c)\<twosuperior>" by simp
+ also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"
+ by (simp only: power2_diff power_mult_distrib)
+ also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"
+ by simp
+ finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+ by simp
+qed
+
+lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply (rule power2_le_imp_le, simp)
+ apply (rule order_trans)
+ apply (rule power_mono)
+ apply (erule add_left_mono)
+ apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
+ apply (simp add: power2_sum)
+ apply (simp add: power_mult_distrib)
+ apply (simp add: right_distrib left_distrib)
+ apply (rule ord_le_eq_trans)
+ apply (rule setL2_mult_ineq_lemma)
+ apply simp
+ apply (intro mult_nonneg_nonneg setL2_nonneg)
+ apply simp
+ done
+
+lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
+ apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
+ apply fast
+ apply (subst setL2_insert)
+ apply simp
+ apply simp
+ apply simp
+ done
+
+subsection {* Norms *}
+
+instantiation "^" :: (real_normed_vector, type) real_normed_vector
+begin
+
+definition vector_norm_def:
+ "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x$i)) {1 .. dimindex (UNIV:: 'b set)}"
+
+definition vector_sgn_def:
+ "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
+
+instance proof
+ fix a :: real and x y :: "'a ^ 'b"
+ show "0 \<le> norm x"
+ unfolding vector_norm_def
+ by (rule setL2_nonneg)
+ show "norm x = 0 \<longleftrightarrow> x = 0"
+ unfolding vector_norm_def
+ by (simp add: setL2_eq_0_iff Cart_eq)
+ show "norm (x + y) \<le> norm x + norm y"
+ unfolding vector_norm_def
+ apply (rule order_trans [OF _ setL2_triangle_ineq])
+ apply (rule setL2_mono)
+ apply (simp add: vector_component norm_triangle_ineq)
+ apply simp
+ done
+ show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
+ unfolding vector_norm_def
+ by (simp add: vector_component norm_scaleR setL2_right_distrib
+ cong: strong_setL2_cong)
+ show "sgn x = scaleR (inverse (norm x)) x"
+ by (rule vector_sgn_def)
+qed
+
+end
+
+subsection {* Inner products *}
+
+instantiation "^" :: (real_inner, type) real_inner
+begin
+
+definition vector_inner_def:
+ "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) {1 .. dimindex(UNIV::'b set)}"
+
+instance proof
+ fix r :: real and x y z :: "'a ^ 'b"
+ show "inner x y = inner y x"
+ unfolding vector_inner_def
+ by (simp add: inner_commute)
+ show "inner (x + y) z = inner x z + inner y z"
+ unfolding vector_inner_def
+ by (vector inner_left_distrib)
+ show "inner (scaleR r x) y = r * inner x y"
+ unfolding vector_inner_def
+ by (vector inner_scaleR_left)
+ show "0 \<le> inner x x"
+ unfolding vector_inner_def
+ by (simp add: setsum_nonneg)
+ show "inner x x = 0 \<longleftrightarrow> x = 0"
+ unfolding vector_inner_def
+ by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
+ show "norm x = sqrt (inner x x)"
+ unfolding vector_inner_def vector_norm_def setL2_def
+ by (simp add: power2_norm_eq_inner)
+qed
+
+end
+
subsection{* Properties of the dot product. *}
lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
@@ -363,18 +629,7 @@
lemma dot_pos_lt: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
by (auto simp add: le_less)
-subsection {* Introduce norms, but defer many properties till we get square roots. *}
-text{* FIXME : This is ugly *}
-defs (overloaded)
- real_of_real_def [code inline, simp]: "real == id"
-
-instantiation "^" :: ("{times, comm_monoid_add}", type) norm begin
-definition real_vector_norm_def: "norm \<equiv> (\<lambda>x. sqrt (real (x \<bullet> x)))"
-instance ..
-end
-
-
-subsection{* The collapse of the general concepts to dimention one. *}
+subsection{* The collapse of the general concepts to dimension one. *}
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
by (vector dimindex_def)
@@ -385,11 +640,15 @@
apply (simp only: vector_one[symmetric])
done
+lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
+ by (simp add: vector_norm_def dimindex_def)
+
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
- by (simp add: real_vector_norm_def)
+ by (simp add: norm_vector_1)
text{* Metric *}
+text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}
definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where
"dist x y = norm (x - y)"
@@ -501,27 +760,18 @@
text{* Hence derive more interesting properties of the norm. *}
lemma norm_0: "norm (0::real ^ 'n) = 0"
- by (simp add: real_vector_norm_def dot_eq_0)
-
-lemma norm_pos_le: "0 <= norm (x::real^'n)"
- by (simp add: real_vector_norm_def dot_pos_le)
-lemma norm_neg: " norm(-x) = norm (x:: real ^ 'n)"
- by (simp add: real_vector_norm_def dot_lneg dot_rneg)
-lemma norm_sub: "norm(x - y) = norm(y - (x::real ^ 'n))"
- by (metis norm_neg minus_diff_eq)
+ by (rule norm_zero)
+
lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
- by (simp add: real_vector_norm_def dot_lmult dot_rmult mult_assoc[symmetric] real_sqrt_mult)
+ by (simp add: vector_norm_def vector_component setL2_right_distrib
+ abs_mult cong: strong_setL2_cong)
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
+ by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
+lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
+ by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
+lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
by (simp add: real_vector_norm_def)
-lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)"
- by (simp add: real_vector_norm_def dot_eq_0)
-lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)"
- by (metis less_le real_vector_norm_def norm_pos_le norm_eq_0)
-lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
- by (simp add: real_vector_norm_def dot_pos_le)
-lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0)
-lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)"
- by (metis norm_eq_0 norm_pos_le order_antisym)
+lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
by vector
lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
@@ -535,14 +785,14 @@
lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y"
proof-
{assume "norm x = 0"
- hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
+ hence ?thesis by (simp add: dot_lzero dot_rzero)}
moreover
{assume "norm y = 0"
- hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
+ hence ?thesis by (simp add: dot_lzero dot_rzero)}
moreover
{assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
let ?z = "norm y *s x - norm x *s y"
- from h have p: "norm x * norm y > 0" by (metis norm_pos_le le_less zero_compare_simps)
+ from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
from dot_pos_le[of ?z]
have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
@@ -553,26 +803,16 @@
ultimately show ?thesis by metis
qed
-lemma norm_abs[simp]: "abs (norm x) = norm (x::real ^'n)"
- using norm_pos_le[of x] by (simp add: real_abs_def linorder_linear)
-
lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
- by (simp add: real_abs_def dot_rneg norm_neg)
-lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)"
- unfolding real_vector_norm_def
- apply (rule real_le_lsqrt)
- apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
- apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
- apply (simp add: dot_ladd dot_radd dot_sym )
- by (simp add: norm_pow_2[symmetric] power2_eq_square ring_simps norm_cauchy_schwarz)
+ by (simp add: real_abs_def dot_rneg)
lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"
- using norm_triangle[of "y" "x - y"] by (simp add: ring_simps)
+ using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e"
- by (metis order_trans norm_triangle)
+ by (metis order_trans norm_triangle_ineq)
lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"
- by (metis basic_trans_rules(21) norm_triangle)
+ by (metis basic_trans_rules(21) norm_triangle_ineq)
lemma setsum_delta:
assumes fS: "finite S"
@@ -597,19 +837,10 @@
qed
lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x$i\<bar> <= norm (x::real ^ 'n)"
-proof(simp add: real_vector_norm_def, rule real_le_rsqrt, clarsimp)
- assume i: "Suc 0 \<le> i" "i \<le> dimindex (UNIV :: 'n set)"
- let ?S = "{1 .. dimindex(UNIV :: 'n set)}"
- let ?f = "(\<lambda>k. if k = i then x$i ^2 else 0)"
- have fS: "finite ?S" by simp
- from i setsum_delta[OF fS, of i "\<lambda>k. x$i ^ 2"]
- have th: "x$i^2 = setsum ?f ?S" by simp
- let ?g = "\<lambda>k. x$k * x$k"
- {fix x assume x: "x \<in> ?S" have "?f x \<le> ?g x" by (simp add: power2_eq_square)}
- with setsum_mono[of ?S ?f ?g]
- have "setsum ?f ?S \<le> setsum ?g ?S" by blast
- then show "x$i ^2 \<le> x \<bullet> (x:: real ^ 'n)" unfolding dot_def th[symmetric] .
-qed
+ apply (simp add: vector_norm_def)
+ apply (rule member_le_setL2, simp_all)
+ done
+
lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e
==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x$i\<bar> <= e"
by (metis component_le_norm order_trans)
@@ -619,24 +850,12 @@
by (metis component_le_norm basic_trans_rules(21))
lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x$i\<bar>) {1..dimindex(UNIV::'n set)}"
-proof (simp add: real_vector_norm_def, rule real_le_lsqrt,simp add: dot_pos_le, simp add: setsum_mono, simp add: dot_def, induct "dimindex(UNIV::'n set)")
- case 0 thus ?case by simp
-next
- case (Suc n)
- have th: "2 * (\<bar>x$(Suc n)\<bar> * (\<Sum>i = Suc 0..n. \<bar>x$i\<bar>)) \<ge> 0"
- apply simp
- apply (rule mult_nonneg_nonneg)
- by (simp_all add: setsum_abs_ge_zero)
-
- from Suc
- show ?case using th by (simp add: power2_eq_square ring_simps)
-qed
+ by (simp add: vector_norm_def setL2_le_setsum)
lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)"
- by (simp add: norm_pos_le)
+ by (rule abs_norm_cancel)
lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n) - norm y\<bar> <= norm(x - y)"
- apply (simp add: abs_le_iff ring_simps)
- by (metis norm_triangle_sub norm_sub)
+ by (rule norm_triangle_ineq3)
lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
by (simp add: real_vector_norm_def)
lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
@@ -652,13 +871,7 @@
by (simp add: real_vector_norm_def dot_pos_le )
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
-proof-
- have th: "\<And>x y::real. x^2 = y^2 \<longleftrightarrow> x = y \<or> x = -y" by algebra
- show ?thesis using norm_pos_le[of x]
- apply (simp add: dot_square_norm th)
- apply arith
- done
-qed
+ by (auto simp add: real_vector_norm_def)
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
proof-
@@ -668,14 +881,14 @@
qed
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
- using norm_pos_le[of x]
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
apply arith
done
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
- using norm_pos_le[of x]
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
apply arith
done
@@ -746,14 +959,14 @@
lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
- by (atomize) (auto simp add: norm_pos_le)
+ by (atomize) (auto simp add: norm_ge_zero)
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
lemma norm_pths:
"(x::real ^'n) = y \<longleftrightarrow> norm (x - y) \<le> 0"
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
- using norm_pos_le[of "x - y"] by (auto simp add: norm_0 norm_eq_0)
+ using norm_ge_zero[of "x - y"] by auto
use "normarith.ML"
@@ -797,11 +1010,6 @@
lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm
-instantiation "^" :: (monoid_add,type) monoid_add
-begin
- instance by (intro_classes)
-end
-
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
apply vector
apply auto
@@ -873,7 +1081,7 @@
assumes fS: "finite S"
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
proof(induct rule: finite_induct[OF fS])
- case 1 thus ?case by (simp add: norm_zero)
+ case 1 thus ?case by simp
next
case (2 x S)
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
@@ -887,10 +1095,10 @@
assumes fS: "finite S"
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
proof(induct rule: finite_induct[OF fS])
- case 1 thus ?case by simp norm
+ case 1 thus ?case by simp
next
case (2 x S)
- from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" apply (simp add: norm_triangle_ineq) by norm
+ from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
using "2.hyps" by simp
finally show ?case using "2.hyps" by simp
@@ -936,45 +1144,6 @@
using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]
by simp
-instantiation "^" :: ("{scaleR, one, times}",type) scaleR
-begin
-
-definition vector_scaleR_def: "(scaleR :: real \<Rightarrow> 'a ^'b \<Rightarrow> 'a ^'b) \<equiv> (\<lambda> c x . (scaleR c 1) *s x)"
-instance ..
-end
-
-instantiation "^" :: ("ring_1",type) ring_1
-begin
-instance by intro_classes
-end
-
-instantiation "^" :: (real_algebra_1,type) real_vector
-begin
-
-instance
- apply intro_classes
- apply (simp_all add: vector_scaleR_def)
- apply (simp_all add: vector_sadd_rdistrib vector_add_ldistrib vector_smult_lid vector_smult_assoc scaleR_left_distrib mult_commute)
- done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra
-begin
-
-instance
- apply intro_classes
- apply (simp_all add: vector_scaleR_def ring_simps)
- apply vector
- apply vector
- done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra_1
-begin
-
-instance ..
-end
-
lemma setsum_vmul:
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}"
assumes fS: "finite S"
@@ -1211,7 +1380,7 @@
by (auto simp add: setsum_component intro: abs_le_D1)
have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"
using i component_le_norm[OF i, of "setsum (\<lambda>x. - f x) ?Pn"] fPs[OF PnP]
- by (auto simp add: setsum_negf norm_neg setsum_component vector_component intro: abs_le_D1)
+ by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)
have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn"
apply (subst thp)
apply (rule setsum_Un_nonzero)
@@ -1535,7 +1704,7 @@
unfolding norm_mul
apply (simp only: mult_commute)
apply (rule mult_mono)
- by (auto simp add: ring_simps norm_pos_le) }
+ by (auto simp add: ring_simps norm_ge_zero) }
then have th: "\<forall>i\<in> ?S. norm ((x$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
@@ -1552,16 +1721,18 @@
let ?K = "\<bar>B\<bar> + 1"
have Kp: "?K > 0" by arith
{assume C: "B < 0"
- have "norm (1::real ^ 'n) > 0" by (simp add: norm_pos_lt)
+ have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
with C have "B * norm (1:: real ^ 'n) < 0"
by (simp add: zero_compare_simps)
- with B[rule_format, of 1] norm_pos_le[of "f 1"] have False by simp
+ with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
}
then have Bp: "B \<ge> 0" by ferrack
{fix x::"real ^ 'n"
have "norm (f x) \<le> ?K * norm x"
- using B[rule_format, of x] norm_pos_le[of x] norm_pos_le[of "f x"] Bp
- by (auto simp add: ring_simps split add: abs_split)
+ using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
+ apply (auto simp add: ring_simps split add: abs_split)
+ apply (erule order_trans, simp)
+ done
}
then show ?thesis using Kp by blast
qed
@@ -1641,9 +1812,9 @@
apply simp
apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
apply (rule mult_mono)
- apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
+ apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
apply (rule mult_mono)
- apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
+ apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
done}
then show ?thesis by metis
qed
@@ -1663,7 +1834,7 @@
have "B * norm x * norm y \<le> ?K * norm x * norm y"
apply -
apply (rule mult_right_mono, rule mult_right_mono)
- by (auto simp add: norm_pos_le)
+ by (auto simp add: norm_ge_zero)
then have "norm (h x y) \<le> ?K * norm x * norm y"
using B[rule_format, of x y] by simp}
with Kp show ?thesis by blast
@@ -2276,21 +2447,21 @@
moreover
{assume H: ?lhs
from H[rule_format, of "basis 1"]
- have bp: "b \<ge> 0" using norm_pos_le[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
- by (auto simp add: norm_basis)
+ have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
+ by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
{fix x :: "real ^'n"
{assume "x = 0"
- then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] norm_0 bp)}
+ then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
moreover
{assume x0: "x \<noteq> 0"
- hence n0: "norm x \<noteq> 0" by (metis norm_eq_0)
+ hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
let ?c = "1/ norm x"
- have "norm (?c*s x) = 1" by (simp add: n0 norm_mul)
+ have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
with H have "norm (f(?c*s x)) \<le> b" by blast
hence "?c * norm (f x) \<le> b"
by (simp add: linear_cmul[OF lf] norm_mul)
hence "norm (f x) \<le> b * norm x"
- using n0 norm_pos_le[of x] by (auto simp add: field_simps)}
+ using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
ultimately have "norm (f x) \<le> b * norm x" by blast}
then have ?rhs by blast}
ultimately show ?thesis by blast
@@ -2322,12 +2493,12 @@
qed
lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
- using order_trans[OF norm_pos_le onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
+ using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
using onorm[OF lf]
- apply (auto simp add: norm_0 onorm_pos_le norm_le_0)
+ apply (auto simp add: onorm_pos_le)
apply atomize
apply (erule allE[where x="0::real"])
using onorm_pos_le[OF lf]
@@ -2365,7 +2536,7 @@
lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) \<le> onorm f"
using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
- unfolding norm_neg by metis
+ unfolding norm_minus_cancel by metis
lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) = onorm f"
@@ -2377,7 +2548,7 @@
shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
apply (rule order_trans)
- apply (rule norm_triangle)
+ apply (rule norm_triangle_ineq)
apply (simp add: distrib)
apply (rule add_mono)
apply (rule onorm(1)[OF lf])
@@ -2594,7 +2765,7 @@
by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square del: One_nat_def)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def real_sqrt_le_iff id_def
by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
qed
@@ -2626,7 +2797,7 @@
by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square setsum_reindex[OF finj, unfolded fS] del: One_nat_def)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def real_sqrt_le_iff id_def
by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
qed
@@ -2683,7 +2854,7 @@
qed
lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ _) + norm(y)"
- unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
apply (rule power2_le_imp_le)
apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])
apply (auto simp add: power2_eq_square ring_simps)
@@ -5007,7 +5178,7 @@
apply blast
by (rule abs_ge_zero)
from real_le_lsqrt[OF dot_pos_le th th1]
- show ?thesis unfolding real_vector_norm_def real_of_real_def id_def .
+ show ?thesis unfolding real_vector_norm_def id_def .
qed
(* Equality in Cauchy-Schwarz and triangle inequalities. *)
@@ -5015,10 +5186,10 @@
lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
{assume h: "x = 0"
- hence ?thesis by (simp add: norm_0)}
+ hence ?thesis by simp}
moreover
{assume h: "y = 0"
- hence ?thesis by (simp add: norm_0)}
+ hence ?thesis by simp}
moreover
{assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
from dot_eq_0[of "norm y *s x - norm x *s y"]
@@ -5032,7 +5203,7 @@
also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
by (simp add: ring_simps dot_sym)
also have "\<dots> \<longleftrightarrow> ?lhs" using x y
- apply (simp add: norm_eq_0)
+ apply simp
by metis
finally have ?thesis by blast}
ultimately show ?thesis by blast
@@ -5043,14 +5214,14 @@
proof-
have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith
have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"
- apply (simp add: norm_neg) by vector
+ apply simp by vector
also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or>
(-x) \<bullet> y = norm x * norm y)"
unfolding norm_cauchy_schwarz_eq[symmetric]
- unfolding norm_neg
+ unfolding norm_minus_cancel
norm_mul by blast
also have "\<dots> \<longleftrightarrow> ?lhs"
- unfolding th[OF mult_nonneg_nonneg, OF norm_pos_le[of x] norm_pos_le[of y]] dot_lneg
+ unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
by arith
finally show ?thesis ..
qed
@@ -5058,17 +5229,17 @@
lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"
proof-
{assume x: "x =0 \<or> y =0"
- hence ?thesis by (cases "x=0", simp_all add: norm_0)}
+ hence ?thesis by (cases "x=0", simp_all)}
moreover
{assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
hence "norm x \<noteq> 0" "norm y \<noteq> 0"
- by (simp_all add: norm_eq_0)
+ by simp_all
hence n: "norm x > 0" "norm y > 0"
- using norm_pos_le[of x] norm_pos_le[of y]
+ using norm_ge_zero[of x] norm_ge_zero[of y]
by arith+
have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)" by algebra
have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
- apply (rule th) using n norm_pos_le[of "x + y"]
+ apply (rule th) using n norm_ge_zero[of "x + y"]
by arith
also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
unfolding norm_cauchy_schwarz_eq[symmetric]
@@ -5138,8 +5309,8 @@
lemma norm_cauchy_schwarz_equal: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"
unfolding norm_cauchy_schwarz_abs_eq
-apply (cases "x=0", simp_all add: collinear_2 norm_0)
-apply (cases "y=0", simp_all add: collinear_2 norm_0 insert_commute)
+apply (cases "x=0", simp_all add: collinear_2)
+apply (cases "y=0", simp_all add: collinear_2 insert_commute)
unfolding collinear_lemma
apply simp
apply (subgoal_tac "norm x \<noteq> 0")
@@ -5164,8 +5335,8 @@
apply (simp add: ring_simps)
apply (case_tac "c <= 0", simp add: ring_simps)
apply (simp add: ring_simps)
-apply (simp add: norm_eq_0)
-apply (simp add: norm_eq_0)
+apply simp
+apply simp
done
-end
\ No newline at end of file
+end