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)"

bundle Mono_Dep_Fun_Rel_syntax begin
syntax
  "_Mono_Fun_Rel_rel" :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒
    ('a ⇒ 'b) ⇒ bool" ("(_) ⇛⊕ (_)" [41, 40] 40)
  "_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)
end
bundle no_Mono_Dep_Fun_Rel_syntax begin
no_syntax
  "_Mono_Fun_Rel_rel" :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒
    ('a ⇒ 'b) ⇒ bool" ("(_) ⇛⊕ (_)" [41, 40] 40)
  "_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)
end
unbundle Mono_Dep_Fun_Rel_syntax

translations
  "R ⇛⊕ S" ⇌ "CONST Mono_Fun_Rel R S"
  "(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)"

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 -
  {
    fix f g x1 x2
    assume "((x y ∷ (≤⇘L⇙)) ⇛ (≤⇘R x y⇙)) f g" "x1 ≤⇘L⇙ x1" "x1 ≤⇘L⇙ x2"
    with assms have "f x1 ≤⇘R x1 x2⇙ g x1" "f x2 ≤⇘R x1 x2⇙ g x2" 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)
  (auto 6 0)

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