add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
authorhuffman
Mon May 14 20:48:32 2007 +0200 (2007-05-14)
changeset 2297364d300e16370
parent 22972 3e96b98d37c6
child 22974 08b0fa905ea0
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
src/HOL/Real/RealVector.thy
     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.5  
     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.9  
    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.14    additive.diff [OF additive_scaleR_right, standard]
    1.15  
    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.30  
    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.40  
    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.48  
    1.49  text{*Collapse nested embeddings*}
    1.50 @@ -604,25 +602,28 @@
    1.51  unfolding sgn_def by simp
    1.52  
    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.56  
    1.57  lemma sgn_minus: "sgn (- x) = - sgn x"
    1.58  unfolding sgn_def by simp
    1.59  
    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.65  
    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.73  
    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.83  
    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)