src/HOL/Library/Inner_Product.thy
changeset 31590 776d6a4c1327
parent 31492 5400beeddb55
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Fri Jun 12 16:04:55 2009 -0700
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Jun 12 16:23:07 2009 -0700
     1.3 @@ -27,28 +27,28 @@
     1.4  class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
     1.5    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
     1.6    assumes inner_commute: "inner x y = inner y x"
     1.7 -  and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
     1.8 -  and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)"
     1.9 +  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    1.10 +  and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
    1.11    and inner_ge_zero [simp]: "0 \<le> inner x x"
    1.12    and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
    1.13    and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
    1.14  begin
    1.15  
    1.16  lemma inner_zero_left [simp]: "inner 0 x = 0"
    1.17 -  using inner_left_distrib [of 0 0 x] by simp
    1.18 +  using inner_add_left [of 0 0 x] by simp
    1.19  
    1.20  lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    1.21 -  using inner_left_distrib [of x "- x" y] by simp
    1.22 +  using inner_add_left [of x "- x" y] by simp
    1.23  
    1.24  lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    1.25 -  by (simp add: diff_minus inner_left_distrib)
    1.26 +  by (simp add: diff_minus inner_add_left)
    1.27  
    1.28  text {* Transfer distributivity rules to right argument. *}
    1.29  
    1.30 -lemma inner_right_distrib: "inner x (y + z) = inner x y + inner x z"
    1.31 -  using inner_left_distrib [of y z x] by (simp only: inner_commute)
    1.32 +lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    1.33 +  using inner_add_left [of y z x] by (simp only: inner_commute)
    1.34  
    1.35 -lemma inner_scaleR_right: "inner x (scaleR r y) = r * (inner x y)"
    1.36 +lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    1.37    using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    1.38  
    1.39  lemma inner_zero_right [simp]: "inner x 0 = 0"
    1.40 @@ -60,9 +60,14 @@
    1.41  lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    1.42    using inner_diff_left [of y z x] by (simp only: inner_commute)
    1.43  
    1.44 +lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    1.45 +lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    1.46 +lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    1.47 +
    1.48 +text {* Legacy theorem names *}
    1.49 +lemmas inner_left_distrib = inner_add_left
    1.50 +lemmas inner_right_distrib = inner_add_right
    1.51  lemmas inner_distrib = inner_left_distrib inner_right_distrib
    1.52 -lemmas inner_diff = inner_diff_left inner_diff_right
    1.53 -lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    1.54  
    1.55  lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    1.56    by (simp add: order_less_le)
    1.57 @@ -81,7 +86,7 @@
    1.58    have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
    1.59      by (rule inner_ge_zero)
    1.60    also have "\<dots> = inner x x - inner y x * ?r"
    1.61 -    by (simp add: inner_diff inner_scaleR)
    1.62 +    by (simp add: inner_diff)
    1.63    also have "\<dots> = inner x x - (inner x y)\<twosuperior> / inner y y"
    1.64      by (simp add: power2_eq_square inner_commute)
    1.65    finally have "0 \<le> inner x x - (inner x y)\<twosuperior> / inner y y" .
    1.66 @@ -116,7 +121,7 @@
    1.67          by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
    1.68        thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
    1.69          unfolding power2_sum power2_norm_eq_inner
    1.70 -        by (simp add: inner_distrib inner_commute)
    1.71 +        by (simp add: inner_add inner_commute)
    1.72        show "0 \<le> norm x + norm y"
    1.73          unfolding norm_eq_sqrt_inner
    1.74          by (simp add: add_nonneg_nonneg)
    1.75 @@ -125,7 +130,7 @@
    1.76      by (simp add: real_sqrt_mult_distrib)
    1.77    then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
    1.78      unfolding norm_eq_sqrt_inner
    1.79 -    by (simp add: inner_scaleR power2_eq_square mult_assoc)
    1.80 +    by (simp add: power2_eq_square mult_assoc)
    1.81  qed
    1.82  
    1.83  end
    1.84 @@ -149,9 +154,9 @@
    1.85  proof
    1.86    fix x y z :: 'a and r :: real
    1.87    show "inner (x + y) z = inner x z + inner y z"
    1.88 -    by (rule inner_left_distrib)
    1.89 +    by (rule inner_add_left)
    1.90    show "inner x (y + z) = inner x y + inner x z"
    1.91 -    by (rule inner_right_distrib)
    1.92 +    by (rule inner_add_right)
    1.93    show "inner (scaleR r x) y = scaleR r (inner x y)"
    1.94      unfolding real_scaleR_def by (rule inner_scaleR_left)
    1.95    show "inner x (scaleR r y) = scaleR r (inner x y)"
    1.96 @@ -244,7 +249,7 @@
    1.97       \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
    1.98    unfolding gderiv_def deriv_fderiv
    1.99    apply (drule (1) FDERIV_compose)
   1.100 -  apply (simp add: inner_scaleR_right mult_ac)
   1.101 +  apply (simp add: mult_ac)
   1.102    done
   1.103  
   1.104  lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   1.105 @@ -286,7 +291,7 @@
   1.106    unfolding gderiv_def
   1.107    apply (rule FDERIV_subst)
   1.108    apply (erule (1) FDERIV_mult)
   1.109 -  apply (simp add: inner_distrib inner_scaleR mult_ac)
   1.110 +  apply (simp add: inner_add mult_ac)
   1.111    done
   1.112  
   1.113  lemma GDERIV_inverse:
   1.114 @@ -302,7 +307,7 @@
   1.115    have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   1.116      by (intro inner.FDERIV FDERIV_ident)
   1.117    have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   1.118 -    by (simp add: expand_fun_eq inner_scaleR inner_commute)
   1.119 +    by (simp add: expand_fun_eq inner_commute)
   1.120    have "0 < inner x x" using `x \<noteq> 0` by simp
   1.121    then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   1.122      by (rule DERIV_real_sqrt)