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. x1L x2  (≤⇘R x2 x2)  (≤⇘R x1 x2)"
  and "x1 x2. x1L 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" "x1L x1" "x1L x2"
    with assms have "f x1 ≤⇘R x1 x2g x1" "f x2 ≤⇘R x1 x2g 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)) m (x3 x4  (≤L) | x1L 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