Theory Cones

(*
   Author: Mike Stannett
   Date: August 2020
   Updated: Feb 2023
*)

section ‹ Cones ›

text ‹This theory defines (light)cones, regular cones, and their properties. ›

theory Cones
  imports WorldLine TangentLines
begin


class Cones = WorldLine + TangentLines
begin

abbreviation tl :: "'a Point set ⇒ Body ⇒ Body ⇒ 'a Point ⇒ bool"
  where "tl l m b x  ≡ tangentLine l (wline m b) x"


text ‹The cone of a body at a point comprises the set of points that lie on
tangent lines of photons emitted by the body at that point.›

abbreviation cone :: "Body ⇒ 'a Point ⇒ 'a Point ⇒ bool"
  where "cone m x p 
             ≡ ∃ l . (onLine p l) ∧  (onLine x l) ∧ (∃ ph . Ph ph ∧ tl l m ph x)" 


abbreviation regularCone :: "'a Point ⇒ 'a Point ⇒ bool"
  where "regularCone x p ≡ ∃ l . (onLine p l) ∧ (onLine x l) 
                                ∧ (∃ v ∈ lineVelocity l . sNorm2 v = 1)"


abbreviation coneSet :: "Body ⇒ 'a Point ⇒ 'a Point set"
  where "coneSet m x ≡ { p . cone m x p }"


abbreviation regularConeSet :: "'a Point ⇒ 'a Point set"
  where "regularConeSet x ≡ { p . regularCone x p }"




end (* of class Cones *)

end (* of theory Cones *)