Theory AxLightMinus

(*
   Mike Stannett
   Feb 2023
*)

section ‹ AXIOM: AxLightMinus ›

text ‹This theory declares the axiom AxLightMinus.›

theory AxLightMinus
  imports WorldLine TangentLines
begin

text ‹AxLightMinus:
   If an observer sends out a light signal, then the speed of the 
   light signal is 1 according to the observer. Moreover it is possible to send
   out a light signal in any direction.›

(*
   (∀m ∈ Ob)(∀p ∈ wline_m(m)(∀v in Q3)
      (∃ph ∈ Ph)vel_m(ph,p) = v  ⟷  |v| = 1

  Given the new definition of velocity, we need to define the worldline
of ph according to m, i.e.

  wl_m(ph) = { q :  m sees ph at q }
           = λ q . m sees ph at q
*)

class axLightMinus = WorldLine + TangentLines
begin

text ‹The definition of AxLightMinus used in this Isabelle proof is slightly
different to the one used in the paper-based proof on which it is based. We
have established elsewhere, however, that each entails the other in all
relevant contexts.›

abbreviation axLightMinusOLD :: "Body ⇒ 'a Point ⇒ 'a Space ⇒ bool" 
  where "axLightMinusOLD m p v ≡ (m sees m at p) ⟶ ( 
     (∃ ph . (Ph ph ∧ (vel (wline m ph) p v)))  ⟷  (sNorm2 v = 1)
   )"

abbreviation axLightMinus :: "Body ⇒ 'a Point ⇒ 'a Space ⇒ bool" 
  where "axLightMinus m p v ≡ (m sees m at p) 
         ⟶ ( ∀ l . ∀ v ∈ lineVelocity l .
                (∃ ph . (Ph ph ∧ (tangentLine l (wline m ph) p)))  ⟷  (sNorm2 v = 1))"

end (* of class axLightMinus *)


class AxLightMinus = axLightMinus +
  assumes AxLightMinus: "∀ m p v  . axLightMinus m p v"
begin
end (* of class AxLightMinus *)

end (* of theory AxLightMinus *)