# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1694283968 -3600
# Node ID 4da1e18a963302532de351d01a92ced4f98c47d7
# Parent  0d065af1a99ca1b598a653829571e53559dfa0a4
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light

diff -r 0d065af1a99c -r 4da1e18a9633 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Convex.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -1773,6 +1773,368 @@
   shows "cone (convex hull S)"
   by (metis (no_types, lifting) affine_hull_convex_hull affine_hull_eq_empty assms cone_iff convex_hull_scaling hull_inc)
 
+section \<open>Conic sets and conic hull\<close>
+
+definition conic :: "'a::real_vector set \<Rightarrow> bool"
+  where "conic S \<equiv> \<forall>x c. x \<in> S \<longrightarrow> 0 \<le> c \<longrightarrow> (c *\<^sub>R x) \<in> S"
+
+lemma conicD: "\<lbrakk>conic S; x \<in> S; 0 \<le> c\<rbrakk> \<Longrightarrow> (c *\<^sub>R x) \<in> S"
+  by (meson conic_def)
+
+lemma subspace_imp_conic: "subspace S \<Longrightarrow> conic S"
+  by (simp add: conic_def subspace_def)
+
+lemma conic_empty [simp]: "conic {}"
+  using conic_def by blast
+
+lemma conic_UNIV: "conic UNIV"
+  by (simp add: conic_def)
+
+lemma conic_Inter: "(\<And>S. S \<in> \<F> \<Longrightarrow> conic S) \<Longrightarrow> conic(\<Inter>\<F>)"
+  by (simp add: conic_def)
+
+lemma conic_linear_image:
+   "\<lbrakk>conic S; linear f\<rbrakk> \<Longrightarrow> conic(f ` S)"
+  by (smt (verit) conic_def image_iff linear.scaleR)
+
+lemma conic_linear_image_eq:
+   "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> conic (f ` S) \<longleftrightarrow> conic S"
+  by (smt (verit) conic_def conic_linear_image inj_image_mem_iff linear_cmul)
+
+lemma conic_mul: "\<lbrakk>conic S; x \<in> S; 0 \<le> c\<rbrakk> \<Longrightarrow> (c *\<^sub>R x) \<in> S"
+  using conic_def by blast
+
+lemma conic_conic_hull: "conic(conic hull S)"
+  by (metis (no_types, lifting) conic_Inter hull_def mem_Collect_eq)
+
+lemma conic_hull_eq: "(conic hull S = S) \<longleftrightarrow> conic S"
+  by (metis conic_conic_hull hull_same)
+
+lemma conic_hull_UNIV [simp]: "conic hull UNIV = UNIV"
+  by simp
+
+lemma conic_negations: "conic S \<Longrightarrow> conic (image uminus S)"
+  by (auto simp: conic_def image_iff)
+
+lemma conic_span [iff]: "conic(span S)"
+  by (simp add: subspace_imp_conic)
+
+lemma conic_hull_explicit:
+   "conic hull S = {c *\<^sub>R x| c x. 0 \<le> c \<and> x \<in> S}"
+  proof (rule hull_unique)
+    show "S \<subseteq> {c *\<^sub>R x |c x. 0 \<le> c \<and> x \<in> S}"
+      by (metis (no_types) cone_hull_expl hull_subset)
+  show "conic {c *\<^sub>R x |c x. 0 \<le> c \<and> x \<in> S}"
+    using mult_nonneg_nonneg by (force simp: conic_def)
+qed (auto simp: conic_def)
+
+lemma conic_hull_as_image:
+   "conic hull S = (\<lambda>z. fst z *\<^sub>R snd z) ` ({0..} \<times> S)"
+  by (force simp: conic_hull_explicit)
+
+lemma conic_hull_linear_image:
+   "linear f \<Longrightarrow> conic hull f ` S = f ` (conic hull S)"
+  by (force simp: conic_hull_explicit image_iff set_eq_iff linear_scale) 
+
+lemma conic_hull_image_scale:
+  assumes "\<And>x. x \<in> S \<Longrightarrow> 0 < c x"
+  shows   "conic hull (\<lambda>x. c x *\<^sub>R x) ` S = conic hull S"
+proof
+  show "conic hull (\<lambda>x. c x *\<^sub>R x) ` S \<subseteq> conic hull S"
+  proof (rule hull_minimal)
+    show "(\<lambda>x. c x *\<^sub>R x) ` S \<subseteq> conic hull S"
+      using assms conic_hull_explicit by fastforce
+  qed (simp add: conic_conic_hull)
+  show "conic hull S \<subseteq> conic hull (\<lambda>x. c x *\<^sub>R x) ` S"
+  proof (rule hull_minimal)
+    show "S \<subseteq> conic hull (\<lambda>x. c x *\<^sub>R x) ` S"
+    proof clarsimp
+      fix x
+      assume "x \<in> S"
+      then have "x = inverse(c x) *\<^sub>R c x *\<^sub>R x"
+        using assms by fastforce
+      then show "x \<in> conic hull (\<lambda>x. c x *\<^sub>R x) ` S"
+        by (smt (verit, best) \<open>x \<in> S\<close> assms conic_conic_hull conic_mul hull_inc image_eqI inverse_nonpositive_iff_nonpositive)
+    qed
+  qed (simp add: conic_conic_hull)
+qed
+
+lemma convex_conic_hull:
+  assumes "convex S"
+  shows "convex (conic hull S)"
+proof (clarsimp simp add: conic_hull_explicit convex_alt)
+  fix c x d y and u :: real
+  assume \<section>: "(0::real) \<le> c" "x \<in> S" "(0::real) \<le> d" "y \<in> S" "0 \<le> u" "u \<le> 1"
+  show "\<exists>c'' x''. ((1 - u) * c) *\<^sub>R x + (u * d) *\<^sub>R y = c'' *\<^sub>R x'' \<and> 0 \<le> c'' \<and> x'' \<in> S"
+  proof (cases "(1 - u) * c = 0")
+    case True
+    with \<open>0 \<le> d\<close> \<open>y \<in> S\<close>\<open>0 \<le> u\<close>  
+    show ?thesis by force
+  next
+    case False
+    define \<xi> where "\<xi> \<equiv> (1 - u) * c + u * d"
+    have *: "c * u \<le> c"
+      by (simp add: "\<section>" mult_left_le)
+    have "\<xi> > 0"
+      using False \<section> by (smt (verit, best) \<xi>_def split_mult_pos_le)
+    then have **: "c + d * u = \<xi> + c * u"
+      by (simp add: \<xi>_def mult.commute right_diff_distrib')
+    show ?thesis
+    proof (intro exI conjI)
+      show "0 \<le> \<xi>"
+        using \<open>0 < \<xi>\<close> by auto
+      show "((1 - u) * c) *\<^sub>R x + (u * d) *\<^sub>R y = \<xi> *\<^sub>R (((1 - u) * c / \<xi>) *\<^sub>R x + (u * d / \<xi>) *\<^sub>R y)"
+        using \<open>\<xi> > 0\<close> by (simp add: algebra_simps diff_divide_distrib)
+      show "((1 - u) * c / \<xi>) *\<^sub>R x + (u * d / \<xi>) *\<^sub>R y \<in> S"
+        using \<open>0 < \<xi>\<close> 
+        by (intro convexD [OF assms]) (auto simp: \<section> field_split_simps * **)
+    qed
+  qed
+qed
+
+lemma conic_halfspace_le: "conic {x. a \<bullet> x \<le> 0}"
+  by (auto simp: conic_def mult_le_0_iff)
+
+lemma conic_halfspace_ge: "conic {x. a \<bullet> x \<ge> 0}"
+  by (auto simp: conic_def mult_le_0_iff)
+
+lemma conic_hull_empty [simp]: "conic hull {} = {}"
+  by (simp add: conic_hull_eq)
+
+lemma conic_contains_0: "conic S \<Longrightarrow> (0 \<in> S \<longleftrightarrow> S \<noteq> {})"
+  by (simp add: Convex.cone_def cone_contains_0 conic_def)
+
+lemma conic_hull_eq_empty: "conic hull S = {} \<longleftrightarrow> (S = {})"
+  using conic_hull_explicit by fastforce
+
+lemma conic_sums: "\<lbrakk>conic S; conic T\<rbrakk> \<Longrightarrow> conic (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
+  by (simp add: conic_def) (metis scaleR_right_distrib)
+
+lemma conic_Times: "\<lbrakk>conic S; conic T\<rbrakk> \<Longrightarrow> conic(S \<times> T)"
+  by (auto simp: conic_def)
+
+lemma conic_Times_eq:
+   "conic(S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> conic S \<and> conic T" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (force simp: conic_def)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (force simp: conic_Times)
+qed
+
+lemma conic_hull_0 [simp]: "conic hull {0} = {0}"
+  by (simp add: conic_hull_eq subspace_imp_conic)
+
+lemma conic_hull_contains_0 [simp]: "0 \<in> conic hull S \<longleftrightarrow> (S \<noteq> {})"
+  by (simp add: conic_conic_hull conic_contains_0 conic_hull_eq_empty)
+
+lemma conic_hull_eq_sing:
+  "conic hull S = {x} \<longleftrightarrow> S = {0} \<and> x = 0"
+proof
+  show "conic hull S = {x} \<Longrightarrow> S = {0} \<and> x = 0"
+    by (metis conic_conic_hull conic_contains_0 conic_def conic_hull_eq hull_inc insert_not_empty singleton_iff)
+qed simp
+
+lemma conic_hull_Int_affine_hull:
+  assumes "T \<subseteq> S" "0 \<notin> affine hull S"
+  shows "(conic hull T) \<inter> (affine hull S) = T"
+proof -
+  have TaffS: "T \<subseteq> affine hull S"
+    using \<open>T \<subseteq> S\<close> hull_subset by fastforce
+  moreover
+  have "conic hull T \<inter> affine hull S \<subseteq> T"
+  proof (clarsimp simp: conic_hull_explicit)
+    fix c x
+    assume "c *\<^sub>R x \<in> affine hull S"
+      and "0 \<le> c"
+      and "x \<in> T"
+    show "c *\<^sub>R x \<in> T"
+    proof (cases "c=1")
+      case True
+      then show ?thesis
+        by (simp add: \<open>x \<in> T\<close>)
+    next
+      case False
+      then have "x /\<^sub>R (1 - c) = x + (c * inverse (1 - c)) *\<^sub>R x"
+        by (smt (verit, ccfv_SIG) diff_add_cancel mult.commute real_vector_affinity_eq scaleR_collapse scaleR_scaleR)
+      then have "0 = inverse(1 - c) *\<^sub>R c *\<^sub>R x + (1 - inverse(1 - c)) *\<^sub>R x"
+        by (simp add: algebra_simps)
+      then have "0 \<in> affine hull S"
+        by (smt (verit) \<open>c *\<^sub>R x \<in> affine hull S\<close> \<open>x \<in> T\<close> affine_affine_hull TaffS in_mono mem_affine)
+      then show ?thesis
+        using assms by auto        
+    qed
+  qed
+  ultimately show ?thesis
+    by (auto simp: hull_inc)
+qed
+
+
+section \<open>Convex cones and corresponding hulls\<close>
+
+definition convex_cone :: "'a::real_vector set \<Rightarrow> bool"
+  where "convex_cone \<equiv> \<lambda>S. S \<noteq> {} \<and> convex S \<and> conic S"
+
+lemma convex_cone_iff:
+   "convex_cone S \<longleftrightarrow>
+        0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>x \<in> S. \<forall>c\<ge>0. c *\<^sub>R x \<in> S)"
+    by (metis cone_def conic_contains_0 conic_def convex_cone convex_cone_def)
+
+lemma convex_cone_add: "\<lbrakk>convex_cone S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x+y \<in> S"
+  by (simp add: convex_cone_iff)
+
+lemma convex_cone_scaleR: "\<lbrakk>convex_cone S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> S"
+  by (simp add: convex_cone_iff)
+
+lemma convex_cone_nonempty: "convex_cone S \<Longrightarrow> S \<noteq> {}"
+  by (simp add: convex_cone_def)
+
+lemma convex_cone_linear_image:
+   "convex_cone S \<and> linear f \<Longrightarrow> convex_cone(f ` S)"
+  by (simp add: conic_linear_image convex_cone_def convex_linear_image)
+
+lemma convex_cone_linear_image_eq:
+   "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> (convex_cone(f ` S) \<longleftrightarrow> convex_cone S)"
+  by (simp add: conic_linear_image_eq convex_cone_def)
+
+lemma convex_cone_halfspace_ge: "convex_cone {x. a \<bullet> x \<ge> 0}"
+  by (simp add: convex_cone_iff inner_simps(2))
+
+lemma convex_cone_halfspace_le: "convex_cone {x. a \<bullet> x \<le> 0}"
+  by (simp add: convex_cone_iff inner_right_distrib mult_nonneg_nonpos)
+
+lemma convex_cone_contains_0: "convex_cone S \<Longrightarrow> 0 \<in> S"
+  using convex_cone_iff by blast
+
+lemma convex_cone_Inter:
+   "(\<And>S. S \<in> f \<Longrightarrow> convex_cone S) \<Longrightarrow> convex_cone(\<Inter> f)"
+  by (simp add: convex_cone_iff)
+
+lemma convex_cone_convex_cone_hull: "convex_cone(convex_cone hull S)"
+  by (metis (no_types, lifting) convex_cone_Inter hull_def mem_Collect_eq)
+
+lemma convex_convex_cone_hull: "convex(convex_cone hull S)"
+  by (meson convex_cone_convex_cone_hull convex_cone_def)
+
+lemma conic_convex_cone_hull: "conic(convex_cone hull S)"
+  by (metis convex_cone_convex_cone_hull convex_cone_def)
+
+lemma convex_cone_hull_nonempty: "convex_cone hull S \<noteq> {}"
+  by (simp add: convex_cone_convex_cone_hull convex_cone_nonempty)
+
+lemma convex_cone_hull_contains_0: "0 \<in> convex_cone hull S"
+  by (simp add: convex_cone_contains_0 convex_cone_convex_cone_hull)
+
+lemma convex_cone_hull_add:
+   "\<lbrakk>x \<in> convex_cone hull S; y \<in> convex_cone hull S\<rbrakk> \<Longrightarrow> x + y \<in> convex_cone hull S"
+  by (simp add: convex_cone_add convex_cone_convex_cone_hull)
+
+lemma convex_cone_hull_mul:
+   "\<lbrakk>x \<in> convex_cone hull S; 0 \<le> c\<rbrakk> \<Longrightarrow> (c *\<^sub>R x) \<in> convex_cone hull S"
+  by (simp add: conic_convex_cone_hull conic_mul)
+
+thm convex_sums
+lemma convex_cone_sums:
+   "\<lbrakk>convex_cone S; convex_cone T\<rbrakk> \<Longrightarrow> convex_cone (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
+  by (simp add: convex_cone_def conic_sums convex_sums)
+
+lemma convex_cone_Times:
+   "\<lbrakk>convex_cone S; convex_cone T\<rbrakk> \<Longrightarrow> convex_cone(S \<times> T)"
+  by (simp add: conic_Times convex_Times convex_cone_def)
+
+lemma convex_cone_Times_D1: "convex_cone (S \<times> T) \<Longrightarrow> convex_cone S"
+  by (metis Times_empty conic_Times_eq convex_cone_def convex_convex_hull convex_hull_Times hull_same times_eq_iff)
+
+lemma convex_cone_Times_eq:
+   "convex_cone(S \<times> T) \<longleftrightarrow> convex_cone S \<and> convex_cone T" 
+proof (cases "S={} \<or> T={}")
+  case True
+  then show ?thesis 
+    by (auto dest: convex_cone_nonempty)
+next
+  case False
+  then have "convex_cone (S \<times> T) \<Longrightarrow> convex_cone T"
+    by (metis conic_Times_eq convex_cone_def convex_convex_hull convex_hull_Times hull_same times_eq_iff)
+  then show ?thesis
+    using convex_cone_Times convex_cone_Times_D1 by blast 
+qed
+
+
+lemma convex_cone_hull_Un:
+  "convex_cone hull(S \<union> T) = (\<Union>x \<in> convex_cone hull S. \<Union>y \<in> convex_cone hull T. {x + y})"
+  (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+  proof (rule hull_minimal)
+    show "S \<union> T \<subseteq> (\<Union>x\<in>convex_cone hull S. \<Union>y\<in>convex_cone hull T. {x + y})"
+      apply (clarsimp simp: subset_iff)
+      by (metis add_0 convex_cone_hull_contains_0 group_cancel.rule0 hull_inc)
+    show "convex_cone (\<Union>x\<in>convex_cone hull S. \<Union>y\<in>convex_cone hull T. {x + y})"
+      by (simp add: convex_cone_convex_cone_hull convex_cone_sums)
+  qed
+next
+  show "?rhs \<subseteq> ?lhs"
+    by clarify (metis convex_cone_hull_add hull_mono le_sup_iff subsetD subsetI)
+qed
+
+lemma convex_cone_singleton [iff]: "convex_cone {0}"
+  by (simp add: convex_cone_iff)
+
+lemma convex_hull_subset_convex_cone_hull:
+   "convex hull S \<subseteq> convex_cone hull S"
+  by (simp add: convex_convex_cone_hull hull_minimal hull_subset)
+
+lemma conic_hull_subset_convex_cone_hull:
+   "conic hull S \<subseteq> convex_cone hull S"
+  by (simp add: conic_convex_cone_hull hull_minimal hull_subset)
+
+lemma subspace_imp_convex_cone: "subspace S \<Longrightarrow> convex_cone S"
+  by (simp add: convex_cone_iff subspace_def)
+
+lemma convex_cone_span: "convex_cone(span S)"
+  by (simp add: subspace_imp_convex_cone)
+
+lemma convex_cone_negations:
+   "convex_cone S \<Longrightarrow> convex_cone (image uminus S)"
+  by (simp add: convex_cone_linear_image module_hom_uminus)
+
+lemma subspace_convex_cone_symmetric:
+   "subspace S \<longleftrightarrow> convex_cone S \<and> (\<forall>x \<in> S. -x \<in> S)"
+  by (smt (verit) convex_cone_iff scaleR_left.minus subspace_def subspace_neg)
+
+lemma convex_cone_hull_separate_nonempty:
+  assumes "S \<noteq> {}"
+  shows "convex_cone hull S = conic hull (convex hull S)"   (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    by (metis assms conic_conic_hull convex_cone_def convex_conic_hull convex_convex_hull hull_subset subset_empty subset_hull)
+  show "?rhs \<subseteq> ?lhs"
+    by (simp add: conic_convex_cone_hull convex_hull_subset_convex_cone_hull subset_hull)
+qed
+
+lemma convex_cone_hull_empty [simp]: "convex_cone hull {} = {0}"
+  by (metis convex_cone_hull_contains_0 convex_cone_singleton hull_redundant hull_same)
+
+lemma convex_cone_hull_separate:
+   "convex_cone hull S = insert 0 (conic hull (convex hull S))"
+proof(cases "S={}")
+  case False
+  then show ?thesis
+    using convex_cone_hull_contains_0 convex_cone_hull_separate_nonempty by blast
+qed auto
+
+lemma convex_cone_hull_convex_hull_nonempty:
+   "S \<noteq> {} \<Longrightarrow> convex_cone hull S = (\<Union>x \<in> convex hull S. \<Union>c\<in>{0..}. {c *\<^sub>R x})"
+  by (force simp: convex_cone_hull_separate_nonempty conic_hull_as_image)
+
+lemma convex_cone_hull_convex_hull:
+   "convex_cone hull S = insert 0 (\<Union>x \<in> convex hull S. \<Union>c\<in>{0..}. {c *\<^sub>R x})"
+  by (force simp: convex_cone_hull_separate conic_hull_as_image)
+
+lemma convex_cone_hull_linear_image:
+   "linear f \<Longrightarrow> convex_cone hull (f ` S) = image f (convex_cone hull S)"
+  by (metis (no_types, lifting) conic_hull_linear_image convex_cone_hull_separate convex_hull_linear_image image_insert linear_0)
+
 subsection \<open>Radon's theorem\<close>
 
 text "Formalized by Lars Schewe."
diff -r 0d065af1a99c -r 4da1e18a9633 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -1092,11 +1092,6 @@
   shows   "lebesgue = density (distr lebesgue lebesgue (\<lambda>x. c * x)) (\<lambda>x. ennreal \<bar>c\<bar>)"
   using assms by (subst lebesgue_affine_euclidean[of "\<lambda>_. c" 0]) simp_all
 
-lemma divideR_right:
-  fixes x y :: "'a::real_normed_vector"
-  shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
-  using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp
-
 lemma lborel_has_bochner_integral_real_affine_iff:
   fixes x :: "'a :: {banach, second_countable_topology}"
   shows "c \<noteq> 0 \<Longrightarrow>
diff -r 0d065af1a99c -r 4da1e18a9633 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -704,7 +704,7 @@
 
 text \<open>Low-dimensional subset is in a hyperplane (weak orthogonal complement).\<close>
 
-lemma span_not_univ_orthogonal:
+lemma span_not_UNIV_orthogonal:
   fixes S :: "'a::euclidean_space set"
   assumes sU: "span S \<noteq> UNIV"
   shows "\<exists>a::'a. a \<noteq> 0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
@@ -754,7 +754,7 @@
   fixes S :: "'a::euclidean_space set"
   assumes SU: "span S \<noteq> UNIV"
   shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
-  using span_not_univ_orthogonal[OF SU] by auto
+  using span_not_UNIV_orthogonal[OF SU] by auto
 
 lemma lowdim_subset_hyperplane:
   fixes S :: "'a::euclidean_space set"
diff -r 0d065af1a99c -r 4da1e18a9633 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -28,8 +28,12 @@
 
 lemma face_of_linear_image:
   assumes "linear f" "inj f"
-    shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
-by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
+  shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
+  by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
+
+lemma faces_of_linear_image:
+   "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> {T. T face_of (f ` S)} = (image f) ` {T. T face_of S}"
+  by (smt (verit) Collect_cong face_of_def face_of_linear_image setcompr_eq_image subset_imageE)
 
 lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
   by (auto simp: face_of_def)
@@ -269,6 +273,39 @@
     using \<open>affine S\<close> xy by (auto simp: affine_alt)
 qed
 
+proposition face_of_conic:
+  assumes "conic S" "f face_of S"
+  shows "conic f"
+  unfolding conic_def
+proof (intro strip)
+  fix x and c::real
+  assume "x \<in> f" and "0 \<le> c"
+  have f: "\<And>a b x. \<lbrakk>a \<in> S; b \<in> S; x \<in> f; x \<in> open_segment a b\<rbrakk> \<Longrightarrow> a \<in> f \<and> b \<in> f"
+    using \<open>f face_of S\<close> face_ofD by blast
+  show "c *\<^sub>R x \<in> f"
+  proof (cases "x=0 \<or> c=1")
+    case True
+    then show ?thesis
+      using \<open>x \<in> f\<close> by auto
+  next
+    case False
+    with \<open>0 \<le> c\<close> obtain d e where de: "0 \<le> d" "0 \<le> e" "d < 1" "1 < e" "d < e" "(d = c \<or> e = c)"
+      apply (simp add: neq_iff)
+      by (metis gt_ex less_eq_real_def order_less_le_trans zero_less_one)
+    then obtain [simp]: "c *\<^sub>R x \<in> S" "e *\<^sub>R x \<in> S" \<open>x \<in> S\<close>
+      using \<open>x \<in> f\<close> assms conic_mul face_of_imp_subset by blast
+    have "x \<in> open_segment (d *\<^sub>R x) (e *\<^sub>R x)" if "c *\<^sub>R x \<notin> f"
+      using de False that
+      apply (simp add: in_segment)
+      apply (rule_tac x="(1 - d) / (e - d)" in exI)
+      apply (simp add: field_simps)
+      by (smt (verit, del_insts) add_divide_distrib divide_self scaleR_collapse)
+    then show ?thesis
+      using \<open>conic S\<close> f [of "d *\<^sub>R x" "e *\<^sub>R x" x] de \<open>x \<in> f\<close>
+      by (force simp: conic_def in_segment)
+  qed
+qed
+
 proposition face_of_convex_hulls:
       assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
       shows  "(convex hull T) face_of (convex hull S)"
@@ -927,6 +964,18 @@
    by (auto simp: face_of_singleton hull_same)
 qed (use assms  in \<open>simp add: hull_inc\<close>)
 
+lemma extreme_point_of_conic:
+  assumes "conic S" and x: "x extreme_point_of S"
+  shows "x = 0"
+proof -
+  have "{x} face_of S"
+    by (simp add: face_of_singleton x)
+  then have "conic{x}"
+    using assms(1) face_of_conic by blast
+  then show ?thesis
+    by (force simp: conic_def)
+qed
+
 subsection\<open>Facets\<close>
 
 definition\<^marker>\<open>tag important\<close> facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
@@ -3826,5 +3875,135 @@
       using that by (auto simp: in\<T>)
   qed
 qed
+section \<open>Finitely generated cone is polyhedral, and hence closed\<close>
+
+proposition polyhedron_convex_cone_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "finite S"
+  shows "polyhedron(convex_cone hull S)"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    by (simp add: affine_imp_polyhedron)
+next
+  case False
+  then have "polyhedron(convex hull (insert 0 S))"
+    by (simp add: assms polyhedron_convex_hull)
+  then obtain F a b where "finite F" 
+         and F: "convex hull (insert 0 S) = \<Inter> F" 
+         and ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
+    unfolding polyhedron_def by metis
+  then have "F \<noteq> {}"
+    by (metis bounded_convex_hull finite_imp_bounded Inf_empty assms finite_insert not_bounded_UNIV)
+  show ?thesis
+    unfolding polyhedron_def
+  proof (intro exI conjI)
+    show "convex_cone hull S = \<Inter> {h \<in> F. b h = 0}" (is "?lhs = ?rhs")
+    proof
+      show "?lhs \<subseteq> ?rhs"
+      proof (rule hull_minimal)
+        show "S \<subseteq> \<Inter> {h \<in> F. b h = 0}"
+          by (smt (verit, best) F InterE InterI hull_subset insert_subset mem_Collect_eq subset_eq)
+        have "\<And>S. \<lbrakk>S \<in> F; b S = 0\<rbrakk> \<Longrightarrow> convex_cone S"
+          by (metis ab convex_cone_halfspace_le)
+        then show "convex_cone (\<Inter> {h \<in> F. b h = 0})"
+          by (force intro: convex_cone_Inter)
+      qed
+      have "x \<in> convex_cone hull S"
+        if x: "\<And>h. \<lbrakk>h \<in> F; b h = 0\<rbrakk> \<Longrightarrow> x \<in> h" for x
+      proof -
+        have "\<exists>t. 0 < t \<and> (t *\<^sub>R x) \<in> h" if "h \<in> F" for h
+        proof (cases "b h = 0")
+          case True
+          then show ?thesis
+            by (metis x linordered_field_no_ub mult_1 scaleR_one that zero_less_mult_iff)
+        next
+          case False
+          then have "b h > 0"
+            by (smt (verit, del_insts) F InterE ab hull_subset inner_zero_right insert_subset mem_Collect_eq that)
+          then have "0 \<in> interior {x. a h \<bullet> x \<le> b h}"
+            by (simp add: ab that)
+          then have "0 \<in> interior h"
+            using ab that by auto
+          then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball 0 \<epsilon> \<subseteq> h"
+            using mem_interior by blast
+          show ?thesis
+          proof (cases "x=0")
+            case True
+            then show ?thesis
+              using \<epsilon> \<open>0 < \<epsilon>\<close> by auto
+          next
+            case False
+            with \<epsilon> \<open>0 < \<epsilon>\<close> show ?thesis
+              by (rule_tac x="\<epsilon> / (2 * norm x)" in exI) (auto simp: divide_simps)
+          qed
+        qed
+        then obtain t where t: "\<And>h. h \<in> F \<Longrightarrow> 0 < t h \<and> (t h *\<^sub>R x) \<in> h" 
+          by metis
+        then have "Inf (t ` F) *\<^sub>R x /\<^sub>R Inf (t ` F) = x"
+          by (smt (verit) \<open>F \<noteq> {}\<close> \<open>finite F\<close> divideR_right finite_imageI finite_less_Inf_iff image_iff image_is_empty)
+        moreover have "Inf (t ` F) *\<^sub>R x /\<^sub>R Inf (t ` F) \<in> convex_cone hull S"
+        proof (rule conicD [OF conic_convex_cone_hull])
+          have "Inf (t ` F) *\<^sub>R x \<in> \<Inter> F"
+          proof clarify
+            fix h
+            assume  "h \<in> F"
+            have eq: "Inf (t ` F) *\<^sub>R x = (1 - Inf(t ` F) / t h) *\<^sub>R 0 + (Inf(t ` F) / t h) *\<^sub>R t h *\<^sub>R x"
+              using \<open>h \<in> F\<close> t by force
+            show "Inf (t ` F) *\<^sub>R x \<in> h"
+              unfolding eq
+            proof (rule convexD_alt)
+              have "h = {x. a h \<bullet> x \<le> b h}"
+                by (simp add: \<open>h \<in> F\<close> ab)
+              then show "convex h"
+                by (metis convex_halfspace_le)
+              show "0 \<in> h"
+                by (metis F InterE \<open>h \<in> F\<close> hull_subset insertCI subsetD)
+              show "t h *\<^sub>R x \<in> h"
+                by (simp add: \<open>h \<in> F\<close> t)
+              show "0 \<le> Inf (t ` F) / t h"
+                by (metis \<open>F \<noteq> {}\<close> \<open>h \<in> F\<close> cINF_greatest divide_nonneg_pos less_eq_real_def t)
+              show "Inf (t ` F) / t h \<le> 1"
+                by (simp add: \<open>finite F\<close> \<open>h \<in> F\<close> cInf_le_finite t)
+            qed
+          qed
+          moreover have "convex hull (insert 0 S) \<subseteq> convex_cone hull S"
+            by (simp add: convex_cone_hull_contains_0 convex_convex_cone_hull hull_minimal hull_subset)
+          ultimately show "Inf (t ` F) *\<^sub>R x \<in> convex_cone hull S"
+            using F by blast
+          show "0 \<le> inverse (Inf (t ` F))"
+            using t by (simp add: \<open>F \<noteq> {}\<close> \<open>finite F\<close> finite_less_Inf_iff less_eq_real_def)
+        qed
+        ultimately show ?thesis
+          by auto
+      qed
+      then show "?rhs \<subseteq> ?lhs"
+        by auto
+    qed
+    show "\<forall>h\<in>{h \<in> F. b h = 0}. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
+      using ab by blast
+  qed (auto simp: \<open>finite F\<close>)
+qed
+
+
+lemma closed_convex_cone_hull:
+  fixes S :: "'a::euclidean_space set"
+  shows "finite S \<Longrightarrow> closed(convex_cone hull S)"
+  by (simp add: polyhedron_convex_cone_hull polyhedron_imp_closed)
+
+lemma polyhedron_convex_cone_hull_polytope:
+  fixes S :: "'a::euclidean_space set"
+  shows "polytope S \<Longrightarrow> polyhedron(convex_cone hull S)"
+  by (metis convex_cone_hull_separate hull_hull polyhedron_convex_cone_hull polytope_def)
+
+lemma polyhedron_conic_hull_polytope:
+  fixes S :: "'a::euclidean_space set"
+  shows "polytope S \<Longrightarrow> polyhedron(conic hull S)"
+  by (metis conic_hull_eq_empty convex_cone_hull_separate_nonempty hull_hull polyhedron_convex_cone_hull_polytope polyhedron_empty polytope_def)
+
+lemma closed_conic_hull_strong:
+  fixes S :: "'a::euclidean_space set"
+  shows "0 \<in> rel_interior S \<or> polytope S \<or> compact S \<and> ~(0 \<in> S) \<Longrightarrow> closed(conic hull S)"
+  using closed_conic_hull polyhedron_conic_hull_polytope polyhedron_imp_closed by blast
 
 end
diff -r 0d065af1a99c -r 4da1e18a9633 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -214,6 +214,84 @@
     by (simp add: closure_mono interior_subset subset_antisym)
 qed
 
+lemma openin_subset_relative_interior:
+  fixes S :: "'a::euclidean_space set"
+  shows "openin (top_of_set (affine hull T)) S \<Longrightarrow> (S \<subseteq> rel_interior T) = (S \<subseteq> T)"
+  by (meson order.trans rel_interior_maximal rel_interior_subset)
+
+lemma conic_hull_eq_span_affine_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "0 \<in> rel_interior S"
+  shows "conic hull S = span S \<and> conic hull S = affine hull S"
+proof -
+  obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<inter> affine hull S \<subseteq> S"
+    using assms mem_rel_interior_cball by blast
+  have *: "affine hull S = span S"
+    by (meson affine_hull_span_0 assms hull_inc mem_rel_interior_cball)
+  moreover
+  have "conic hull S \<subseteq> span S"
+    by (simp add: hull_minimal span_superset)
+  moreover
+  have "affine hull S \<subseteq> conic hull S"
+  proof clarsimp
+    fix x
+    assume "x \<in> affine hull S"
+    show "x \<in> conic hull S"
+    proof (cases "x=0")
+      case True
+      then show ?thesis
+        using \<open>x \<in> affine hull S\<close> by auto
+    next
+      case False
+      then have "(\<epsilon> / norm x) *\<^sub>R x \<in> cball 0 \<epsilon> \<inter> affine hull S"
+        using \<open>0 < \<epsilon>\<close> \<open>x \<in> affine hull S\<close> * span_mul by fastforce
+      then have "(\<epsilon> / norm x) *\<^sub>R x \<in> S"
+        by (meson \<epsilon> subsetD)
+      then have "\<exists>c xa. x = c *\<^sub>R xa \<and> 0 \<le> c \<and> xa \<in> S"
+        by (smt (verit, del_insts) \<open>0 < \<epsilon>\<close> divide_nonneg_nonneg eq_vector_fraction_iff norm_eq_zero norm_ge_zero)
+      then show ?thesis
+        by (simp add: conic_hull_explicit)
+    qed
+  qed
+  ultimately show ?thesis
+    by blast
+qed
+
+lemma conic_hull_eq_span:
+  fixes S :: "'a::euclidean_space set"
+  assumes "0 \<in> rel_interior S"
+  shows "conic hull S = span S"
+  by (simp add: assms conic_hull_eq_span_affine_hull)
+
+lemma conic_hull_eq_affine_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "0 \<in> rel_interior S"
+  shows "conic hull S = affine hull S"
+  using assms conic_hull_eq_span_affine_hull by blast
+
+lemma conic_hull_eq_span_eq:
+  fixes S :: "'a::euclidean_space set"
+  shows "0 \<in> rel_interior(conic hull S) \<longleftrightarrow> conic hull S = span S" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (metis conic_hull_eq_span conic_span hull_hull hull_minimal hull_subset span_eq)
+  show "?rhs \<Longrightarrow> ?lhs"
+  by (metis rel_interior_affine subspace_affine subspace_span)
+qed
+
+lemma aff_dim_psubset:
+   "(affine hull S) \<subset> (affine hull T) \<Longrightarrow> aff_dim S < aff_dim T"
+  by (metis aff_dim_affine_hull aff_dim_empty aff_dim_subset affine_affine_hull affine_dim_equal order_less_le)
+
+lemma aff_dim_eq_full_gen:
+   "S \<subseteq> T \<Longrightarrow> (aff_dim S = aff_dim T \<longleftrightarrow> affine hull S = affine hull T)"
+  by (smt (verit, del_insts) aff_dim_affine_hull2 aff_dim_psubset hull_mono psubsetI)
+
+lemma aff_dim_eq_full:
+  fixes S :: "'n::euclidean_space set"
+  shows "aff_dim S = (DIM('n)) \<longleftrightarrow> affine hull S = UNIV"
+  by (metis aff_dim_UNIV aff_dim_affine_hull affine_hull_UNIV)
+
 lemma closure_convex_Int_superset:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "interior S \<noteq> {}" "interior S \<subseteq> closure T"
@@ -772,6 +850,61 @@
   qed auto
 qed
 
+lemma empty_interior_subset_hyperplane_aux:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" "0 \<in> S" and empty_int: "interior S = {}"
+  shows "\<exists>a b. a\<noteq>0 \<and> S \<subseteq> {x. a \<bullet> x = b}"
+proof -
+  have False if "\<And>a. a = 0 \<or> (\<forall>b. \<exists>T \<in> S. a \<bullet> T \<noteq> b)"
+  proof -
+    have rel_int: "rel_interior S \<noteq> {}"
+      using assms rel_interior_eq_empty by auto
+    moreover 
+    have "dim S \<noteq> dim (UNIV::'a set)"
+      by (metis aff_dim_zero affine_hull_UNIV \<open>0 \<in> S\<close> dim_UNIV empty_int hull_inc rel_int rel_interior_interior)
+    then obtain a where "a \<noteq> 0" and a: "span S \<subseteq> {x. a \<bullet> x = 0}"
+      using lowdim_subset_hyperplane
+      by (metis dim_UNIV dim_subset_UNIV order_less_le)
+    have "span UNIV = span S"
+      by (metis span_base span_not_UNIV_orthogonal that)
+    then have "UNIV \<subseteq> affine hull S"
+      by (simp add: \<open>0 \<in> S\<close> hull_inc affine_hull_span_0)
+    ultimately show False
+      using \<open>rel_interior S \<noteq> {}\<close> empty_int rel_interior_interior by blast
+  qed
+  then show ?thesis
+    by blast
+qed
+
+lemma empty_interior_subset_hyperplane:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" and int: "interior S = {}"
+  obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x = b}"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    using that by blast
+next
+  case False
+  then obtain u where "u \<in> S"
+    by blast
+  have "\<exists>a b. a \<noteq> 0 \<and> (\<lambda>x. x - u) ` S \<subseteq> {x. a \<bullet> x = b}"
+  proof (rule empty_interior_subset_hyperplane_aux)
+    show "convex ((\<lambda>x. x - u) ` S)"
+      using \<open>convex S\<close> by force
+    show "0 \<in> (\<lambda>x. x - u) ` S"
+      by (simp add: \<open>u \<in> S\<close>)
+    show "interior ((\<lambda>x. x - u) ` S) = {}"
+      by (simp add: int interior_translation_subtract)
+  qed
+  then obtain a b where "a \<noteq> 0" and ab: "(\<lambda>x. x - u) ` S \<subseteq> {x. a \<bullet> x = b}"
+    by metis
+  then have "S \<subseteq> {x. a \<bullet> x = b + (a \<bullet> u)}"
+    using ab by (auto simp: algebra_simps)
+  then show ?thesis
+    using \<open>a \<noteq> 0\<close> that by auto
+qed
+
 lemma rel_interior_same_affine_hull:
   fixes S :: "'n::euclidean_space set"
   assumes "convex S"
@@ -1327,118 +1460,119 @@
   then show ?thesis by auto
 qed
 
-lemma convex_closure_rel_interior_inter:
-  assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
-    and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-  shows "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
+lemma convex_closure_rel_interior_Int:
+  assumes "\<And>S. S\<in>\<F> \<Longrightarrow> convex (S :: 'n::euclidean_space set)"
+    and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+  shows "\<Inter>(closure ` \<F>) \<subseteq> closure (\<Inter>(rel_interior ` \<F>))"
 proof -
-  obtain x where x: "\<forall>S\<in>I. x \<in> rel_interior S"
+  obtain x where x: "\<forall>S\<in>\<F>. x \<in> rel_interior S"
     using assms by auto
-  {
+  show ?thesis
+  proof
     fix y
-    assume "y \<in> \<Inter>{closure S |S. S \<in> I}"
-    then have y: "\<forall>S \<in> I. y \<in> closure S"
-      by auto
-    {
-      assume "y = x"
-      then have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})"
-        using x closure_subset[of "\<Inter>{rel_interior S |S. S \<in> I}"] by auto
-    }
-    moreover
-    {
-      assume "y \<noteq> x"
-      { fix e :: real
-        assume e: "e > 0"
-        define e1 where "e1 = min 1 (e/norm (y - x))"
-        then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (y - x) \<le> e"
-          using \<open>y \<noteq> x\<close> \<open>e > 0\<close> le_divide_eq[of e1 e "norm (y - x)"]
+    assume y: "y \<in> \<Inter> (closure ` \<F>)"
+    show "y \<in> closure (\<Inter>(rel_interior ` \<F>))"
+    proof (cases "y=x")
+      case True
+      with closure_subset x show ?thesis 
+        by fastforce
+    next
+      case False
+      show ?thesis
+      proof (clarsimp simp: closure_approachable_le)
+        fix \<epsilon> :: real
+        assume e: "\<epsilon> > 0"
+        define e1 where "e1 = min 1 (\<epsilon>/norm (y - x))"
+        then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (y - x) \<le> \<epsilon>"
+          using \<open>y \<noteq> x\<close> \<open>\<epsilon> > 0\<close> le_divide_eq[of e1 \<epsilon> "norm (y - x)"]
           by simp_all
         define z where "z = y - e1 *\<^sub>R (y - x)"
         {
           fix S
-          assume "S \<in> I"
+          assume "S \<in> \<F>"
           then have "z \<in> rel_interior S"
             using rel_interior_closure_convex_shrink[of S x y e1] assms x y e1 z_def
             by auto
         }
-        then have *: "z \<in> \<Inter>{rel_interior S |S. S \<in> I}"
+        then have *: "z \<in> \<Inter>(rel_interior ` \<F>)"
           by auto
-        have "\<exists>z. z \<in> \<Inter>{rel_interior S |S. S \<in> I} \<and> z \<noteq> y \<and> dist z y \<le> e"
+        show "\<exists>x\<in>\<Inter> (rel_interior ` \<F>). dist x y \<le> \<epsilon>"
           using \<open>y \<noteq> x\<close> z_def * e1 e dist_norm[of z y]
-          by (rule_tac x="z" in exI) auto
-      }
-      then have "y islimpt \<Inter>{rel_interior S |S. S \<in> I}"
-        unfolding islimpt_approachable_le by blast
-      then have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})"
-        unfolding closure_def by auto
-    }
-    ultimately have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})"
-      by auto
-  }
-  then show ?thesis by auto
-qed
-
-lemma convex_closure_inter:
-  assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
-    and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-  shows "closure (\<Inter>I) = \<Inter>{closure S |S. S \<in> I}"
+          by force
+      qed
+    qed
+  qed
+qed
+
+
+lemma closure_Inter_convex:
+  fixes \<F> :: "'n::euclidean_space set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S" and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+  shows "closure(\<Inter>\<F>) = \<Inter>(closure ` \<F>)"
 proof -
-  have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
-    using convex_closure_rel_interior_inter assms by auto
+  have "\<Inter>(closure ` \<F>) \<le> closure (\<Inter>(rel_interior ` \<F>))"
+    by (meson assms convex_closure_rel_interior_Int)
   moreover
-  have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
-    using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
+  have "closure (\<Inter>(rel_interior ` \<F>)) \<subseteq> closure (\<Inter>\<F>)"
+    using rel_interior_inter_aux closure_mono[of "\<Inter>(rel_interior ` \<F>)" "\<Inter>\<F>"]
     by auto
   ultimately show ?thesis
-    using closure_Int[of I] by auto
-qed
-
-lemma convex_inter_rel_interior_same_closure:
-  assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
-    and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-  shows "closure (\<Inter>{rel_interior S |S. S \<in> I}) = closure (\<Inter>I)"
+    using closure_Int[of \<F>] by blast
+qed
+
+lemma closure_Inter_convex_open:
+    "(\<And>S::'n::euclidean_space set. S \<in> \<F> \<Longrightarrow> convex S \<and> open S)
+        \<Longrightarrow> closure(\<Inter>\<F>) = (if \<Inter>\<F> = {} then {} else \<Inter>(closure ` \<F>))"
+  by (simp add: closure_Inter_convex rel_interior_open)
+
+lemma convex_Inter_rel_interior_same_closure:
+  fixes \<F> :: "'n::euclidean_space set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S"
+    and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+  shows "closure (\<Inter>(rel_interior ` \<F>)) = closure (\<Inter>\<F>)"
 proof -
-  have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
-    using convex_closure_rel_interior_inter assms by auto
+  have "\<Inter>(closure ` \<F>) \<subseteq> closure (\<Inter>(rel_interior ` \<F>))"
+    by (meson assms convex_closure_rel_interior_Int)
   moreover
-  have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
-    using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
-    by auto
+  have "closure (\<Inter>(rel_interior ` \<F>)) \<subseteq> closure (\<Inter>\<F>)"
+    by (metis Setcompr_eq_image closure_mono rel_interior_inter_aux)
   ultimately show ?thesis
-    using closure_Int[of I] by auto
-qed
-
-lemma convex_rel_interior_inter:
-  assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
-    and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-  shows "rel_interior (\<Inter>I) \<subseteq> \<Inter>{rel_interior S |S. S \<in> I}"
+    by (simp add: assms closure_Inter_convex)
+qed
+
+lemma convex_rel_interior_Inter:
+  fixes \<F> :: "'n::euclidean_space set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S"
+    and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+  shows "rel_interior (\<Inter>\<F>) \<subseteq> \<Inter>(rel_interior ` \<F>)"
 proof -
-  have "convex (\<Inter>I)"
+  have "convex (\<Inter>\<F>)"
     using assms convex_Inter by auto
   moreover
-  have "convex (\<Inter>{rel_interior S |S. S \<in> I})"
-    using assms convex_rel_interior by (force intro: convex_Inter)
+  have "convex (\<Inter>(rel_interior ` \<F>))"
+    using assms by (metis convex_rel_interior convex_INT)
   ultimately
-  have "rel_interior (\<Inter>{rel_interior S |S. S \<in> I}) = rel_interior (\<Inter>I)"
-    using convex_inter_rel_interior_same_closure assms
-      closure_eq_rel_interior_eq[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
+  have "rel_interior (\<Inter>(rel_interior ` \<F>)) = rel_interior (\<Inter>\<F>)"
+    using convex_Inter_rel_interior_same_closure assms
+      closure_eq_rel_interior_eq[of "\<Inter>(rel_interior ` \<F>)" "\<Inter>\<F>"]
     by blast
   then show ?thesis
-    using rel_interior_subset[of "\<Inter>{rel_interior S |S. S \<in> I}"] by auto
-qed
-
-lemma convex_rel_interior_finite_inter:
-  assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
-    and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-    and "finite I"
-  shows "rel_interior (\<Inter>I) = \<Inter>{rel_interior S |S. S \<in> I}"
+    using rel_interior_subset[of "\<Inter>(rel_interior ` \<F>)"] by auto
+qed
+
+lemma convex_rel_interior_finite_Inter:
+  fixes \<F> :: "'n::euclidean_space set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S"
+    and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+    and "finite \<F>"
+  shows "rel_interior (\<Inter>\<F>) = \<Inter>(rel_interior ` \<F>)"
 proof -
-  have "\<Inter>I \<noteq> {}"
-    using assms rel_interior_inter_aux[of I] by auto
-  have "convex (\<Inter>I)"
+  have "\<Inter>\<F> \<noteq> {}"
+    using assms rel_interior_inter_aux[of \<F>] by auto
+  have "convex (\<Inter>\<F>)"
     using convex_Inter assms by auto
   show ?thesis
-  proof (cases "I = {}")
+  proof (cases "\<F> = {}")
     case True
     then show ?thesis
       using Inter_empty rel_interior_UNIV by auto
@@ -1446,43 +1580,43 @@
     case False
     {
       fix z
-      assume z: "z \<in> \<Inter>{rel_interior S |S. S \<in> I}"
+      assume z: "z \<in> \<Inter>(rel_interior ` \<F>)"
       {
         fix x
-        assume x: "x \<in> \<Inter>I"
+        assume x: "x \<in> \<Inter>\<F>"
         {
           fix S
-          assume S: "S \<in> I"
+          assume S: "S \<in> \<F>"
           then have "z \<in> rel_interior S" "x \<in> S"
             using z x by auto
           then have "\<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e)*\<^sub>R x + e *\<^sub>R z \<in> S)"
             using convex_rel_interior_if[of S z] S assms hull_subset[of S] by auto
         }
         then obtain mS where
-          mS: "\<forall>S\<in>I. mS S > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> mS S \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)" by metis
-        define e where "e = Min (mS ` I)"
-        then have "e \<in> mS ` I" using assms \<open>I \<noteq> {}\<close> by simp
+          mS: "\<forall>S\<in>\<F>. mS S > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> mS S \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)" by metis
+        define e where "e = Min (mS ` \<F>)"
+        then have "e \<in> mS ` \<F>" using assms \<open>\<F> \<noteq> {}\<close> by simp
         then have "e > 1" using mS by auto
-        moreover have "\<forall>S\<in>I. e \<le> mS S"
+        moreover have "\<forall>S\<in>\<F>. e \<le> mS S"
           using e_def assms by auto
-        ultimately have "\<exists>e > 1. (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> \<Inter>I"
+        ultimately have "\<exists>e > 1. (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> \<Inter>\<F>"
           using mS by auto
       }
-      then have "z \<in> rel_interior (\<Inter>I)"
-        using convex_rel_interior_iff[of "\<Inter>I" z] \<open>\<Inter>I \<noteq> {}\<close> \<open>convex (\<Inter>I)\<close> by auto
+      then have "z \<in> rel_interior (\<Inter>\<F>)"
+        using convex_rel_interior_iff[of "\<Inter>\<F>" z] \<open>\<Inter>\<F> \<noteq> {}\<close> \<open>convex (\<Inter>\<F>)\<close> by auto
     }
     then show ?thesis
-      using convex_rel_interior_inter[of I] assms by auto
+      using convex_rel_interior_Inter[of \<F>] assms by auto
   qed
 qed
 
-lemma convex_closure_inter_two:
+lemma closure_Int_convex:
   fixes S T :: "'n::euclidean_space set"
   assumes "convex S"
     and "convex T"
   assumes "rel_interior S \<inter> rel_interior T \<noteq> {}"
   shows "closure (S \<inter> T) = closure S \<inter> closure T"
-  using convex_closure_inter[of "{S,T}"] assms by auto
+  using closure_Inter_convex[of "{S,T}"] assms by auto
 
 lemma convex_rel_interior_inter_two:
   fixes S T :: "'n::euclidean_space set"
@@ -1490,7 +1624,7 @@
     and "convex T"
     and "rel_interior S \<inter> rel_interior T \<noteq> {}"
   shows "rel_interior (S \<inter> T) = rel_interior S \<inter> rel_interior T"
-  using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto
+  using convex_rel_interior_finite_Inter[of "{S,T}"] assms by auto
 
 lemma convex_affine_closure_Int:
   fixes S T :: "'n::euclidean_space set"
@@ -1498,7 +1632,7 @@
     and "affine T"
     and "rel_interior S \<inter> T \<noteq> {}"
   shows "closure (S \<inter> T) = closure S \<inter> T"
-  by (metis affine_imp_convex assms convex_closure_inter_two rel_interior_affine rel_interior_eq_closure)
+  by (metis affine_imp_convex assms closure_Int_convex rel_interior_affine rel_interior_eq_closure)
 
 lemma connected_component_1_gen:
   fixes S :: "'a :: euclidean_space set"
@@ -1749,22 +1883,21 @@
   shows "convex (((*\<^sub>R) c) ` S) \<and> rel_open (((*\<^sub>R) c) ` S)"
   by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
 
-lemma convex_rel_open_finite_inter:
-  assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set) \<and> rel_open S"
-    and "finite I"
-  shows "convex (\<Inter>I) \<and> rel_open (\<Inter>I)"
-proof (cases "\<Inter>{rel_interior S |S. S \<in> I} = {}")
+lemma convex_rel_open_finite_Inter:
+  fixes \<F> :: "'n::euclidean_space set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S \<and> rel_open S"
+    and "finite \<F>"
+  shows "convex (\<Inter>\<F>) \<and> rel_open (\<Inter>\<F>)"
+proof (cases "\<Inter>{rel_interior S |S. S \<in> \<F>} = {}")
   case True
-  then have "\<Inter>I = {}"
+  then have "\<Inter>\<F> = {}"
     using assms unfolding rel_open_def by auto
   then show ?thesis
     unfolding rel_open_def by auto
 next
   case False
-  then have "rel_open (\<Inter>I)"
-    using assms unfolding rel_open_def
-    using convex_rel_interior_finite_inter[of I]
-    by auto
+  then have "rel_open (\<Inter>\<F>)"
+    using assms convex_rel_interior_finite_Inter[of \<F>] by (force simp: rel_open_def)
   then show ?thesis
     using convex_Inter assms by auto
 qed
@@ -2880,12 +3013,9 @@
           by (auto simp: algebra_simps sum_subtractf sum.distrib)
       qed
       have "y \<notin> rel_interior (convex hull S)"
-        using y
-        apply (simp add: mem_rel_interior)
-        apply (auto simp: convex_hull_finite [OF fs])
-        apply (drule_tac x=u in spec)
-        apply (auto intro: *)
-        done
+        using y convex_hull_finite [OF fs] *
+        apply simp
+        by (metis (no_types, lifting) IntD1 affine_hull_convex_hull mem_rel_interior)
     } with rel_interior_subset show "?lhs \<le> ?rhs"
       by blast
   qed
@@ -4022,6 +4152,133 @@
     by (force simp: closedin_limpt)
 qed
 
+subsection \<open>Closure of conic hulls\<close>
+proposition closedin_conic_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "compact T" "0 \<notin> T" "T \<subseteq> S"
+  shows   "closedin (top_of_set (conic hull S)) (conic hull T)"
+proof -
+  have **: "compact ({0..} \<times> T \<inter> (\<lambda>z. fst z *\<^sub>R snd z) -` K)" (is "compact ?L")
+    if "K \<subseteq> (\<lambda>z. (fst z) *\<^sub>R snd z) ` ({0..} \<times> S)" "compact K" for K
+  proof -
+    obtain r where "r > 0" and r: "\<And>x. x \<in> K \<Longrightarrow> norm x \<le> r"
+      by (metis \<open>compact K\<close> bounded_normE compact_imp_bounded)
+    show ?thesis
+      unfolding compact_eq_bounded_closed
+    proof
+      have "bounded ({0..r / setdist{0}T} \<times> T)"
+        by (simp add: assms(1) bounded_Times compact_imp_bounded)
+      moreover have "?L \<subseteq> ({0..r / setdist{0}T} \<times> T)"
+      proof clarsimp
+        fix a b
+        assume "a *\<^sub>R b \<in> K" and "b \<in> T" and "0 \<le> a"
+        have "setdist {0} T \<noteq> 0"
+          using \<open>b \<in> T\<close> assms compact_imp_closed setdist_eq_0_closed by auto
+        then have T0: "setdist {0} T > 0"
+          using less_eq_real_def by fastforce
+        then have "a * setdist {0} T \<le> r"
+          by (smt (verit, ccfv_SIG) \<open>0 \<le> a\<close> \<open>a *\<^sub>R b \<in> K\<close> \<open>b \<in> T\<close> dist_0_norm mult_mono' norm_scaleR r setdist_le_dist singletonI)
+        with T0 \<open>r>0\<close> show "a \<le> r / setdist {0} T"
+          by (simp add: divide_simps)
+      qed
+      ultimately show "bounded ?L"
+        by (meson bounded_subset)
+      show "closed ?L"
+      proof (rule continuous_closed_preimage)
+        show "continuous_on ({0..} \<times> T) (\<lambda>z. fst z *\<^sub>R snd z)"
+          by (intro continuous_intros)
+        show "closed ({0::real..} \<times> T)"
+          by (simp add: assms(1) closed_Times compact_imp_closed)
+        show "closed K"
+          by (simp add: compact_imp_closed that(2))
+      qed
+    qed
+  qed
+  show ?thesis
+    unfolding conic_hull_as_image
+  proof (rule proper_map)
+    show  "compact ({0..} \<times> T \<inter> (\<lambda>z. fst z *\<^sub>R snd z) -` K)" (is "compact ?L")
+      if "K \<subseteq> (\<lambda>z. (fst z) *\<^sub>R snd z) ` ({0..} \<times> S)" "compact K" for K
+    proof -
+      obtain r where "r > 0" and r: "\<And>x. x \<in> K \<Longrightarrow> norm x \<le> r"
+        by (metis \<open>compact K\<close> bounded_normE compact_imp_bounded)
+      show ?thesis
+        unfolding compact_eq_bounded_closed
+      proof
+        have "bounded ({0..r / setdist{0}T} \<times> T)"
+          by (simp add: assms(1) bounded_Times compact_imp_bounded)
+        moreover have "?L \<subseteq> ({0..r / setdist{0}T} \<times> T)"
+        proof clarsimp
+          fix a b
+          assume "a *\<^sub>R b \<in> K" and "b \<in> T" and "0 \<le> a"
+          have "setdist {0} T \<noteq> 0"
+            using \<open>b \<in> T\<close> assms compact_imp_closed setdist_eq_0_closed by auto
+          then have T0: "setdist {0} T > 0"
+            using less_eq_real_def by fastforce
+          then have "a * setdist {0} T \<le> r"
+            by (smt (verit, ccfv_SIG) \<open>0 \<le> a\<close> \<open>a *\<^sub>R b \<in> K\<close> \<open>b \<in> T\<close> dist_0_norm mult_mono' norm_scaleR r setdist_le_dist singletonI)
+          with T0 \<open>r>0\<close> show "a \<le> r / setdist {0} T"
+            by (simp add: divide_simps)
+        qed
+        ultimately show "bounded ?L"
+          by (meson bounded_subset)
+        show "closed ?L"
+        proof (rule continuous_closed_preimage)
+          show "continuous_on ({0..} \<times> T) (\<lambda>z. fst z *\<^sub>R snd z)"
+            by (intro continuous_intros)
+          show "closed ({0::real..} \<times> T)"
+            by (simp add: assms(1) closed_Times compact_imp_closed)
+          show "closed K"
+            by (simp add: compact_imp_closed that(2))
+        qed
+      qed
+    qed
+    show "(\<lambda>z. fst z *\<^sub>R snd z) ` ({0::real..} \<times> T) \<subseteq> (\<lambda>z. fst z *\<^sub>R snd z) ` ({0..} \<times> S)"
+      using \<open>T \<subseteq> S\<close> by force
+  qed auto
+qed
+
+lemma closed_conic_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "0 \<in> rel_interior S \<or> compact S \<and> 0 \<notin> S"
+  shows   "closed(conic hull S)"
+  using assms
+proof
+  assume "0 \<in> rel_interior S"
+  then show "closed (conic hull S)"
+    by (simp add: conic_hull_eq_span)
+next
+  assume "compact S \<and> 0 \<notin> S"
+  then have "closedin (top_of_set UNIV) (conic hull S)"
+    using closedin_conic_hull by force
+  then show "closed (conic hull S)"
+    by simp
+qed 
+
+lemma conic_closure:
+  fixes S :: "'a::euclidean_space set"
+  shows "conic S \<Longrightarrow> conic(closure S)"
+  by (meson Convex.cone_def cone_closure conic_def)
+
+lemma closure_conic_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "0 \<in> rel_interior S \<or> bounded S \<and> ~(0 \<in> closure S)"
+  shows   "closure(conic hull S) = conic hull (closure S)"
+  using assms
+proof
+  assume "0 \<in> rel_interior S"
+  then show "closure (conic hull S) = conic hull closure S"
+    by (metis closed_affine_hull closure_closed closure_same_affine_hull closure_subset conic_hull_eq_affine_hull subsetD subset_rel_interior)
+next
+  have "\<And>x. x \<in> conic hull closure S \<Longrightarrow> x \<in> closure (conic hull S)"
+    by (metis (no_types, opaque_lifting) closure_mono conic_closure conic_conic_hull subset_eq subset_hull)
+  moreover 
+  assume "bounded S \<and> 0 \<notin> closure S"
+  then have "\<And>x. x \<in> closure (conic hull S) \<Longrightarrow> x \<in> conic hull closure S"
+    by (metis closed_conic_hull closure_Un_frontier closure_closed closure_mono compact_closure hull_Un_subset le_sup_iff subsetD)
+  ultimately show "closure (conic hull S) = conic hull closure S"
+    by blast
+qed
 
 lemma compact_continuous_image_eq:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
diff -r 0d065af1a99c -r 4da1e18a9633 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Binomial.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -115,6 +115,9 @@
 lemma binomial_1 [simp]: "n choose Suc 0 = n"
   by (induct n) simp_all
 
+lemma choose_one: "n choose 1 = n" for n :: nat
+  by simp
+
 lemma choose_reduce_nat:
   "0 < n \<Longrightarrow> 0 < k \<Longrightarrow>
     n choose k = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
@@ -1084,109 +1087,190 @@
 qed
 
 
-subsection \<open>More on Binomial Coefficients\<close>
+subsection \<open>Inclusion-exclusion principle\<close>
+
+lemma Inter_over_Union:
+  "\<Inter> {\<Union> (\<F> x) |x. x \<in> S} = \<Union> {\<Inter> (G ` S) |G. \<forall>x\<in>S. G x \<in> \<F> x}" 
+proof -
+  have "\<And>x. \<forall>s\<in>S. \<exists>X \<in> \<F> s. x \<in> X \<Longrightarrow> \<exists>G. (\<forall>x\<in>S. G x \<in> \<F> x) \<and> (\<forall>s\<in>S. x \<in> G s)"
+    by metis
+  then show ?thesis
+    by (auto simp flip: all_simps ex_simps)
+qed
+
+lemma subset_insert_lemma:
+  "{T. T \<subseteq> (insert a S) \<and> P T} = {T. T \<subseteq> S \<and> P T} \<union> {insert a T |T. T \<subseteq> S \<and> P(insert a T)}" (is "?L=?R")
+proof
+  show "?L \<subseteq> ?R"
+    by (smt (verit) UnI1 UnI2 insert_Diff mem_Collect_eq subsetI subset_insert_iff)
+qed blast
+
+
+text\<open>Versions for additive real functions, where the additivity applies only to some
+ specific subsets (e.g. cardinality of finite sets, measurable sets with bounded measure.
+ (From HOL Light)\<close>
+
+locale Incl_Excl =
+  fixes P :: "'a set \<Rightarrow> bool" and f :: "'a set \<Rightarrow> 'b::ring_1"
+  assumes disj_add: "\<lbrakk>P S; P T; disjnt S T\<rbrakk> \<Longrightarrow> f(S \<union> T) = f S + f T"
+    and empty: "P{}"
+    and Int: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)"
+    and Un: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<union> T)"
+    and Diff: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S - T)"
+
+begin
+
+lemma f_empty [simp]: "f{} = 0"
+  using disj_add empty by fastforce
+
+lemma f_Un_Int: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> f(S \<union> T) + f(S \<inter> T) = f S + f T"
+  by (smt (verit, ccfv_threshold) Groups.add_ac(2) Incl_Excl.Diff Incl_Excl.Int Incl_Excl_axioms Int_Diff_Un Int_Diff_disjoint Int_absorb Un_Diff Un_Int_eq(2) disj_add disjnt_def group_cancel.add2 sup_bot.right_neutral)
 
-lemma choose_one: "n choose 1 = n" for n :: nat
-  by simp
+lemma restricted_indexed:
+  assumes "finite A" and X: "\<And>a. a \<in> A \<Longrightarrow> P(X a)"
+  shows "f(\<Union>(X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+proof -
+  have "\<lbrakk>finite A; card A = n; \<forall>a \<in> A. P (X a)\<rbrakk>
+              \<Longrightarrow> f(\<Union>(X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))" for n X and A :: "'c set"
+  proof (induction n arbitrary: A X rule: less_induct)
+    case (less n0 A0 X)
+    show ?case
+    proof (cases "n0=0")
+      case True
+      with less show ?thesis
+       by fastforce
+    next
+      case False
+      with less.prems obtain A n a where *: "n0 = Suc n" "A0 = insert a A" "a \<notin> A" "card A = n" "finite A"
+        by (metis card_Suc_eq_finite not0_implies_Suc)
+      with less have "P (X a)" by blast
+      have APX: "\<forall>a \<in> A. P (X a)"
+        by (simp add: "*" less.prems)
+      have PUXA: "P (\<Union> (X ` A))"
+        using \<open>finite A\<close> APX
+        by (induction) (auto simp: empty Un)
+      have "f (\<Union> (X ` A0)) = f (X a \<union> \<Union> (X ` A))"
+        by (simp add: *)
+      also have "... = f (X a) + f (\<Union> (X ` A)) - f (X a \<inter> \<Union> (X ` A))"
+        using f_Un_Int add_diff_cancel PUXA \<open>P (X a)\<close> by metis
+      also have "... = f (X a) - (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ card B * f (\<Inter> (X ` B))) +
+                       (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B)))"
+      proof -
+        have 1: "f (\<Union>i\<in>A. X a \<inter> X i) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter>b\<in>B. X a \<inter> X b))"
+          using less.IH [of n A "\<lambda>i. X a \<inter> X i"] APX Int \<open>P (X a)\<close>  by (simp add: *)
+        have 2: "X a \<inter> \<Union> (X ` A) = (\<Union>i\<in>A. X a \<inter> X i)"
+          by auto
+        have 3: "f (\<Union> (X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+          using less.IH [of n A X] APX Int \<open>P (X a)\<close>  by (simp add: *)
+        show ?thesis
+          unfolding 3 2 1
+          by (simp add: sum_negf)
+      qed
+      also have "... = (\<Sum>B | B \<subseteq> A0 \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+      proof -
+         have F: "{insert a B |B. B \<subseteq> A} = insert a ` Pow A \<and> {B. B \<subseteq> A \<and> B \<noteq> {}} = Pow A - {{}}"
+          by auto
+        have G: "(\<Sum>B\<in>Pow A. (- 1) ^ card (insert a B) * f (X a \<inter> \<Inter> (X ` B))) = (\<Sum>B\<in>Pow A. - ((- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B))))"
+        proof (rule sum.cong [OF refl])
+          fix B
+          assume B: "B \<in> Pow A"
+          then have "finite B"
+            using \<open>finite A\<close> finite_subset by auto
+          show "(- 1) ^ card (insert a B) * f (X a \<inter> \<Inter> (X ` B)) = - ((- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B)))"
+            using B * by (auto simp add: card_insert_if \<open>finite B\<close>)
+        qed
+        have disj: "{B. B \<subseteq> A \<and> B \<noteq> {}} \<inter> {insert a B |B. B \<subseteq> A} = {}"
+          using * by blast
+        have inj: "inj_on (insert a) (Pow A)"
+          using "*" inj_on_def by fastforce
+        show ?thesis
+          apply (simp add: * subset_insert_lemma sum.union_disjoint disj sum_negf)
+          apply (simp add: F G sum_negf sum.reindex [OF inj] o_def sum_diff *)
+          done
+      qed
+      finally show ?thesis .
+    qed   
+  qed
+  then show ?thesis
+    by (meson assms)
+qed
+
+lemma restricted:
+  assumes "finite A" "\<And>a. a \<in> A \<Longrightarrow> P a"
+  shows  "f(\<Union> A) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> B))"
+  using restricted_indexed [of A "\<lambda>x. x"] assms by auto
+
+end
+
+subsection\<open>Versions for unrestrictedly additive functions\<close>
+
+lemma Incl_Excl_UN:
+  fixes f :: "'a set \<Rightarrow> 'b::ring_1"
+  assumes "\<And>S T. disjnt S T \<Longrightarrow> f(S \<union> T) = f S + f T" "finite A"
+  shows "f(\<Union>(G ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (-1) ^ (card B + 1) * f (\<Inter> (G ` B)))"
+proof -
+  interpret Incl_Excl "\<lambda>x. True" f
+    by (simp add: Incl_Excl.intro assms(1))
+  show ?thesis
+    using restricted_indexed assms by blast
+qed
+
+lemma Incl_Excl_Union:
+  fixes f :: "'a set \<Rightarrow> 'b::ring_1"
+  assumes "\<And>S T. disjnt S T \<Longrightarrow> f(S \<union> T) = f S + f T" "finite A"
+  shows "f(\<Union> A) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> B))"
+  using Incl_Excl_UN[of f A "\<lambda>X. X"] assms by simp
 
 text \<open>The famous inclusion-exclusion formula for the cardinality of a union\<close>
 lemma int_card_UNION:
-  assumes "finite A"
-    and "\<forall>k \<in> A. finite k"
+  assumes "finite A" "\<And>K. K \<in> A \<Longrightarrow> finite K"
   shows "int (card (\<Union>A)) = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
-  (is "?lhs = ?rhs")
+proof -
+  interpret Incl_Excl finite "int o card"
+  proof qed (auto simp add: card_Un_disjnt)
+  show ?thesis
+    using restricted assms by auto
+qed
+
+text\<open>A more conventional form\<close>
+lemma inclusion_exclusion:
+  assumes "finite A" "\<And>K. K \<in> A \<Longrightarrow> finite K"
+  shows "int(card(\<Union> A)) =
+         (\<Sum>n=1..card A. (-1) ^ (Suc n) * (\<Sum>B | B \<subseteq> A \<and> card B = n. int (card (\<Inter> B))))" (is "_=?R")
 proof -
-  have "?rhs = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))"
-    by simp
-  also have "\<dots> = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))"
-    by (subst sum_distrib_left) simp
-  also have "\<dots> = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
-    using assms by (subst sum.Sigma) auto
-  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
-    by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI)
-  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
-    using assms
-    by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
-  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))"
-    using assms by (subst sum.Sigma) auto
-  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "sum ?lhs _ = _")
-  proof (rule sum.cong[OF refl])
-    fix x
-    assume x: "x \<in> \<Union>A"
-    define K where "K = {X \<in> A. x \<in> X}"
-    with \<open>finite A\<close> have K: "finite K"
-      by auto
-    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
-    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
-      using assms by (auto intro!: inj_onI)
-    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
-      using assms
-      by (auto intro!: rev_image_eqI[where x="(card a, a)" for a]
-        simp add: card_gt_0_iff[folded Suc_le_eq]
-        dest: finite_subset intro: card_mono)
-    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
-      by (rule sum.reindex_cong [where l = snd]) fastforce
-    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
-      using assms by (subst sum.Sigma) auto
-    also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
-      by (subst sum_distrib_left) simp
-    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))"
-      (is "_ = ?rhs")
-    proof (rule sum.mono_neutral_cong_right[rule_format])
-      show "finite {1..card A}"
-        by simp
-      show "{1..card K} \<subseteq> {1..card A}"
-        using \<open>finite A\<close> by (auto simp add: K_def intro: card_mono)
-    next
-      fix i
-      assume "i \<in> {1..card A} - {1..card K}"
-      then have i: "i \<le> card A" "card K < i"
-        by auto
-      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}"
-        by (auto simp add: K_def)
-      also have "\<dots> = {}"
-        using \<open>finite A\<close> i by (auto simp add: K_def dest: card_mono[rotated 1])
-      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
-        by (metis mult_zero_right sum.empty)
-    next
-      fix i
-      have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
-        (is "?lhs = ?rhs")
-        by (rule sum.cong) (auto simp add: K_def)
-      then show "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs"
-        by simp
-    qed
-    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}"
-      using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset)
-    then have "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
-      by (subst (2) sum.atLeast_Suc_atMost) simp_all
-    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
-      using K by (subst n_subsets[symmetric]) simp_all
-    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
-      by (subst sum_distrib_left[symmetric]) simp
-    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
-      by (subst binomial_ring) (simp add: ac_simps atMost_atLeast0)
-    also have "\<dots> = 1"
-      using x K by (auto simp add: K_def card_gt_0_iff)
-    finally show "?lhs x = 1" .
+  have fin: "finite {I. I \<subseteq> A \<and> I \<noteq> {}}"
+    by (simp add: assms)
+  have "\<And>k. \<lbrakk>Suc 0 \<le> k; k \<le> card A\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>A. B \<noteq> {} \<and> k = card B"
+    by (metis (mono_tags, lifting) Suc_le_D Zero_neq_Suc card_eq_0_iff obtain_subset_with_card_n)
+  with \<open>finite A\<close> finite_subset
+  have card_eq: "card ` {I. I \<subseteq> A \<and> I \<noteq> {}} = {1..card A}"
+    using not_less_eq_eq card_mono by (fastforce simp: image_iff)
+  have "int(card(\<Union> A)) 
+      = (\<Sum>y = 1..card A. \<Sum>I\<in>{x. x \<subseteq> A \<and> x \<noteq> {} \<and> card x = y}. - ((- 1) ^ y * int (card (\<Inter> I))))"
+    by (simp add: int_card_UNION assms sum.image_gen [OF fin, where g=card] card_eq)
+  also have "... = ?R"
+  proof -
+    have "{B. B \<subseteq> A \<and> B \<noteq> {} \<and> card B = k} = {B. B \<subseteq> A \<and> card B = k}"
+      if "Suc 0 \<le> k" and "k \<le> card A" for k
+      using that by auto
+    then show ?thesis
+      by (clarsimp simp add: sum_negf simp flip: sum_distrib_left)
   qed
-  also have "\<dots> = int (card (\<Union>A))"
-    by simp
-  finally show ?thesis ..
+  finally show ?thesis .
 qed
 
 lemma card_UNION:
-  assumes "finite A"
-    and "\<forall>k \<in> A. finite k"
+  assumes "finite A" and "\<And>K. K \<in> A \<Longrightarrow> finite K"
   shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
   by (simp only: flip: int_card_UNION [OF assms])
 
 lemma card_UNION_nonneg:
-  assumes "finite A"
-    and "\<forall>k \<in> A. finite k"
+  assumes "finite A" and "\<And>K. K \<in> A \<Longrightarrow> finite K"
   shows "(\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I))) \<ge> 0"
   using int_card_UNION [OF assms] by presburger
 
+subsection \<open>More on Binomial Coefficients\<close>
+
 text \<open>The number of nat lists of length \<open>m\<close> summing to \<open>N\<close> is \<^term>\<open>(N + m - 1) choose N\<close>:\<close>
 lemma card_length_sum_list_rec:
   assumes "m \<ge> 1"
diff -r 0d065af1a99c -r 4da1e18a9633 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -142,7 +142,7 @@
 
 lemma scaleR_minus1_left [simp]: "scaleR (-1) x = - x"
   for x :: "'a::real_vector"
-  using scaleR_minus_left [of 1 x] by simp
+  by simp
 
 lemma scaleR_2:
   fixes x :: "'a::real_vector"
@@ -786,6 +786,11 @@
 class real_normed_div_algebra = real_div_algebra + real_normed_vector +
   assumes norm_mult: "norm (x * y) = norm x * norm y"
 
+lemma divideR_right:
+  fixes x y :: "'a::real_normed_vector"
+  shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
+  by auto
+
 class real_normed_field = real_field + real_normed_div_algebra
 
 instance real_normed_div_algebra < real_normed_algebra_1