author wenzelm Thu, 04 Mar 2021 22:44:31 +0100 changeset 73372 10b9b3341c26 parent 73371 70c801965fec child 73373 3bb9df8900fd
tuned proofs;
```--- a/src/HOL/Analysis/Affine.thy	Thu Mar 04 22:03:33 2021 +0100
+++ b/src/HOL/Analysis/Affine.thy	Thu Mar 04 22:44:31 2021 +0100
@@ -1612,26 +1612,29 @@
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
-    assume yt: "y \<in> affine hull t" and yu: "y \<in> affine hull u"
-    then obtain a b
-           where a1 [simp]: "sum a t = 1" and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
-             and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
+  from assms(1) have "finite s"
+  with assms(2,3) have "finite t" "finite u"
+    by (blast intro: finite_subset)+
+  have False if "y \<in> affine hull t" and "y \<in> affine hull u" for y
+  proof -
+    from that obtain a b
+      where a1 [simp]: "sum a t = 1"
+        and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
+        and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = 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
+    from assms(2,3,4) have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u"
+      by auto
have "sum c s = 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.neutral zero_neq_one)
moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
-      by (simp add: c_def if_smult sum_negf