1.1 --- a/src/HOL/FrechetDeriv.thy Sun Dec 14 18:45:16 2008 +0100
1.2 +++ b/src/HOL/FrechetDeriv.thy Sun Dec 14 18:45:51 2008 +0100
1.3 @@ -65,8 +65,8 @@
1.4 assumes "bounded_linear g"
1.5 shows "bounded_linear (\<lambda>x. f x + g x)"
1.6 proof -
1.7 - interpret f: bounded_linear [f] by fact
1.8 - interpret g: bounded_linear [g] by fact
1.9 + interpret f: bounded_linear f by fact
1.10 + interpret g: bounded_linear g by fact
1.11 show ?thesis apply (unfold_locales)
1.12 apply (simp only: f.add g.add add_ac)
1.13 apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
1.14 @@ -124,7 +124,7 @@
1.15 assumes "bounded_linear f"
1.16 shows "bounded_linear (\<lambda>x. - f x)"
1.17 proof -
1.18 - interpret f: bounded_linear [f] by fact
1.19 + interpret f: bounded_linear f by fact
1.20 show ?thesis apply (unfold_locales)
1.21 apply (simp add: f.add)
1.22 apply (simp add: f.scaleR)
1.23 @@ -151,7 +151,7 @@
1.24 assumes f: "FDERIV f x :> F"
1.25 shows "isCont f x"
1.26 proof -
1.27 - from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
1.28 + from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
1.29 have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
1.30 by (rule FDERIV_D [OF f])
1.31 hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
1.32 @@ -180,8 +180,8 @@
1.33 assumes "bounded_linear g"
1.34 shows "bounded_linear (\<lambda>x. f (g x))"
1.35 proof -
1.36 - interpret f: bounded_linear [f] by fact
1.37 - interpret g: bounded_linear [g] by fact
1.38 + interpret f: bounded_linear f by fact
1.39 + interpret g: bounded_linear g by fact
1.40 show ?thesis proof (unfold_locales)
1.41 fix x y show "f (g (x + y)) = f (g x) + f (g y)"
1.42 by (simp only: f.add g.add)
1.43 @@ -223,8 +223,8 @@
1.44 let ?k = "\<lambda>h. f (x + h) - f x"
1.45 let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
1.46 let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
1.47 - from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
1.48 - from g interpret G: bounded_linear ["G"] by (rule FDERIV_bounded_linear)
1.49 + from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
1.50 + from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
1.51 from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
1.52 from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
1.53
1.54 @@ -375,9 +375,9 @@
1.55 by (simp only: FDERIV_lemma)
1.56 qed
1.57
1.58 -lemmas FDERIV_mult = bounded_bilinear_locale.mult.prod.FDERIV
1.59 +lemmas FDERIV_mult = mult.FDERIV
1.60
1.61 -lemmas FDERIV_scaleR = bounded_bilinear_locale.scaleR.prod.FDERIV
1.62 +lemmas FDERIV_scaleR = scaleR.FDERIV
1.63
1.64
1.65 subsection {* Powers *}
1.66 @@ -409,10 +409,10 @@
1.67 by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
1.68
1.69 lemmas bounded_linear_mult_const =
1.70 - bounded_bilinear_locale.mult.prod.bounded_linear_left [THEN bounded_linear_compose]
1.71 + mult.bounded_linear_left [THEN bounded_linear_compose]
1.72
1.73 lemmas bounded_linear_const_mult =
1.74 - bounded_bilinear_locale.mult.prod.bounded_linear_right [THEN bounded_linear_compose]
1.75 + mult.bounded_linear_right [THEN bounded_linear_compose]
1.76
1.77 lemma FDERIV_inverse:
1.78 fixes x :: "'a::real_normed_div_algebra"
1.79 @@ -492,7 +492,7 @@
1.80 fixes x :: "'a::real_normed_field" shows
1.81 "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
1.82 apply (unfold fderiv_def)
1.83 - apply (simp add: bounded_bilinear_locale.mult.prod.bounded_linear_left)
1.84 + apply (simp add: mult.bounded_linear_left)
1.85 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
1.86 apply (subst diff_divide_distrib)
1.87 apply (subst times_divide_eq_left [symmetric])