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