Theory Vectors

(*
   Mike Stannett
   Date: June 2020
   Updated: Jan 2023
*)
section ‹ Vectors ›

text ‹In this theory we define dot-products, and explain what we mean by
timelike, lightlike (null), causal and spacelike vectors. ›

theory Vectors
  imports Norms
begin

class Vectors = Norms
begin

fun dot :: "'a Point ⇒ 'a Point ⇒ 'a" (‹_ ⊙ _›)
  where "dot u v = (tval u)*(tval v) + (xval u)*(xval v) +
                     (yval u)*(yval v) + (zval u)*(zval v)"

fun sdot :: "'a Space ⇒ 'a Space ⇒ 'a" (‹_ ⊙s _›)
  where "sdot u v = (svalx u)*(svalx v) + (svaly u)*(svaly v) + (svalz u)*(svalz v)"

fun mdot :: "'a Point ⇒ 'a Point ⇒ 'a" (‹_ ⊙m _ ›)
  where "mdot u v = (tval u)*(tval v) - ((sComponent u) ⊙s (sComponent v))"

abbreviation timelike :: "'a Point ⇒ bool"
  where "timelike p ≡ mNorm2 p > 0"

(* For simplicity, assume p isn't the origin *)
abbreviation lightlike :: "'a Point ⇒ bool"
  where "lightlike p ≡ (p ≠ origin ∧ mNorm2 p = 0)"

abbreviation spacelike :: "'a Point ⇒ bool"
  where "spacelike p ≡ mNorm2 p < 0"

abbreviation causal :: "'a Point ⇒ bool"
  where "causal p ≡ timelike p ∨ lightlike p"

abbreviation orthog :: "'a Point ⇒ 'a Point ⇒ bool"
  where "orthog p q ≡ (p ⊙ q) = 0"

abbreviation orthogs :: "'a Space ⇒ 'a Space ⇒ bool"
  where "orthogs p q ≡ (p ⊙s q) = 0"

abbreviation orthogm :: "'a Point ⇒ 'a Point ⇒ bool"
  where "orthogm p q ≡ (p ⊙m q) = 0"


(* LEMMAS *)


lemma lemDotDecomposition:
  shows "(u ⊙ v) = (tval u * tval v) + ((sComponent u) ⊙s (sComponent v))"
  by (simp add: add_commute local.add.left_commute)


lemma lemDotCommute: "dot u v = dot v u"
  by (simp add: mult_commute)

lemma lemDotScaleLeft: "dot (a⊗u) v = a * (dot u v)"
  using mult_assoc distrib_left by force

lemma lemDotScaleRight: "dot u (a⊗v) = a * (dot u v)"
  using mult_assoc mult_commute distrib_left by auto 

lemma lemDotSumLeft: "dot (u⊕v) w = (dot u w) + (dot v w)"
  using distrib_right add_assoc add_commute by force

lemma lemDotSumRight: "dot u (v⊕w) = (dot u v) + (dot u w)"
  using distrib_left add_assoc add_commute by auto

lemma lemDotDiffLeft: "dot (u⊖v) w = (dot u w) - (dot v w)"
  by (simp add: field_simps)

lemma lemDotDiffRight: "dot u (v⊖w) = (dot u v) - (dot u w)"
  by (simp add: field_simps)


lemma lemNorm2OfSum: "norm2 (u ⊕ v) = norm2 u + 2*(u ⊙ v) + norm2 v"
proof -
  have "norm2 (u ⊕ v) = ((u ⊕ v) ⊙ (u ⊕ v))" by auto
  also have "… = (u ⊙ (u ⊕ v)) + (v ⊙ (u ⊕ v))" 
    using lemDotSumLeft[of "u" "v" "(u ⊕ v)"] by auto
  also have "… = (u⊙u) + ((u⊙v) + (v⊙u)) + (v⊙v)"
    using lemDotSumRight[of "u" "u" "v"] lemDotSumRight[of "v" "u" "v"]
          add_assoc by auto
  finally show ?thesis using  mult_2 lemDotCommute[of "u" "v"]
    by auto
qed


lemma lemSDotCommute: "sdot u v = sdot v u"
  by (simp add: mult_commute)

lemma lemSDotScaleLeft: "sdot (a ⊗s u) v = a * (sdot u v)"
  using mult_assoc distrib_left by force

lemma lemSDotScaleRight: "sdot u (a ⊗s v) = a * (sdot u v)"
  using mult_assoc mult_commute distrib_left by auto 

lemma lemSDotSumLeft: "sdot (u ⊕s v) w = (sdot u w) + (sdot v w)"
  using distrib_right add_assoc add_commute by force

lemma lemSDotSumRight: "sdot u ( v⊕s w) = (sdot u v) + (sdot u w)"
  using distrib_left add_assoc add_commute by auto

lemma lemSDotDiffLeft: "sdot (u ⊖s v) w = (sdot u w) - (sdot v w)"
  by (simp add: field_simps)

lemma lemSDotDiffRight: "sdot u ( v⊖s w) = (sdot u v) - (sdot u w)"
  by (simp add: field_simps)



lemma lemMDotDiffLeft: "mdot (u⊖v) w = (mdot u w) - (mdot v w)"
  by (simp add: field_simps)


lemma lemMDotSumLeft: "mdot (u ⊕ v) w = (mdot u w) + (mdot v w)"
proof -
  have "mdot (u⊕v) w = (tval (u⊕v))*(tval w) - ((sComponent (u⊕v))⊙s(sComponent w))"
    by auto
  also have "… = (tval u*tval w) + (tval v*tval w) 
                     - ( ((sComponent u)⊙s(sComponent w)) + ((sComponent v)⊙s(sComponent w)))" 
    using distrib lemSDotSumLeft[of "(sComponent u)" "(sComponent v)" "(sComponent w)"] 
    by auto
  also have "… = ((tval u*tval w) - ((sComponent u)⊙s(sComponent w)))
                + ((tval v*tval w) - ((sComponent v)⊙s(sComponent w)))"
    using add_diff_eq add_commute diff_diff_add by auto
  finally show ?thesis by simp
qed


lemma lemMDotScaleLeft: "mdot (a ⊗ u) v = a * (mdot u v)"
proof -
  have "mdot (a ⊗ u) v = a*(tval u*tval v) - a*((sComponent u)⊙s(sComponent v))"
    using lemSDotScaleLeft[of "a" "sComponent u" "sComponent v"]
    by (simp add: mult_assoc)
  thus ?thesis by (simp add: local.right_diff_distrib')
qed
  
  
lemma lemMDotScaleRight: "mdot u (a ⊗ v) = a * (mdot u v)"
proof -
  have "mdot u (a ⊗ v) = a*(tval u*tval v) - a*((sComponent u)⊙s(sComponent v))"
    using lemSDotScaleRight[of "sComponent u" "a" "sComponent v"] 
    by (simp add: local.mult.left_commute)
  thus ?thesis by (simp add: local.right_diff_distrib')
qed
  
  

lemma lemSNorm2OfSum: "sNorm2 (u ⊕s v) = sNorm2 u + 2*(u ⊙s v) + sNorm2 v"
proof -
  have "sNorm2 (u ⊕s v) = ((u ⊕s v) ⊙s (u ⊕s v))" by auto
  also have "… = (u ⊙s (u ⊕s v)) + (v ⊙s (u ⊕s v))" 
    using lemSDotSumLeft[of "u" "v" "(u ⊕s v)"] by auto
  also have "… = (u ⊙s u) + ((u ⊙s v) + (v ⊙s u)) + (v ⊙s v)"
    using lemSDotSumRight[of "u" "u" "v"] lemSDotSumRight[of "v" "u" "v"]
          add_assoc by auto
  finally show ?thesis using mult_2 lemSDotCommute[of "u" "v"]
    by auto
qed


lemma lemSNormNonNeg:
  shows "sNorm v ≥ 0"
proof -
  have "hasUniqueRoot (sNorm2 v)" using AxEField lemSqrt by auto
  thus ?thesis using the1_equality[of "isNonNegRoot (sNorm2 v)"] by blast
qed


lemma lemMNorm2OfSum: "mNorm2 (u ⊕ v) = mNorm2 u + 2*(u ⊙m v) + mNorm2 v"
proof -
  define su where su: "su = sComponent u"
  define sv where sv: "sv = sComponent v"

  have "mNorm2 (u ⊕ v) = ((u ⊕ v) ⊙m (u ⊕ v))" by auto
  also have "… = (sqr (tval u) + 2*(tval u)*(tval v) + sqr (tval v)) - sNorm2 (su ⊕s sv)"
    using lemSqrSum su sv by auto
  also have "… = (sqr (tval u) + 2*(tval u)*(tval v) + sqr (tval v))
                - ( sNorm2 su + 2*(su ⊙s sv) + sNorm2 sv)"
    using lemSNorm2OfSum by auto
  also have "… = ( sqr (tval u) - sNorm2 su )
                  + ( 2*(tval u)*(tval v) - 2*(su ⊙s sv) )
                    + ( sqr (tval v) - sNorm2 sv )"
    using add_commute add_assoc add_diff_eq diff_add_eq diff_diff_add by simp
  finally show ?thesis using su sv right_diff_distrib' mult_assoc by auto
qed


lemma lemMNorm2OfDiff: "mNorm2 (u ⊖ v) = mNorm2 u - 2*(u ⊙m v) + mNorm2 v"
proof -
  define vm where vm: "vm = ((-1)⊗v)"
  hence "mNorm2 (u ⊖ v) = mNorm2 (u ⊕ vm)" by auto
  hence "mNorm2 (u ⊖ v) =  mNorm2 u + 2*(u ⊙m vm) + mNorm2 vm"
    using lemMNorm2OfSum by auto
  moreover have "(u ⊙m vm) = -(u ⊙m v)" 
    using lemMDotScaleRight[of "u" "(-1)" "v"] vm by auto
  moreover have "mNorm2 vm = mNorm2 v" using vm lemMNorm2OfScaled by auto
  ultimately show ?thesis 
    by (metis local.diff_conv_add_uminus local.mult_minus_right)
qed
  

lemma lemMNorm2Decomposition: "mNorm2 p = (p ⊙m p)"
  by auto



lemma lemMDecomposition: 
  assumes "(u ⊙m v) ≠ 0"
and       "mNorm2 v ≠ 0"
and       "a = (u ⊙m v)/(mNorm2 v)"
and       "up = (a ⊗ v)"
and       "uo = (u ⊖ up)"
  shows "u = (up ⊕ uo) ∧ parallel up v ∧ orthogm uo v ∧ (up ⊙m v) = (u ⊙m v)"
proof -
  have anz: "a ≠ 0" using assms by auto

  have psum: "u = (up ⊕ uo)" using assms  add_diff_eq by auto
  moreover have "parallel up v" using assms(4) anz by auto
  moreover have ppdot: "(up ⊙m v) = (u ⊙m v)"
  proof -
    have "(up ⊙m v) = a*(v ⊙m v)"  using assms lemMDotScaleLeft[of "a" "v" "v"] by auto
    thus ?thesis using assms by auto
  qed
  moreover have "orthogm uo v"
  proof -
    have "(uo ⊙m v) = (u ⊙m v) - (up ⊙m v)" using lemMDotSumLeft psum by force
    thus ?thesis using ppdot by auto
  qed
  ultimately show ?thesis by blast
qed



end (* of class Vectors *)

end (* of theory Vectors *)