Theory Points

(*
   Author: Mike Stannett
   Date: 22 October 2012
   m.stannett@sheffield.ac.uk
   Updated 28 June 2016 to run under Isabelle2016.
   Updates June & July 2020 for GenRel-NoFTL
   Refactored Feb 2023
*)

section ‹ Points ›

text ‹This theory defines (1+3)-dimensional spacetime points. The first
coordinate is the time coordinate, and the remaining three coordinates
give the spatial component.›

theory Points
  imports Sorts 
begin

(*
  A point has four coordinates, but can be thought of in different ways
*)
record 'a Point = 
  tval :: "'a"
  xval :: "'a"
  yval :: "'a"
  zval :: "'a"

  
record 'a Space =
  svalx :: "'a"
  svaly :: "'a"
  svalz :: "'a"


abbreviation tComponent :: "'a Point ⇒ 'a" where
  "tComponent p ≡ tval p"

abbreviation sComponent :: "'a Point ⇒ 'a Space" where
  "sComponent p ≡ ⦇ svalx = xval p, svaly = yval p, svalz = zval p ⦈"

abbreviation mkPoint :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a Point" where
  "mkPoint t x y z ≡ ⦇ tval = t, xval = x, yval =y, zval = z ⦈"

abbreviation stPoint :: "'a ⇒ 'a Space ⇒ 'a Point" where
  "stPoint t s ≡ mkPoint t (svalx s) (svaly s) (svalz s)"

abbreviation mkSpace :: "'a ⇒ 'a ⇒ 'a ⇒ 'a Space" where
  "mkSpace x y z ≡ ⦇ svalx = x, svaly =y, svalz = z ⦈"



text ‹ Points have coordinates in the field of quantities, 
and can be thought of as the end-points of
vectors pinned to the origin. We can translate and scale them, 
define accumulation points, etc.›

class Points = Quantities 
begin

(* Translations *)
abbreviation moveBy :: "'a Point ⇒ 'a Point ⇒ 'a Point" (‹_ ⊕ _›) where
"(p ⊕ q) ≡ ⦇ tval = tval p + tval q,
           xval = xval p + xval q,
           yval = yval p + yval q,
           zval = zval p + zval q ⦈"


abbreviation movebackBy :: "'a Point ⇒ 'a Point ⇒ 'a Point" (‹_ ⊖ _›) where
"(p ⊖ q)  ≡ ⦇ tval = tval p - tval q,
           xval = xval p - xval q,
           yval = yval p - yval q,
           zval = zval p - zval q ⦈"

  
abbreviation sMoveBy :: "'a Space ⇒ 'a Space ⇒ 'a Space" (‹_ ⊕s _›) where
"(p ⊕s q) ≡ ⦇ svalx = svalx p + svalx q,
              svaly = svaly p + svaly q,
              svalz = svalz p + svalz q ⦈"
  

abbreviation sMovebackBy :: "'a Space ⇒ 'a Space ⇒ 'a Space" (‹_ ⊖s _›) where
"(p ⊖s q) ≡ ⦇ svalx = svalx p - svalx q,
              svaly = svaly p - svaly q,
              svalz = svalz p - svalz q ⦈"
  

(* Scaling *)
abbreviation scaleBy :: "'a ⇒ 'a Point ⇒ 'a Point" (‹_ ⊗ _›)  where
  "scaleBy a p ≡ ⦇ tval = a*tval p, xval = a*xval p,
                   yval = a*yval p, zval = a*zval p⦈"

abbreviation sScaleBy :: "'a ⇒ 'a Space ⇒ 'a Space"  (‹ _ ⊗s _›) where
  "sScaleBy a p ≡ ⦇ svalx = a*svalx p,
                   svaly = a*svaly p, 
                   svalz = a*svalz p⦈"


(* Origins *)
abbreviation sOrigin :: "'a Space" where
  "sOrigin ≡ ⦇ svalx = 0, svaly = 0, svalz = 0 ⦈"
  
abbreviation origin :: "'a Point" where
"origin ≡ ⦇ tval = 0, xval = 0, yval = 0, zval = 0 ⦈"

abbreviation tUnit :: "'a Point" where
"tUnit ≡ ⦇ tval = 1, xval = 0, yval = 0, zval = 0 ⦈"

abbreviation xUnit :: "'a Point" where
"xUnit ≡ ⦇ tval = 0, xval = 1, yval = 0, zval = 0 ⦈"

abbreviation yUnit :: "'a Point" where
"yUnit ≡ ⦇ tval = 0, xval = 0, yval = 1, zval = 0 ⦈"

abbreviation zUnit :: "'a Point" where
"zUnit ≡ ⦇ tval = 0, xval = 0, yval = 0, zval = 1 ⦈"

(* Time Axis *)    

abbreviation timeAxis :: "'a Point set" where
"timeAxis ≡ { p . xval p = 0 ∧ yval p = 0 ∧ zval p = 0 }"

abbreviation onTimeAxis :: "'a Point ⇒ bool"
  where "onTimeAxis p ≡ (p ∈ timeAxis)"

(* Separation functions *)  
subsection ‹ Squared norms and separation functions ›

text ‹This theory defines squared norms and separations. We do not yet
define unsquared norms because we are not assuming here that quantities
necessarily have square roots.›

abbreviation norm2 :: "'a Point ⇒ 'a" where
  "norm2 p ≡ sqr (tval p) + sqr (xval p) + sqr (yval p) + sqr (zval p)"

abbreviation sep2 :: "'a Point ⇒ 'a Point ⇒ 'a" where
  "sep2 p q ≡ norm2 (p ⊖ q)"

abbreviation sNorm2 :: "'a Space ⇒ 'a" where
  "sNorm2 s ≡ sqr (svalx s)
            + sqr (svaly s)
            + sqr (svalz s)"

abbreviation sSep2 :: "'a Point ⇒ 'a Point ⇒ 'a" where
  "sSep2 p q ≡ sqr (xval p - xval q)
             + sqr (yval p - yval q)
             + sqr (zval p - zval q)" 

abbreviation mNorm2 :: "'a Point ⇒ 'a" (‹∥ _ ∥m›)
  where "∥ p ∥m ≡ sqr (tval p) - sNorm2 (sComponent p)"

subsection ‹ Topological concepts ›

text ‹We will need to define topological concepts like continuity and
affine approximation later, so here we define open balls and accumulation points.›

(* Open balls in Q^4 and accumulation points *)
abbreviation inBall :: "'a Point ⇒ 'a ⇒ 'a Point ⇒ bool"
(‹_ within _ of _›)
where "inBall q ε p ≡ sep2 q p < sqr ε"

abbreviation ball :: "'a Point ⇒ 'a ⇒ 'a Point set"
  where "ball q ε ≡ { p . inBall q ε p }"

abbreviation accPoint :: "'a Point ⇒ 'a Point set ⇒ bool"
  where "accPoint p s ≡ ∀ ε > 0. ∃ q ∈ s. (p ≠ q) ∧ (inBall q ε p)"

subsection ‹ Lines ›

text ‹ A line is specified by giving a point on the line, 
and a point (thought of as a vector) giving its direction. For
these purposes it doesn't matter whether the direction is "positive" 
or "negative". ›


abbreviation line :: "'a Point ⇒ 'a Point ⇒ 'a Point set"
  where "line base drtn ≡ { p . ∃ α . p = (base ⊕ (α⊗drtn)) }"

abbreviation lineJoining :: "'a Point ⇒ 'a Point ⇒ 'a Point set" 
  where "lineJoining p q ≡ line p (q⊖p)"

abbreviation isLine :: "'a Point set ⇒ bool" 
  where "isLine l ≡ ∃ b d . (l = line b d)"

abbreviation sameLine :: "'a Point set ⇒ 'a Point set ⇒ bool"
  where "sameLine l1 l2 ≡ ((isLine l1) ∨ (isLine l2)) ∧ (l1 = l2)"

abbreviation onLine :: "'a Point ⇒ 'a Point set ⇒ bool"
  where "onLine p l ≡ (isLine l) ∧ (p ∈ l)"

subsection ‹ Directions ›

text ‹ Given any two distinct points on a line, the vector joining them 
can be used to specify the line's direction. The direction of a line is
therefore a \emph{set} of points/vectors. By lemDrtn these are all parallel ›

fun drtn :: "'a Point set ⇒ 'a Point set"
  where "drtn l = { d . ∃ p q . (p ≠ q) ∧ (onLine p l) ∧ (onLine q l) ∧ (d = (q ⊖ p)) }"

abbreviation parallelLines :: "'a Point set ⇒ 'a Point set  ⇒ bool"
  where "parallelLines l1 l2 ≡ (drtn l1) ∩ (drtn l2) ≠ {}"

abbreviation parallel :: "'a Point ⇒ 'a Point ⇒ bool" (‹ _ ∥ _ ›)
  where "parallel p q ≡ (∃ α ≠ 0 . p = (α ⊗ q))"

text ‹The "slope" of a line can be either finite or infinite. We will often
need to consider these two cases separately.›

abbreviation slopeFinite :: "'a Point ⇒ 'a Point ⇒ bool" 
  where "slopeFinite p q ≡ (tval p ≠ tval q)"


abbreviation slopeInfinite :: "'a Point ⇒ 'a Point ⇒ bool" 
  where "slopeInfinite p q ≡ (tval p = tval q)"


abbreviation lineSlopeFinite :: "'a Point set ⇒ bool" 
  where "lineSlopeFinite l ≡ (∃ x y . (onLine x l) ∧ (onLine y l) 
                                ∧ (x ≠ y) ∧ (slopeFinite x y))"


(* "origin" indicates infinite slope (or else p = q) *)
subsection ‹ Slopes and slopers ›

text ‹We specify the slope of a line by giving the spatial component ("sloper") 
of the point on the line at time 1. This is defined if and only if the slope is finite. 
If the slope is infinite (the line is "horizontal") we return the spatial origin. This 
avoids using "option" but means we need to consider carefully whether a sloper with
value sOrigin indicates a truly zero slope or an infinite one.›

fun sloper :: "'a Point ⇒ 'a Point ⇒ 'a Point" 
  where "sloper p q = (if (slopeFinite p q) then ((1 / (tval p - tval q)) ⊗ (p ⊖ q))
                       else origin)"

fun velocityJoining :: "'a Point ⇒ 'a Point ⇒ 'a Space" 
  where "velocityJoining p q = sComponent (sloper p q)"  


fun lineVelocity :: "'a Point set ⇒ 'a Space set" 
  where "lineVelocity l = { v . ∃ d ∈ drtn l . v = velocityJoining origin d }"






(* ********************************************************************** *)
(* LEMMAS *)

lemma lemNorm2Decomposition:
  shows "norm2 u = sqr (tval u) + sNorm2 (sComponent u)"
  by (simp add: add_commute local.add.left_commute)



(* Structure *)

lemma lemPointDecomposition:
  shows "p = (((tval p)⊗tUnit) ⊕ (((xval p)⊗xUnit) 
                     ⊕ (((yval p)⊗yUnit) ⊕ ((zval p)⊗zUnit))))"
  by force


(* Arithmetic *)

lemma lemScaleLeftSumDistrib: "((a + b) ⊗ p) = ((a⊗p) ⊕ (b⊗p))"
  using distrib_right by auto

lemma lemScaleLeftDiffDistrib: "((a - b) ⊗ p) = ((a⊗p) ⊖ (b⊗p))"
  using left_diff_distrib by auto

lemma lemScaleAssoc: "(α ⊗ (β ⊗ p)) = ((α * β) ⊗ p)"
  using semiring_normalization_rules(18) by auto

lemma lemScaleCommute: "(α ⊗ (β ⊗ p)) = (β ⊗ (α ⊗ p))"
  using mult.left_commute by auto

lemma lemScaleDistribSum: "(α ⊗ (p ⊕ q)) = ((α⊗p) ⊕ (α⊗q))"
  using distrib_left by auto

lemma lemScaleDistribDiff: "(α ⊗ (p ⊖ q)) = ((α⊗p) ⊖ (α⊗q))"
  using right_diff_distrib by auto

lemma lemScaleOrigin: "(α ⊗ origin) = origin"
  by auto

(* Scaling *)
lemma lemMNorm2OfScaled: "mNorm2 (scaleBy α p) = (sqr α) * mNorm2 p"
  using lemSqrMult distrib_left right_diff_distrib' by simp

lemma lemSNorm2OfScaled: "sNorm2 (sScaleBy α p) = (sqr α) * sNorm2 p"
  using lemSqrMult distrib_left by auto

lemma lemNorm2OfScaled: "norm2 (α ⊗ p) = (sqr α) * norm2 p"
  using lemSqrMult distrib_left by auto

lemma lemScaleSep2: "(sqr a) * (sep2 p q) = sep2 (a⊗p) (a⊗q)"
  using lemNorm2OfScaled[of "a" "p⊖q"] lemScaleDistribDiff by auto

lemma lemSScaleAssoc: "(α ⊗s (β ⊗s p)) = ((α * β) ⊗s p)"
  using semiring_normalization_rules(18) by auto



lemma lemScaleBall: 
  assumes "x within e of y"
and       "a ≠ 0"
shows     "(a⊗x) within (a*e) of (a⊗y)"
proof - 
  have a2pos: "sqr a > 0" using assms(2) lemSquaresPositive by auto
  have "sep2 (a⊗x) (a⊗y) = (sqr a) * (sep2 x y)" using lemScaleSep2 by auto
  hence "sep2 (a⊗x) (a⊗y) < (sqr a) * (sqr e)"
    using assms mult_strict_left_mono a2pos by auto
  thus ?thesis using mult_commute mult_assoc by auto
qed


lemma lemScaleBallAndBoundary: 
  assumes "sep2 x y ≤ sqr e"
and       "a ≠ 0"
shows     "sep2 (a⊗x) (a⊗y) ≤ sqr (a*e)"
proof - 
  have a2pos: "sqr a > 0" using assms(2) lemSquaresPositive by auto
  have "sep2 (a⊗x) (a⊗y) = (sqr a) * (sep2 x y)" using lemScaleSep2 by auto
  hence "sep2 (a⊗x) (a⊗y) ≤ (sqr a) * (sqr e)"
    using assms mult_left_mono a2pos by auto
  thus ?thesis using mult_commute mult_assoc by auto
qed



(* lines *)

lemma lemTimeAxisIsLine: "isLine timeAxis"
proof -
  { fix p
    { assume p: "p ∈ timeAxis"
      hence "p = (origin ⊕ ((tval p) ⊗ tUnit))" by auto
    }
    hence l2r: "onTimeAxis p ⟶ (∃ v . (p = (origin ⊕ (v ⊗ tUnit))))" by blast

    { assume v: "∃ v . p = (origin ⊕ (v ⊗ tUnit))"
      hence "onTimeAxis p" by auto
    }
    hence "(∃ v . (p = (origin ⊕ (v ⊗ tUnit)))) ⟷ onTimeAxis p" 
      using l2r by blast
  }
  hence "timeAxis = line origin tUnit" by blast
  thus ?thesis by blast
qed



lemma lemSameLine:
  assumes "p ∈ line b d"
shows     "sameLine (line b d) (line p d)"
proof -
  define l1 where l1: "l1 = line b d"
  define l2 where l2: "l2 = line p d"
  have lines: "isLine l1 ∧ isLine l2" using l1 l2 by blast

  obtain A where p: "p = (b ⊕ (A ⊗ d))" using assms by auto
  hence b: "b = (p ⊖ (A ⊗ d))" by auto

  { fix x
    { assume x: "x ∈ l1"
      then obtain a where a: "x = (b ⊕ (a⊗d))" using l1 by auto
      hence "x = ((p ⊖ (A ⊗ d)) ⊕ (a⊗d))" using b by simp
      also have "… = (p ⊕ ((a⊗d)⊖(A⊗d)))" 
        using add_diff_eq diff_add_eq add_commute add_assoc by simp
      finally have "x = (p ⊕ ((a-A)⊗d))" 
        using lemScaleLeftDiffDistrib by presburger
      hence "x ∈ l2" using l2 by auto
    }
    hence l2r: "(x ∈ l1) ⟶ (x ∈ l2)" using l2 by simp

    { assume x: "x ∈ l2"
      then obtain a where a: "x = (p ⊕ (a ⊗ d))" using l2 by auto
      hence "x = (b ⊕ ((A+ a)⊗d))"
        using p add_assoc lemScaleAssoc distrib by auto
      hence "x ∈ l1" using l1 by auto
    }
    hence "(x ∈ l1) ⟷ (x ∈ l2)" using l2r by auto
  }
  thus ?thesis using lines l1 l2 by auto
qed


(* Separation symmetry lemmas *)


lemma lemSSep2Symmetry: "sSep2 p q = sSep2 q p"
  using lemSqrDiffSymmetrical by simp

lemma lemSep2Symmetry: "sep2 p q = sep2 q p"
  using lemSqrDiffSymmetrical by simp


(* Only origin has zero size *)
lemma lemSpatialNullImpliesSpatialOrigin:
assumes "sNorm2 s = 0"
shows "s = sOrigin" 
  using assms local.add_nonneg_eq_0_iff by auto


lemma lemNorm2NonNeg: "norm2 p ≥ 0"
  by simp


lemma lemNullImpliesOrigin:
assumes "norm2 p = 0"
shows "p = origin"
proof -
  have "norm2 p = sqr (tval p) + sNorm2 (sComponent p)" using add_assoc by simp
  hence a: "sqr (tval p) + sNorm2 (sComponent p) = 0" using assms by auto
  { assume b: "sNorm2 (sComponent p) > 0"
    have "sqr (tval p) + sNorm2 (sComponent p) > 0"
      using b lemSumOfNonNegAndPos by auto
    hence "False" using a by auto
  }
  hence c: "¬(sNorm2 (sComponent p) > 0)" by auto
  have d: "sNorm2 (sComponent p) ≥ 0" by auto
  
  have "∀ x . (¬(x > 0))  ∧  (x ≥ 0)  ⟶  x = 0" by auto
  hence e: "sNorm2 (sComponent p) = 0" using c d by force
  hence f: "sComponent p = sOrigin" 
    using lemSpatialNullImpliesSpatialOrigin by blast
  
  have     "norm2 p = sqr (tval p)" using e add_assoc by auto
  hence    "sqr (tval p) = 0" using assms  by simp
  hence    "(tval p) = 0" using lemZeroRoot by simp
  
  thus ?thesis using f by auto
qed


lemma lemNotOriginImpliesPosNorm2:
assumes "p ≠ origin"
shows "norm2 p > 0"
proof -
have 1: "norm2 p ≥ 0" by simp
have 2: "norm2 p ≠ 0" using assms(1) lemNullImpliesOrigin by force
thus ?thesis using 1 2 dual_order.not_eq_order_implies_strict by fast
qed


lemma lemNotEqualImpliesSep2Pos:
  assumes "y ≠ x"
  shows "sep2 y x > 0"
proof -
  have "(y⊖x) ≠ origin" using assms by auto
  hence 1: "norm2 (y⊖x) > 0" using lemNotOriginImpliesPosNorm2 by fast
  have "sep2 y x = norm2 (y⊖x)" by auto
  thus ?thesis using 1 by auto
qed


lemma lemBallContainsCentre:
  assumes "ε > 0"
  shows "x within ε of x"
proof -
  have "sep2 x x = 0" by auto
  thus ?thesis using assms by auto
qed


lemma lemPointLimit:
  assumes "∀ ε > 0 . (v within ε of u)"
  shows "v = u"
proof -
  define d where d: "d = sep2 v u"
  { assume "v ≠ u"
    hence "d > 0" using lemNotEqualImpliesSep2Pos d by auto
    then obtain s where s: "(0 < s) ∧ (sqr s < d)" using lemSmallSquares by auto
    hence "v within s of u" using d assms(1) by auto
    hence "sep2 v u < sep2 v u" using s d by auto
    hence "False" by auto
  }
  thus ?thesis by auto
qed


lemma lemBallPopulated:
  assumes "e > 0"
  shows "∃ y . (y within e of x) ∧ (y ≠ x)"
proof -
  obtain e1 where e1: "(0 < e1) ∧ (e1 < e) ∧ (sqr e1 < e1)" 
    using assms lemReducedBound by auto
  hence e2: "sqr e1 < sqr e" using lemSqrMonoStrict[of "e1" "e"] by auto

  define y where y: "y = (x ⊕ ⦇ tval = e1, xval=0, yval=0, zval=0 ⦈)"
  hence "(y ⊖ x) = ⦇ tval = e1, xval=0, yval=0, zval=0 ⦈" by auto
  hence "sep2 y x = sqr e1" by auto
  hence 1: "y within e of x" using e2  by auto

  have "tval y = tval x + e1" using y by simp
  hence "y ≠ x" using e1 by auto
  thus ?thesis using 1 by auto
qed

lemma lemBallInBall:
  assumes "p within x of q"
and       "0 < x ≤ y"
shows     "p within y of q"
proof -
  have "sqr x ≤ sqr y" using assms(2) lemSqrMono by auto
  thus ?thesis using le_less_trans using assms(1) by auto
qed



lemma lemSmallPoints:
  assumes "e > 0"
  shows "∃ a > 0 . norm2 (a⊗p) < sqr e"
proof -

  { assume po: "p = origin"
    define a where a: "a = 1"
    hence apos: "a > 0" by auto
    have "norm2 (a⊗p) < sqr e" using a po assms by auto
    hence ?thesis using apos by auto
  }
  hence case1: "p = origin ⟶ ?thesis" by auto

  { assume pnoto: "p ≠ origin"

    obtain e1 where e1: "(e1 > 0) ∧ (e1 < e) ∧ (sqr e1 < e1)" 
      using lemReducedBound assms by auto
    hence e1sqr: "0 < (sqr e1) < (sqr e)" using lemSqrMonoStrict by auto

    define n2 where n2: "n2 = norm2 p"
    hence n2pos: "n2 > 0" using pnoto lemNotOriginImpliesPosNorm2 by auto
    then obtain s where s: "(s > 0) ∧ (sqr s > n2)" 
      using lemSquareExistsAbove by auto
    hence "0 < (n2/(sqr s)) < 1" using n2pos by auto
    hence "(sqr e1)*(n2/(sqr s)) < sqr e1" 
      using lemMultPosLT1[of "sqr e1" "(n2/(sqr s))"] e1sqr by auto
    hence ineq: "(sqr e1)*(n2/(sqr s)) < sqr e" using e1sqr by auto

    define a where a: "a = e1/s"
    have "e1 > 0 ∧ s > 0" using e1 s by auto
    hence apos: "a > 0" using a by auto
    have "norm2 (a⊗p) = (sqr e1)*(n2/(sqr s))" 
      using lemNorm2OfScaled[of "a"] a n2 by auto
    hence "norm2 (a⊗p) < sqr e" using ineq by auto
    hence ?thesis using apos by auto
  }
  hence "p ≠ origin ⟶ ?thesis" by auto

  thus ?thesis using case1 by auto
qed


lemma lemLineJoiningContainsEndPoints:
  assumes "l = lineJoining x p"
  shows "onLine x l ∧ onLine p l"
proof -
  have line: "isLine l" using assms(1) by blast
  have p: "x = (x ⊕ (0 ⊗ (p⊖x)))" by simp
  have x: "p = (x ⊕ (1 ⊗ (p⊖x)))" using add_commute diff_add_cancel by fastforce
  thus ?thesis using p line assms(1) by blast
qed


lemma lemLineAndPoints:
  assumes "p ≠ q"
  shows   "(onLine p l ∧ onLine q l) ⟷ (l = lineJoining p q)"
proof -
  
  define lj  where lj : "lj  = lineJoining p q"
  define lhs where lhs: "lhs = (onLine p l ∧ onLine q l)"
  define rhs where rhs: "rhs = (l = lj)"

  { assume hyp: "lhs"
    then obtain b d where bd: "l = { x. ∃ a. x = (b ⊕ (a⊗d)) }" using lhs by auto

    obtain ap where ap: "p = (b ⊕ (ap ⊗ d))" using hyp lhs bd by auto
    obtain aq where aq: "q = (b ⊕ (aq ⊗ d))" using hyp lhs bd by auto
    hence "(q⊖p) = ((b ⊕ (aq ⊗ d)) ⊖  (b ⊕ (ap ⊗ d)))" using ap by fast
    also have "... = ((aq ⊗ d) ⊖ (ap ⊗ d))" using add_diff_cancel by auto
    finally have qdiffp: "(q⊖p) = ((aq - ap) ⊗ d)" 
      using lemScaleLeftDiffDistrib[of "aq" "ap" "d"] by auto

    define R where R: "R = aq - ap"
    hence Rnz: "R ≠ 0" using assms(1) qdiffp by auto
    define r where r: "r = 1/R"
    hence "(r⊗(R ⊗ d)) = (r ⊗ (q⊖p))" using R qdiffp by auto
    hence d: "d = (r ⊗ (q⊖p))" using lemScaleAssoc[of "r" "R" "d"] r Rnz by force

    have "b = (p ⊖ (ap ⊗ d))" using ap by auto
    also have "... = (p ⊖ (ap ⊗ (r ⊗ (q⊖p))))" using d by auto
    finally have b: "b = (p ⊖ ( (ap*r) ⊗ (q⊖p)))" 
      using lemScaleAssoc[of "ap" "r" "q⊖p"] by auto

    { fix x
      assume "x ∈ l"
      then obtain a where "x = (b ⊕ (a ⊗ d))" using bd by auto
      hence "x = ((p ⊖ ((ap*r) ⊗ (q⊖p))) ⊕ ((a*r) ⊗ (q⊖p)))"
        using b d lemScaleAssoc[of "a" "r" "q⊖p"] by fastforce
      also have "... = (p ⊕ ( ((a*r)⊗(q⊖p)) ⊖ ((ap*r)⊗(q⊖p)) ))"
        using add_diff_eq diff_add_eq by force
      also have "... = (p ⊕ (((a*r)-(ap*r))⊗(q⊖p)))"
        using left_diff_distrib by force
      finally have "x ∈ lj" using lj by auto
    }
    hence l2r: "l ⊆ lj" by auto

    { fix x
      assume "x ∈ lj"
      then obtain a where a: "x = (p ⊕ (a ⊗(q⊖p)))" using lj by auto
      hence "x = ((b ⊕ (ap ⊗ d)) ⊕ (a ⊗(R ⊗ d)))" using ap qdiffp R by auto
      also have "... = (b ⊕ ((ap + a*R)⊗d))" 
        using add_assoc distrib_right lemScaleAssoc
        by auto
      finally have "onLine x l" using bd by auto
    }
    hence "lj ⊆ l" by auto
    hence "l = lj" using l2r by auto
  }
  hence L2R: "lhs ⟶ rhs" using rhs by auto

  { assume l: "rhs"
    hence line: "isLine l" using rhs lj by blast
    have p: "p = (p ⊕ (0 ⊗ (q⊖p)))" by simp
    have q: "q = (p ⊕ (1 ⊗ (q⊖p)))" using add_commute diff_add_cancel by fastforce
    hence "lhs" using p line l lhs rhs lj by blast
  }
  hence "rhs ⟶ lhs" by auto

  hence "lhs ⟷ rhs" using L2R by auto

  thus ?thesis using lhs rhs lj by auto
qed



lemma lemLineDefinedByPair:
  assumes "x ≠ p"
and       "(onLine p l1) ∧ (onLine x l1)"
and       "(onLine p l2) ∧ (onLine x l2)"
  shows "l1 = l2"
proof - 
  have "l1 = lineJoining x p" 
    using lemLineAndPoints[of "x" "p" "l1"] assms(1) assms(2) by auto
  also have "... = l2" 
    using lemLineAndPoints[of "x" "p" "l2"] assms(1) assms(3) by auto
  finally show "l1 = l2" by auto
qed


lemma lemDrtn: 
  assumes "{ d1, d2 } ⊆ drtn l" 
  shows "∃ α ≠ 0 . d2 = (α ⊗ d1)"
proof -
  have d1d2: "{d1,d2} ⊆ { d . ∃ p q . (p ≠ q) ∧ onLine p l ∧ onLine q l ∧ (d = (q ⊖ p)) }"
    using assms(1) by auto
  have d1: "∃ p1 q1 . (p1 ≠ q1) ∧ (onLine p1 l) ∧ (onLine q1 l) ∧ (d1 = (q1 ⊖ p1))"
    using d1d2 by auto
  then obtain p1 q1 
    where pq1: "(p1 ≠ q1) ∧ (onLine p1 l) ∧ (onLine q1 l) ∧ (d1 = (q1 ⊖ p1))"
    by blast
  hence l1: "l = lineJoining p1 q1" using lemLineAndPoints[of "p1" "q1" "l"] by auto

  have d2: "∃ p2 q2 . (p2 ≠ q2) ∧ (onLine p2 l) ∧ (onLine q2 l) ∧ (d2 = (q2 ⊖ p2))"
    using d1d2 by auto
  then obtain p2 q2 
    where pq2: "(p2 ≠ q2) ∧ (onLine p2 l) ∧ (onLine q2 l) ∧ (d2 = (q2 ⊖ p2))"
    by blast

  hence "(p2 ∈ lineJoining p1 q1) ∧ (q2 ∈ lineJoining p1 q1)" using l1 by blast
  then obtain ap aq 
    where apaq: "(p2 = (p1 ⊕ (ap⊗(q1⊖p1)))) ∧ ((q2 = (p1 ⊕ (aq⊗(q1⊖p1)))))"
    by blast

  define diff where diff: "diff = aq - ap"
  hence diffnz: "diff ≠ 0" using apaq pq2 by auto

  have "d2 = (q2 ⊖ p2)" using pq2 by simp
  also have "... = ((p1 ⊕ (aq⊗(q1⊖p1))) ⊖ (p1 ⊕ (ap⊗(q1⊖p1))))" using apaq by force
  also have "... = ((aq⊗(q1⊖p1)) ⊖ (ap⊗(q1⊖p1)))" by auto
  also have "... = ((aq - ap) ⊗ d1)" 
    using pq1 lemScaleLeftDiffDistrib[ of "aq" "ap" "d1"] by auto
  finally have "(d2 = (diff ⊗ d1)) ∧ (diff ≠ 0)" using diff diffnz by auto

  thus ?thesis by auto
qed


lemma lemLineDeterminedByPointAndDrtn:
  assumes "(x ≠ p) ∧ (p ∈ l1) ∧ (onLine x l1) ∧ (onLine x l2)"
and       "drtn l1 = drtn l2"
shows     "l1 = l2"
proof - 
  define d1 where d1: "d1 = drtn l1"
  define d2 where d2: "d2 = drtn l2"
  hence dd: "d1 = d2" using assms(2) d1 by auto

  define px where px: "px = (p ⊖ x)"

  have l1: "(x ≠ p) ∧ (onLine p l1) ∧ (onLine x l1)" using assms(1) by auto
  hence "∃ p q . (p ≠ q) ∧ onLine p l1 ∧ onLine q l1 ∧ (px = (q ⊖ p))" using px by blast
  hence "px ∈ { d . ∃ p q . (p ≠ q) ∧ onLine p l1 ∧ onLine q l1 ∧ (d = (q ⊖ p)) }" 
    by blast
  hence "px ∈ d1" using d1 subst[of "d1" "drtn l1" "λs. px ∈ s"] by auto
  hence "px ∈ d2" using dd by simp
  hence pxonl2: "px ∈ drtn l2" using d2 by simp
  hence "∃ u v . (u ≠ v) ∧ onLine u l2 ∧ onLine v l2 ∧ (px = (v ⊖ u))" by auto
  then obtain u v where uv: "(u ≠ v) ∧ onLine u l2 ∧ onLine v l2 ∧ (px = (v ⊖ u))" by blast

  hence "(x ≠ u) ∨ (x ≠ v)" by blast
  then obtain w where w: "((w = u) ∨ (w = v)) ∧ (x ≠ w)" by blast
  hence xw: "(x ≠ w) ∧ (onLine x l2) ∧ (onLine w l2)" using uv assms(1) by blast
  hence l2: "l2 = lineJoining x w" using lemLineAndPoints[of "x" "w" "l2"] by auto
  hence "(w ⊖ x) ∈ drtn l2 ∧ px ∈ drtn l2" using xw pxonl2 by auto
  then obtain a where a: "(a ≠ 0) ∧  (p ⊖ x) = (a ⊗ (w ⊖ x))" 
    using lemDrtn[of "w⊖x" "p⊖x" "l2"] px xw pxonl2 by blast
  hence "p = (x ⊕ (a ⊗ (w ⊖ x)))" by (auto simp add: field_simps)
  hence "onLine p (lineJoining x w)" by blast

  hence l2lj: "l2 = lineJoining x p" 
    using lemLineAndPoints[of "x" "p" "l2"] assms(1) l2 xw
    by auto

  have l1lj: "l1 = lineJoining x p"
    using lemLineAndPoints[of "x" "p" "l1"] assms(1)
    by auto

  thus ?thesis using l2lj by blast
qed

end (* of class Points *)

end (* of theory Points *)