# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1690307545 -3600
# Node ID 51b8f6a19978c84cd2a61b25282a192d9fdefcd6
# Parent  b221d12978ee893df70c2835ec3daa44e5596a06
A few more cosmetic changes to proofs

diff -r b221d12978ee -r 51b8f6a19978 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Mon Jul 17 21:49:58 2023 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Tue Jul 25 18:52:25 2023 +0100
@@ -214,18 +214,13 @@
       fixes S :: "'a::real_normed_vector set"
       assumes "T face_of S" "T \<noteq> S"
         shows "T \<inter> interior S = {}"
-proof -
-  have "T \<inter> interior S \<subseteq> rel_interior S"
-    by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans)
-  thus ?thesis
-    by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
-qed
+  using assms face_of_disjoint_rel_interior interior_subset_rel_interior by fastforce
 
 lemma face_of_subset_rel_boundary:
   fixes S :: "'a::real_normed_vector set"
   assumes "T face_of S" "T \<noteq> S"
     shows "T \<subseteq> (S - rel_interior S)"
-by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
+  by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset subset_iff)
 
 lemma face_of_subset_rel_frontier:
     fixes S :: "'a::real_normed_vector set"
@@ -241,13 +236,8 @@
   have "aff_dim T \<le> aff_dim S"
     by (simp add: face_of_imp_subset aff_dim_subset assms)
   moreover have "aff_dim T \<noteq> aff_dim S"
-  proof (cases "T = {}")
-    case True then show ?thesis
-      by (metis aff_dim_empty \<open>T \<noteq> S\<close>)
-  next 
-    case False then show ?thesis
-      by (smt (verit) aff_dim_empty assms convex_rel_frontier_aff_dim face_of_imp_convex face_of_subset_rel_frontier)
-  qed
+    by (metis aff_dim_empty assms convex_rel_frontier_aff_dim face_of_imp_convex 
+        face_of_subset_rel_frontier order_less_irrefl)
   ultimately show ?thesis
     by simp
 qed
@@ -258,7 +248,7 @@
   shows "U \<subseteq> T"
 proof (rule subset_of_face_of [OF T \<open>U \<subseteq> S\<close>])
   show "T \<inter> rel_interior U \<noteq> {}"
-    using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T] rel_interior_subset [of U] dis \<open>U \<subseteq> S\<close> disjnt_def 
+    using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T] rel_interior_subset dis \<open>U \<subseteq> S\<close> disjnt_def 
     by fastforce
 qed
 
@@ -478,7 +468,7 @@
 qed
 
 lemma faces_of_translation:
-   "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
+   "{F. F face_of (+) a ` S} = (image ((+) a)) ` {F. F face_of S}"
 proof -
   have "\<And>F. F face_of (+) a ` S \<Longrightarrow> \<exists>G. G face_of S \<and> F = (+) a ` G"
     by (metis face_of_imp_subset face_of_translation_eq subset_imageE)
@@ -560,15 +550,12 @@
     qed
     with fst snd show ?thesis by metis
   qed
-next
-  assume ?rhs with face_of_Times show ?lhs by auto
-qed
+qed (use face_of_Times in auto)
 
 lemma face_of_Times_eq:
-    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
-    shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
-           F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
-by (auto simp: face_of_Times_decomp times_eq_iff)
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow> F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
+  by (auto simp: face_of_Times_decomp times_eq_iff)
 
 lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
 proof -
@@ -588,8 +575,7 @@
 
 lemma face_of_halfspace_le:
   fixes a :: "'n::euclidean_space"
-  shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
-         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
+  shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
      (is "?lhs = ?rhs")
 proof (cases "a = 0")
   case True then show ?thesis
@@ -623,9 +609,8 @@
 
 lemma face_of_halfspace_ge:
   fixes a :: "'n::euclidean_space"
-  shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
-         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
-using face_of_halfspace_le [of F "-a" "-b"] by simp
+  shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
+  using face_of_halfspace_le [of F "-a" "-b"] by simp
 
 subsection\<open>Exposed faces\<close>
 
@@ -670,31 +655,31 @@
 qed
 
 lemma exposed_face_of_Int_supporting_hyperplane_le:
-   "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
-by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
+  "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
+  by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
 
 lemma exposed_face_of_Int_supporting_hyperplane_ge:
-   "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
-using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
+  "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
+  using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
 
 proposition exposed_face_of_Int:
   assumes "T exposed_face_of S"
-      and "u exposed_face_of S"
-    shows "(T \<inter> u) exposed_face_of S"
+      and "U exposed_face_of S"
+    shows "(T \<inter> U) exposed_face_of S"
 proof -
   obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
                and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
                and teq: "T = S \<inter> {x. a \<bullet> x = b}"
     using assms by (auto simp: exposed_face_of_def)
-  obtain a' b' where u: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
+  obtain a' b' where U: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
                  and s': "S \<subseteq> {x. a' \<bullet> x \<le> b'}"
-                 and ueq: "u = S \<inter> {x. a' \<bullet> x = b'}"
+                 and ueq: "U = S \<inter> {x. a' \<bullet> x = b'}"
     using assms by (auto simp: exposed_face_of_def)
-  have tu: "T \<inter> u face_of S"
-    using T teq u ueq by (simp add: face_of_Int)
+  have tu: "T \<inter> U face_of S"
+    using T teq U ueq by (simp add: face_of_Int)
   have ss: "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'}"
     using S s' by (force simp: inner_left_distrib)
-  have "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'} \<and> T \<inter> u = S \<inter> {x. (a + a') \<bullet> x = b + b'}"
+  have "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'} \<and> T \<inter> U = S \<inter> {x. (a + a') \<bullet> x = b + b'}"
     using S s' by (fastforce simp: ss inner_left_distrib teq ueq)
   then show ?thesis
     using exposed_face_of_def tu by auto
@@ -860,8 +845,8 @@
   by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
 
 lemma face_of_singleton:
-   "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
-by (fastforce simp add: extreme_point_of_def face_of_def)
+  "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
+  by (fastforce simp add: extreme_point_of_def face_of_def)
 
 lemma extreme_point_not_in_REL_INTERIOR:
     fixes S :: "'a::real_normed_vector set"
@@ -871,11 +856,7 @@
 lemma extreme_point_not_in_interior:
   fixes S :: "'a::{real_normed_vector, perfect_space} set"
   assumes "x extreme_point_of S" shows "x \<notin> interior S"
-proof (cases "S = {x}")
-  case False
-  then show ?thesis
-    by (meson assms subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
-qed (simp add: empty_interior_finite)
+  using assms extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior by fastforce
 
 lemma extreme_point_of_face:
      "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
@@ -914,8 +895,8 @@
   by simp
 
 lemma extreme_point_of_Int:
-   "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
-by (simp add: extreme_point_of_def)
+  "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
+  by (simp add: extreme_point_of_def)
 
 lemma extreme_point_of_Int_supporting_hyperplane_le:
    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
@@ -965,16 +946,16 @@
   by (simp add: face_of_imp_subset facet_of_def)
 
 lemma hyperplane_facet_of_halfspace_le:
-   "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
-unfolding facet_of_def hyperplane_eq_empty
-by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
-           Suc_leI of_nat_diff aff_dim_halfspace_le)
+  "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
+  unfolding facet_of_def hyperplane_eq_empty
+  by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
+      Suc_leI of_nat_diff aff_dim_halfspace_le)
 
 lemma hyperplane_facet_of_halfspace_ge:
-    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
-unfolding facet_of_def hyperplane_eq_empty
-by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
-           Suc_leI of_nat_diff aff_dim_halfspace_ge)
+  "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
+  unfolding facet_of_def hyperplane_eq_empty
+  by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
+      Suc_leI of_nat_diff aff_dim_halfspace_ge)
 
 lemma facet_of_halfspace_le:
     "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
@@ -989,8 +970,8 @@
 qed
 
 lemma facet_of_halfspace_ge:
-    "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
-using facet_of_halfspace_le [of F "-a" "-b"] by simp
+  "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
+  using facet_of_halfspace_le [of F "-a" "-b"] by simp
 
 subsection \<open>Edges: faces of affine dimension 1\<close> (*FIXME too small subsection, rearrange? *)
 
@@ -1161,12 +1142,7 @@
     qed
 next
   show "convex hull {x. x extreme_point_of S} \<subseteq> S"
-  proof -
-    have "{a. a extreme_point_of S} \<subseteq> S"
-      using extreme_point_of_def by blast
-    then show ?thesis
-      by (simp add: \<open>convex S\<close> hull_minimal)
-  qed
+    using \<open>convex S\<close> extreme_point_of_stillconvex subset_hull by fastforce
 qed
 
 
@@ -1183,9 +1159,9 @@
 lemma extreme_points_of_convex_hull_eq:
   fixes S :: "'a::euclidean_space set"
   shows
-   "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
+    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
         \<Longrightarrow> {x. x extreme_point_of (convex hull S)} = S"
-by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
+  by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
 
 
 lemma extreme_point_of_convex_hull_eq:
@@ -1221,33 +1197,23 @@
 lemma extreme_point_of_convex_hull_2:
   fixes x :: "'a::euclidean_space"
   shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
-proof -
-  have "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x \<in> {a,b}"
-    by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2)
-  then show ?thesis
-    by simp
-qed
+  by (simp add: extreme_point_of_convex_hull_affine_independent)
 
 lemma extreme_point_of_segment:
   fixes x :: "'a::euclidean_space"
-  shows
-   "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
-by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
+  shows "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
+  by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
 
 lemma face_of_convex_hull_subset:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and T: "T face_of (convex hull S)"
-  obtains s' where "s' \<subseteq> S" "T = convex hull s'"
+  obtains S' where "S' \<subseteq> S" "T = convex hull S'"
 proof
   show "{x. x extreme_point_of T} \<subseteq> S"
     using T extreme_point_of_convex_hull extreme_point_of_face by blast
   show "T = convex hull {x. x extreme_point_of T}"
-  proof (rule Krein_Milman_Minkowski)
-    show "compact T"
-      using T assms compact_convex_hull face_of_imp_compact by auto
-    show "convex T"
-      using T face_of_imp_convex by blast
-  qed
+    by (metis Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull 
+        face_of_imp_compact face_of_imp_convex)
 qed
 
 
@@ -1431,14 +1397,14 @@
     by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
 next
   assume ?rhs
-  then obtain c where "c \<subseteq> S" and T: "T = convex hull c"
+  then obtain C where "C \<subseteq> S" and T: "T = convex hull C"
     by blast
-  have "affine hull c \<inter> affine hull (S - c) = {}"
-    by (intro disjoint_affine_hull [OF assms \<open>c \<subseteq> S\<close>], auto)
-  then have "affine hull c \<inter> convex hull (S - c) = {}"
+  have "affine hull C \<inter> affine hull (S - C) = {}"
+    by (intro disjoint_affine_hull [OF assms \<open>C \<subseteq> S\<close>], auto)
+  then have "affine hull C \<inter> convex hull (S - C) = {}"
     using convex_hull_subset_affine_hull by fastforce
   then show ?lhs
-    by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
+    by (metis face_of_convex_hulls \<open>C \<subseteq> S\<close> aff_independent_finite assms T)
 qed
 
 lemma facet_of_convex_hull_affine_independent:
@@ -1555,13 +1521,9 @@
 definition\<^marker>\<open>tag important\<close> polytope where
  "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
 
-lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
-proof -
-  have "\<And>a A. polytope A \<Longrightarrow> polytope ((+) a ` A)"
-    by (metis (no_types) convex_hull_translation finite_imageI polytope_def)
-  then show ?thesis
-    by (metis (no_types) add.left_inverse image_add_0 translation_assoc)
-qed
+lemma polytope_translation_eq: "polytope ((+) a ` S) \<longleftrightarrow> polytope S"
+  unfolding polytope_def
+  by (metis (no_types, opaque_lifting) add.left_inverse convex_hull_translation finite_imageI image_add_0 translation_assoc)
 
 lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
   unfolding polytope_def using convex_hull_linear_image by blast
@@ -1604,12 +1566,12 @@
 
 lemma polytope_scaling:
   assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
-by (simp add: assms polytope_linear_image)
+  by (simp add: assms polytope_linear_image)
 
 lemma polytope_imp_compact:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> compact S"
-by (metis finite_imp_compact_convex_hull polytope_def)
+  by (metis finite_imp_compact_convex_hull polytope_def)
 
 lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
   by (metis convex_convex_hull polytope_def)
@@ -1617,12 +1579,12 @@
 lemma polytope_imp_closed:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> closed S"
-by (simp add: compact_imp_closed polytope_imp_compact)
+  by (simp add: compact_imp_closed polytope_imp_compact)
 
 lemma polytope_imp_bounded:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> bounded S"
-by (simp add: compact_imp_bounded polytope_imp_compact)
+  by (simp add: compact_imp_bounded polytope_imp_compact)
 
 lemma polytope_interval: "polytope(cbox a b)"
   unfolding polytope_def by (meson closed_interval_as_convex_hull)