a few new lemmas

--- a/src/HOL/Deriv.thy	Fri Mar 07 01:02:21 2014 +0100
+++ b/src/HOL/Deriv.thy	Fri Mar 07 12:35:06 2014 +0000
@@ -389,11 +389,29 @@
 
 lemma FDERIV_divide[simp, FDERIV_intros]:
   fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
-  assumes g: "FDERIV g x : s :> g'"
-  assumes x:  "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
-  shows "FDERIV (\<lambda>x. g x / f x) x : s :> (\<lambda>h. - g x * (inverse (f x) * f' h * inverse (f x)) + g' h / f x)"
-  using FDERIV_mult[OF g FDERIV_inverse[OF x f]]
-  by (simp add: divide_inverse)
+  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" 
+  assumes x: "g x \<noteq> 0"
+  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
+                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)"
+  using FDERIV_mult[OF f FDERIV_inverse[OF x g]]
+  by (simp add: divide_inverse field_simps)
+
+text{*Conventional form requires mult-AC laws. Types real and complex only.*}
+lemma FDERIV_divide'[FDERIV_intros]: 
+  fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
+  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" and x: "g x \<noteq> 0"
+  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
+                (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))"
+proof -
+  { fix h
+    have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
+          (f' h * g x - f x * g' h) / (g x * g x)"
+      by (simp add: divide_inverse field_simps nonzero_inverse_mult_distrib x)
+   }
+  then show ?thesis
+    using FDERIV_divide [OF f g] x
+    by simp
+qed
 
 subsection {* Uniqueness *}
 
@@ -605,6 +623,10 @@
   "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
   by (drule DERIV_mult' [OF DERIV_const], simp)
 
+lemma DERIV_cmult_right:
+  "DERIV f x : s :> D ==> DERIV (%x. f x * c) x : s :> D * c"
+  using DERIV_cmult   by (force simp add: mult_ac)
+
 lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
   by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
 
@@ -674,13 +696,33 @@
   using FDERIV_compose[of f "\<lambda>x. x * D" x s g "\<lambda>x. x * E"]
   by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset)
 
+corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
+  by (rule DERIV_chain')
+
 text {* Standard version *}
 
 lemma DERIV_chain: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
   by (drule (1) DERIV_chain', simp add: o_def mult_commute)
 
-lemma DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
-  by (auto dest: DERIV_chain simp add: o_def)
+lemma DERIV_image_chain: 
+  "DERIV f (g x) : (g ` s) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
+  using FDERIV_in_compose [of g "\<lambda>x. x * Db" x s f "\<lambda>x. x * Da "]
+  by (simp add: deriv_fderiv o_def  mult_ac)
+
+(*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
+lemma DERIV_chain_s:
+  assumes "(\<And>x. x \<in> s \<Longrightarrow> DERIV g x :> g'(x))"
+      and "DERIV f x :> f'" 
+      and "f x \<in> s"
+    shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
+  by (metis (full_types) DERIV_chain' mult_commute assms)
+
+lemma DERIV_chain3: (*HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV*)
+  assumes "(\<And>x. DERIV g x :> g'(x))"
+      and "DERIV f x :> f'" 
+    shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
+  by (metis UNIV_I DERIV_chain_s [of UNIV] assms)
+
 
 subsubsection {* @{text "DERIV_intros"} *}
 

--- a/src/HOL/NthRoot.thy	Fri Mar 07 01:02:21 2014 +0100
+++ b/src/HOL/NthRoot.thy	Fri Mar 07 12:35:06 2014 +0000
@@ -534,14 +534,35 @@
 
 subsection {* Square Root of Sum of Squares *}
 
-lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
-  by simp (* TODO: delete *)
+lemma sum_squares_bound: 
+  fixes x:: "'a::linordered_field"
+  shows "2*x*y \<le> x^2 + y^2"
+proof -
+  have "(x-y)^2 = x*x - 2*x*y + y*y"
+    by algebra
+  then have "0 \<le> x^2 - 2*x*y + y^2"
+    by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square)
+  then show ?thesis
+    by arith
+qed
 
-declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
+lemma arith_geo_mean: 
+  fixes u:: "'a::linordered_field" assumes "u\<^sup>2 = x*y" "x\<ge>0" "y\<ge>0" shows "u \<le> (x + y)/2"
+    apply (rule power2_le_imp_le)
+    using sum_squares_bound assms
+    apply (auto simp: zero_le_mult_iff)
+    by (auto simp: algebra_simps power2_eq_square)
+
+lemma arith_geo_mean_sqrt: 
+  fixes x::real assumes "x\<ge>0" "y\<ge>0" shows "sqrt(x*y) \<le> (x + y)/2"
+  apply (rule arith_geo_mean)
+  using assms
+  apply (auto simp: zero_le_mult_iff)
+  done
 
 lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
      "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"
-  by (simp add: zero_le_mult_iff)
+  by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero)
 
 lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
      "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)"