Theory WorldLine

(*
   Mike Stannett, April 2020
   Updated: Jan 2023
*)

section ‹ WorldLine ›

text ‹This theory defines worldlines.›

theory WorldLine
  imports WorldView Functions
begin


class WorldLine = WorldView + Functions
begin

abbreviation wline :: "Body ⇒ Body ⇒ 'a Point set"
  where "wline m k ≡ { p . m sees k at p }"

(* Lemmas *)
lemma lemWorldLineUnderWVT: 
  shows "applyToSet (wvtFunc m k) (wline m b) ⊆  wline k b"
  by auto

lemma lemFiniteLineVelocityUnique:
  assumes "(u ∈ lineVelocity l) ∧ (v ∈ lineVelocity l)"
and       "lineSlopeFinite l"
  shows   "u = v"
proof - 
  have "∃ d1 ∈ drtn l . u = velocityJoining origin d1" using assms by simp
  then obtain d1 
    where d1: "d1 ∈ drtn l ∧ u = velocityJoining origin d1" by blast

  have "∃ d2 ∈ drtn l . v = velocityJoining origin d2" using assms by simp
  then obtain d2 
    where d2:  "d2 ∈ drtn l ∧ v = velocityJoining origin d2" by blast

  hence "(d1 ∈ drtn l) ∧ (d2 ∈ drtn l)" using d1 d2 by auto

  then obtain a where a: "(a ≠ 0) ∧ (d2 = (a ⊗ d1))" 
    using lemDrtn[of "d1" "d2" "l"] by blast

(* TODO: Show that the slopes are finite *)
  have slopes: "(tval d1 ≠ 0) ∧ (tval d2 ≠ 0) 
                  ∧ (slopeFinite origin d1) ∧ (slopeFinite origin d2)"
  proof -
    obtain x y where xy: "(x ≠ y) ∧ (onLine x l) ∧ (onLine y l) ∧ (slopeFinite x y)"
      using assms(2) by blast
    hence "slopeFinite x y" by blast
    hence tvalnz: "tval y - tval x ≠ 0" by simp

    define yx where "yx = (y⊖x)"
    hence "(x ≠ y) ∧ (onLine x l) ∧ (onLine y l) ∧ (yx = (y ⊖ x))" using xy by simp
    hence "∃ x y . (x ≠ y) ∧ (onLine x l) ∧ (onLine y l) ∧ (yx = (y ⊖ x))" by blast
    hence "(y ⊖ x) ∈ drtn l" using yx_def by auto
    then obtain b where b: "(b ≠ 0) ∧ (d2 = (b ⊗ (y⊖x)))" 
      using d2 lemDrtn[of "y⊖x" "d2" "l"] by blast

    hence tval2: "tval d2 ≠ tval origin" using tvalnz b by simp
    hence tval1: "tval d1 ≠ tval origin" using a by auto
    hence finite: "(slopeFinite origin d1) ∧ (slopeFinite origin d2)" 
      using tval2 by auto
    have "tval origin = 0" by simp
    thus ?thesis using tval1 tval2 finite by blast
  qed

  have t1nz: "tval d1 ≠ 0" using slopes by auto
  have anz: "a ≠ 0" using a by blast
  hence equ: "1/(tval d1) = (1/(a*tval d1))*a" by simp

  hence "sloper origin d1 = (((1/(a*tval d1))*a) ⊗ d1)" using slopes by auto
  also have "... =  ((1/(tval d2)) ⊗ d2)" 
    using lemScaleAssoc[of "1/(a*tval d1)" "a" "d1"] a by auto
  finally have equalslopers: "sloper origin d1 = sloper origin d2" using slopes by auto

  thus ?thesis using d1 d2 by auto
qed

end (* of class WorldLine *)

end (* of theory WorldLine *)