diff -r 57dd0b45fc21 -r 7d04351c795a src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Mon Jul 27 16:52:57 2015 +0100 @@ -228,6 +228,29 @@ apply (erule (1) nonzero_inverse_scaleR_distrib) done +lemma real_vector_affinity_eq: + fixes x :: "'a :: real_vector" + assumes m0: "m \ 0" + shows "m *\<^sub>R x + c = y \ x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)" +proof + assume h: "m *\<^sub>R x + c = y" + hence "m *\<^sub>R x = y - c" by (simp add: field_simps) + hence "inverse m *\<^sub>R (m *\<^sub>R x) = inverse m *\<^sub>R (y - c)" by simp + then show "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)" + using m0 + by (simp add: real_vector.scale_right_diff_distrib) +next + assume h: "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)" + show "m *\<^sub>R x + c = y" unfolding h + using m0 by (simp add: real_vector.scale_right_diff_distrib) +qed + +lemma real_vector_eq_affinity: + fixes x :: "'a :: real_vector" + shows "m \ 0 ==> (y = m *\<^sub>R x + c \ inverse m *\<^sub>R y - (inverse m *\<^sub>R c) = x)" + using real_vector_affinity_eq[where m=m and x=x and y=y and c=c] + by metis + subsection \Embedding of the Reals into any @{text real_algebra_1}: @{term of_real}\ @@ -763,6 +786,18 @@ finally show ?thesis . qed +lemma norm_diff_triangle_le: + fixes x y z :: "'a::real_normed_vector" + assumes "norm (x - y) \ e1" "norm (y - z) \ e2" + shows "norm (x - z) \ e1 + e2" + using norm_diff_triangle_ineq [of x y y z] assms by simp + +lemma norm_diff_triangle_less: + fixes x y z :: "'a::real_normed_vector" + assumes "norm (x - y) < e1" "norm (y - z) < e2" + shows "norm (x - z) < e1 + e2" + using norm_diff_triangle_ineq [of x y y z] assms by simp + lemma norm_triangle_mono: fixes a b :: "'a::real_normed_vector" shows "\norm a \ r; norm b \ s\ \ norm (a + b) \ r + s" @@ -1123,6 +1158,11 @@ end +lemma dist_of_real [simp]: + fixes a :: "'a::real_normed_div_algebra" + shows "dist (of_real x :: 'a) (of_real y) = dist x y" +by (metis dist_norm norm_of_real of_real_diff real_norm_def) + declare [[code abort: "open :: real set \ bool"]] instance real :: linorder_topology @@ -1249,6 +1289,10 @@ locale linear = additive f for f :: "'a::real_vector \ 'b::real_vector" + assumes scaleR: "f (scaleR r x) = scaleR r (f x)" +lemma linear_imp_scaleR: + assumes "linear D" obtains d where "D = (\x. x *\<^sub>R d)" + by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def) + lemma linearI: assumes "\x y. f (x + y) = f x + f y" assumes "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" @@ -1503,6 +1547,11 @@ by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left) qed +lemma bij_linear_imp_inv_linear: + assumes "linear f" "bij f" shows "linear (inv f)" + using assms unfolding linear_def linear_axioms_def additive_def + by (auto simp: bij_is_surj bij_is_inj surj_f_inv_f intro!: Hilbert_Choice.inv_f_eq) + instance real_normed_algebra_1 \ perfect_space proof fix x::'a