src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

     using assms by (simp add: ab_group_add_class.ab_left_minus image_iff)
   with aff_dim_zero show ?thesis
     by (metis aff_dim_translation_eq)
 qed
 
-lemma aff_dim_univ: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
+lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
   using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"]
     dim_UNIV[where 'a="'n::euclidean_space"]
   by auto
 
 lemma aff_dim_geq:

 lemma aff_dim_le_DIM:
   fixes S :: "'n::euclidean_space set"
   shows "aff_dim S \<le> int (DIM('n))"
 proof -
   have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
-    using aff_dim_univ by auto
+    using aff_dim_UNIV by auto
   then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
     using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
 qed
 
 lemma affine_dim_equal:

   have "S \<noteq> {}"
     using assms aff_dim_empty[of S] by auto
   have h0: "S \<subseteq> affine hull S"
     using hull_subset[of S _] by auto
   have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S"
-    using aff_dim_univ assms by auto
+    using aff_dim_UNIV assms by auto
   then have h2: "aff_dim (affine hull S) \<le> aff_dim (UNIV :: ('n::euclidean_space) set)"
     using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto
   have h3: "aff_dim S \<le> aff_dim (affine hull S)"
     using h0 aff_dim_subset[of S "affine hull S"] assms by auto
   then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)"

   apply auto
   using openin_subopen[of "subtopology euclidean (affine hull S)" S]
   apply auto
   done
 
-lemma opein_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
+lemma openin_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
   apply (simp add: rel_interior_def)
   apply (subst openin_subopen)
   apply blast
   done
 

   fixes S :: "'n::euclidean_space set"
   assumes "convex S"
   shows "rel_interior (rel_interior S) = rel_interior S"
 proof -
   have "openin (subtopology euclidean (affine hull (rel_interior S))) (rel_interior S)"
-    using opein_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
+    using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
   then show ?thesis
     using rel_interior_def by auto
 qed
 
 lemma rel_interior_rel_open:

   shows "closed (rel_frontier S)"
 proof -
   have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
     apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"])
     using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S]
-      closure_affine_hull[of S] opein_rel_interior[of S]
+      closure_affine_hull[of S] openin_rel_interior[of S]
     apply auto
     done
   show ?thesis
     apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
     unfolding rel_frontier_def

         by auto
     }
     then have "affine hull S = UNIV"
       by auto
     then have "aff_dim S = int DIM('n)"
-      using aff_dim_affine_hull[of S] by (simp add: aff_dim_univ)
+      using aff_dim_affine_hull[of S] by (simp add: aff_dim_UNIV)
     then have False
       using False by auto
   }
   ultimately show ?thesis by auto
 next

   fixes a :: "'a::euclidean_space"
   shows "aff_dim {x. a \<bullet> x \<le> r} =
         (if a = 0 \<and> r < 0 then -1 else DIM('a))"
 proof -
   have "int (DIM('a)) = aff_dim (UNIV::'a set)"
-    by (simp add: aff_dim_univ)
+    by (simp add: aff_dim_UNIV)
   then have "aff_dim (affine hull {x. a \<bullet> x \<le> r}) = DIM('a)" if "(a = 0 \<longrightarrow> r \<ge> 0)"
     using that by (simp add: affine_hull_halfspace_le not_less)
   then show ?thesis
     by (force simp: aff_dim_affine_hull)
 qed

     using \<open>a \<in> span (op + (- z) ` S)\<close> affine_hull_insert_span_gen apply blast
     apply (simp_all add: \<open>a \<noteq> 0\<close> szx)
     done
 qed
 
-proposition supporting_hyperplane_relative_boundary:
+proposition supporting_hyperplane_rel_boundary:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "x \<in> S" and xno: "x \<notin> rel_interior S"
   obtains a where "a \<noteq> 0"
               and "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y"
               and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y"

   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "x \<in> closure S" "x \<notin> rel_interior S"
   obtains a where "a \<noteq> 0"
               and "\<And>y. y \<in> closure S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y"
               and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y"
-using supporting_hyperplane_relative_boundary [of "closure S" x]
+using supporting_hyperplane_rel_boundary [of "closure S" x]
 by (metis assms convex_closure convex_rel_interior_closure)
 
 subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
 
 lemma 

       by (metis (no_types) aff_dim_affine_hull eq)
     then have "int (card b) = 1 + aff_dim s"
       by (simp add: aff_dim_affine_independent indb)
     then show ?thesis
       using fbc aff
-      by (simp add: \<open>\<not> affine_dependent c\<close> \<open>b \<subseteq> c\<close> aff_dim_affine_independent aff_dim_univ card_Diff_subset of_nat_diff)
+      by (simp add: \<open>\<not> affine_dependent c\<close> \<open>b \<subseteq> c\<close> aff_dim_affine_independent aff_dim_UNIV card_Diff_subset of_nat_diff)
   qed
   show ?thesis
   proof (cases "c = b")
     case True show ?thesis
       apply (rule_tac f="{}" in that)
       using True affc
       apply (simp_all add: eq [symmetric])
-      by (metis aff_dim_univ aff_dim_affine_hull)
+      by (metis aff_dim_UNIV aff_dim_affine_hull)
   next
     case False
     have ind: "\<not> affine_dependent (\<Union>a\<in>c - b. c - {a})"
       by (rule affine_independent_subset [OF indc]) auto
     have affeq: "affine hull s = (\<Inter>x\<in>(\<lambda>a. c - {a}) ` (c - b). affine hull x)"

             if t: "t \<in> c" for t
     proof -
       have "insert t c = c"
         using t by blast
       then show ?thesis
-        by (metis (full_types) add.commute aff_dim_affine_hull aff_dim_insert aff_dim_univ affc affine_dependent_def indc insert_Diff_single t)
+        by (metis (full_types) add.commute aff_dim_affine_hull aff_dim_insert aff_dim_UNIV affc affine_dependent_def indc insert_Diff_single t)
     qed
     show ?thesis
       apply (rule_tac f = "(\<lambda>x. affine hull x) ` ((\<lambda>a. c - {a}) ` (c - b))" in that)
          using \<open>finite c\<close> apply blast
         apply (simp add: imeq card1 card2)