Theory WorldView

(*
   Author: Edward Higgins and Mike Stannett
   Date: July 2019

   Updated August 2019 for GenRel
   Updated: (MS) Jan 2023

*)

section ‹ WorldView ›

text ‹This theory defines worldview transformations. These form the ultimate
foundation for all of GenRel's axioms.›

theory WorldView
  imports Points
begin

(* 
  Worldview transformation 
  haromsalzburg: w_mk(p,q) defined by  ev_m(p) = ev_k(q) ≠ ∅
  where
    ev_m(p) := { b : W(m,b,p) }

*)


class WorldView = Points + 
fixes
(* Worldview relation *)
  W :: "Body ⇒ Body ⇒ 'a Point ⇒ bool" (‹_ sees _ at _›)
begin

abbreviation ev :: "Body ⇒ 'a Point ⇒ Body set"
  where "ev h x ≡ { b . h sees b at x }"

fun wvt :: "Body ⇒ Body ⇒ 'a Point ⇒ 'a Point set"
  where "wvt m k p = { q. (∃ b . (m sees b at p)) ∧ (ev m p = ev k q) }"

abbreviation wvtFunc :: "Body ⇒ Body ⇒ ('a Point ⇒ 'a Point ⇒ bool)"
  where "wvtFunc m k ≡ (λ p q . q ∈ wvt m k p)"

(* image of a line under a WVT *)
abbreviation wvtLine :: "Body ⇒ Body ⇒ 'a Point set ⇒ 'a Point set ⇒ bool"
  where "wvtLine m k l l' ≡   ∃ p q p' q' . (
                                   (wvtFunc m k p p') ∧ (wvtFunc m k q q') ∧
                                   (l = lineJoining p q) ∧ (l' = lineJoining p' q'))"

end (* of class WorldView *)

end (* of theory WorldView *)