declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
authorhuffman
Fri Jun 12 16:23:07 2009 -0700 (2009-06-12)
changeset 31590776d6a4c1327
parent 31589 eeebb2915035
child 31591 c8c96efa4488
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Jun 12 16:04:55 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Jun 12 16:23:07 2009 -0700
     1.3 @@ -809,10 +809,10 @@
     1.4      by (simp add: inner_commute)
     1.5    show "inner (x + y) z = inner x z + inner y z"
     1.6      unfolding vector_inner_def
     1.7 -    by (simp add: inner_left_distrib setsum_addf)
     1.8 +    by (simp add: inner_add_left setsum_addf)
     1.9    show "inner (scaleR r x) y = r * inner x y"
    1.10      unfolding vector_inner_def
    1.11 -    by (simp add: inner_scaleR_left setsum_right_distrib)
    1.12 +    by (simp add: setsum_right_distrib)
    1.13    show "0 \<le> inner x x"
    1.14      unfolding vector_inner_def
    1.15      by (simp add: setsum_nonneg)
     2.1 --- a/src/HOL/Library/Inner_Product.thy	Fri Jun 12 16:04:55 2009 -0700
     2.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Jun 12 16:23:07 2009 -0700
     2.3 @@ -27,28 +27,28 @@
     2.4  class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
     2.5    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
     2.6    assumes inner_commute: "inner x y = inner y x"
     2.7 -  and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
     2.8 -  and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)"
     2.9 +  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    2.10 +  and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
    2.11    and inner_ge_zero [simp]: "0 \<le> inner x x"
    2.12    and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
    2.13    and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
    2.14  begin
    2.15  
    2.16  lemma inner_zero_left [simp]: "inner 0 x = 0"
    2.17 -  using inner_left_distrib [of 0 0 x] by simp
    2.18 +  using inner_add_left [of 0 0 x] by simp
    2.19  
    2.20  lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    2.21 -  using inner_left_distrib [of x "- x" y] by simp
    2.22 +  using inner_add_left [of x "- x" y] by simp
    2.23  
    2.24  lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    2.25 -  by (simp add: diff_minus inner_left_distrib)
    2.26 +  by (simp add: diff_minus inner_add_left)
    2.27  
    2.28  text {* Transfer distributivity rules to right argument. *}
    2.29  
    2.30 -lemma inner_right_distrib: "inner x (y + z) = inner x y + inner x z"
    2.31 -  using inner_left_distrib [of y z x] by (simp only: inner_commute)
    2.32 +lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    2.33 +  using inner_add_left [of y z x] by (simp only: inner_commute)
    2.34  
    2.35 -lemma inner_scaleR_right: "inner x (scaleR r y) = r * (inner x y)"
    2.36 +lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    2.37    using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    2.38  
    2.39  lemma inner_zero_right [simp]: "inner x 0 = 0"
    2.40 @@ -60,9 +60,14 @@
    2.41  lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    2.42    using inner_diff_left [of y z x] by (simp only: inner_commute)
    2.43  
    2.44 +lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    2.45 +lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    2.46 +lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    2.47 +
    2.48 +text {* Legacy theorem names *}
    2.49 +lemmas inner_left_distrib = inner_add_left
    2.50 +lemmas inner_right_distrib = inner_add_right
    2.51  lemmas inner_distrib = inner_left_distrib inner_right_distrib
    2.52 -lemmas inner_diff = inner_diff_left inner_diff_right
    2.53 -lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    2.54  
    2.55  lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    2.56    by (simp add: order_less_le)
    2.57 @@ -81,7 +86,7 @@
    2.58    have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
    2.59      by (rule inner_ge_zero)
    2.60    also have "\<dots> = inner x x - inner y x * ?r"
    2.61 -    by (simp add: inner_diff inner_scaleR)
    2.62 +    by (simp add: inner_diff)
    2.63    also have "\<dots> = inner x x - (inner x y)\<twosuperior> / inner y y"
    2.64      by (simp add: power2_eq_square inner_commute)
    2.65    finally have "0 \<le> inner x x - (inner x y)\<twosuperior> / inner y y" .
    2.66 @@ -116,7 +121,7 @@
    2.67          by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
    2.68        thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
    2.69          unfolding power2_sum power2_norm_eq_inner
    2.70 -        by (simp add: inner_distrib inner_commute)
    2.71 +        by (simp add: inner_add inner_commute)
    2.72        show "0 \<le> norm x + norm y"
    2.73          unfolding norm_eq_sqrt_inner
    2.74          by (simp add: add_nonneg_nonneg)
    2.75 @@ -125,7 +130,7 @@
    2.76      by (simp add: real_sqrt_mult_distrib)
    2.77    then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
    2.78      unfolding norm_eq_sqrt_inner
    2.79 -    by (simp add: inner_scaleR power2_eq_square mult_assoc)
    2.80 +    by (simp add: power2_eq_square mult_assoc)
    2.81  qed
    2.82  
    2.83  end
    2.84 @@ -149,9 +154,9 @@
    2.85  proof
    2.86    fix x y z :: 'a and r :: real
    2.87    show "inner (x + y) z = inner x z + inner y z"
    2.88 -    by (rule inner_left_distrib)
    2.89 +    by (rule inner_add_left)
    2.90    show "inner x (y + z) = inner x y + inner x z"
    2.91 -    by (rule inner_right_distrib)
    2.92 +    by (rule inner_add_right)
    2.93    show "inner (scaleR r x) y = scaleR r (inner x y)"
    2.94      unfolding real_scaleR_def by (rule inner_scaleR_left)
    2.95    show "inner x (scaleR r y) = scaleR r (inner x y)"
    2.96 @@ -244,7 +249,7 @@
    2.97       \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
    2.98    unfolding gderiv_def deriv_fderiv
    2.99    apply (drule (1) FDERIV_compose)
   2.100 -  apply (simp add: inner_scaleR_right mult_ac)
   2.101 +  apply (simp add: mult_ac)
   2.102    done
   2.103  
   2.104  lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   2.105 @@ -286,7 +291,7 @@
   2.106    unfolding gderiv_def
   2.107    apply (rule FDERIV_subst)
   2.108    apply (erule (1) FDERIV_mult)
   2.109 -  apply (simp add: inner_distrib inner_scaleR mult_ac)
   2.110 +  apply (simp add: inner_add mult_ac)
   2.111    done
   2.112  
   2.113  lemma GDERIV_inverse:
   2.114 @@ -302,7 +307,7 @@
   2.115    have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   2.116      by (intro inner.FDERIV FDERIV_ident)
   2.117    have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   2.118 -    by (simp add: expand_fun_eq inner_scaleR inner_commute)
   2.119 +    by (simp add: expand_fun_eq inner_commute)
   2.120    have "0 < inner x x" using `x \<noteq> 0` by simp
   2.121    then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   2.122      by (rule DERIV_real_sqrt)
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Jun 12 16:04:55 2009 -0700
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Jun 12 16:23:07 2009 -0700
     3.3 @@ -381,10 +381,10 @@
     3.4      by (simp add: inner_commute)
     3.5    show "inner (x + y) z = inner x z + inner y z"
     3.6      unfolding inner_prod_def
     3.7 -    by (simp add: inner_left_distrib)
     3.8 +    by (simp add: inner_add_left)
     3.9    show "inner (scaleR r x) y = r * inner x y"
    3.10      unfolding inner_prod_def
    3.11 -    by (simp add: inner_scaleR_left right_distrib)
    3.12 +    by (simp add: right_distrib)
    3.13    show "0 \<le> inner x x"
    3.14      unfolding inner_prod_def
    3.15      by (intro add_nonneg_nonneg inner_ge_zero)