src/HOL/Analysis/Convex_Euclidean_Space.thy

 
 lemma affine_hyperplane: "affine {x. a \<bullet> x = b}"
   by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
 
 
-subsubsection%unimportant \<open>Some explicit formulations (from Lars Schewe)\<close>
+subsubsection%unimportant \<open>Some explicit formulations\<close>
+
+text "Formalized by Lars Schewe."
 
 lemma affine:
   fixes V::"'a::real_vector set"
   shows "affine V \<longleftrightarrow>
          (\<forall>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> V \<and> sum u S = 1 \<longrightarrow> (\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V)"

   then show ?thesis
     using False cone_iff[of "closure S"] by auto
 qed
 
 
-subsection \<open>Affine dependence and consequential theorems (from Lars Schewe)\<close>
+subsection \<open>Affine dependence and consequential theorems\<close>
+
+text "Formalized by Lars Schewe."
 
 definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
   where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
 
 lemma affine_dependent_subset:

 apply (simp add: affine_dependent_def Bex_def)
 apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]])
 done
 
 lemma affine_independent_subset:
-  shows "\<lbrakk>~ affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> ~ affine_dependent s"
+  shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
 by (metis affine_dependent_subset)
 
 lemma affine_independent_Diff:
-   "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
+   "\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
 by (meson Diff_subset affine_dependent_subset)
 
 proposition affine_dependent_explicit:
   "affine_dependent p \<longleftrightarrow>
     (\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"

              (\<Sum>x\<in>S. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>S. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>S. uy x *\<^sub>R x)"
     by (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI, auto)
 qed (use assms in \<open>auto simp: convex_explicit\<close>)
 
 
-subsubsection%unimportant \<open>Another formulation from Lars Schewe\<close>
+subsubsection%unimportant \<open>Another formulation\<close>
+
+text "Formalized by Lars Schewe."
 
 lemma convex_hull_explicit:
   fixes p :: "'a::real_vector set"
   shows "convex hull p =
     {y. \<exists>S u. finite S \<and> S \<subseteq> p \<and> (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"

   shows "of_nat (card B) = aff_dim B + 1"
   using aff_dim_unique[of B B] assms by auto
 
 lemma affine_independent_iff_card:
     fixes s :: "'a::euclidean_space set"
-    shows "~ affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
+    shows "\<not> affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
   apply (rule iffI)
   apply (simp add: aff_dim_affine_independent aff_independent_finite)
   by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
 
 lemma aff_dim_sing [simp]:

     by (rule that[OF \<open>a \<noteq> 0\<close>])
 qed
 
 lemma affine_independent_card_dim_diffs:
   fixes S :: "'a :: euclidean_space set"
-  assumes "~ affine_dependent S" "a \<in> S"
+  assumes "\<not> affine_dependent S" "a \<in> S"
     shows "card S = dim {x - a|x. x \<in> S} + 1"
 proof -
   have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
   have 2: "x - a \<in> span {b - a |b. b \<in> S - {a}}" if "x \<in> S" for x
   proof (cases "x = a")

   case False
   then obtain a where "a \<in> S" by auto
   show ?thesis
   proof safe
     assume 0: "aff_dim S = 0"
-    have "~ {a,b} \<subseteq> S" if "b \<noteq> a" for b
+    have "\<not> {a,b} \<subseteq> S" if "b \<noteq> a" for b
       by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that)
     then show "\<exists>a. S = {a}"
       using \<open>a \<in> S\<close> by blast
   qed auto
 qed

     by auto
 qed
 
 lemma disjoint_affine_hull:
   fixes s :: "'n::euclidean_space set"
-  assumes "~ affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
+  assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
     shows "(affine hull t) \<inter> (affine hull u) = {}"
 proof -
   have "finite s" using assms by (simp add: aff_independent_finite)
   then have "finite t" "finite u" using assms finite_subset by blast+
   { fix y

       by (auto simp: affine_hull_finite \<open>finite t\<close> \<open>finite u\<close>)
     define c where "c x = (if x \<in> t then a x else if x \<in> u then -(b x) else 0)" for x
     have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u" using assms by auto
     have "sum c s = 0"
       by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
-    moreover have "~ (\<forall>v\<in>s. c v = 0)"
+    moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
       by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum_not_0 zero_neq_one)
     moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
       by (simp add: c_def if_smult sum_negf
              comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
     ultimately have False

     apply (erule_tac x="-b" in allE, auto)
     done
 qed auto
 
 
-subsection \<open>Radon's theorem (from Lars Schewe)\<close>
+subsection \<open>Radon's theorem\<close>
+
+text "Formalized by Lars Schewe."
 
 lemma radon_ex_lemma:
   assumes "finite c" "affine_dependent c"
   shows "\<exists>u. sum u c = 0 \<and> (\<exists>v\<in>c. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) c = 0"
 proof -