src/HOL/Multivariate_Analysis/Derivative.thy

-(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
-    Author:                     John Harrison
-    Translation from HOL light: Robert Himmelmann, TU Muenchen *)
+(*  Title:                       HOL/Multivariate_Analysis/Derivative.thy
+    Author:                      John Harrison
+    Translation from HOL Light:  Robert Himmelmann, TU Muenchen
+*)
 
 header {* Multivariate calculus in Euclidean space. *}
 
 theory Derivative
-  imports Brouwer_Fixpoint RealVector
+imports Brouwer_Fixpoint RealVector
 begin
 
 
 (* Because I do not want to type this all the time *)
 lemmas linear_linear = linear_conv_bounded_linear[THEN sym]

 next assume ?r note this[unfolded has_derivative_def Lim_at] note as=conjunct2[OF this,rule_format]
   have *:"\<And>x xa f'. xa \<noteq> 0 \<Longrightarrow> \<bar>(f (xa + x) - f x) / xa - f'\<bar> = \<bar>(f (xa + x) - f x) - xa * f'\<bar> / \<bar>xa\<bar>" by(auto simp add:field_simps) 
   show ?l unfolding deriv_def LIM_def apply safe apply(drule as,safe)
     apply(rule_tac x=d in exI,safe) apply(erule_tac x="xa + x" in allE)
     unfolding vector_dist_norm diff_0_right norm_scaleR
-    unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps *) qed
+    unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed
 
 lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof 
   assume ?l note as = this[unfolded fderiv_def]
   show ?r unfolding has_derivative_def Lim_at apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
     fix e::real assume "e>0"
     guess d using as[THEN conjunct2,unfolded LIM_def,rule_format,OF`e>0`] ..
     thus "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
       dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e"
       apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE)
-      unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps) qed next
+      unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next
   assume ?r note as = this[unfolded has_derivative_def]
   show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
     fix e::real assume "e>0"
     guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] ..
     thus "\<exists>s>0. \<forall>xa. xa \<noteq> 0 \<and> dist xa 0 < s \<longrightarrow> dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply-
       apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE)
-      unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps) qed qed
+      unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
 
 subsection {* These are the only cases we'll care about, probably. *}
 
 lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
          bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"

 lemma has_derivative_within':
   "(f has_derivative f')(at x within s) \<longleftrightarrow> bounded_linear f' \<and>
         (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm(x' - x) \<and> norm(x' - x) < d
         \<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"
   unfolding has_derivative_within Lim_within vector_dist_norm
-  unfolding diff_0_right norm_mul by(simp add: group_simps)
+  unfolding diff_0_right norm_mul by (simp add: diff_diff_eq)
 
 lemma has_derivative_at':
  "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
    (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm(x' - x) \<and> norm(x' - x) < d
         \<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"

 lemma has_derivative_add: assumes "(f has_derivative f') net" "(g has_derivative g') net"
   shows "((\<lambda>x. f(x) + g(x)) has_derivative (\<lambda>h. f'(h) + g'(h))) net" proof-
   note as = assms[unfolded has_derivative_def]
   show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
     using Lim_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
-    by(auto simp add:group_simps scaleR_right_diff_distrib scaleR_right_distrib) qed
+    by (auto simp add:algebra_simps scaleR_right_diff_distrib scaleR_right_distrib) qed
 
 lemma has_derivative_add_const:"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
   apply(drule has_derivative_add) apply(rule has_derivative_const) by auto
 
 lemma has_derivative_sub:
  "(f has_derivative f') net \<Longrightarrow> (g has_derivative g') net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) has_derivative (\<lambda>h. f'(h) - g'(h))) net"
-  apply(drule has_derivative_add) apply(drule has_derivative_neg,assumption) by(simp add:group_simps)
+  apply(drule has_derivative_add) apply(drule has_derivative_neg,assumption) by(simp add:algebra_simps)
 
 lemma has_derivative_setsum: assumes "finite s" "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
   shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
   apply(induct_tac s rule:finite_subset_induct[where A=s]) apply(rule assms(1)) 
 proof- fix x F assume as:"finite F" "x \<notin> F" "x\<in>s" "((\<lambda>x. \<Sum>a\<in>F. f a x) has_derivative (\<lambda>h. \<Sum>a\<in>F. f' a h)) net" 

     show "norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)" proof(cases "y=x")
       case True thus ?thesis using `bounded_linear f'` by(auto simp add: zero) next
       case False hence "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" using as(4)[rule_format, OF `y\<in>s`]
 	unfolding vector_dist_norm diff_0_right norm_mul using as(3)
 	using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded vector_dist_norm]
-	by(auto simp add:linear_0 linear_sub group_simps)
-      thus ?thesis by(auto simp add:group_simps) qed qed next
+	by (auto simp add: linear_0 linear_sub)
+      thus ?thesis by(auto simp add:algebra_simps) qed qed next
   assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within apply-apply(erule conjE,rule,assumption)
     apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer apply(erule exE,rule_tac x=d in exI)
     apply(erule conjE,rule,assumption,rule,rule) unfolding vector_dist_norm diff_0_right norm_scaleR
     apply(erule_tac x=xa in ballE,erule impE) proof-
     fix e d y assume "bounded_linear f'" "0 < e" "0 < d" "y \<in> s" "0 < norm (y - x) \<and> norm (y - x) < d"
         "norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)"
     thus "\<bar>1 / norm (y - x)\<bar> * norm (f y - (f x + f' (y - x))) < e"
-      apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed
+      apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:algebra_simps) qed auto qed
 
 lemma has_derivative_at_alt:
   "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
   (\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm(f y - f x - f'(y - x)) \<le> e * norm(y - x))"
   using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto

     proof(rule,rule `d>0`,rule,rule) 
     fix y assume as:"y \<in> s" "norm (y - x) < d"
     hence 1:"norm (f y - f x - f' (y - x)) \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x))" using d1 d2 d by auto
 
     have "norm (f y - f x) \<le> norm (f y - f x - f' (y - x)) + norm (f' (y - x))"
-      using norm_triangle_sub[of "f y - f x" "f' (y - x)"] by(auto simp add:group_simps)
-    also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)" apply(rule add_left_mono) using B1 by(auto simp add:group_simps)
+      using norm_triangle_sub[of "f y - f x" "f' (y - x)"] by(auto simp add:algebra_simps)
+    also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)" apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps)
     also have "\<dots> \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x)) + B1 * norm (y - x)" apply(rule add_right_mono) using d1 d2 d as by auto
     also have "\<dots> \<le> norm (y - x) + B1 * norm (y - x)" by auto
     also have "\<dots> = norm (y - x) * (1 + B1)" by(auto simp add:field_simps)
     finally have 3:"norm (f y - f x) \<le> norm (y - x) * (1 + B1)" by auto 
 

     finally have 4:"norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
     
     interpret g': bounded_linear g' using assms(2) by auto
     interpret f': bounded_linear f' using assms(1) by auto
     have "norm (- g' (f' (y - x)) + g' (f y - f x)) = norm (g' (f y - f x - f' (y - x)))"
-      by(auto simp add:group_simps f'.diff g'.diff g'.add)
-    also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2 by(auto simp add:group_simps)
+      by(auto simp add:algebra_simps f'.diff g'.diff g'.add)
+    also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2 by(auto simp add:algebra_simps)
     also have "\<dots> \<le> B2 * (e / 2 / B2 * norm (y - x))" apply(rule mult_left_mono) using as d1 d2 d B2 by auto 
     also have "\<dots> \<le> e / 2 * norm (y - x)" using B2 by auto
     finally have 5:"norm (- g' (f' (y - x)) + g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
     
     have "norm (g (f y) - g (f x) - g' (f y - f x)) + norm (g (f y) - g (f x) - g' (f' (y - x)) - (g (f y) - g (f x) - g' (f y - f x))) \<le> e * norm (y - x)" using 5 4 by auto

     guess c using assms(3)[rule_format,OF d[THEN conjunct1],of i] .. note c=this
     have *:"norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R basis i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R basis i)) = norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R basis i)) + f'' (c *\<^sub>R basis i)))"
       unfolding scaleR_right_distrib by auto
     also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' (basis i)) + f'' (basis i))))"  
       unfolding f'.scaleR f''.scaleR unfolding scaleR_right_distrib scaleR_minus_right by auto
-    also have "\<dots> = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by(auto simp add:group_simps)
+    also have "\<dots> = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by (auto simp add: add.commute ab_diff_minus)
     finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding vector_dist_norm 
       unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib by auto qed qed
 
 lemma frechet_derivative_unique_at: fixes f::"real^'a \<Rightarrow> real^'b"
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"

   hence **:"((f (x - d *\<^sub>R basis j))$k \<le> (f x)$k \<and> (f (x + d *\<^sub>R basis j))$k \<le> (f x)$k) \<or>
          ((f (x - d *\<^sub>R basis j))$k \<ge> (f x)$k \<and> (f (x + d *\<^sub>R basis j))$k \<ge> (f x)$k)" using assms(2) by auto
   have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
   show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"]) 
     using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
-    unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding group_simps by (auto intro: mult_pos_pos)
+    unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
 qed
 
 subsection {* In particular if we have a mapping into @{typ "real^1"}. *}
 
 lemma differential_zero_maxmin: fixes f::"real^'a \<Rightarrow> real"

 lemma differentiable_bound: fixes f::"real^'a \<Rightarrow> real^'b"
   assumes "convex s" "\<forall>x\<in>s. (f has_derivative f'(x)) (at x within s)" "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
   shows "norm(f x - f y) \<le> B * norm(x - y)" proof-
   let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
   have *:"\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
-    using assms(1)[unfolded convex_alt,rule_format,OF x y] unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by(auto simp add:group_simps)
+    using assms(1)[unfolded convex_alt,rule_format,OF x y] unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by(auto simp add:algebra_simps)
   hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply- apply(rule continuous_on_intros continuous_on_vmul)+
     unfolding continuous_on_eq_continuous_within apply(rule,rule differentiable_imp_continuous_within)
     unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
     apply(rule has_derivative_within_subset) apply(rule assms(2)[rule_format]) by auto
   have 2:"\<forall>u\<in>{0<..<1}. ((f \<circ> ?p) has_derivative f' (x + u *\<^sub>R (y - x)) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u)" proof rule case goal1

 
 lemma brouwer_surjective: fixes f::"real^'n \<Rightarrow> real^'n"
   assumes "compact t" "convex t"  "t \<noteq> {}" "continuous_on t f"
   "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t" "x\<in>s"
   shows "\<exists>y\<in>t. f y = x" proof-
-  have *:"\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y" by(auto simp add:group_simps)
+  have *:"\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y" by(auto simp add:algebra_simps)
   show ?thesis  unfolding * apply(rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
     apply(rule continuous_on_intros assms)+ using assms(4-6) by auto qed
 
 lemma brouwer_surjective_cball: fixes f::"real^'n \<Rightarrow> real^'n"
   assumes "0 < e" "continuous_on (cball a e) f"

     also have "\<dots> \<le> e * B" apply(rule mult_right_mono) using as(2)[unfolded mem_cball vector_dist_norm] and B unfolding norm_minus_commute by auto
     also have "\<dots> < e0" using e and B unfolding less_divide_eq by auto
     finally have *:"norm (x + g' (z - f x) - x) < e0" by auto
     have **:"f x + f' (x + g' (z - f x) - x) = z" using assms(6)[unfolded o_def id_def,THEN cong] by auto
     have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le> norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
-      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:group_simps)
-    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding group_simps ** by auto 
+      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:algebra_simps)
+    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding algebra_simps ** by auto 
     also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball vector_dist_norm] by auto
     also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2" using * and B by(auto simp add:field_simps)
     also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2" by auto
     also have "\<dots> \<le> e/2 + e/2" apply(rule add_right_mono) using as(2)[unfolded mem_cball vector_dist_norm] unfolding norm_minus_commute by auto
     finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e" unfolding mem_cball vector_dist_norm by auto

 (* It's only for this we need continuity of the derivative, except of course *)
 (* if we want the fact that the inverse derivative is also continuous. So if *)
 (* we know for some other reason that the inverse function exists, it's OK. *}
 
 lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g ==> bounded_linear (\<lambda>x. f x - g x)"
-  using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g] by(auto simp add:group_simps)
+  using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g] by(auto simp add:algebra_simps)
 
 lemma has_derivative_locally_injective: fixes f::"real^'n \<Rightarrow> real^'m"
   assumes "a \<in> s" "open s" "bounded_linear g'" "g' o f'(a) = id"
   "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
   "\<forall>e>0. \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm(\<lambda>v. f' x v - f' a v) < e"

   guess d using real_lbound_gt_zero[OF d1[THEN conjunct1] d2[THEN conjunct1]] .. note d = this
   show ?thesis proof show "a\<in>ball a d" using d by auto
     show "\<forall>x\<in>ball a d. \<forall>x'\<in>ball a d. f x' = f x \<longrightarrow> x' = x" proof(intro strip)
       fix x y assume as:"x\<in>ball a d" "y\<in>ball a d" "f x = f y"
       def ph \<equiv> "\<lambda>w. w - g'(f w - f x)" have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
-	unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:group_simps)
+	unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:algebra_simps)
       have "norm (ph x - ph y) \<le> (1/2) * norm (x - y)"
 	apply(rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
 	apply(rule_tac[!] ballI) proof- fix u assume u:"u \<in> ball a d" hence "u\<in>s" using d d2 by auto
 	have *:"(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)" unfolding o_def and diff using f'g' by auto
 	show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"

 	  apply(rule_tac[!] derivative_linear) using assms(5) `u\<in>s` `a\<in>s` by auto
 	have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)" unfolding * apply(rule onorm_compose)
 	  unfolding linear_conv_bounded_linear by(rule assms(3) **)+ 
 	also have "\<dots> \<le> onorm g' * k" apply(rule mult_left_mono) 
 	  using d1[THEN conjunct2,rule_format,of u] using onorm_neg[OF **(1)[unfolded linear_linear]]
-	  using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:group_simps) 
+	  using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:algebra_simps) 
 	also have "\<dots> \<le> 1/2" unfolding k_def by auto
 	finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" by assumption qed
       moreover have "norm (ph y - ph x) = norm (y - x)" apply(rule arg_cong[where f=norm])
 	unfolding ph_def using diff unfolding as by auto
       ultimately show "x = y" unfolding norm_minus_commute by auto qed qed auto qed

   show "norm((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm(x - y)"
     apply(rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)]) apply(rule_tac[!] ballI) proof-
     fix x assume "x\<in>s" show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
       by(rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
     { fix h have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
-	using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:group_simps) 
+	using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:algebra_simps) 
       also have "\<dots> \<le> e * norm h+ e * norm h"  using assms(3)[rule_format,OF `N\<le>m` `x\<in>s`, of h] assms(3)[rule_format,OF `N\<le>n` `x\<in>s`, of h]
 	by(auto simp add:field_simps)
       finally have "norm (f' m x h - f' n x h) \<le> 2 * e * norm h" by auto }
     thus "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e" apply-apply(rule onorm(2)) apply(rule linear_compose_sub)
       unfolding linear_conv_bounded_linear using assms(2)[rule_format,OF `x\<in>s`, THEN derivative_linear] by auto qed qed

     show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)" apply(rule_tac x=N in exI) proof(default+)
       fix n x y assume as:"N \<le> n" "x \<in> s" "y \<in> s"
       have "eventually (\<lambda>xa. norm (f n x - f n y - (f xa x - f xa y)) \<le> e * norm (x - y)) sequentially" 
 	unfolding eventually_sequentially apply(rule_tac x=N in exI) proof(rule,rule)
 	fix m assume "N\<le>m" thus "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
-	  using N[rule_format, of n m x y] and as by(auto simp add:group_simps) qed
+	  using N[rule_format, of n m x y] and as by(auto simp add:algebra_simps) qed
       thus "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)" apply-
 	apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\<lambda>m. (f n x - f n y) - (f m x - f m y)"])
 	apply(rule Lim_sub Lim_const g[rule_format] as)+ by assumption qed qed
   show ?thesis unfolding has_derivative_within_alt apply(rule_tac x=g in exI)
     apply(rule,rule,rule g[rule_format],assumption) proof fix x assume "x\<in>s"

 	have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e /3 * norm (y - x)" apply(subst norm_minus_cancel[THEN sym])
 	  using N2[rule_format, OF _ `y\<in>s` `x\<in>s`, of ?N] by auto moreover
 	have "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)" using d1 and as by auto ultimately
 	have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)" 
 	  using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] 
-	  by (auto simp add:group_simps) moreover
+	  by (auto simp add:algebra_simps) moreover
 	have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)" using N1 `x\<in>s` by auto
 	ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
-	  using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:group_simps)
+	  using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:algebra_simps)
 	qed qed qed qed
 
 subsection {* Can choose to line up antiderivatives if we want. *}
 
 lemma has_antiderivative_sequence: fixes f::"nat\<Rightarrow> real^'m \<Rightarrow> real^'n"

 
 lemma has_vector_derivative_id: "((\<lambda>x::real. x) has_vector_derivative 1) net"
   unfolding has_vector_derivative_def using has_derivative_id by auto
 
 lemma has_vector_derivative_cmul:  "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
-  unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:group_simps)
+  unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:algebra_simps)
 
 lemma has_vector_derivative_cmul_eq: assumes "c \<noteq> 0"
   shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
   apply rule apply(drule has_vector_derivative_cmul[where c="1/c"]) defer
   apply(rule has_vector_derivative_cmul) using assms by auto