src/HOL/Library/Inner_Product.thy

 (*  Title:      HOL/Library/Inner_Product.thy
     Author:     Brian Huffman
 *)
 
-section {* Inner Product Spaces and the Gradient Derivative *}
+section \<open>Inner Product Spaces and the Gradient Derivative\<close>
 
 theory Inner_Product
 imports "~~/src/HOL/Complex_Main"
 begin
 
-subsection {* Real inner product spaces *}
-
-text {*
+subsection \<open>Real inner product spaces\<close>
+
+text \<open>
   Temporarily relax type constraints for @{term "open"},
   @{term dist}, and @{term norm}.
-*}
-
-setup {* Sign.add_const_constraint
-  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"}) *}
-
-setup {* Sign.add_const_constraint
-  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
-
-setup {* Sign.add_const_constraint
-  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
+\<close>
+
+setup \<open>Sign.add_const_constraint
+  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close>
+
+setup \<open>Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
+
+setup \<open>Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
 
 class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_add_left: "inner (x + y) z = inner x z + inner y z"

   using inner_add_left [of x "- y" z] by simp
 
 lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
   by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
 
-text {* Transfer distributivity rules to right argument. *}
+text \<open>Transfer distributivity rules to right argument.\<close>
 
 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
   using inner_add_left [of y z x] by (simp only: inner_commute)
 
 lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"

 
 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
 lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
 
-text {* Legacy theorem names *}
+text \<open>Legacy theorem names\<close>
 lemmas inner_left_distrib = inner_add_left
 lemmas inner_right_distrib = inner_add_right
 lemmas inner_distrib = inner_left_distrib inner_right_distrib
 
 lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"

     by (simp add: power2_eq_square mult.assoc)
 qed
 
 end
 
-text {*
+text \<open>
   Re-enable constraints for @{term "open"},
   @{term dist}, and @{term norm}.
-*}
-
-setup {* Sign.add_const_constraint
-  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
-
-setup {* Sign.add_const_constraint
-  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
-
-setup {* Sign.add_const_constraint
-  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
+\<close>
+
+setup \<open>Sign.add_const_constraint
+  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
+
+setup \<open>Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
+
+setup \<open>Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
 
 lemma bounded_bilinear_inner:
   "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
 proof
   fix x y z :: 'a and r :: real

 
 lemma differentiable_inner [simp]:
   "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
   unfolding differentiable_def by (blast intro: has_derivative_inner)
 
-subsection {* Class instances *}
+subsection \<open>Class instances\<close>
 
 instantiation real :: real_inner
 begin
 
 definition inner_real_def [simp]: "inner = op *"

 
 lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
   unfolding inner_complex_def by simp
 
 
-subsection {* Gradient derivative *}
+subsection \<open>Gradient derivative\<close>
 
 definition
   gderiv ::
     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)

 proof -
   have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
     by (intro has_derivative_inner has_derivative_ident)
   have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
     by (simp add: fun_eq_iff inner_commute)
-  have "0 < inner x x" using `x \<noteq> 0` by simp
+  have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
   then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
     by (rule DERIV_real_sqrt)
   have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
     by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   show ?thesis