author nipkow Thu, 05 Dec 2019 19:53:41 +0100 changeset 71241 d9e747cafb04 parent 71239 acc6cb1a1a67 (current diff) parent 71240 67880e7ee08d (diff) child 71242 ec5090faf541
merged
```--- a/src/HOL/Analysis/Convex.thy	Thu Dec 05 12:09:35 2019 +0000
+++ b/src/HOL/Analysis/Convex.thy	Thu Dec 05 19:53:41 2019 +0100
@@ -2887,14 +2887,11 @@
done
qed

-lemma affine_hull_nonempty: "S \<noteq> {} \<longleftrightarrow> affine hull S \<noteq> {}"
-proof -
-  have "S = {} \<Longrightarrow> affine hull S = {}"
-    using affine_hull_empty by auto
-  moreover have "affine hull S = {} \<Longrightarrow> S = {}"
-    unfolding hull_def by auto
-  ultimately show ?thesis by blast
-qed
+lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
+by (metis affine_empty subset_empty subset_hull)
+
+lemma empty_eq_affine_hull[simp]: "{} = affine hull S \<longleftrightarrow> S = {}"
+by (metis affine_hull_eq_empty)

lemma aff_dim_parallel_subspace_aux:
fixes B :: "'n::euclidean_space set"
@@ -2939,7 +2936,7 @@
B: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1"
using aff_dim_basis_exists by auto
then have "B \<noteq> {}"
-    using assms B affine_hull_nonempty[of V] affine_hull_nonempty[of B]
+    using assms B
by auto
then obtain a where a: "a \<in> B" by auto
define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
@@ -2951,7 +2948,7 @@
moreover have "subspace Lb"
using Lb_def subspace_span by auto
moreover have "affine hull B \<noteq> {}"
-    using assms B affine_hull_nonempty[of V] by auto
+    using assms B by auto
ultimately have "L = Lb"
using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B
by auto
@@ -3031,7 +3028,7 @@
using aff_dim_basis_exists by auto
moreover
from * have "S = {} \<longleftrightarrow> B = {}"
-    using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto
+    by auto
ultimately show ?thesis
using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
qed
@@ -3054,7 +3051,7 @@
proof (cases "B = {}")
case True
then have "V = {}"
-    using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms
+    using assms
by auto
then have "aff_dim V = (-1::int)"
using aff_dim_empty by auto
@@ -3140,7 +3137,7 @@
assume "T \<noteq> {}" "S \<noteq> {}"
then obtain L where L: "subspace L \<and> affine_parallel (affine hull T) L"
using affine_parallel_subspace[of "affine hull T"]
-        affine_affine_hull[of T] affine_hull_nonempty
+        affine_affine_hull[of T]
by auto
then have "aff_dim T = int (dim L)"
using aff_dim_parallel_subspace \<open>T \<noteq> {}\<close> by auto
@@ -3154,7 +3151,7 @@
{
assume "S = {}"
then have "S = {}" and "T = {}"
-      using assms affine_hull_nonempty
+      using assms
unfolding affine_parallel_def
by auto
then have ?thesis using aff_dim_empty by auto
@@ -3163,7 +3160,7 @@
{
assume "T = {}"
then have "S = {}" and "T = {}"
-      using assms affine_hull_nonempty
+      using assms
unfolding affine_parallel_def
by auto
then have ?thesis```
```--- a/src/HOL/Analysis/Starlike.thy	Thu Dec 05 12:09:35 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Thu Dec 05 19:53:41 2019 +0100
@@ -3842,9 +3842,6 @@
by (simp add: collinear_subset)
qed

-lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
-  using affine_hull_nonempty by blast
-
lemma affine_hull_2_alt:
fixes a b :: "'a::real_vector"
shows "affine hull {a,b} = range (\<lambda>u. a + u *\<^sub>R (b - a))"```