1.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Inner Product Spaces and the Gradient Derivative *}
     1.5  
     1.6  theory Inner_Product
     1.7 -imports Complex_Main FrechetDeriv
     1.8 +imports FrechetDeriv
     1.9  begin
    1.10  
    1.11  subsection {* Real inner product spaces *}
    1.12 @@ -43,6 +43,9 @@
    1.13  lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    1.14    by (simp add: diff_minus inner_add_left)
    1.15  
    1.16 +lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
    1.17 +  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    1.18 +
    1.19  text {* Transfer distributivity rules to right argument. *}
    1.20  
    1.21  lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    1.22 @@ -60,6 +63,9 @@
    1.23  lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    1.24    using inner_diff_left [of y z x] by (simp only: inner_commute)
    1.25  
    1.26 +lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    1.27 +  using inner_setsum_left [of f A x] by (simp only: inner_commute)
    1.28 +
    1.29  lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    1.30  lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    1.31  lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    1.32 @@ -148,8 +154,8 @@
    1.33  setup {* Sign.add_const_constraint
    1.34    (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
    1.35  
    1.36 -interpretation inner:
    1.37 -  bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
    1.38 +lemma bounded_bilinear_inner:
    1.39 +  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
    1.40  proof
    1.41    fix x y z :: 'a and r :: real
    1.42    show "inner (x + y) z = inner x z + inner y z"
    1.43 @@ -167,15 +173,20 @@
    1.44    qed
    1.45  qed
    1.46  
    1.47 -interpretation inner_left:
    1.48 -  bounded_linear "\<lambda>x::'a::real_inner. inner x y"
    1.49 -  by (rule inner.bounded_linear_left)
    1.50 +lemmas tendsto_inner [tendsto_intros] =
    1.51 +  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
    1.52 +
    1.53 +lemmas isCont_inner [simp] =
    1.54 +  bounded_bilinear.isCont [OF bounded_bilinear_inner]
    1.55  
    1.56 -interpretation inner_right:
    1.57 -  bounded_linear "\<lambda>y::'a::real_inner. inner x y"
    1.58 -  by (rule inner.bounded_linear_right)
    1.59 +lemmas FDERIV_inner =
    1.60 +  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
    1.61  
    1.62 -declare inner.isCont [simp]
    1.63 +lemmas bounded_linear_inner_left =
    1.64 +  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
    1.65 +
    1.66 +lemmas bounded_linear_inner_right =
    1.67 +  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
    1.68  
    1.69  
    1.70  subsection {* Class instances *}
    1.71 @@ -260,29 +271,29 @@
    1.72    by simp
    1.73  
    1.74  lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
    1.75 -  unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
    1.76 +  unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
    1.77  
    1.78  lemma GDERIV_add:
    1.79      "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
    1.80       \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
    1.81 -  unfolding gderiv_def inner_right.add by (rule FDERIV_add)
    1.82 +  unfolding gderiv_def inner_add_right by (rule FDERIV_add)
    1.83  
    1.84  lemma GDERIV_minus:
    1.85      "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
    1.86 -  unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
    1.87 +  unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
    1.88  
    1.89  lemma GDERIV_diff:
    1.90      "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
    1.91       \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
    1.92 -  unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
    1.93 +  unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
    1.94  
    1.95  lemma GDERIV_scaleR:
    1.96      "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
    1.97       \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
    1.98        :> (scaleR (f x) dg + scaleR df (g x))"
    1.99 -  unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
   1.100 +  unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
   1.101    apply (rule FDERIV_subst)
   1.102 -  apply (erule (1) scaleR.FDERIV)
   1.103 +  apply (erule (1) FDERIV_scaleR)
   1.104    apply (simp add: mult_ac)
   1.105    done
   1.106  
   1.107 @@ -306,7 +317,7 @@
   1.108    assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   1.109  proof -
   1.110    have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   1.111 -    by (intro inner.FDERIV FDERIV_ident)
   1.112 +    by (intro FDERIV_inner FDERIV_ident)
   1.113    have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   1.114      by (simp add: fun_eq_iff inner_commute)
   1.115    have "0 < inner x x" using `x \<noteq> 0` by simp