Theory Order_Functors_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Order Functors›
subsubsection ‹Basic Setup and Results›
theory Order_Functors_Base
  imports
    Functions_Inverse
    Order_Functions_Base
begin

text ‹In the following, we do not add any assumptions to our locales but rather
add them as needed to the theorem statements. This allows consumers to
state preciser results; particularly, the development of Transport depends
on this setup.›

locale orders =
  fixes L :: "'a ⇒ 'b ⇒ bool"
  and R :: "'c ⇒ 'd ⇒ bool"
begin

notation L (infix ‹≤⇘L⇙› 50)
notation R (infix ‹≤⇘R⇙› 50)

text‹We call @{term "(≤⇘L⇙)"} the ∗‹left relation› and @{term "(≤⇘R⇙)"} the
∗‹right relation›.›

abbreviation (input) "ge_left ≡ (≤⇘L⇙)¯"
notation ge_left (infix ‹≥⇘L⇙› 50)

abbreviation (input) "ge_right ≡ (≤⇘R⇙)¯"
notation ge_right (infix ‹≥⇘R⇙› 50)

end

text ‹Homogeneous orders›
locale hom_orders = orders L R
  for L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"

locale order_functor = hom_orders L R
  for L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'b ⇒ 'b ⇒ bool"
  and l :: "'a ⇒ 'b"
begin

lemma left_right_rel_left_self_if_reflexive_on_left_if_mono_left:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "reflexive_on P (≤⇘L⇙)"
  and "P x"
  shows "l x ≤⇘R⇙ l x"
  using assms by blast

lemma left_right_rel_left_self_if_reflexive_on_in_dom_right_if_mono_left:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "reflexive_on (in_dom (≤⇘R⇙)) (≤⇘R⇙)"
  and "in_dom (≤⇘L⇙) x"
  shows "l x ≤⇘R⇙ l x"
  using assms by blast

lemma left_right_rel_left_self_if_reflexive_on_in_codom_right_if_mono_left:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "reflexive_on (in_codom (≤⇘R⇙)) (≤⇘R⇙)"
  and "in_codom (≤⇘L⇙) x"
  shows "l x ≤⇘R⇙ l x"
  using assms by blast

lemma left_right_rel_left_self_if_reflexive_on_in_field_right_if_mono_left:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "reflexive_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  and "in_field (≤⇘L⇙) x"
  shows "l x ≤⇘R⇙ l x"
  using assms by blast

lemma mono_wrt_rel_left_if_reflexive_on_if_le_eq_if_mono_wrt_in_field:
  assumes "(in_field (≤⇘L⇙) ⇒ P) l"
  and "(≤⇘L⇙) ≤ (=)"
  and "reflexive_on P (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  using assms by (intro mono_wrt_relI) auto

end


locale order_functors = order_functor L R l + flip_of : order_functor R L r
  for L R l r
begin

text ‹We call the composition \<^term>‹r ∘ l› the ∗‹unit›
and the term \<^term>‹l ∘ r› the ∗‹counit› of the order functors pair.
This is terminology is borrowed from category theory - the functors
are an ∗‹adjoint›.›

definition "unit ≡ r ∘ l"

notation unit (‹η›)

lemma unit_eq_comp: "η = r ∘ l" unfolding unit_def by simp

lemma unit_eq [simp]: "η x = r (l x)" by (simp add: unit_eq_comp)

context
begin

text ‹Note that by flipping the roles of the left and rights functors,
we obtain a flipped interpretation of @{locale order_functors}.
In many cases, this allows us to obtain symmetric definitions and theorems for free.
As such, in many cases, we do we do not explicitly state those free results but
users can obtain them as needed by creating said flipped interpretation.›

interpretation flip : order_functors R L r l .

definition "counit ≡ flip.unit"

notation counit (‹ε›)

lemma counit_eq_comp: "ε = l ∘ r" unfolding counit_def flip.unit_def by simp

lemma counit_eq [simp]: "ε x = l (r x)" by (simp add: counit_eq_comp)

end

context
begin

interpretation flip : order_functors R L r l .

lemma flip_counit_eq_unit: "flip.counit = η"
  by (intro ext) simp

lemma flip_unit_eq_counit: "flip.unit = ε"
  by (intro ext) simp

lemma inflationary_on_unit_if_left_rel_right_if_left_right_relI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "reflexive_on P (≤⇘L⇙)"
  and "⋀x y. P x ⟹ l x ≤⇘R⇙ y ⟹ x ≤⇘L⇙ r y"
  shows "inflationary_on P (≤⇘L⇙) η"
  using assms by (intro inflationary_onI) fastforce

lemma deflationary_on_unit_if_right_left_rel_if_right_rel_leftI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "reflexive_on P (≤⇘L⇙)"
  and "⋀x y. P x ⟹ y ≤⇘R⇙ l x ⟹ r y ≤⇘L⇙ x"
  shows "deflationary_on P (≤⇘L⇙) η"
  using assms by (intro deflationary_onI) fastforce

context
  fixes P :: "'a ⇒ bool"
begin

lemma rel_equivalence_on_unit_iff_inflationary_on_if_inverse_on:
  assumes "inverse_on P l r"
  shows "rel_equivalence_on P (≤⇘L⇙) η ⟷ inflationary_on P (≤⇘L⇙) η"
  using assms by (intro iffI rel_equivalence_onI inflationary_onI deflationary_onI)
  (fastforce dest: inverse_onD)+

lemma reflexive_on_left_if_inflationary_on_unit_if_inverse_on:
  assumes "inverse_on P l r"
  and "inflationary_on P (≤⇘L⇙) η"
  shows "reflexive_on P (≤⇘L⇙)"
  using assms by (intro reflexive_onI) (force dest: inverse_onD)

lemma rel_equivalence_on_unit_if_reflexive_on_if_inverse_on:
  assumes "inverse_on P l r"
  and "reflexive_on P (≤⇘L⇙)"
  shows "rel_equivalence_on P (≤⇘L⇙) η"
  using assms by (intro rel_equivalence_onI inflationary_onI deflationary_onI) (force dest: inverse_onD)+

end

corollary rel_equivalence_on_unit_iff_reflexive_on_if_inverse_on:
  fixes P :: "'a ⇒ bool"
  assumes "inverse_on P l r"
  shows "rel_equivalence_on P (≤⇘L⇙) η ⟷ reflexive_on P (≤⇘L⇙)"
  using assms reflexive_on_left_if_inflationary_on_unit_if_inverse_on
    rel_equivalence_on_unit_if_reflexive_on_if_inverse_on
  by (intro iffI) auto

end


text ‹Here is an example of a free theorem.›

notepad
begin
  interpret flip : order_functors R L r l
    rewrites "flip.unit ≡ ε" by (simp only: flip_unit_eq_counit)
  have "⟦((≤⇘R⇙) ⇒ (≤⇘L⇙)) r; reflexive_on P (≤⇘R⇙); ⋀x y. ⟦P x; r x ≤⇘L⇙ y⟧ ⟹ x ≤⇘R⇙ l y⟧
      ⟹ inflationary_on P (≤⇘R⇙) ε" for P
    by (fact flip.inflationary_on_unit_if_left_rel_right_if_left_right_relI)
end

end


end