src/HOL/Analysis/Inner_Product.thy
changeset 67986 b65c4a6a015e
parent 67962 0acdcd8f4ba1
child 68072 493b818e8e10
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Sun Apr 15 17:22:58 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Sun Apr 15 21:41:40 2018 +0100
     1.3 @@ -49,6 +49,9 @@
     1.4  lemma inner_sum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
     1.5    by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
     1.6  
     1.7 +lemma all_zero_iff [simp]: "(\<forall>u. inner x u = 0) \<longleftrightarrow> (x = 0)"
     1.8 +  by auto (use inner_eq_zero_iff in blast)
     1.9 +
    1.10  text \<open>Transfer distributivity rules to right argument.\<close>
    1.11  
    1.12  lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    1.13 @@ -420,32 +423,12 @@
    1.14  lemma GDERIV_inverse:
    1.15      "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
    1.16       \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
    1.17 -  apply (erule GDERIV_DERIV_compose)
    1.18 -  apply (erule DERIV_inverse [folded numeral_2_eq_2])
    1.19 -  done
    1.20 -
    1.21 +  by (metis DERIV_inverse GDERIV_DERIV_compose numerals(2))
    1.22 +  
    1.23  lemma GDERIV_norm:
    1.24    assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
    1.25 -proof -
    1.26 -  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
    1.27 -    by (intro has_derivative_inner has_derivative_ident)
    1.28 -  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
    1.29 -    by (simp add: fun_eq_iff inner_commute)
    1.30 -  have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
    1.31 -  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
    1.32 -    by (rule DERIV_real_sqrt)
    1.33 -  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
    1.34 -    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
    1.35 -  show ?thesis
    1.36 -    unfolding norm_eq_sqrt_inner
    1.37 -    apply (rule GDERIV_subst [OF _ 4])
    1.38 -    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
    1.39 -    apply (subst gderiv_def)
    1.40 -    apply (rule has_derivative_subst [OF _ 2])
    1.41 -    apply (rule 1)
    1.42 -    apply (rule 3)
    1.43 -    done
    1.44 -qed
    1.45 +    unfolding gderiv_def norm_eq_sqrt_inner
    1.46 +    by (rule derivative_eq_intros | force simp add: inner_commute sgn_div_norm norm_eq_sqrt_inner assms)+
    1.47  
    1.48  lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
    1.49