--- a/src/HOL/Library/Euclidean_Space.thy Mon Feb 23 10:07:57 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Feb 23 06:51:26 2009 -0800
@@ -1010,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
--- a/src/HOL/Library/Inner_Product.thy Mon Feb 23 10:07:57 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy Mon Feb 23 06:51:26 2009 -0800
@@ -21,19 +21,10 @@
begin
lemma inner_zero_left [simp]: "inner 0 x = 0"
-proof -
- have "inner 0 x = inner (0 + 0) x" by simp
- also have "\<dots> = inner 0 x + inner 0 x" by (rule inner_left_distrib)
- finally show "inner 0 x = 0" by simp
-qed
+ using inner_left_distrib [of 0 0 x] by simp
lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
-proof -
- have "inner (- x) y + inner x y = inner (- x + x) y"
- by (rule inner_left_distrib [symmetric])
- also have "\<dots> = - inner x y + inner x y" by simp
- finally show "inner (- x) y = - inner x y" by simp
-qed
+ using inner_left_distrib [of x "- x" y] by simp
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
by (simp add: diff_minus inner_left_distrib)
--- a/src/HOL/RealVector.thy Mon Feb 23 10:07:57 2009 +0100
+++ b/src/HOL/RealVector.thy Mon Feb 23 06:51:26 2009 -0800
@@ -46,8 +46,10 @@
locale vector_space =
fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
- assumes scale_right_distrib: "scale a (x + y) = scale a x + scale a y"
- and scale_left_distrib: "scale (a + b) x = scale a x + scale b x"
+ assumes scale_right_distrib [algebra_simps]:
+ "scale a (x + y) = scale a x + scale a y"
+ and scale_left_distrib [algebra_simps]:
+ "scale (a + b) x = scale a x + scale b x"
and scale_scale [simp]: "scale a (scale b x) = scale (a * b) x"
and scale_one [simp]: "scale 1 x = x"
begin
@@ -58,7 +60,8 @@
lemma scale_zero_left [simp]: "scale 0 x = 0"
and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
- and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
+ and scale_left_diff_distrib [algebra_simps]:
+ "scale (a - b) x = scale a x - scale b x"
proof -
interpret s: additive "\<lambda>a. scale a x"
proof qed (rule scale_left_distrib)
@@ -69,7 +72,8 @@
lemma scale_zero_right [simp]: "scale a 0 = 0"
and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
- and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
+ and scale_right_diff_distrib [algebra_simps]:
+ "scale a (x - y) = scale a x - scale a y"
proof -
interpret s: additive "\<lambda>x. scale a x"
proof qed (rule scale_right_distrib)
@@ -135,21 +139,11 @@
end
-instantiation real :: scaleR
-begin
-
-definition
- real_scaleR_def [simp]: "scaleR a x = a * x"
-
-instance ..
-
-end
-
class real_vector = scaleR + ab_group_add +
assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
- and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
- and scaleR_one [simp]: "scaleR 1 x = x"
+ and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
+ and scaleR_one: "scaleR 1 x = x"
interpretation real_vector!:
vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
@@ -185,15 +179,16 @@
class real_field = real_div_algebra + field
-instance real :: real_field
-apply (intro_classes, unfold real_scaleR_def)
-apply (rule right_distrib)
-apply (rule left_distrib)
-apply (rule mult_assoc [symmetric])
-apply (rule mult_1_left)
-apply (rule mult_assoc)
-apply (rule mult_left_commute)
-done
+instantiation real :: real_field
+begin
+
+definition
+ real_scaleR_def [simp]: "scaleR a x = a * x"
+
+instance proof
+qed (simp_all add: algebra_simps)
+
+end
interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_left_distrib)
@@ -307,7 +302,7 @@
definition
Reals :: "'a::real_algebra_1 set" where
- [code del]: "Reals \<equiv> range of_real"
+ [code del]: "Reals = range of_real"
notation (xsymbols)
Reals ("\<real>")
@@ -421,16 +416,6 @@
class norm =
fixes norm :: "'a \<Rightarrow> real"
-instantiation real :: norm
-begin
-
-definition
- real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
-
-instance ..
-
-end
-
class sgn_div_norm = scaleR + norm + sgn +
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
@@ -462,7 +447,13 @@
thus "norm (1::'a) = 1" by simp
qed
-instance real :: real_normed_field
+instantiation real :: real_normed_field
+begin
+
+definition
+ real_norm_def [simp]: "norm r = \<bar>r\<bar>"
+
+instance
apply (intro_classes, unfold real_norm_def real_scaleR_def)
apply (simp add: real_sgn_def)
apply (rule abs_ge_zero)
@@ -472,6 +463,8 @@
apply (rule abs_mult)
done
+end
+
lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
by simp