Theory AxDiff

(*
   Mike Stannett
   Feb 2023
*)

section ‹ AXIOM: AxDiff ›

text ‹ This theory declares the axiom AxDiff. ›

theory AxDiff
  imports Affine WorldView
begin

text ‹AxDiff:
  Worldview transformations are differentiable wherever they are defined - 
  they can be approximated locally by affine transformations.›

(*
  ADDED JUDIT'S ASSUMPTION to affApprox definition: A is invertible
*)
class axDiff = Affine + WorldView
begin
  abbreviation axDiff :: "Body ⇒ Body ⇒ 'a Point ⇒ bool" 
    where "axDiff m k p ≡ (definedAt (wvtFunc m k) p) 
                              ⟶ (∃ A . (affineApprox A (wvtFunc m k) p ))"
end (* of class axDiff *)


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

end (* of theory AxDiff *)