Theory Axioms

(*
   Author: Mike Stannett
   Date: 22 October 2012
   m.stannett@sheffield.ac.uk
*)
theory Axioms
imports SpaceTime SomeFunc
begin

record Body =
  Ph :: "bool"
  IOb :: "bool"


class WorldView = SpaceTime +
fixes
  (* Worldview relation *)
  W :: "Body ⇒ Body ⇒ 'a Point ⇒ bool" (‹_ sees _ at _›)
and
  (* Worldview transformation *)
  wvt :: "Body ⇒ Body ⇒ 'a Point ⇒ 'a Point"
assumes
  AxWVT: "⟦ IOb m; IOb k ⟧ ⟹ (W k b x ⟷ W m b (wvt m k x))"
and
  AxWVTSym: "⟦ IOb m; IOb k ⟧ ⟹ (y = wvt k m x  ⟷  x = wvt m k y)"
begin
end


(* THE BASIC AXIOMS *)
(* ================ *)


class AxiomPreds = WorldView 
begin
  fun sqrtTest :: "'a ⇒ 'a ⇒ bool" where
     "sqrtTest x r = ((r ≥ 0) ∧ (r*r = x))"

  fun cTest :: "Body ⇒ 'a ⇒ bool" where
    "cTest m v = ( (v > 0) ∧ ( ∀x y . ( 
               (∃p. (Ph p ∧ W m p x ∧ W m p y)) ⟷ (space2 x y = (v * v)*(time2 x y)) 
             )))"
end

(*
  AxEuclidean
  Quantities form a Euclidean field, ie positive quantities have
  square roots. We introduce a function, sqrt, that determines them.
*)
class AxEuclidean = AxiomPreds + Quantities +
assumes
  AxEuclidean: "(x ≥ Groups.zero_class.zero) ⟹ (∃r. sqrtTest x r)"
begin

  abbreviation sqrt :: "'a ⇒ 'a" where
     "sqrt ≡ someFunc sqrtTest"

  lemma lemSqrt: 
    assumes "x ≥ 0"
      and   "r = sqrt x"
    shows   "r ≥ 0  ∧  r*r = x"
  proof -
    have rootExists: "(∃r. sqrtTest x r)" by (metis AxEuclidean assms(1))
    hence "sqrtTest x (sqrt x)" by (metis lemSomeFunc)
    thus ?thesis using assms(2) by simp
  qed

end


(* 
   AxLight
   There is an inertial observer, according to whom, any light
   signal moves with the same velocity in any direction 
*)
class AxLight = WorldView +
assumes
  AxLight: "∃m v.( IOb m ∧ (v > (0::'a)) ∧ ( ∀x y.( 
              (∃p.(Ph p ∧ W m p x ∧ W m p y)) ⟷ (space2 x y = (v * v)*time2 x y) 
            )))"
begin
end



(*
  AxPh
  For any inertial observer, the speed of light is the same in every
  direction everywhere, and it is finite. Furthermore, it is possible
  to send out a light signal in any direction.
*)
class AxPh = WorldView + AxiomPreds +
assumes
  AxPh: "IOb m ⟹ (∃v. cTest m v)"
begin

  abbreviation c :: "Body ⇒ 'a" where
    "c ≡ someFunc cTest"

  fun lightcone :: "Body ⇒ 'a Point ⇒ 'a Cone" where
    "lightcone m v = mkCone v (c m)"


lemma lemCProps:
  assumes "IOb m"
     and  "v = c m"
  shows "(v > 0) ∧ (∀x y.((∃p. (Ph p ∧ W m p x ∧ W m p y)) 
                      ⟷ ( space2 x y = (c m * c m)*time2 x y )))"
proof -
  have vExists: "(∃v. cTest m v)" by (metis AxPh assms(1))
  hence "cTest m (c m)" by (metis lemSomeFunc)
  thus ?thesis using assms(2) by simp
qed


lemma lemCCone: 
  assumes "IOb m"
    and   "onCone y (lightcone m x)"
  shows   "∃p. (Ph p ∧ W m p x ∧ W m p y)"
proof -
  have "(∃p.(Ph p ∧ W m p x ∧ W m p y)) 
                      ⟷ ( space2 x y = (c m * c m)*time2 x y )"
    by (simp add: assms(1) lemCProps)
  hence ph_exists: "(space2 x y = (c m * c m)*time2 x y) ⟶ (∃p.(Ph p ∧ W m p x ∧ W m p y))"
    by metis
  define lcmx where "lcmx = lightcone m x"
  have lcmx_vertex: "vertex lcmx = x" by (simp add: lcmx_def)
  have lcmx_slope: "slope lcmx = c m" by (simp add: lcmx_def)
  have "onCone y lcmx ⟶ (space2 x y = (c m * c m)*time2 x y)" 
    by (metis lcmx_vertex lcmx_slope onCone.simps)
  hence "space2 x y = (c m * c m)*time2 x y" by (metis lcmx_def assms(2))
  thus ?thesis by (metis ph_exists)
qed


lemma lemCPos: 
  assumes "IOb m"
  shows   "c m > 0"
  by (metis assms(1) lemCProps)


lemma lemCPhoton:
  assumes "IOb m"
  shows "∀x y. (∃p. (Ph p ∧ W m p x ∧ W m p y)) ⟷ (space2 x y = (c m * c m)*(time2 x y))"
  by (metis assms(1) lemCProps)

end



(*
  AxEv
  Inertial observers see the same events (meetings of bodies).
  This also enables us to discuss the worldview transformation.
*)
class AxEv = WorldView +
assumes
  AxEv: "⟦ IOb m; IOb k⟧ ⟹  (∃y. (∀b. (W m b x  ⟷ W k b y)))"
begin
end



(*
  Inertial observers can move with any speed slower than that of light
*)
class AxThExp = WorldView + AxPh +
assumes
    AxThExp: "IOb m ⟹ (∀x y .( 
       (∃k.(IOb k ∧ W m k x ∧ W m k y)) ⟷ (space2 x y < (c m * c m) * time2 x y) 
       ))"

begin
end



(*
  Every inertial observer is stationary according to himself
*)
class AxSelf = WorldView +
assumes
  AxSelf: "IOb m  ⟹  (W m m x) ⟶ (onAxisT x)"
begin
end



(* 
  All inertial observers agree that the speed of light is 1
*)
class AxC = WorldView + AxPh +
assumes
  AxC: "IOb m ⟹ c m = 1"
begin
end


(*
  Inertial observers agree as to the spatial distance between two
  events if these two events are simultaneous for both of them.
*)
class AxSym = WorldView +
assumes
  AxSym: "⟦ IOb m; IOb k ⟧ ⟹
            (W m e x ∧ W m f y ∧ W k e x'∧ W k f y' ∧
            tval x = tval y ∧ tval x' = tval y' )
          ⟶ (space2 x y = space2 x' y')"
begin
end



(*
  AxLines
  All observers agree about lines
*)
class AxLines = WorldView + 
assumes
  AxLines: "⟦ IOb m; IOb k; collinear x p q ⟧ ⟹ 
     collinear (wvt k m x) (wvt k m p) (wvt k m q)"
begin
end



(*
  AxPlanes
  All observers agree about planes
*)
class AxPlanes = WorldView +
assumes
  AxPlanes: "⟦ IOb m; IOb k ⟧ ⟹ 
     (coplanar e x y z  ⟶ coplanar (wvt k m e) (wvt k m x) (wvt k m y) (wvt k m z))"
begin
end



(*
  AxCones
  All observers agree about lightcones
*)
class AxCones = WorldView + AxPh +
assumes
  AxCones: "⟦ IOb m; IOb k ⟧ ⟹ 
     ( onCone x (lightCone m v) ⟶ onCone (wvt k m x) (lightcone k (wvt k m v)))"
begin
end



(*
  All inertial observers see time travelling in the same direction. That
  is, if m thinks that k reached y after he reached x, then
  k should also think that he reached y after he reached x.
*)
class AxTime = WorldView +
assumes 
  AxTime: "⟦ IOb m; IOb k ⟧ 
              ⟹( x ≲ y ⟶ wvt k m x ≲ wvt k m y )"
begin
end


end