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
```