src/HOL/Library/Euclidean_Space.thy

 qed
 
 
 subsection{* General linear decision procedure for normed spaces. *}
 
-lemma norm_cmul_rule_thm: "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(c *s x)"
-  apply (clarsimp simp add: norm_mul)
-  apply (rule mult_mono1)
-  apply simp_all
+lemma norm_cmul_rule_thm:
+  fixes x :: "'a::real_normed_vector"
+  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+  unfolding norm_scaleR
+  apply (erule mult_mono1)
+  apply simp
   done
 
   (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
-lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n::finite) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)"
-  apply (rule norm_triangle_le) by simp
+lemma norm_add_rule_thm:
+  fixes x1 x2 :: "'a::real_normed_vector"
+  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
+  by (rule order_trans [OF norm_triangle_ineq add_mono])
 
 lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a - b \<ge> 0"
   by (simp add: ring_simps)
 
-lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid)
-lemma pth_2: "x - (y::real^'n) == x + -y" by (atomize (full)) simp
-lemma pth_3: "(-x::real^'n) == -1 *s x" by vector
-lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+
-lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector
-lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps)
-lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all
-lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps)
-lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z"
-  "c *s x + (d *s x + z) == (c + d) *s x + z"
-  "(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+
-lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector
-lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y"
-  "(c *s x + z) + d *s y == c *s x + (z + d *s y)"
-  "c *s x + (d *s y + z) == c *s x + (d *s y + z)"
-  "(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))"
-  by ((atomize (full)), vector)+
-lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x"
-  "(c *s x + z) + d *s y == d *s y + (c *s x + z)"
-  "c *s x + (d *s y + z) == d *s y + (c *s x + z)"
-  "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+
-lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
-
-lemma norm_imp_pos_and_ge: "norm (x::real ^ _) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
-  by (atomize) (auto simp add: norm_ge_zero)
+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"
+  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
+  "(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"
+  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
+  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
+  "(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"
+  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
+  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
+  "(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 \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+  by atomize auto
 
 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::finite) = y \<longleftrightarrow> norm (x - y) \<le> 0"
+  fixes x :: "'a::real_normed_vector" shows
+  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
   "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   using norm_ge_zero[of "x - y"] by auto
 
 lemma vector_dist_norm:
-  fixes x y :: "real ^ _"
+  fixes x :: "'a::real_normed_vector"
   shows "dist x y = norm (x - y)"
   by (rule dist_norm)
 
 use "normarith.ML"
 
 method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
 *} "Proves simple linear statements about vector norms"
-
 
 
 text{* Hence more metric properties. *}
 
 lemma dist_triangle_alt:

 by (rule dist_triangle_half_l, simp_all add: dist_commute)
 
 lemma dist_triangle_add:
   fixes x y x' y' :: "'a::real_normed_vector"
   shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
-unfolding dist_norm by (rule norm_diff_triangle_ineq)
+  by norm
 
 lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
   unfolding dist_norm vector_ssub_ldistrib[symmetric] norm_mul ..
 
 lemma dist_triangle_add_half:
   fixes x x' y y' :: "'a::real_normed_vector"
   shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
-by (rule le_less_trans [OF dist_triangle_add], simp)
+  by norm
 
 lemma setsum_component [simp]:
   fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
   shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"
   by (cases "finite S", induct S set: finite, simp_all)