Theory Proposition1

(*
   Author: Mike Stannett
   Date: August 2020
   Updated: Feb 2023
*)

section ‹ Proposition1 ›

text ‹This theory shows that observers consider their own lightcones to be upright.›

theory Proposition1
  imports Cones AxLightMinus
begin


class Proposition1 = Cones + AxLightMinus
begin

lemma lemProposition1:
  assumes "x ∈ wline m m"
  shows   "cone m x p = regularCone x p"
proof -
  have mmx: "m sees m at x" using assms by simp

  have  axlight: "∀ l . ∀ v ∈ lineVelocity l .
           (∃ ph . (Ph ph ∧ (tangentLine l (wline m ph) x)))  ⟷  (sNorm2 v = 1)" 
    using AxLightMinus mmx by auto
(*
  "cone m x p ≡ ∃ l . onLine p l ∧  onLine x l  ∧ (∃ ph . Ph ph ∧ tl l m ph x)
  "regularCone x p ≡ ∃ l . onLine p l ∧  onLine x l ∧ (∃ v ∈ lineVelocity l . sNorm2 v = 1)
*)

  (* This term is too complex for isabelle to reason about quickly. Abbreviate it! *)
  define axph where axph: "axph = (λ l . λ ph . (Ph ph ∧ (tangentLine l (wline m ph) x)))"

  (* Likewise this speeds up the final steps *)
  define lhs where lhs: "lhs = cone m x p"
  define rhs where rhs: "rhs = regularCone x p"

  { assume "lhs"
    hence "∃ l . onLine p l ∧  onLine x l  ∧ (∃ ph . axph l ph)" 
      using lhs axph by auto 
    then obtain l 
      where l: "onLine p l ∧  onLine x l  ∧ (∃ ph . axph l ph)" by auto

    (* establish basic facts *)
    have xonl: "onLine x l" using l by auto
    have ponl: "onLine p l" using l by auto

    (* Can choose v ∈ lineVelocity l *)
    have exph: "∃ ph . axph l ph" using l by auto
    then obtain ph where ph: "axph l ph" by auto

    have axlight': "∀ v ∈ lineVelocity l . (∃ ph . axph l ph)  ⟷  (sNorm2 v = 1)" 
      using axph axlight by force

    hence lv1: "∀ v ∈ lineVelocity l . (sNorm2 v = 1)" using exph by blast

    have  tterm1: "tl l m ph x" using ph axph by force

    hence "∃ p . ( (onLine p l) ∧ (p ≠ x) ∧ (∀ ε > 0 .  ∃ δ > 0 . ∀ y ∈ (wline m ph). (
      ( (y within δ of x) ∧ (y ≠ x) ) ⟶
      ( ∃ r . ((onLine r (lineJoining x y)) ∧ (r within ε of p))))))"
      by auto
    then obtain q where q: "onLine q l ∧ q ≠ x" by auto
    define qx where qx: "qx = (q ⊖ x)"
    hence "(x ≠ q) ∧ onLine x l ∧ onLine q l ∧ (qx = (q ⊖ x))" using q xonl by auto
    hence "∃ p q . (p ≠ q) ∧ onLine p l ∧ onLine q l ∧ (qx = (q ⊖ p))" by blast
    hence qxl: "qx ∈ drtn l" by auto
    
    define v where v: "v = velocityJoining origin qx"
    hence "∃ d ∈ drtn l . v = velocityJoining origin d" using qxl by blast
    hence existsv: "v ∈ lineVelocity l" by auto
    hence norm2v: "sNorm2 v = 1" using lv1 by auto
    hence "∃ v ∈ lineVelocity l . sNorm2 v = 1" using existsv by force

    hence "onLine p l ∧  onLine x l ∧ (∃ v ∈ lineVelocity l . sNorm2 v = 1)"
      using ponl xonl by auto
    hence "∃ l . onLine p l ∧  onLine x l ∧ (∃ v ∈ lineVelocity l . sNorm2 v = 1)"
      by blast
    hence "regularCone x p" by auto
  }
  hence l2r: "lhs ⟶ rhs" using rhs by blast

  (* CONVERSE *)
  { assume "rhs"
    hence "∃ l . onLine p l ∧  onLine x l ∧ (∃ v ∈ lineVelocity l . sNorm2 v = 1)" 
      using rhs by auto
    then obtain l 
      where l: "(onLine p l) ∧  (onLine x l) ∧ (∃ v ∈ lineVelocity l . sNorm2 v = 1)" 
      by blast

    have xonl: "onLine x l" using l by auto
    have ponl: "onLine p l" using l by auto

    have "∃ v ∈ lineVelocity l . sNorm2 v = 1" using l  by blast
    then obtain v where v: "(v ∈ lineVelocity l) ∧ (sNorm2 v = 1)" by blast

    define final 
      where final: "final = (λ l . onLine p l ∧  onLine x l  ∧ (∃ ph . axph l ph))"

    have "∃ ph . axph l ph" using v axlight axph by blast
    hence "final l" using ponl xonl final by auto
    hence "∃ l . final l" by auto
    hence "cone m x p" using final axph by auto
    hence "lhs" using lhs by auto
  }
  hence r2l: "rhs ⟶ lhs" using lhs by blast

  hence "lhs ⟷ rhs" using l2r by auto
  thus ?thesis using lhs rhs by auto
qed




end (* of class Proposition1 *)

end (* of theory Proposition1 *)