Theory Monotone_Function_Relator

✐‹creator "Kevin Kappelmann"›
section ‹Monotone Function Relator›
theory Monotone_Function_Relator
  imports
    Reflexive_Relator
begin

abbreviation "Mono_Dep_Fun_Rel (R :: 'a ⇒ 'a ⇒ bool) (S :: 'a ⇒ 'a ⇒ 'b ⇒ 'b ⇒ bool) ≡
  ((x y ∷ R) ⇛ S x y)⇧⊕"
abbreviation "Mono_Fun_Rel R S ≡ Mono_Dep_Fun_Rel R (λ_ _. S)"

open_bundle Mono_Dep_Fun_Rel_syntax
begin
notation "Mono_Fun_Rel" (infixr ‹⇛⊕› 50)
syntax
  "_Mono_Dep_Fun_Rel_rel" :: "idt ⇒ idt ⇒ 'a ⇒ 'b ⇒ 'c" (‹('(_ _ ∷ _') ⇛⊕/ _)› [0,0, 0, 10] 50)
syntax_consts
  "_Mono_Dep_Fun_Rel_rel" ⇌ Mono_Dep_Fun_Rel
translations
  "(x y ∷ R) ⇛⊕ S" ⇌ "CONST Mono_Dep_Fun_Rel R (λx y. S)"
end

text ‹The monotone function relator is the function relator restricted to monotone functions:›

lemma Mono_Dep_Fun_Rel_eq_Dep_Fun_Rel_restrict_dep_monos:
  fixes R S defines "dep_mono ≡ ((x y ∷ R) ⇒ S x y)"
  shows "((x y ∷ R) ⇛⊕ S x y) = ((x y ∷ R) ⇛ S x y)↾⇘dep_mono⇙↿⇘dep_mono⇙"
  unfolding dep_mono_def by force

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

sublocale o : orders L "R a b" for a b .

notation o.ge_left (infix ‹≥⇘L⇙› 50)

notation (input) R (‹('(≤(⇘R (_) (_)⇙)'))›)
notation (output) R (‹('(≤(⇘R ('(_')) ('(_'))⇙)'))›)
abbreviation "right_infix c a b d ≡ (≤⇘R a b⇙) c d"
notation (input) right_infix (‹(_ ≤(⇘R (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) right_infix (‹(_ ≤(⇘R ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)

notation (input) o.ge_right (‹('(≥(⇘R (_) (_)⇙)'))›)
notation (output) o.ge_right (‹('(≥(⇘R ('(_')) ('(_'))⇙)'))›)
abbreviation (input) "ge_right_infix d a b c ≡ (≤⇘R a b⇙) d c"
notation (input) ge_right_infix (‹(_ ≥(⇘R (_) (_)⇙) _)› [51,0,0,51] 50)
notation (output) ge_right_infix (‹(_ ≥(⇘R ('(_')) ('(_'))⇙) _)› [51,0,0,51] 50)

abbreviation (input) "DFR ≡ ((a b ∷ (≤⇘L⇙)) ⇛ (≤⇘R a b⇙))"

end

locale hom_Dep_Fun_Rel_orders = Dep_Fun_Rel_orders L R
  for L :: "'a ⇒ 'a ⇒ bool"
  and R :: "'a ⇒ 'a ⇒ 'b ⇒ 'b ⇒ bool"
begin

sublocale ho : hom_orders L "R a b" for a b .

lemma Mono_Dep_Fun_Refl_Rel_right_eq_Mono_Dep_Fun_if_le_if_reflexive_onI:
  assumes refl_L: "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x2 x2⇙) ≤ (≤⇘R x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L⇙ x2 ⟹ (≤⇘R x1 x1⇙) ≤ (≤⇘R x1 x2⇙)"
  shows "((x y ∷ (≤⇘L⇙)) ⇛⊕ (≤⇘R x y⇙)⇧⊕) = ((x y ∷ (≤⇘L⇙)) ⇛⊕ (≤⇘R x y⇙))"
proof -
  have "f x1 ≤⇘R x1 x2⇙ g x1" "f x2 ≤⇘R x1 x2⇙ g x2"
    if "((x y ∷ (≤⇘L⇙)) ⇛ (≤⇘R x y⇙)) f g" "x1 ≤⇘L⇙ x1" "x1 ≤⇘L⇙ x2" for f g x1 x2
    using that assms by blast+
  with refl_L show ?thesis
    by (intro ext iffI Refl_RelI Dep_Fun_Rel_relI) (auto elim!: Refl_RelE)
qed

lemma Mono_Dep_Fun_Refl_Rel_right_eq_Mono_Dep_Fun_if_mono_if_reflexive_onI:
  assumes "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  and "((x1 x2 ∷ (≥⇘L⇙)) ⇒ ⦇x3 x4 ∷ (≤⇘L⇙) | x1 ≤⇘L⇙ x3⦈ ⇛ (≤)) R"
  shows "((x y ∷ (≤⇘L⇙)) ⇛⊕ (≤⇘R x y⇙)⇧⊕) = ((x y ∷ (≤⇘L⇙)) ⇛⊕ (≤⇘R x y⇙))"
  using assms
  by (intro Mono_Dep_Fun_Refl_Rel_right_eq_Mono_Dep_Fun_if_le_if_reflexive_onI)
  blast+

end

context hom_orders
begin

sublocale fro : hom_Dep_Fun_Rel_orders L "λ_ _. R" .

corollary Mono_Fun_Rel_Refl_Rel_right_eq_Mono_Fun_RelI:
  assumes "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)"
  shows "((≤⇘L⇙) ⇛⊕ (≤⇘R⇙)⇧⊕) = ((≤⇘L⇙) ⇛⊕ (≤⇘R⇙))"
  using assms by (intro fro.Mono_Dep_Fun_Refl_Rel_right_eq_Mono_Dep_Fun_if_le_if_reflexive_onI)
  simp_all

end

end