# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1706267962 0
# Node ID bb5d036f352376a1713f8ff0d72a0f49f566cdc9
# Parent  1b0fc6ceb750641b4ad0d223ce65e6600bff3f4d
Type class patch suggested by Achim Brucker, plus tidied lemma

diff -r 1b0fc6ceb750 -r bb5d036f3523 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Thu Jan 25 17:08:07 2024 +0000
+++ b/src/HOL/Analysis/Convex.thy	Fri Jan 26 11:19:22 2024 +0000
@@ -911,14 +911,10 @@
 next
   case True
   define r where "r \<equiv> (\<Sum>i\<in>I. a i * b i) / (\<Sum>i\<in>I. (b i)\<^sup>2)"
-  with True have *: "(\<Sum>i\<in>I. a i * b i) = r * (\<Sum>i\<in>I. (b i)\<^sup>2)"
-    by simp
   have "0 \<le> (\<Sum>i\<in>I. (a i - r * b i)\<^sup>2)"
-    by (meson sum_nonneg zero_le_power2)
+    by (simp add: sum_nonneg)
   also have "... = (\<Sum>i\<in>I. (a i)\<^sup>2) - 2 * r * (\<Sum>i\<in>I. a i * b i) + r\<^sup>2 * (\<Sum>i\<in>I. (b i)\<^sup>2)"
     by (simp add: algebra_simps power2_eq_square sum_distrib_left flip: sum.distrib)
-  also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - (\<Sum>i\<in>I. a i * b i) * r"
-    by (simp add: * power2_eq_square)
   also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)"
     by (simp add: r_def power2_eq_square)
   finally have "0 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)" .
@@ -2436,4 +2432,4 @@
   "convex hull (\<Sum>i\<in>A. B i) = (\<Sum>i\<in>A. convex hull (B i))"
   by (induction A rule: infinite_finite_induct) (auto simp: convex_hull_set_plus)
 
-end
\ No newline at end of file
+end
diff -r 1b0fc6ceb750 -r bb5d036f3523 src/HOL/Library/Interval.thy
--- a/src/HOL/Library/Interval.thy	Thu Jan 25 17:08:07 2024 +0000
+++ b/src/HOL/Library/Interval.thy	Fri Jan 26 11:19:22 2024 +0000
@@ -178,7 +178,7 @@
 instance ..
 end
 
-instantiation "interval" :: (linordered_semiring) times
+instantiation "interval" :: ("{times, linorder}") times
 begin
 
 lift_definition times_interval :: "'a interval \<Rightarrow> 'a interval \<Rightarrow> 'a interval"
@@ -429,7 +429,7 @@
 qed
 
 lemma times_in_intervalE:
-  fixes xy :: "'a :: {linordered_semiring, real_normed_algebra, linear_continuum_topology}"
+  fixes xy :: "'a :: {linorder, real_normed_algebra, linear_continuum_topology}"
     \<comment> \<open>TODO: linear continuum topology is pretty strong\<close>
   assumes "xy \<in>\<^sub>i X * Y"
   obtains x y where "xy = x * y" "x \<in>\<^sub>i X" "y \<in>\<^sub>i Y"
@@ -446,7 +446,7 @@
   obtain x y where "xy = x * y" "x \<in>\<^sub>i X" "y \<in>\<^sub>i Y" by (auto simp: set_of_eq)
   then show ?thesis ..
 qed
-
+thm times_in_intervalE[of "1::real"]
 lemma set_of_times: "set_of (X * Y) = {x * y | x y. x \<in> set_of X \<and> y \<in> set_of Y}"
   for X Y::"'a :: {linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
   by (auto intro!: times_in_intervalI elim!: times_in_intervalE)
@@ -475,14 +475,14 @@
 instance proof qed
 end
 
-instance interval :: ("{one, preorder, linordered_semiring}") power
+instance interval :: ("{one, preorder, linorder, times}") power
 proof qed
 
 lemma set_of_one[simp]: "set_of (1::'a::{one, order} interval) = {1}"
   by (auto simp: set_of_eq)
 
 instance "interval" ::
-  ("{linordered_idom,linordered_ring, real_normed_algebra, linear_continuum_topology}") monoid_mult
+  ("{linordered_idom, real_normed_algebra, linear_continuum_topology}") monoid_mult
   apply standard
   unfolding interval_eq_set_of_iff set_of_times
   subgoal
@@ -670,7 +670,7 @@
   by (auto simp: set_of_eq lower_times upper_times algebra_simps mult_le_0_iff
       mult_bounds_enclose_zero1 mult_bounds_enclose_zero2)
 
-instance "interval" :: (linordered_semiring) mult_zero
+instance "interval" :: ("{linordered_semiring, zero, times}") mult_zero
   apply standard
   subgoal by transfer auto
   subgoal by transfer auto