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 ‹⇛⊕› 40)
syntax
  "_Mono_Dep_Fun_Rel_rel" :: "idt ⇒ idt ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒
    ('a ⇒ 'c) ⇒ ('b ⇒ 'd) ⇒ bool" (‹'(_/ _/ ∷/ _') ⇛⊕ (_)› [41, 41, 41, 40] 40)
  "_Mono_Dep_Fun_Rel_rel_if" :: "idt ⇒ idt ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool ⇒ ('c ⇒ 'd ⇒ bool) ⇒
    ('a ⇒ 'c) ⇒ ('b ⇒ 'd) ⇒ bool" (‹'(_/ _/ ∷/ _/ |/ _') ⇛⊕ (_)› [41, 41, 41, 41, 40] 40)
syntax_consts
  "_Mono_Dep_Fun_Rel_rel" "_Mono_Dep_Fun_Rel_rel_if" ⇌ Mono_Dep_Fun_Rel
translations
  "(x y ∷ R) ⇛⊕ S" ⇌ "CONST Mono_Dep_Fun_Rel R (λx y. S)"
  "(x y ∷ R | B) ⇛⊕ S" ⇌ "CONST Mono_Dep_Fun_Rel R (λx y. CONST rel_if B 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 L (infix ‹≤⇘L⇙› 50)
notation o.ge_left (infix ‹≥⇘L⇙› 50)

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

notation o.ge_right (‹(≥⇘R (_) (_)⇙)› 50)

abbreviation (input) "ge_right_infix d a b c ≡ (≥⇘R a b⇙) d c"
notation ge_right_infix (‹(_) ≥⇘R (_) (_)⇙ (_)› [51,51,51,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