author huffman Mon May 14 20:48:32 2007 +0200 (2007-05-14) changeset 22973 64d300e16370 parent 22972 3e96b98d37c6 child 22974 08b0fa905ea0
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
1.1 --- a/src/HOL/Real/RealVector.thy	Mon May 14 20:14:31 2007 +0200
1.2 +++ b/src/HOL/Real/RealVector.thy	Mon May 14 20:48:32 2007 +0200
1.3 @@ -58,7 +58,7 @@
1.4    divideR (infixl "'/\<^sub>R" 70)
1.6  instance real :: scaleR
1.7 -  real_scaleR_def: "scaleR a x \<equiv> a * x" ..
1.8 +  real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
1.10  axclass real_vector < scaleR, ab_group_add
1.11    scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
1.12 @@ -115,7 +115,7 @@
1.13  lemmas scaleR_right_diff_distrib =
1.16 -lemma scaleR_eq_0_iff:
1.17 +lemma scaleR_eq_0_iff [simp]:
1.18    fixes x :: "'a::real_vector"
1.19    shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)"
1.20  proof cases
1.21 @@ -136,8 +136,7 @@
1.22    assume "scaleR a x = scaleR a y"
1.23    hence "scaleR a (x - y) = 0"
1.24       by (simp add: scaleR_right_diff_distrib)
1.25 -  hence "x - y = 0"
1.26 -     by (simp add: scaleR_eq_0_iff nonzero)
1.27 +  hence "x - y = 0" by (simp add: nonzero)
1.28    thus "x = y" by simp
1.29  qed
1.31 @@ -149,8 +148,7 @@
1.32    assume "scaleR a x = scaleR b x"
1.33    hence "scaleR (a - b) x = 0"
1.34       by (simp add: scaleR_left_diff_distrib)
1.35 -  hence "a - b = 0"
1.36 -     by (simp add: scaleR_eq_0_iff nonzero)
1.37 +  hence "a - b = 0" by (simp add: nonzero)
1.38    thus "a = b" by simp
1.39  qed
1.41 @@ -239,7 +237,7 @@
1.42  proof
1.43    fix r
1.44    show "of_real r = id r"
1.45 -    by (simp add: of_real_def real_scaleR_def)
1.46 +    by (simp add: of_real_def)
1.47  qed
1.49  text{*Collapse nested embeddings*}
1.50 @@ -604,25 +602,28 @@
1.51  unfolding sgn_def by simp
1.53  lemma sgn_zero_iff: "(sgn x = 0) = (x = 0)"
1.54 -unfolding sgn_def by (simp add: scaleR_eq_0_iff)
1.55 +unfolding sgn_def by simp
1.57  lemma sgn_minus: "sgn (- x) = - sgn x"
1.58  unfolding sgn_def by simp
1.60 +lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
1.61 +unfolding sgn_def by (simp add: norm_scaleR mult_ac)
1.62 +
1.63  lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
1.64  unfolding sgn_def by simp
1.66 -lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
1.67 -unfolding sgn_def
1.68 -by (simp add: real_scaleR_def norm_scaleR mult_ac)
1.69 -
1.70  lemma sgn_of_real:
1.71    "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
1.72  unfolding of_real_def by (simp only: sgn_scaleR sgn_one)
1.74 +lemma sgn_mult:
1.75 +  fixes x y :: "'a::real_normed_div_algebra"
1.76 +  shows "sgn (x * y) = sgn x * sgn y"
1.77 +unfolding sgn_def by (simp add: norm_mult mult_commute)
1.78 +
1.79  lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
1.80 -unfolding sgn_def real_scaleR_def
1.81 -by (simp add: divide_inverse)
1.82 +unfolding sgn_def by (simp add: divide_inverse)
1.84  lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
1.85  unfolding real_sgn_eq by simp
1.86 @@ -764,7 +765,7 @@
1.87  apply (rule bounded_bilinear.intro)
1.88  apply (rule scaleR_left_distrib)
1.89  apply (rule scaleR_right_distrib)
1.90 -apply (simp add: real_scaleR_def)
1.91 +apply simp
1.92  apply (rule scaleR_left_commute)
1.93  apply (rule_tac x="1" in exI)
1.94  apply (simp add: norm_scaleR)