Theory Functions

(*
   Mike Stannett
   Date: April 2020
   Updated: Jan 2023
*)

section ‹ Functions ›

text ‹This theory characterises the various types of function 
(injective, bijective, etc).›

theory Functions
  imports Points
begin

text ‹ We do not assume a priori that all of the functions we define are
well-defined or total. We therefore need to allow for functions which are 
only partially defined, and also for "functions" which might be multi-valued.
For example, we cannot say in advance whether one observer might see another's
worldline as a bifurcating structure rather than a basic single-valued trajectory.

To achieve this we'll often think of functions as relations and write
"f x y = true" instead of "f x = y". Similarly, a spacetime set S will be 
sometimes be expressed as its characteristic function.
›


class Functions = Points 
begin

abbreviation bounded :: "('a Point ⇒ 'a Point) ⇒ bool" 
  where "bounded f ≡ ∃ bnd > 0 . (∀ p . (norm2 (f p)  ≤ bnd * (norm2 p)))"


(* Standard terminology translated to the relational viewpoint *)

abbreviation composeRel :: 
" ('a Point ⇒ 'a Point ⇒ bool)
⇒('a Point ⇒ 'a Point ⇒ bool)
⇒('a Point ⇒ 'a Point ⇒ bool)"
  where "(composeRel g f) p r ≡ (∃ q . ((f p q) ∧ (g q r)))"


abbreviation injective :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ bool" 
  where "injective f ≡ ∀ x1 x2 y1 y2. 
                (f x1 y1 ∧ f x2 y2) ∧ (x1 ≠ x2) ⟶ (y1 ≠ y2)"

abbreviation definedAt :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ 'a Point ⇒ bool"
  where "definedAt f x ≡ ∃ y . f x y"

abbreviation domain :: "('a Point => 'a Point ⇒ bool) ⇒ 'a Point set"
  where "domain f  ≡ { x . definedAt f x }"

abbreviation total :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ bool" 
  where "total f ≡ ∀ x . (definedAt f x)"

abbreviation surjective :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ bool" 
  where "surjective f ≡ ∀ y . ∃ x . f x y"

abbreviation bijective :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ bool" 
  where "bijective f ≡ (injective f) ∧ (surjective f)"

abbreviation invertible :: "('a Point ⇒ 'a Point) ⇒ bool"
  where "invertible f ≡ ∀ q . (∃ p . (f p = q) ∧ (∀x. f x = q ⟶ x = p))"

  (* Image of a set *)

fun applyToSet :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ 'a Point set ⇒ 'a Point set" 
  where "applyToSet f s = { q . ∃ p ∈ s . f p q }" 


(* Recovering normal-style functions *)
abbreviation singleValued :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ 'a Point ⇒ bool"
  where "singleValued f x  ≡   ∀ y z . (((f x y) ∧ (f x z)) ⟶ (y = z))"

abbreviation isFunction :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ bool"
  where "isFunction f ≡ ∀ x . singleValued f x"

abbreviation isTotalFunction :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ bool"
  where "isTotalFunction f ≡ (total f) ∧ (isFunction f)"

fun toFunc:: "('a Point ⇒ 'a Point ⇒ bool) ⇒ 'a Point ⇒ 'a Point"
  where "toFunc f x = (SOME y . f x y)"

fun asFunc :: "('a Point ⇒ 'a Point) ⇒ ('a Point ⇒ 'a Point ⇒ bool)"
  where "(asFunc f) x y = (y = f x)"



(* g approximates f at x *)
(* Email of 16/07/2019 says final inequality should be ≤ not <. *)

subsection ‹ Differentiable approximation ›

text ‹Here we define differentiable approximation. This will be used later
when we define what it means for a worldview transformation to be "approximated"
by an affine transformation.›

abbreviation diffApprox :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ 
                            ('a Point ⇒ 'a Point ⇒ bool) ⇒
                             'a Point ⇒ bool"
  where "diffApprox g f x ≡ (definedAt f x) ∧
    (∀ ε > 0 . (∃ δ > 0 . (∀ y .
      ( (y within δ of x)
        ⟶ 
        ( (definedAt f y) ∧ (∀ u v . (f y u ∧ g y v) ⟶
         ( sep2 v u ) ≤ (sqr ε) * sep2 y x )))  )
  ))"


abbreviation cts ::  "('a Point ⇒ 'a Point ⇒ bool) ⇒ 'a Point ⇒ bool"
  where "cts f x ≡ ∀y . (f x y) ⟶ (∀ε>0. ∃δ>0. 
          (applyToSet f (ball x δ)) ⊆ ball y ε)"
                    

fun invFunc :: "('a Point ⇒ 'a Point ⇒ bool) ⇒ ('a Point ⇒ 'a Point ⇒ bool)"
  where "(invFunc f) p q = f q p"


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

lemma lemBijInv: "bijective (asFunc f) ⟷ invertible f"  
  by (metis asFunc.elims(1))
  

(* if g approximates f at x, then g(x) and f(x) share at least one value *)
subsection ‹ lemApproxEqualAtBase ›

text ‹The following lemma shows (as one would expect) that when one 
function differentiably approximates another at a point, they take equal values 
at that point.›

lemma lemApproxEqualAtBase:
assumes "diffApprox g f x"
shows "(f x y ∧ g x z) ⟶ (y = z)"
proof -
  { fix y z
    assume hyp: "f x y ∧ g x z"

    have lt01: "0 < 1" by auto
    then obtain d where dprops: "(d > 0) ∧ (∀ y .
        ( (y within d of x) 
          ⟶ 
          ( ∀ u v . (f y u ∧ g y v) ⟶
           ( sep2 v u ) ≤ (sqr 1) * sep2 y x ))  )
        " using assms(1) by best
  
    hence "x within d of x" by auto
    hence "∀ u v . (f x u ∧ g x v) ⟶ (sep2 v u) ≤ (sqr 1) * sep2 x x" 
      using dprops by blast
    hence sep0: "(sep2 z y) ≤ 0" using hyp by auto
    { assume "z ≠ y"
      hence "sep2 z y > 0" using lemNotEqualImpliesSep2Pos[of "z" "y"] by auto
      hence "False" using sep0 by auto
    }
    hence "z = y" by auto
  }
  thus ?thesis by auto
qed


lemma lemCtsOfCtsIsCts:
  assumes "cts f x"
and       "∀y . (f x y) ⟶ (cts g y)"
shows     "cts (composeRel g f) x"
proof -
  { fix z
    assume z: "(composeRel g f) x z"
    then obtain y where y: "f x y ∧ g y z" by auto

    { fix e
      assume epos: "e > 0"

      have "(∀ε>0. ∃δ>0.(applyToSet g (ball y δ)) ⊆ ball z ε)"
        using assms(2) y by auto
      then obtain dy 
        where dy: "(dy > 0) ∧ ((applyToSet g (ball y dy)) ⊆ ball z e)"
        using epos y by auto

      have "(∀ε>0. ∃δ>0.(applyToSet f (ball x δ)) ⊆ ball y ε)"
        using y assms(1) by auto
      then obtain d
        where d: "(d > 0) ∧ ((applyToSet f (ball x d)) ⊆ ball y dy)"
        using dy by auto

      { fix w
        assume w: "w ∈ applyToSet (composeRel g f) (ball x d)"
        then obtain u v 
          where v: "(u ∈ ball x d) ∧ (f u v) ∧ (g v w)" by auto
        hence "v ∈ ball y dy" using d by auto
        hence "w ∈ ball z e" using v dy by auto
      }
      hence "applyToSet (composeRel g f) (ball x d) ⊆ ball z e" by auto
      hence "∃d>0. (applyToSet (composeRel g f) (ball x d) ⊆ ball z e)" 
        using d by auto
    }
    hence "∀e>0. ∃d>0. applyToSet (composeRel g f) (ball x d) ⊆ ball z e" by auto
  }
  thus ?thesis by auto
qed


lemma lemInjOfInjIsInj:
  assumes "injective f"
and       "injective g"
shows     "injective (composeRel g f)"
proof -
  { fix x1 z1 x2 z2
    assume hyp: "(composeRel g f) x1 z1 ∧ (composeRel g f) x2 z2 ∧ (x1 ≠ x2)"
    then obtain y1 y2 
      where ys: "(f x1 y1) ∧ (g y1 z1) ∧ (f x2 y2) ∧ (g y2 z2)" by auto
    hence "y1 ≠ y2" using hyp assms(1) by auto
    hence "z1 ≠ z2" using  assms(2) ys by auto
  }
  thus ?thesis by auto
qed


lemma lemInverseComposition:
  assumes "h = composeRel g f"
  shows   "(invFunc h) = composeRel (invFunc f) (invFunc g)"
proof -
  { fix p r
    { assume hyp: "h p r"
      then obtain q where "f p q ∧ g q r" using assms by auto
      hence "(invFunc g) r q ∧ (invFunc f) q p" by force
      hence "(composeRel (invFunc f) (invFunc g)) r p" by blast
    }
    hence l2r: "(invFunc h) r p  ⟶ (composeRel (invFunc f) (invFunc g)) r p" by auto

    { assume "(composeRel (invFunc f) (invFunc g)) r p"
      then obtain q where "(invFunc g) r q  ∧  (invFunc f) q p" by auto
      hence "(invFunc h) r p" using assms by auto
    }

    hence "(composeRel (invFunc f) (invFunc g)) r p  ⟷ (invFunc h) r p"
      using l2r by auto
  }
  thus ?thesis by fastforce
qed


lemma lemToFuncAsFunc:
  assumes "isFunction f"
and       "total f"
shows     "asFunc (toFunc f) = f"
proof -
  { fix p r
    { assume "(asFunc (toFunc f)) p r"
      hence "f p r" using someI[of "f p"] assms(2) by auto
    }
    hence l2r: "(asFunc (toFunc f)) p r ⟶ f p r" by auto
    { assume fpr: "f p r"
      hence "(asFunc (toFunc f)) p r" using someI[of "f p"] assms(1) by auto
    }

    hence "f p r ⟷ (asFunc (toFunc f)) p r" using l2r by auto
  }
  thus ?thesis by blast
qed


lemma lemAsFuncToFunc: "toFunc (asFunc f) = f"
  by fastforce




end (* of class Functions *)

end (* of theory Functions *)