src/HOL/Analysis/Linear_Algebra.thy
 changeset 66287 005a30862ed0 parent 65680 378a2f11bec9 child 66297 d425bdf419f5
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Jul 18 11:35:32 2017 +0200
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jul 19 16:41:26 2017 +0100
1.3 @@ -3140,6 +3140,44 @@
1.4  definition collinear :: "'a::real_vector set \<Rightarrow> bool"
1.5    where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
1.6
1.7 +lemma collinear_alt:
1.8 +     "collinear S \<longleftrightarrow> (\<exists>u v. \<forall>x \<in> S. \<exists>c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs")
1.9 +proof
1.10 +  assume ?lhs
1.11 +  then show ?rhs
1.12 +    unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel)
1.13 +next
1.14 +  assume ?rhs
1.15 +  then obtain u v where *: "\<And>x. x \<in> S \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v"
1.16 +    by (auto simp: )
1.17 +  have "\<exists>c. x - y = c *\<^sub>R v" if "x \<in> S" "y \<in> S" for x y
1.18 +        by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left)
1.19 +  then show ?lhs
1.20 +    using collinear_def by blast
1.21 +qed
1.22 +
1.23 +lemma collinear:
1.24 +  fixes S :: "'a::{perfect_space,real_vector} set"
1.25 +  shows "collinear S \<longleftrightarrow> (\<exists>u. u \<noteq> 0 \<and> (\<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u))"
1.26 +proof -
1.27 +  have "\<exists>v. v \<noteq> 0 \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v)"
1.28 +    if "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R u" "u=0" for u
1.29 +  proof -
1.30 +    have "\<forall>x\<in>S. \<forall>y\<in>S. x = y"
1.31 +      using that by auto
1.32 +    moreover
1.33 +    obtain v::'a where "v \<noteq> 0"
1.34 +      using UNIV_not_singleton [of 0] by auto
1.35 +    ultimately have "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v"
1.36 +      by auto
1.37 +    then show ?thesis
1.38 +      using \<open>v \<noteq> 0\<close> by blast
1.39 +  qed
1.40 +  then show ?thesis
1.41 +    apply (clarsimp simp: collinear_def)
1.42 +    by (metis real_vector.scale_zero_right vector_fraction_eq_iff)
1.43 +qed
1.44 +
1.45  lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
1.46    by (meson collinear_def subsetCE)
1.47
```