Theory Functions_Monotone

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Monotonicity›
theory Functions_Monotone
  imports
    Binary_Relations_Order_Base
    Function_Relators
    Predicates_Order
begin

paragraph ‹Summary›
text ‹Introduces the concept of monotone functions. A function is monotone
if it is related to itself - see \<^term>‹Dep_Fun_Rel_rel›.›

declare le_funI[intro]
declare le_funE[elim]

consts dep_mono_wrt_rel :: "'a ⇒ 'b ⇒ 'c"
consts dep_mono_wrt_pred :: "'a ⇒ 'b ⇒ 'c"
consts mono_wrt :: "'a ⇒ 'b ⇒ 'c"

nonterminal dep_pred_restrict and dep_mono_wrt_rel_pttrn and dep_mono_wrt_pred_pttrn
open_bundle dep_mono_wrt_syntax
begin
no_notation disj (infixr ‹|› 30)
notation "mono_wrt" (infixr ‹⇒› 50)
syntax
  "_dep_pred_restrict_if" :: "'a ⇒ dep_pred_restrict" (‹(|/ _)›)
  "_dep_mono_wrt_rel" :: "dep_mono_wrt_rel_pttrn ⇒ 'a ⇒ bool" (‹(_ ⇒/ _)› [0, 10] 50)
  "_dep_mono_wrt_rel_standard" :: "idt ⇒ idt ⇒ 'a ⇒ dep_mono_wrt_rel_pttrn" (‹('(_ _ ∷ _'))›)
  "_dep_mono_wrt_rel_restrict" :: "idt ⇒ idt ⇒ 'a ⇒ dep_rel_restrict  ⇒ dep_mono_wrt_rel_pttrn" (‹('(_ _ ∷ _ _'))›)
  "_dep_mono_wrt_pred" :: "dep_mono_wrt_pred_pttrn ⇒ 'a ⇒ bool" (‹(_ ⇒/ _)› [0, 10] 50)
  "_dep_mono_wrt_pred_standard" :: "idt ⇒ 'a ⇒ dep_mono_wrt_pred_pttrn" (‹('(_ : _'))›)
  "_dep_mono_wrt_pred_restrict" :: "idt ⇒ 'a ⇒ dep_pred_restrict  ⇒ dep_mono_wrt_pred_pttrn" (‹('(_ : _ _'))›)
syntax_consts
  "_dep_pred_restrict_if" ⇌ pred_if
  and "_dep_mono_wrt_rel" "_dep_mono_wrt_rel_standard" "_dep_mono_wrt_rel_restrict" ⇌ dep_mono_wrt_rel
  and "_dep_mono_wrt_pred" "_dep_mono_wrt_pred_standard" "_dep_mono_wrt_pred_restrict" ⇌ dep_mono_wrt_pred
translations
  "(x y ∷ R | P) ⇒ S" ⇌ "CONST dep_mono_wrt_rel R (λx y. CONST rel_if P S)"
  "(x y ∷ R) ⇒ S" ⇌ "CONST dep_mono_wrt_rel R (λx y. S)"
  "(x : P | Q) ⇒ U" ⇌ "CONST dep_mono_wrt_pred P (λx. CONST pred_if Q U)"
  "(x : P) ⇒ Q" ⇌ "CONST dep_mono_wrt_pred P (λx. Q)"
end

definition "dep_mono_wrt_rel_rel (R :: 'a ⇒ 'a ⇒ bool)
  (S :: 'a ⇒ 'a ⇒ 'b ⇒ 'b ⇒ bool) (f :: 'a ⇒ 'b) ≡ ((x y ∷ R) ⇛ S x y) f f"
adhoc_overloading dep_mono_wrt_rel ⇌ dep_mono_wrt_rel_rel

definition "mono_wrt_rel (R :: 'a ⇒ 'a ⇒ bool) (S :: 'b ⇒ 'b ⇒ bool) ≡
  ((_ _ ∷ R) ⇒ S) :: ('a ⇒ 'b) ⇒ bool"
adhoc_overloading mono_wrt ⇌ mono_wrt_rel

definition "dep_mono_wrt_pred_pred (P :: 'a ⇒ bool) (Q :: 'a ⇒ 'b ⇒ bool) (f :: 'a ⇒ 'b) ≡
  ((x : P) ⇛ (λ(_ :: 'b). Q x)) f f"
adhoc_overloading dep_mono_wrt_pred ⇌ dep_mono_wrt_pred_pred

definition "mono_wrt_pred (P :: 'a ⇒ bool) (Q :: 'b ⇒ bool) ≡
  (((_ :: 'a) : P) ⇒ Q) :: ('a ⇒ 'b) ⇒ bool"
adhoc_overloading mono_wrt ⇌ mono_wrt_pred

lemma mono_wrt_rel_eq_dep_mono_wrt_rel:
  "((R :: 'a ⇒ 'a ⇒ bool) ⇒ (S :: 'b ⇒ 'b ⇒ bool)) = ((_ _ ∷ R) ⇒ S)"
  unfolding mono_wrt_rel_def by simp

lemma mono_wrt_rel_eq_dep_mono_wrt_rel_uhint [uhint]:
  assumes "R ≡ R'"
  and "⋀x y. S' x y ≡ S"
  shows "((R :: 'a ⇒ 'a ⇒ bool) ⇒ (S :: 'b ⇒ 'b ⇒ bool)) = ((x y ∷ R') ⇒ S' x y)"
  using assms by (simp add: mono_wrt_rel_eq_dep_mono_wrt_rel)

lemma mono_wrt_rel_iff_dep_mono_wrt_rel:
  "((R :: 'a ⇒ 'a ⇒ bool) ⇒ (S :: 'b ⇒ 'b ⇒ bool)) f ⟷
    dep_mono_wrt_rel R (λ(_ :: 'a) (_ :: 'a). S) (f :: 'a ⇒ 'b)"
  by (simp add: mono_wrt_rel_eq_dep_mono_wrt_rel)

lemma mono_wrt_pred_eq_dep_mono_wrt_pred:
  "((P :: 'a ⇒ bool) ⇒ (Q :: 'b ⇒ bool)) = (((_ :: 'a) : P) ⇒ Q)"
  unfolding mono_wrt_pred_def by simp

lemma mono_wrt_pred_eq_dep_mono_wrt_pred_uhint [uhint]:
  assumes "P ≡ P'"
  and "⋀x. Q ≡ Q' x"
  shows "((P :: 'a ⇒ bool) ⇒ (Q :: 'b ⇒ bool)) = (((x : P') ⇒ Q' x) :: ('a ⇒ 'b) ⇒ bool)"
  using assms by (simp add: mono_wrt_pred_eq_dep_mono_wrt_pred)

lemma mono_wrt_pred_iff_dep_mono_wrt_pred:
  "((P :: 'a ⇒ bool) ⇒ (Q :: 'b ⇒ bool)) f ⟷ (((_ :: 'a) : P) ⇒ Q) (f :: 'a ⇒ 'b)"
  by (simp add: mono_wrt_pred_eq_dep_mono_wrt_pred)

lemma dep_mono_wrt_relI [intro]:
  assumes "⋀x y. R x y ⟹ S x y (f x) (f y)"
  shows "((x y ∷ R) ⇒ S x y) f"
  using assms unfolding dep_mono_wrt_rel_rel_def by blast

lemma dep_mono_wrt_relE:
  assumes "((x y ∷ R) ⇒ S x y) f"
  obtains "⋀x y. R x y ⟹ S x y (f x) (f y)"
  using assms unfolding dep_mono_wrt_rel_rel_def by blast

lemma dep_mono_wrt_relD [dest]:
  assumes "((x y ∷ R) ⇒ S x y) f"
  and "R x y"
  shows "S x y (f x) (f y)"
  using assms unfolding dep_mono_wrt_rel_rel_def by blast

lemma dep_mono_wrt_rel_cong [cong]:
  assumes "R = R'"
  and "⋀x y. R' x y ⟹ S x y = S' x y"
  shows "((x y ∷ R) ⇒ S x y) = ((x y ∷ R') ⇒ S' x y)"
  using assms by force

lemma mono_wrt_relI [intro]:
  assumes "⋀x y. R x y ⟹ S (f x) (f y)"
  shows "(R ⇒ S) f"
  using assms by (urule dep_mono_wrt_relI)

lemma mono_wrt_relE:
  assumes "(R ⇒ S) f"
  obtains "⋀x y. R x y ⟹ S (f x) (f y)"
  using assms by (urule (e) dep_mono_wrt_relE)

lemma mono_wrt_relD [dest]:
  assumes "(R ⇒ S) f"
  and "R x y"
  shows "S (f x) (f y)"
  using assms by (urule dep_mono_wrt_relD)

lemma dep_mono_wrt_rel_collect_eq_dep_mono_wrt_rel_if [simp]:
  "((x y ∷ ⦇x y ∷ R | P x y⦈) ⇒ S x y) = ((x y ∷ R | P x y) ⇒ S x y)"
  by fastforce

lemma mono_wrt_rel_collect_eq_dep_mono_wrt_rel_if [simp]:
  "(⦇x y ∷ R | P x y⦈ ⇒ S) = ((x y ∷ R | P x y) ⇒ S)"
  by fastforce

lemma dep_mono_wrt_predI [intro]:
  assumes "⋀x. P x ⟹ Q x (f x)"
  shows "((x : P) ⇒ Q x) f"
  using assms unfolding dep_mono_wrt_pred_pred_def by blast

lemma dep_mono_wrt_predE:
  assumes "((x : P) ⇒ Q x) f"
  obtains "⋀x. P x ⟹ Q x (f x)"
  using assms unfolding dep_mono_wrt_pred_pred_def by blast

lemma dep_mono_wrt_predD [dest]:
  assumes "((x : P) ⇒ Q x) f"
  and "P x"
  shows "Q x (f x)"
  using assms unfolding dep_mono_wrt_pred_pred_def by blast

lemma dep_mono_wrt_pred_cong [cong]:
  assumes "P = P'"
  and "⋀x. P' x ⟹ Q x = Q' x"
  shows "((x : P) ⇒ Q x) = ((x : P') ⇒ Q' x)"
  using assms by force

lemma dep_mono_wrt_pred_codom_iff_cong:
  assumes "P = P'"
  and "⋀x. P' x ⟹ Q x (f x) ⟷ Q' x (f' x)"
  shows "((x : P) ⇒ Q x) f ⟷ ((x : P') ⇒ Q' x) f'"
  using assms by force

lemma mono_wrt_predI [intro]:
  assumes "⋀x. P x ⟹ Q (f x)"
  shows "(P ⇒ Q) f"
  using assms by (urule dep_mono_wrt_predI)

lemma mono_wrt_predE:
  assumes "(P ⇒ Q) f"
  obtains "⋀x. P x ⟹ Q (f x)"
  using assms by (urule (e) dep_mono_wrt_predE)

lemma mono_wrt_predD [dest]:
  assumes "(P ⇒ Q) f"
  and "P x"
  shows "Q (f x)"
  using assms by (urule dep_mono_wrt_predD)

lemma Dep_Fun_Rel_pred_collect_eq_Dep_Fun_Rel_pred_if [simp]:
  "((x : ⦇x : P | Q x⦈) ⇒ R x) = ((x : P | Q x) ⇒ R x)"
  by fastforce

lemma Fun_Rel_pred_collect_eq_Dep_Fun_Rel_pred_if [simp]:
  "(⦇x : P | Q x⦈ ⇒ R) = ((x : P | Q x) ⇒ R)"
  by fastforce

context
  fixes R :: "'a ⇒ 'a ⇒ bool" and S :: "'a ⇒ 'a ⇒ 'b ⇒ 'b ⇒ bool" and f :: "'a ⇒ 'b"
  and P :: "'a ⇒ bool" and Q :: "'a ⇒ 'b ⇒ bool"
begin

lemma dep_mono_wrt_rel_if_Dep_Fun_Rel_rel_self:
  assumes "((x y ∷ R) ⇛ S x y) f f"
  shows "((x y ∷ R) ⇒ S x y) f"
  using assms by blast

lemma dep_mono_wrt_pred_if_Dep_Fun_Rel_pred_self:
  assumes "((x : P) ⇛ (λ_. Q x)) f f"
  shows "((x : P) ⇒ Q x) f"
  using assms by blast

lemma Dep_Fun_Rel_rel_self_if_dep_mono_wrt_rel:
  assumes "((x y ∷ R) ⇒ S x y) f"
  shows "((x y ∷ R) ⇛ S x y) f f"
  using assms by blast

lemma Dep_Fun_Rel_pred_self_if_dep_mono_wrt_pred:
  assumes "((x : P) ⇒ Q x) f"
  shows "((x : P) ⇛ (λ_. Q x)) f f"
  using assms by blast

corollary Dep_Fun_Rel_rel_self_iff_dep_mono_wrt_rel:
  "((x y ∷ R) ⇛ S x y) f f ⟷ ((x y ∷ R) ⇒ S x y) f"
  using dep_mono_wrt_rel_if_Dep_Fun_Rel_rel_self
    Dep_Fun_Rel_rel_self_if_dep_mono_wrt_rel by blast

corollary Dep_Fun_Rel_pred_self_iff_dep_mono_wrt_pred:
  "((x : P) ⇛ (λ(_ :: 'b). Q x)) f f ⟷ ((x : P) ⇒ Q x) f"
  using dep_mono_wrt_pred_if_Dep_Fun_Rel_pred_self
    Dep_Fun_Rel_pred_self_if_dep_mono_wrt_pred by blast

lemma dep_mono_wrt_rel_eq_Dep_Fun_Rel_rel [uhint]:
  assumes "R ≡ R'"
  and "⋀x y. S x y ≡ S' x y"
  and "f ≡ f'"
  shows "((x y ∷ R) ⇒ S x y) f ≡ ((x y ∷ R') ⇛ S' x y) f' f'"
  using assms unfolding Dep_Fun_Rel_rel_self_iff_dep_mono_wrt_rel atomize_eq by auto

lemma dep_mono_wrt_pred_eq_Dep_Fun_Rel_pred [uhint]:
  assumes "P ≡ P'"
  and "⋀x y. Q x y ≡ Q' x y y"
  and "f ≡ f'"
  shows "((x : P) ⇒ Q x) f ≡ ((x : P') ⇛ Q' x) f' f'"
  using assms unfolding Dep_Fun_Rel_pred_self_iff_dep_mono_wrt_pred atomize_eq by auto

lemma dep_mono_wrt_rel_inv_inv_eq [simp]:
  "((y x ∷ R¯) ⇒ (S x y)¯) = ((x y ∷ R) ⇒ S x y)"
  by (intro ext) force

lemma in_dom_if_rel_if_dep_mono_wrt_rel:
  assumes "((x y ∷ R) ⇒ S x y) f"
  and "R x y"
  shows "in_dom (S x y) (f x)"
  using assms by (intro in_domI) blast

end

context
  fixes R :: "'a ⇒ 'a ⇒ bool" and f :: "'a ⇒ 'b"
begin

lemma mono_wrt_rel_eq_Fun_Rel_rel [uhint]:
  assumes "R ≡ R'"
  and "S ≡ S'"
  and "f ≡ f'"
  shows "(R ⇒ S) f ≡ (R' ⇛ S') f' f'"
  using assms by (urule dep_mono_wrt_rel_eq_Dep_Fun_Rel_rel)

lemma mono_wrt_pred_eq_Fun_Rel_pred [uhint]:
  assumes "P :: _ ⇒ bool ≡ P'"
  and "⋀y. Q y ≡ Q' y y"
  and "f ≡ f'"
  shows "(P ⇒ Q) f ≡ (P' ⇛ Q') f' f'"
  using assms by (urule dep_mono_wrt_pred_eq_Dep_Fun_Rel_pred)

corollary in_dom_if_in_dom_if_mono_wrt_rel:
  assumes "(R ⇒ S) f"
  shows "(in_dom R ⇒ in_dom S) f"
  using assms in_dom_if_rel_if_dep_mono_wrt_rel by fast

lemma in_codom_if_rel_if_dep_mono_wrt_rel:
  assumes "((x y ∷ R) ⇒ S x y) f"
  and "R x y"
  shows "in_codom (S x y) (f y)"
  using assms by (intro in_codomI) blast

corollary in_codom_if_in_codom_if_mono_wrt_rel:
  assumes "(R ⇒ S) f"
  shows "(in_codom R ⇒ in_codom S) f"
  using assms in_dom_if_rel_if_dep_mono_wrt_rel
  by fast

corollary in_field_if_in_field_if_mono_wrt_rel:
  assumes "(R ⇒ S) f"
  shows "(in_field R ⇒ in_field S) f"
  using assms by fast

lemma le_rel_map_if_mono_wrt_rel:
  assumes "(R ⇒ S) f"
  shows "R ≤ rel_map f S"
  using assms by (intro le_relI) auto

lemma le_pred_map_if_mono_wrt_pred:
  assumes "(P ⇒ Q) f"
  shows "P ≤ pred_map f Q"
  using assms by (intro le_predI) auto

lemma mono_wrt_rel_if_le_rel_map:
  assumes "R ≤ rel_map f S"
  shows "(R ⇒ S) f"
  using assms by (intro mono_wrt_relI) auto

lemma mono_wrt_pred_if_le_pred_map:
  assumes "P ≤ pred_map f Q"
  shows "(P ⇒ Q) f"
  using assms by (intro mono_wrt_predI) auto

corollary mono_wrt_rel_iff_le_rel_map: "(R ⇒ S) f ⟷ R ≤ rel_map f S"
  using mono_wrt_rel_if_le_rel_map le_rel_map_if_mono_wrt_rel by auto

corollary mono_wrt_pred_iff_le_pred_map: "(P ⇒ Q) f ⟷ P ≤ pred_map f Q"
  using mono_wrt_pred_if_le_pred_map le_pred_map_if_mono_wrt_pred by auto

end

lemma dep_mono_comp_iff_dep_mono_if_all_app_eq:
  assumes "⋀x. A x ⟹ f (m x) = g x"
  shows "((x : (A :: _ ⇒ bool)) ⇒ B x) (f ∘ m) ⟷ ((x : A) ⇒ B x) g"
  using assms by fastforce

lemma dep_mono_pred_map_comp_iff_dep_mono_if_all_app_eq:
  assumes "⋀x y. A x ⟹ B x y ⟹ f x (m y) = g x y"
  shows "((x : A) ⇒ pred_map (λf. f ∘ m) ((y : B x) ⇒ C x y)) f
    ⟷ ((x : A) ⇒ (y : (B x :: _ ⇒ bool)) ⇒ C x y) g"
  using assms by (simp cong: dep_mono_wrt_pred_codom_iff_cong)

definition "mono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool
  ≡ (((≤) :: 'a ⇒ 'a ⇒ bool) ⇒ ((≤) :: 'b ⇒ 'b ⇒ bool))"

lemma mono_eq_mono_wrt_le [simp]: "(mono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool) =
  (((≤) :: 'a ⇒ 'a ⇒ bool) ⇒ ((≤) :: 'b ⇒ 'b ⇒ bool))"
  unfolding mono_def by simp

lemma mono_eq_mono_wrt_le_uhint [uhint]:
  assumes "R ≡ (≤) :: 'a ⇒ 'a ⇒ bool"
  and "S ≡ (≤) :: 'b ⇒ 'b ⇒ bool"
  shows "mono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool ≡ (R ⇒ S)"
  using assms by simp

lemma mono_iff_mono_wrt_le [iff]: "mono f ⟷ ((≤) ⇒ (≤)) f" by simp

lemma monoI [intro]:
  assumes "⋀x y. x ≤ y ⟹ f x ≤ f y"
  shows "mono f"
  using assms by (urule mono_wrt_relI)

lemma monoE [elim]:
  assumes "mono f"
  obtains "⋀x y. x ≤ y ⟹ f x ≤ f y"
  using assms by (urule (e) mono_wrt_relE)

lemma monoD:
  assumes "mono f"
  and "x ≤ y"
  shows "f x ≤ f y"
  using assms by (urule mono_wrt_relD)

definition "antimono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool
  ≡ (((≤) :: 'a ⇒ 'a ⇒ bool) ⇒ ((≥) :: 'b ⇒ 'b ⇒ bool))"

lemma antimono_eq_mono_wrt_le_ge [simp]: "(antimono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool) =
  (((≤) :: 'a ⇒ 'a ⇒ bool) ⇒ ((≥) :: 'b ⇒ 'b ⇒ bool))"
  unfolding antimono_def by simp

lemma antimono_eq_mono_wrt_le_ge_uhint [uhint]:
  assumes "R ≡ (≤) :: 'a ⇒ 'a ⇒ bool"
  and "S ≡ (≥) :: 'b ⇒ 'b ⇒ bool"
  shows "antimono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool ≡ (R ⇒ S)"
  using assms by simp

lemma antimono_iff_mono_wrt_le_ge [iff]: "antimono f ⟷ ((≤) ⇒ (≥)) f" by simp

lemma antimonoI [intro]:
  assumes "⋀x y. x ≤ y ⟹ f x ≥ f y"
  shows "antimono f"
  by (urule mono_wrt_relI) (urule assms)

lemma antimonoE [elim]:
  assumes "antimono f"
  obtains "⋀x y. x ≤ y ⟹ f x ≥ f y"
  using assms by (urule (e) mono_wrt_relE)

lemma antimonoD:
  assumes "antimono f"
  and "x ≤ y"
  shows "f x ≥ f y"
  using assms by (urule mono_wrt_relD)

lemma antimono_Dep_Fun_Rel_rel_left: "antimono (λ(R :: 'a ⇒ 'b ⇒ bool). ((x y ∷ R) ⇛ S x y))"
  by (intro antimonoI) auto

lemma antimono_Dep_Fun_Rel_pred_left: "antimono (λ(P :: 'a ⇒ bool). ((x : P) ⇛ Q x))"
  by (intro antimonoI) auto

lemma antimono_dep_mono_wrt_rel_left: "antimono (λ(R :: 'a ⇒ 'a ⇒ bool). ((x y ∷ R) ⇒ S x y))"
  by (intro antimonoI) blast

lemma antimono_dep_mono_wrt_pred_left: "antimono (λ(P :: 'a ⇒ bool). ((x : P) ⇒ Q x))"
  by (intro antimonoI) blast

lemma Dep_Fun_Rel_rel_if_le_left_if_Dep_Fun_Rel_rel:
  fixes R R' :: "'a ⇒ 'b ⇒ bool"
  assumes "((x y ∷ R) ⇛ S x y) f g"
  and "R' ≤ R"
  shows "((x y ∷ R) ⇛ S x y) f g"
  using assms by blast

lemma Dep_Fun_Rel_pred_if_le_left_if_Dep_Fun_Rel_pred:
  fixes P P' :: "'a ⇒ bool"
  assumes "((x : P) ⇛ Q x) f g"
  and "P' ≤ P"
  shows "((x : P') ⇛ Q x) f g"
  using assms by blast

lemma dep_mono_wrt_rel_if_le_left_if_dep_mono_wrt_rel:
  fixes R R' :: "'a ⇒ 'a ⇒ bool"
  assumes "((x y ∷ R) ⇒ S x y) f"
  and "R' ≤ R"
  shows "((x y ∷ R') ⇒ S x y) f"
  using assms by blast

lemma dep_mono_wrt_pred_if_le_left_if_dep_mono_wrt_pred:
  fixes P P' :: "'a ⇒ bool"
  assumes "((x : P) ⇒ Q x) f"
  and "P' ≤ P"
  shows "((x : P') ⇒ Q x) f"
  using assms by blast

lemma mono_Dep_Fun_Rel_rel_right: "mono (λ(S :: 'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool). ((x y ∷ R) ⇛ S x y))"
  by (intro monoI) blast

lemma mono_Dep_Fun_Rel_pred_right: "mono (λ(Q :: 'a ⇒ 'b ⇒ 'c ⇒ bool). ((x : P) ⇛ Q x))"
  by (intro monoI) blast

lemma mono_dep_mono_wrt_rel_right: "mono (λ(S :: 'a ⇒ 'a ⇒ 'b ⇒ 'b ⇒ bool). ((x y ∷ R) ⇒ S x y))"
  by (intro monoI) blast

lemma mono_dep_mono_wrt_pred_right: "mono (λ(Q :: 'a ⇒ 'b ⇒ bool). ((x : P) ⇒ Q x))"
  by (intro monoI) blast

lemma Dep_Fun_Rel_rel_if_le_right_if_Dep_Fun_Rel_rel:
  assumes "((x y ∷ R) ⇛ S x y) f g"
  and "⋀x y. R x y ⟹ S x y (f x) (g y) ⟹ T x y (f x) (g y)"
  shows "((x y ∷ R) ⇛ T x y) f g"
  using assms by (intro Dep_Fun_Rel_relI) blast

lemma Dep_Fun_Rel_pred_if_le_right_if_Dep_Fun_Rel_pred:
  assumes "((x : P) ⇛ Q x) f g"
  and "⋀x. P x ⟹ Q x (f x) (g x) ⟹ T x (f x) (g x)"
  shows "((x : P) ⇛ T x) f g"
  using assms by blast

lemma dep_mono_wrt_rel_if_le_right_if_dep_mono_wrt_rel:
  assumes "((x y ∷ R) ⇒ S x y) f"
  and "⋀x y. R x y ⟹ S x y (f x) (f y) ⟹ T x y (f x) (f y)"
  shows "((x y ∷ R) ⇒ T x y) f"
  using assms by (intro dep_mono_wrt_relI) blast

lemma dep_mono_wrt_pred_if_le_right_if_dep_mono_wrt_pred:
  assumes "((x : P) ⇒ Q x) f"
  and "⋀x. P x ⟹ Q x (f x) ⟹ T x (f x)"
  shows "((x : P) ⇒ T x) f"
  using assms by blast


paragraph ‹Composition›

lemma dep_mono_wrt_rel_compI:
  assumes "((x y ∷ R) ⇒ S x y) f"
  and "⋀x y. R x y ⟹ ((x' y' ∷ T x y) ⇒ U x y x' y') f'"
  and "⋀x y. R x y ⟹ S x y (f x) (f y) ⟹ T x y (f x) (f y)"
  shows "((x y ∷ R) ⇒ U x y (f x) (f y)) (f' ∘ f)"
  using assms by (intro dep_mono_wrt_relI) force

corollary dep_mono_wrt_rel_compI':
  assumes "((x y ∷ R) ⇒ S x y) f"
  and "⋀x y. R x y ⟹ ((x' y' ∷ S x y) ⇒ T x y x' y') f'"
  shows "((x y ∷ R) ⇒ T x y (f x) (f y)) (f' ∘ f)"
  using assms by (intro dep_mono_wrt_rel_compI)

lemma dep_mono_wrt_pred_comp_dep_mono_wrt_rel_compI:
  assumes "((x : P) ⇒ Q x) f"
  and "⋀x. P x ⟹ ((x' y' ∷ R x) ⇒ S x x' y') f'"
  and "⋀x. P x ⟹ Q x (f x) ⟹ R x (f x) (f x)"
  shows "((x : P) ⇒ (λy. S x (f x) (f x) y y)) (f' ∘ f)"
  using assms by (intro dep_mono_wrt_predI) force

lemma dep_mono_wrt_pred_comp_dep_mono_wrt_pred_compI:
  assumes "((x : P) ⇒ Q x) f"
  and "⋀x. P x ⟹ ((x' : R x) ⇒ S x x') f'"
  and "⋀x. P x ⟹ Q x (f x) ⟹ R x (f x)"
  shows "((x : P) ⇒ S x (f x)) (f' ∘ f)"
  using assms by (intro dep_mono_wrt_predI) force

corollary dep_mono_wrt_pred_comp_dep_mono_wrt_pred_compI':
  assumes "((x : P) ⇒ Q x) f"
  and "⋀x. P x ⟹ ((x' : Q x) ⇒ S x x') f'"
  shows "((x : P) ⇒ S x (f x)) (f' ∘ f)"
  using assms by (intro dep_mono_wrt_pred_comp_dep_mono_wrt_pred_compI)

lemma mono_wrt_rel_top [iff]:
  fixes R :: "'a ⇒ 'a ⇒ bool" and f :: "'a ⇒ 'b"
  shows "(R ⇒ (⊤ :: 'b ⇒ 'b ⇒ bool)) f"
  by auto

lemma mono_wrt_pred_top [iff]:
  fixes P :: "'a ⇒ bool" and f :: "'a ⇒ 'b"
  shows "(P ⇒ (⊤ :: 'b ⇒ bool)) f"
  by auto

paragraph ‹Instantiations›

lemma mono_wrt_rel_self_id:
  fixes R :: "'a ⇒ 'a ⇒ bool"
  shows "(R ⇒ R) (id :: 'a ⇒ 'a)"
  by auto

lemma mono_wrt_pred_self_id:
  fixes P :: "'a ⇒ bool"
  shows "(P ⇒ P) (id :: 'a ⇒ 'a)"
  by auto

lemma mono_dep_mono_wrt_dep_mono_wrt_comp:
  "(((x : (B :: 'b ⇒ bool)) ⇒ C x) ⇒ (f : A ⇒ B) ⇒ (x : A) ⇒ C (f x)) (∘)"
  by force

lemma mono_wrt_dep_mono_wrt_dep_fun_map:
  fixes A :: "'a ⇒ bool"
  shows "((f : A ⇒ B) ⇒ ((x : A) ⇒ (y : B) ⇒ (z : C (f x)) ⇒ D x y z) ⇒
    (h : (x : B) ⇒ C x) ⇒ (x : A) ⇒ D x (f x) (h (f x))) dep_fun_map"
  by fastforce

lemma mono_wrt_dep_mono_wrt_fun_map:
  fixes A :: "'a ⇒ bool"
  shows "((f : A ⇒ B) ⇒ ((x : C) ⇒ D x) ⇒ (h : B ⇒ C) ⇒ (x : A) ⇒ D (h (f x))) fun_map"
  by fastforce

lemma mono_in_dom: "mono in_dom" by (intro monoI) fast
lemma mono_in_codom: "mono in_codom" by (intro monoI) fast
lemma mono_in_field: "mono in_field" by (intro monoI) fast
lemma mono_rel_comp: "((≤) ⇒ (≤) ⇛ (≤)) (∘∘)" by (intro mono_wrt_relI Fun_Rel_relI le_relI) fast
lemma mono_rel_inv: "mono rel_inv" by (intro monoI) fast

lemma mono_rel_restrict_left:
  "((≤) ⇒ (≤) ⇛ (≤)) (rel_restrict_left :: ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool)"
  by (intro mono_wrt_relI Fun_Rel_relI le_relI) fastforce

lemma mono_rel_restrict_right:
  "((≤) ⇒ (≤) ⇛ (≤)) (rel_restrict_right :: ('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool)"
  by (intro mono_wrt_relI Fun_Rel_relI le_relI) fastforce

lemma mono_ball: "((≥) ⇒ (≤) ⇛ (≤)) ball" by fast
lemma mono_bex: "((≤) ⇒ (≤) ⇛ (≤)) bex" by fast

end