Theory Translations

(*
   Mike Stannett
   Feb 2023
*)

section ‹ Translations ›

text ‹This theory describes translation maps. ›


theory Translations
  imports Functions
begin

class Translations = Functions
begin

(*
  These functions are all single-valued, so we define them
  as having type ('a Point ⇒ 'a Point). We can use the
  asFunc function to convert them to relational form
  where necessary.
*)

abbreviation mkTranslation :: "'a Point ⇒ ('a Point ⇒ 'a Point)"
  where "(mkTranslation t) ≡ (λ p . (p ⊕ t))"


abbreviation translation :: "('a Point ⇒ 'a Point) ⇒ bool" 
  where "translation T ≡ ∃ q . ∀ p . ((T p) = (p ⊕ q))"



(* ****************************************************************** *)
(* LEMMAS *)

lemma lemMkTrans: "∀ t . translation (mkTranslation t)"
  by auto


lemma lemInverseTranslation:
  assumes "(T = mkTranslation t) ∧ (T' = mkTranslation (origin ⊖ t))"
  shows     "(T' ∘ T = id) ∧ (T ∘ T' = id)"
using assms by auto


lemma lemTranslationSum:
  assumes "translation T"
  shows   "T (u ⊕ v) = ((T u) ⊕ v)"
proof -
  obtain t where t: "∀ x. T x = (x ⊕ t)" using assms(1) by auto
  thus ?thesis using add_commute add_assoc t by auto
qed


lemma lemIdIsTranslation: "translation id"
proof -
  have "∀ p . (id p) = (p ⊕ origin)" by simp
  thus ?thesis by blast
qed



lemma lemTranslationCancel:
  assumes "translation T"
  shows   "((T p) ⊖ (T q)) = (p ⊖ q)"
proof -
  obtain t where t: "∀ x. T x = (x ⊕ t)" using assms(1) by auto
  hence "((p ⊕ t) ⊖ (q ⊕ t)) = (p ⊖ q)" by simp
  thus ?thesis using t by auto
qed  


lemma lemTranslationSwap:
  assumes "translation T"
  shows   "(p ⊕ (T q)) = ((T p) ⊕ q)"
proof -
  obtain t where t: "∀ x . T x = (x ⊕ t)" using assms(1) by auto
  thus ?thesis using add_commute add_assoc by simp
qed


(* TRANSLATION LEMMAS *)

lemma lemTranslationPreservesSep2:
  assumes "translation T"
  shows "sep2 p q = sep2 (T p) (T q)"
proof -
  obtain t where "∀x. T x = (x ⊕ t)" using assms(1) by auto
  thus ?thesis by force
qed



lemma lemTranslationInjective:
  assumes "translation T"
  shows   "injective (asFunc T)"
proof -
  obtain t where t: "∀ x . T x = (x ⊕ t)" using assms(1) by auto
  define Tinv where Tinv: "Tinv = mkTranslation (origin ⊖ t)"
  { fix x y
    assume "T x = T y"
    hence "(Tinv ∘ T) x = (Tinv ∘ T) y" by auto
    hence "x = y" using Tinv t by auto
  }
  thus ?thesis by auto
qed


lemma lemTranslationSurjective:
  assumes "translation T"
  shows   "surjective (asFunc T)"
proof -
  obtain t where t: "∀ x . T x = (x ⊕ t)" using assms(1) by auto
  hence mkT: "T = mkTranslation t" by auto
  define Tinv where Tinv: "Tinv = mkTranslation (origin ⊖ t)"
  hence "∀y . y = T (Tinv y)" using mkT lemInverseTranslation by auto
  thus ?thesis by auto
qed


lemma lemTranslationTotalFunction:
  assumes "translation T"
  shows   "isTotalFunction (asFunc T)"
by simp


lemma lemTranslationOfLine: 
  assumes "translation T"
  shows   "(applyToSet (asFunc T) (line B D)) = line (T B) D"
proof -
  define l where l: "l = line B D"
  { fix q'
    { assume "q' ∈ (applyToSet (asFunc T) l)"
      then obtain q where q: "q ∈ l ∧ (asFunc T) q q'" by auto
      then obtain α where α: "q = (B ⊕ (α⊗D))" using l by auto
      have "q' = T q" using q by auto
      also have "… = ((T B) ⊕ (α⊗D))" using α assms lemTranslationSum by blast
      finally have "q' ∈ line (T B) D" by auto
    }
    hence l2r: "q' ∈ (applyToSet (asFunc T) l) ⟶ q' ∈ line (T B) D" by auto
    { assume "q' ∈ line (T B) D"
      then obtain α where α: "q' = ((T B) ⊕ (α⊗D))" by auto
      hence "q' = T (B ⊕ (α⊗D))" using assms lemTranslationSum[of "T" "B" "(α⊗D)"] by auto
      moreover have "(B ⊕ (α⊗D)) ∈ l" using l by auto
      ultimately have "q' ∈ (applyToSet (asFunc T) l)" by auto
    }
    hence "q' ∈ line (T B) D ⟷ q' ∈ (applyToSet (asFunc T) l)" using l2r by auto
  }
  thus ?thesis using l by auto
qed


lemma lemOnLineTranslation:
  assumes "(translation T) ∧ (onLine p l)"
shows     "onLine (T p) (applyToSet (asFunc T) l)"
proof -
  obtain B D where BD: "l = line B D" using assms by auto
  hence "(applyToSet (asFunc T) l) = line (T B) D" using assms lemTranslationOfLine by auto
  moreover have "T p ∈ (applyToSet (asFunc T) l)" using assms by auto
  ultimately show ?thesis by blast
qed



lemma lemLineJoiningTranslation:
  assumes "translation T"
  shows   "applyToSet (asFunc T) (lineJoining p q) = lineJoining (T p) (T q)"
proof -
  define D where D: "D = (q⊖p)"
  hence "lineJoining p q = line p D" by auto
  hence "applyToSet (asFunc T) (lineJoining p q) =  line (T p) D" 
    using assms lemTranslationOfLine by auto
  moreover have "((T q) ⊖ (T p)) = (q⊖p)" using assms lemTranslationCancel by auto
  ultimately show ?thesis using D by auto
qed





lemma lemBallTranslation:
  assumes "translation T"
and       "x within e of y"
  shows   "(T x) within e of (T y)"
proof -
  have "sep2 (T x) (T y) = sep2 x y" 
    using assms(1) lemTranslationPreservesSep2[of "T"] by auto
  thus ?thesis using assms(2) by auto
qed


lemma lemBallTranslationWithBoundary:
  assumes "translation T"
and       "sep2 x y ≤ sqr e"
  shows   "sep2 (T x) (T y) ≤ sqr e"
proof -
  have "sep2 (T x) (T y) = sep2 x y" 
    using assms(1) lemTranslationPreservesSep2[of "T" "x" "y"] by simp
  thus ?thesis using assms(2) by auto
qed


lemma lemTranslationIsCts:
  assumes "translation T"
  shows "cts (asFunc T) x"
proof -
  { fix x'
    assume x': "x' = T x"

    { fix e
      assume epos: "e > 0"
      { fix p'
        assume p': "p' ∈ applyToSet (asFunc T) (ball x e)"
        then obtain p where p: "(p ∈ ball x e) ∧ p' = T p" by auto
        hence "sep2 p x < sqr e" using lemSep2Symmetry by force
        hence "sep2 p' x' < sqr e" using assms(1) p x' lemBallTranslation by auto
      }
      hence "applyToSet (asFunc T) (ball x e) ⊆ ball x' e"
        using lemSep2Symmetry by force
      hence "∃d>0. applyToSet (asFunc T) (ball x d) ⊆ ball x' e"
        using epos lemSep2Symmetry by auto
    }
    hence "∀e>0. ∃d>0. applyToSet (asFunc T) (ball x d) ⊆ ball x' e"
      by auto
  }
  thus ?thesis by auto
qed



lemma lemAccPointTranslation:
  assumes "translation T"
and       "accPoint x s"
shows     "accPoint (T x) (applyToSet (asFunc T) s)"
proof -
  { fix e
    assume "e > 0"
    then obtain q where q: "q ∈ s ∧ (x ≠ q) ∧ (inBall q e x)" 
      using assms(2) by auto

    have acc1: "q ∈ s" using q by auto
    have acc2: "x ≠ q" using q by auto
    have acc3: "inBall q e x" using q by auto

    define q' where q': "q' = T q"

    have rtp1: "q' ∈ applyToSet (asFunc T) s" using q' acc1 by auto
    have rtp2: "T x ≠ q'" using assms(1) acc2 lemTranslationInjective[of "T"] q' by force
    have rtp3: "inBall q' e (T x)" 
      using assms(1) acc3 q' lemBallTranslation[of "T" "q" "x" "e"] by auto

    hence "∃ q' . (q' ∈ applyToSet (asFunc T) s) ∧ (T x ≠ q')
                    ∧ (inBall q' e (T x))"
      using rtp1 rtp2 by auto
  }
  thus ?thesis by auto
qed


lemma lemInverseOfTransIsTrans:
  assumes "translation T"
and       "T' = invFunc (asFunc T)"
  shows   "translation (toFunc T')"
proof -
  obtain t where t: "∀p . T p = (p ⊕ t)" using assms(1) by auto
  hence mkT: "T = mkTranslation t" by auto
  define T1 where T1: "T1 = mkTranslation (origin ⊖ t)"
  hence transT1: "translation T1" using lemMkTrans by blast

  have TT1: "(T ∘ T1 = id) ∧ (T1 ∘ T = id)" using t T1 lemInverseTranslation by auto

  { fix p r
    { assume "invFunc (asFunc T) p r"
      hence "T r = p" by simp
      hence "T1 p = (T1∘T) r" by auto
      hence "T1 p = r" using TT1 by simp
    }
    hence l2r: "invFunc (asFunc T) p r ⟶ (asFunc T1) p r" by auto
    { assume "(asFunc T1) p r"
      hence T'p: "T1 p = r" by simp
      have "(T ∘ T1) p = T r" using T'p by auto
      hence "p = T r" using TT1 by auto
    }
    hence "(asFunc T1) p r ⟷ invFunc (asFunc T) p r" using l2r by force
  }
  hence "(asFunc T1) = T'" using assms(2) by fastforce

  hence "toFunc T' = toFunc (asFunc T1)" using assms(2) by fastforce
  hence "toFunc T' = T1" by fastforce
  thus ?thesis using transT1 by auto
qed



lemma lemInverseTrans:
assumes "translation T"
shows   "∃T' . (translation T') ∧ (∀ p q . T p = q ⟷ T' q = p)"
proof -
  obtain t where t: "∀p . T p = (p ⊕ t)" using assms by auto
  hence mkT: "T = mkTranslation t" by auto
  define T' where T': "T' = mkTranslation (origin ⊖ t)"
  hence trans': "translation T'" using lemMkTrans by blast

  have TT': "(T'∘T = id) ∧ (T∘T' = id)" using mkT T' lemInverseTranslation by auto

  { fix p q
    { assume "T p = q"
      hence "T' q = (T' ∘ T) p" by auto
      hence "T' q = p" using TT' by auto
    }
    hence l2r: "T p = q ⟶ T' q = p" by auto
    { assume "T' q = p"
      hence "T p = (T∘T') q" by auto
      hence "T p = q" using TT' by auto
    }
    hence "T' q = p ⟷ T p = q" using l2r by blast
  }
  thus ?thesis using trans' by blast
qed
    



end (* of class Translations *)


end (* of theory Translation *)