src/HOL/Analysis/Starlike.thy

     using at_within_interior assms by fastforce
 qed
 
 lemma affine_independent_convex_affine_hull:
   fixes s :: "'a::euclidean_space set"
-  assumes "~affine_dependent s" "t \<subseteq> s"
+  assumes "\<not> affine_dependent s" "t \<subseteq> s"
     shows "convex hull t = affine hull t \<inter> convex hull s"
 proof -
   have fin: "finite s" "finite t" using assms aff_independent_finite finite_subset by auto
     { fix u v x
       assume uv: "sum u t = 1" "\<forall>x\<in>s. 0 \<le> v x" "sum v s = 1"

     by blast
 qed
 
 lemma affine_independent_span_eq:
   fixes s :: "'a::euclidean_space set"
-  assumes "~affine_dependent s" "card s = Suc (DIM ('a))"
+  assumes "\<not> affine_dependent s" "card s = Suc (DIM ('a))"
     shows "affine hull s = UNIV"
 proof (cases "s = {}")
   case True then show ?thesis
     using assms by simp
 next

       done
 qed
 
 lemma affine_independent_span_gt:
   fixes s :: "'a::euclidean_space set"
-  assumes ind: "~ affine_dependent s" and dim: "DIM ('a) < card s"
+  assumes ind: "\<not> affine_dependent s" and dim: "DIM ('a) < card s"
     shows "affine hull s = UNIV"
   apply (rule affine_independent_span_eq [OF ind])
   apply (rule antisym)
   using assms
   apply auto

              \<subseteq> rel_interior (convex hull s)"
   by (force simp add:  rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=s, simplified])
 
 lemma rel_interior_convex_hull_explicit:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ affine_dependent s"
+  assumes "\<not> affine_dependent s"
   shows "rel_interior(convex hull s) =
          {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
          (is "?lhs = ?rhs")
 proof
   show "?rhs \<le> ?lhs"

 qed
 
 lemma interior_convex_hull_explicit_minimal:
   fixes s :: "'a::euclidean_space set"
   shows
-   "~ affine_dependent s
+   "\<not> affine_dependent s
         ==> interior(convex hull s) =
              (if card(s) \<le> DIM('a) then {}
               else {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> sum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = y})"
   apply (simp add: aff_independent_finite empty_interior_convex_hull, clarify)
   apply (rule trans [of _ "rel_interior(convex hull s)"])
-  apply (simp add: affine_hull_convex_hull affine_independent_span_gt rel_interior_interior)
+  apply (simp add: affine_independent_span_gt rel_interior_interior)
   by (simp add: rel_interior_convex_hull_explicit)
 
 lemma interior_convex_hull_explicit:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ affine_dependent s"
+  assumes "\<not> affine_dependent s"
   shows
    "interior(convex hull s) =
              (if card(s) \<le> DIM('a) then {}
               else {y. \<exists>u. (\<forall>x \<in> s. 0 < u x \<and> u x < 1) \<and> sum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = y})"
 proof -

   shows "compact s ==> closure(convex hull s) = convex hull s"
   by (simp add: compact_imp_closed compact_convex_hull)
 
 lemma rel_frontier_convex_hull_explicit:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ affine_dependent s"
+  assumes "\<not> affine_dependent s"
   shows "rel_frontier(convex hull s) =
          {y. \<exists>u. (\<forall>x \<in> s. 0 \<le> u x) \<and> (\<exists>x \<in> s. u x = 0) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
 proof -
   have fs: "finite s"
     using assms by (simp add: aff_independent_finite)

     done
 qed
 
 lemma frontier_convex_hull_explicit:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ affine_dependent s"
+  assumes "\<not> affine_dependent s"
   shows "frontier(convex hull s) =
          {y. \<exists>u. (\<forall>x \<in> s. 0 \<le> u x) \<and> (DIM ('a) < card s \<longrightarrow> (\<exists>x \<in> s. u x = 0)) \<and>
              sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
 proof -
   have fs: "finite s"

   qed
 qed
 
 lemma rel_frontier_convex_hull_cases:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ affine_dependent s"
+  assumes "\<not> affine_dependent s"
   shows "rel_frontier(convex hull s) = \<Union>{convex hull (s - {x}) |x. x \<in> s}"
 proof -
   have fs: "finite s"
     using assms by (simp add: aff_independent_finite)
   { fix u a

     done
 qed
 
 lemma frontier_convex_hull_eq_rel_frontier:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ affine_dependent s"
+  assumes "\<not> affine_dependent s"
   shows "frontier(convex hull s) =
            (if card s \<le> DIM ('a) then convex hull s else rel_frontier(convex hull s))"
   using assms
   unfolding rel_frontier_def frontier_def
   by (simp add: affine_independent_span_gt rel_interior_interior
                 finite_imp_compact empty_interior_convex_hull aff_independent_finite)
 
 lemma frontier_convex_hull_cases:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ affine_dependent s"
+  assumes "\<not> affine_dependent s"
   shows "frontier(convex hull s) =
            (if card s \<le> DIM ('a) then convex hull s else \<Union>{convex hull (s - {x}) |x. x \<in> s})"
 by (simp add: assms frontier_convex_hull_eq_rel_frontier rel_frontier_convex_hull_cases)
 
 lemma in_frontier_convex_hull:

 apply (simp add: algebra_simps)
 done
 
 lemma interior_convex_hull_3_minimal:
   fixes a :: "'a::euclidean_space"
-  shows "\<lbrakk>~ collinear{a,b,c}; DIM('a) = 2\<rbrakk>
+  shows "\<lbrakk>\<not> collinear{a,b,c}; DIM('a) = 2\<rbrakk>
          \<Longrightarrow> interior(convex hull {a,b,c}) =
                 {v. \<exists>x y z. 0 < x \<and> 0 < y \<and> 0 < z \<and> x + y + z = 1 \<and>
                             x *\<^sub>R a + y *\<^sub>R b + z *\<^sub>R c = v}"
 apply (simp add: collinear_3_eq_affine_dependent interior_convex_hull_explicit_minimal, safe)
 apply (rule_tac x="u a" in exI, simp)

     by (force simp add:span_zero insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert)
 qed
 
 lemma affine_dependent_choose:
   fixes a :: "'a :: euclidean_space"
-  assumes "~(affine_dependent S)"
+  assumes "\<not>(affine_dependent S)"
   shows "affine_dependent(insert a S) \<longleftrightarrow> a \<notin> S \<and> a \<in> affine hull S"
         (is "?lhs = ?rhs")
 proof safe
   assume "affine_dependent (insert a S)" and "a \<in> S"
   then show "False"

     by (simp add: \<open>a \<in> affine hull S\<close> \<open>a \<notin> S\<close> affine_dependent_def)
 qed
 
 lemma affine_independent_insert:
   fixes a :: "'a :: euclidean_space"
-  shows "\<lbrakk>~(affine_dependent S); a \<notin> affine hull S\<rbrakk> \<Longrightarrow> ~(affine_dependent(insert a S))"
+  shows "\<lbrakk>\<not> affine_dependent S; a \<notin> affine hull S\<rbrakk> \<Longrightarrow> \<not> affine_dependent(insert a S)"
   by (simp add: affine_dependent_choose)
 
 lemma subspace_bounded_eq_trivial:
   fixes S :: "'a::real_normed_vector set"
   assumes "subspace S"

 
 subsection%unimportant\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
 
 lemma
   fixes s :: "'a::euclidean_space set"
-  assumes "~ (affine_dependent(s \<union> t))"
+  assumes "\<not> affine_dependent(s \<union> t)"
     shows convex_hull_Int_subset: "convex hull s \<inter> convex hull t \<subseteq> convex hull (s \<inter> t)" (is ?C)
       and affine_hull_Int_subset: "affine hull s \<inter> affine hull t \<subseteq> affine hull (s \<inter> t)" (is ?A)
 proof -
   have [simp]: "finite s" "finite t"
     using aff_independent_finite assms by blast+

 qed
 
 
 proposition affine_hull_Int:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ (affine_dependent(s \<union> t))"
+  assumes "\<not> affine_dependent(s \<union> t)"
     shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t"
 apply (rule subset_antisym)
 apply (simp add: hull_mono)
 by (simp add: affine_hull_Int_subset assms)
 
 proposition convex_hull_Int:
   fixes s :: "'a::euclidean_space set"
-  assumes "~ (affine_dependent(s \<union> t))"
+  assumes "\<not> affine_dependent(s \<union> t)"
     shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t"
 apply (rule subset_antisym)
 apply (simp add: hull_mono)
 by (simp add: convex_hull_Int_subset assms)
 
 proposition
   fixes s :: "'a::euclidean_space set set"
-  assumes "~ (affine_dependent (\<Union>s))"
+  assumes "\<not> affine_dependent (\<Union>s)"
     shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A")
       and convex_hull_Inter: "convex hull (\<Inter>s) = (\<Inter>t\<in>s. convex hull t)" (is "?C")
 proof -
   have "finite s"
     using aff_independent_finite assms finite_UnionD by blast

     by auto
 qed
 
 proposition in_convex_hull_exchange_unique:
   fixes S :: "'a::euclidean_space set"
-  assumes naff: "~ affine_dependent S" and a: "a \<in> convex hull S"
+  assumes naff: "\<not> affine_dependent S" and a: "a \<in> convex hull S"
       and S: "T \<subseteq> S" "T' \<subseteq> S"
       and x:  "x \<in> convex hull (insert a T)"
       and x': "x \<in> convex hull (insert a T')"
     shows "x \<in> convex hull (insert a (T \<inter> T'))"
 proof (cases "a \<in> S")

   qed
 qed
 
 corollary convex_hull_exchange_Int:
   fixes a  :: "'a::euclidean_space"
-  assumes "~ affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
+  assumes "\<not> affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
   shows "(convex hull (insert a T)) \<inter> (convex hull (insert a T')) =
          convex hull (insert a (T \<inter> T'))"
 apply (rule subset_antisym)
   using in_convex_hull_exchange_unique assms apply blast
   by (metis hull_mono inf_le1 inf_le2 insert_inter_insert le_inf_iff)
 
 lemma Int_closed_segment:
   fixes b :: "'a::euclidean_space"
-  assumes "b \<in> closed_segment a c \<or> ~collinear{a,b,c}"
+  assumes "b \<in> closed_segment a c \<or> \<not> collinear{a,b,c}"
     shows "closed_segment a b \<inter> closed_segment b c = {b}"
 proof (cases "c = a")
   case True
   then show ?thesis
     using assms collinear_3_eq_affine_dependent by fastforce

 
 proposition affine_parallel_slice:
   fixes S :: "'a :: euclidean_space set"
   assumes "affine S"
       and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
-      and "~ (S \<subseteq> {x. a \<bullet> x \<le> b})"
+      and "\<not> (S \<subseteq> {x. a \<bullet> x \<le> b})"
   obtains a' b' where "a' \<noteq> 0"
                    "S \<inter> {x. a' \<bullet> x \<le> b'} = S \<inter> {x. a \<bullet> x \<le> b}"
                    "S \<inter> {x. a' \<bullet> x = b'} = S \<inter> {x. a \<bullet> x = b}"
                    "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S"
 proof (cases "S \<inter> {x. a \<bullet> x = b} = {}")

 
 lemma continuous_on_cases_local_open:
   assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
       and opT: "openin (subtopology euclidean (S \<union> T)) T"
       and contf: "continuous_on S f" and contg: "continuous_on T g"
-      and fg: "\<And>x. x \<in> S \<and> ~P x \<or> x \<in> T \<and> P x \<Longrightarrow> f x = g x"
+      and fg: "\<And>x. x \<in> S \<and> \<not>P x \<or> x \<in> T \<and> P x \<Longrightarrow> f x = g x"
     shows "continuous_on (S \<union> T) (\<lambda>x. if P x then f x else g x)"
 proof -
   have "\<And>x. x \<in> S \<Longrightarrow> (if P x then f x else g x) = f x"  "\<And>x. x \<in> T \<Longrightarrow> (if P x then f x else g x) = g x"
     by (simp_all add: fg)
   then have "continuous_on S (\<lambda>x. if P x then f x else g x)" "continuous_on T (\<lambda>x. if P x then f x else g x)"