a few new lemmas
authorpaulson <lp15@cam.ac.uk>
Fri Mar 07 12:35:06 2014 +0000 (2014-03-07)
changeset 559675dadc93ff3df
parent 55966 972f0aa7091b
child 55968 94242fa87638
a few new lemmas
src/HOL/Deriv.thy
src/HOL/NthRoot.thy
     1.1 --- a/src/HOL/Deriv.thy	Fri Mar 07 01:02:21 2014 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 07 12:35:06 2014 +0000
     1.3 @@ -389,11 +389,29 @@
     1.4  
     1.5  lemma FDERIV_divide[simp, FDERIV_intros]:
     1.6    fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
     1.7 -  assumes g: "FDERIV g x : s :> g'"
     1.8 -  assumes x:  "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
     1.9 -  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)"
    1.10 -  using FDERIV_mult[OF g FDERIV_inverse[OF x f]]
    1.11 -  by (simp add: divide_inverse)
    1.12 +  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" 
    1.13 +  assumes x: "g x \<noteq> 0"
    1.14 +  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
    1.15 +                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)"
    1.16 +  using FDERIV_mult[OF f FDERIV_inverse[OF x g]]
    1.17 +  by (simp add: divide_inverse field_simps)
    1.18 +
    1.19 +text{*Conventional form requires mult-AC laws. Types real and complex only.*}
    1.20 +lemma FDERIV_divide'[FDERIV_intros]: 
    1.21 +  fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
    1.22 +  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" and x: "g x \<noteq> 0"
    1.23 +  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
    1.24 +                (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))"
    1.25 +proof -
    1.26 +  { fix h
    1.27 +    have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
    1.28 +          (f' h * g x - f x * g' h) / (g x * g x)"
    1.29 +      by (simp add: divide_inverse field_simps nonzero_inverse_mult_distrib x)
    1.30 +   }
    1.31 +  then show ?thesis
    1.32 +    using FDERIV_divide [OF f g] x
    1.33 +    by simp
    1.34 +qed
    1.35  
    1.36  subsection {* Uniqueness *}
    1.37  
    1.38 @@ -605,6 +623,10 @@
    1.39    "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
    1.40    by (drule DERIV_mult' [OF DERIV_const], simp)
    1.41  
    1.42 +lemma DERIV_cmult_right:
    1.43 +  "DERIV f x : s :> D ==> DERIV (%x. f x * c) x : s :> D * c"
    1.44 +  using DERIV_cmult   by (force simp add: mult_ac)
    1.45 +
    1.46  lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
    1.47    by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
    1.48  
    1.49 @@ -674,13 +696,33 @@
    1.50    using FDERIV_compose[of f "\<lambda>x. x * D" x s g "\<lambda>x. x * E"]
    1.51    by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset)
    1.52  
    1.53 +corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
    1.54 +  by (rule DERIV_chain')
    1.55 +
    1.56  text {* Standard version *}
    1.57  
    1.58  lemma DERIV_chain: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
    1.59    by (drule (1) DERIV_chain', simp add: o_def mult_commute)
    1.60  
    1.61 -lemma DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
    1.62 -  by (auto dest: DERIV_chain simp add: o_def)
    1.63 +lemma DERIV_image_chain: 
    1.64 +  "DERIV f (g x) : (g ` s) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
    1.65 +  using FDERIV_in_compose [of g "\<lambda>x. x * Db" x s f "\<lambda>x. x * Da "]
    1.66 +  by (simp add: deriv_fderiv o_def  mult_ac)
    1.67 +
    1.68 +(*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
    1.69 +lemma DERIV_chain_s:
    1.70 +  assumes "(\<And>x. x \<in> s \<Longrightarrow> DERIV g x :> g'(x))"
    1.71 +      and "DERIV f x :> f'" 
    1.72 +      and "f x \<in> s"
    1.73 +    shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
    1.74 +  by (metis (full_types) DERIV_chain' mult_commute assms)
    1.75 +
    1.76 +lemma DERIV_chain3: (*HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV*)
    1.77 +  assumes "(\<And>x. DERIV g x :> g'(x))"
    1.78 +      and "DERIV f x :> f'" 
    1.79 +    shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
    1.80 +  by (metis UNIV_I DERIV_chain_s [of UNIV] assms)
    1.81 +
    1.82  
    1.83  subsubsection {* @{text "DERIV_intros"} *}
    1.84  
     2.1 --- a/src/HOL/NthRoot.thy	Fri Mar 07 01:02:21 2014 +0100
     2.2 +++ b/src/HOL/NthRoot.thy	Fri Mar 07 12:35:06 2014 +0000
     2.3 @@ -534,14 +534,35 @@
     2.4  
     2.5  subsection {* Square Root of Sum of Squares *}
     2.6  
     2.7 -lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<^sup>2 + y\<^sup>2)"
     2.8 -  by simp (* TODO: delete *)
     2.9 +lemma sum_squares_bound: 
    2.10 +  fixes x:: "'a::linordered_field"
    2.11 +  shows "2*x*y \<le> x^2 + y^2"
    2.12 +proof -
    2.13 +  have "(x-y)^2 = x*x - 2*x*y + y*y"
    2.14 +    by algebra
    2.15 +  then have "0 \<le> x^2 - 2*x*y + y^2"
    2.16 +    by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square)
    2.17 +  then show ?thesis
    2.18 +    by arith
    2.19 +qed
    2.20  
    2.21 -declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
    2.22 +lemma arith_geo_mean: 
    2.23 +  fixes u:: "'a::linordered_field" assumes "u\<^sup>2 = x*y" "x\<ge>0" "y\<ge>0" shows "u \<le> (x + y)/2"
    2.24 +    apply (rule power2_le_imp_le)
    2.25 +    using sum_squares_bound assms
    2.26 +    apply (auto simp: zero_le_mult_iff)
    2.27 +    by (auto simp: algebra_simps power2_eq_square)
    2.28 +
    2.29 +lemma arith_geo_mean_sqrt: 
    2.30 +  fixes x::real assumes "x\<ge>0" "y\<ge>0" shows "sqrt(x*y) \<le> (x + y)/2"
    2.31 +  apply (rule arith_geo_mean)
    2.32 +  using assms
    2.33 +  apply (auto simp: zero_le_mult_iff)
    2.34 +  done
    2.35  
    2.36  lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
    2.37       "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))"
    2.38 -  by (simp add: zero_le_mult_iff)
    2.39 +  by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero)
    2.40  
    2.41  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
    2.42       "(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)"