Theory Proposition3

(*
   Proposition3.thy
   Author: Mike Stannett
   m.stannett@sheffield.ac.uk
   Date: Aug 2020
   Updated: Feb 2023
*)

section ‹ Proposition3 ›

text ‹This theory collects together earlier results to show that 
worldview transformations can be approximated by affine transformations
that have various useful properties. ›

theory Proposition3
  imports Proposition1 Proposition2 AxEventMinus
begin

class Proposition3 = Proposition1 + Proposition2 + AxEventMinus
begin




lemma lemProposition3:
  assumes "m sees k at x"
  shows   "∃ A y . (wvtFunc m k x y)
              ∧    (affineApprox A (wvtFunc m k) x)
              ∧    (applyToSet (asFunc A) (coneSet m x) ⊆ coneSet k y)
              ∧    (coneSet k y = regularConeSet y)"
proof -
  define g1 where g1: "g1 = (λ y . wvtFunc m k x y)"
  define g2 where g2: "g2 = (λ A . affineApprox A (wvtFunc m k) x)"
  define g3 where g3: "g3 = (λ A y . applyToSet (asFunc A) (coneSet m x) ⊆ coneSet k y)"
  define g4 where g4: "g4 = (λ y . coneSet k y = regularConeSet y)"

  have "axEventMinus m k x" using AxEventMinus by simp
  hence "(∃ q . ∀ b . ( (m sees b at x) ⟷ (k sees b at q)))"
    using assms by simp

  (* goal 1 *)
  then obtain y where y: "∀ b . ( (m sees b at x) ⟷ (k sees b at y))" by auto
  hence "ev m x = ev k y" by blast
  hence goal1: "g1 y" using assms g1 by auto

  (* goal 2*)
  have "axDiff m k x" using AxDiff by simp
  hence "∃ A . affineApprox A (wvtFunc m k) x" using g1 goal1 by blast
  then obtain A where goal2: "g2 A" using g2 by auto

  (* goal 3 *)
  have "applyToSet (asFunc A) (coneSet m x) ⊆ coneSet k (A x)"
    using g2 goal2 lemProposition2[of "m" "k" "A" "x"]
    by auto
  moreover have "A x = y"
    using goal1 goal2 g1 g2 lemAffineEqualAtBase[of "wvtFunc m k" "A" "x"]
    by blast
  ultimately have goal3: "g3 A y" using g3 by auto

  (* goal 4 *)
  have "k sees k at y" using assms(1) g1 goal1 by fastforce
  hence "∀ p . cone k y p = regularCone y p" 
    using lemProposition1[of "y" "k"] by auto
  hence goal4: "g4 y" using g4 by force

  (* and finally *)
  hence "∃ A  y . (g1 y) ∧ (g2 A) ∧ (g3 A y) ∧ (g4 y)"  
    using goal1 goal2 goal3 goal4 by blast

  thus ?thesis using g1 g2 g3 g4 by fastforce
qed 



end (* of class Proposition3 *)

end (* of theory Proposition3 *)