Theory AxEventMinus

(*
   Mike Stannett
   Feb 2023
*)

section ‹ AXIOM: AxEventMinus ›

text ‹This theory declares the axiom AxEventMinus ›

theory AxEventMinus
  imports WorldView
begin

text ‹AxEventMinus: 
  An observer encounters the events in which they are observed.
›
(*
  (∀m,k ∈ Ob)(∀p ∈ Q4)
    k ∈ ev_m(p) ⟶ (∃q ∈ Q4) ev_m(p) = ev_k(q)

*)
class axEventMinus = WorldView
begin

  abbreviation axEventMinus :: "Body ⇒ Body ⇒ 'a Point ⇒ bool" 
    where "axEventMinus m k p ≡ (m sees k at p) 
                   ⟶ (∃ q . ∀ b . ( (m sees b at p) ⟷ (k sees b at q)))"

end (* of class axEventMinus *)





class AxEventMinus = axEventMinus +
  assumes AxEventMinus: "∀ m k p  . axEventMinus m k p"
begin
end (* of class AxEventMinus *)

end (* of theory AxEventMinus *)