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