Theory Functions_Monotone

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Monotonicity›
theory Functions_Monotone
  imports
    Binary_Relations_Order_Base
    Function_Relators
    Predicate_Functions
    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 :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
consts mono_wrt :: "'a ⇒ 'b ⇒ 'c ⇒ bool"

bundle dep_mono_wrt_syntax begin
syntax
  "_mono_wrt" :: "'a ⇒ 'b ⇒ 'c ⇒ bool" ("(_) ⇛⇩m (_)" [41, 40] 40)
  "_dep_mono_wrt_rel" :: "idt ⇒ idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool"
    ("'(_/ _/ ∷/ _') ⇛⇩m (_)" [41, 41, 41, 40] 40)
  "_dep_mono_wrt_rel_if" :: "idt ⇒ idt ⇒ 'a ⇒ bool ⇒ 'b ⇒ 'c ⇒ bool"
    ("'(_/ _/ ∷/ _/ |/ _') ⇛⇩m (_)" [41, 41, 41, 40, 40] 40)
  "_dep_mono_wrt_pred" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool" ("'(_/ :/ _') ⇛⇩m (_)" [41, 41, 40] 40)
  "_dep_mono_wrt_pred_if" :: "idt ⇒ 'a ⇒ bool ⇒ 'b ⇒ 'c ⇒ bool"
    ("'(_/ :/ _/ |/ _') ⇛⇩m (_)" [41, 41, 40, 40] 40)
end
bundle no_dep_mono_wrt_syntax begin
no_syntax
  "_mono_wrt" :: "'a ⇒ 'b ⇒ 'c ⇒ bool" ("(_) ⇛⇩m (_)" [41, 40] 40)
  "_dep_mono_wrt_rel" :: "idt ⇒ idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool"
    ("'(_/ _/ ∷/ _') ⇛⇩m (_)" [41, 41, 41, 40] 40)
  "_dep_mono_wrt_rel_if" :: "idt ⇒ idt ⇒ 'a ⇒ bool ⇒ 'b ⇒ 'c ⇒ bool"
    ("'(_/ _/ ∷/ _/ |/ _') ⇛⇩m (_)" [41, 41, 41, 40, 40] 40)
  "_dep_mono_wrt_pred" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool" ("'(_/ :/ _') ⇛⇩m (_)" [41, 41, 40] 40)
  "_dep_mono_wrt_pred_if" :: "idt ⇒ 'a ⇒ bool ⇒ 'b ⇒ 'c ⇒ bool"
    ("'(_/ :/ _/ |/ _') ⇛⇩m (_)" [41, 41, 40, 40] 40)
end
unbundle dep_mono_wrt_syntax
translations
  "R ⇛⇩m S" ⇌ "CONST mono_wrt R S"
  "(x y ∷ R) ⇛⇩m S" ⇌ "CONST dep_mono_wrt R (λx y. S)"
  "(x y ∷ R | B) ⇛⇩m S" ⇌ "CONST dep_mono_wrt R (λx y. CONST rel_if B S)"
  "(x : P) ⇛⇩m Q" ⇌ "CONST dep_mono_wrt P (λx. Q)"
  "(x : P | B) ⇛⇩m Q" ⇌ "CONST dep_mono_wrt P (λx. CONST pred_if B Q)"


definition "dep_mono_wrt_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 dep_mono_wrt_rel

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

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

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

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

lemma mono_wrt_rel_eq_dep_mono_wrt_rel_uhint [uhint]:
  assumes "R ≡ R'"
  and "S' ≡ (λ(_ :: 'a) (_ :: 'a). S)"
  shows "((R :: 'a ⇒ 'a ⇒ bool) ⇛⇩m (S :: 'b ⇒ 'b ⇒ bool)) = ((x y ∷ R') ⇛⇩m 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) ⇛⇩m (S :: 'b ⇒ 'b ⇒ bool)) f ⟷
    dep_mono_wrt 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) ⇛⇩m (Q :: 'b ⇒ bool)) = (((_ :: 'a) : P) ⇛⇩m Q)"
  unfolding mono_wrt_pred_def by simp

lemma mono_wrt_pred_eq_dep_mono_wrt_pred_uhint [uhint]:
  assumes "P ≡ P'"
  and "Q' ≡ (λ(_ :: 'a). Q)"
  shows "((P :: 'a ⇒ bool) ⇛⇩m (Q :: 'b ⇒ bool)) = (((x : P') ⇛⇩m 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) ⇛⇩m (Q :: 'b ⇒ bool)) f ⟷ (((_ :: 'a) : P) ⇛⇩m 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) ⇛⇩m S x y) f"
  using assms unfolding dep_mono_wrt_rel_def by blast

lemma dep_mono_wrt_relE:
  assumes "((x y ∷ R) ⇛⇩m S x y) f"
  obtains "⋀x y. R x y ⟹ S x y (f x) (f y)"
  using assms unfolding dep_mono_wrt_rel_def by blast

lemma dep_mono_wrt_relD [dest]:
  assumes "((x y ∷ R) ⇛⇩m S x y) f"
  and "R x y"
  shows "S x y (f x) (f y)"
  using assms unfolding dep_mono_wrt_rel_def by blast

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

lemma mono_wrt_relE:
  assumes "(R ⇛⇩m 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 ⇛⇩m S) f"
  and "R x y"
  shows "S (f x) (f y)"
  using assms by (urule dep_mono_wrt_relD)

lemma dep_mono_wrt_predI [intro]:
  assumes "⋀x. P x ⟹ Q x (f x)"
  shows "((x : P) ⇛⇩m Q x) f"
  using assms unfolding dep_mono_wrt_pred_def by blast

lemma dep_mono_wrt_predE:
  assumes "((x : P) ⇛⇩m Q x) f"
  obtains "⋀x. P x ⟹ Q x (f x)"
  using assms unfolding dep_mono_wrt_pred_def by blast

lemma dep_mono_wrt_predD [dest]:
  assumes "((x : P) ⇛⇩m Q x) f"
  and "P x"
  shows "Q x (f x)"
  using assms unfolding dep_mono_wrt_pred_def by blast

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

lemma mono_wrt_predE:
  assumes "(P ⇛⇩m 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 ⇛⇩m Q) f"
  and "P x"
  shows "Q (f x)"
  using assms by (urule dep_mono_wrt_predD)

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) ⇛⇩m 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) ⇛⇩m Q x) f"
  using assms by blast

lemma Dep_Fun_Rel_rel_self_if_dep_mono_wrt_rel:
  assumes "((x y ∷ R) ⇛⇩m 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) ⇛⇩m 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) ⇛⇩m 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) ⇛⇩m 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_inv_eq [simp]:
  "((y x ∷ R¯) ⇛⇩m (S x y)¯) = ((x y ∷ R) ⇛⇩m S x y)"
  by (intro ext) force

lemma in_dom_if_rel_if_dep_mono_wrt_rel:
  assumes "((x y ∷ R) ⇛⇩m 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

corollary in_dom_if_in_dom_if_mono_wrt_rel:
  assumes "(R ⇛⇩m S) f"
  shows "(in_dom R ⇛⇩m 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) ⇛⇩m 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 ⇛⇩m S) f"
  shows "(in_codom R ⇛⇩m 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 ⇛⇩m S) f"
  shows "(in_field R ⇛⇩m in_field S) f"
  using assms by fast

lemma le_rel_map_if_mono_wrt_rel:
  assumes "(R ⇛⇩m 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 ⇛⇩m 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 ⇛⇩m 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 ⇛⇩m Q) f"
  using assms by (intro mono_wrt_predI) auto

corollary mono_wrt_rel_iff_le_rel_map: "(R ⇛⇩m 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 ⇛⇩m 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

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

lemma mono_eq_mono_wrt_le [simp]: "(mono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool) =
  (((≤) :: 'a ⇒ 'a ⇒ bool) ⇛⇩m ((≤) :: '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 ⇛⇩m S)"
  using assms by simp

lemma mono_iff_mono_wrt_le [iff]: "mono f ⟷ ((≤) ⇛⇩m (≤)) 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) ⇛⇩m ((≥) :: 'b ⇒ 'b ⇒ bool))"

lemma antimono_eq_mono_wrt_le_ge [simp]: "(antimono :: (('a :: ord) ⇒ ('b :: ord)) ⇒ bool) =
  (((≤) :: 'a ⇒ 'a ⇒ bool) ⇛⇩m ((≥) :: '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 ⇛⇩m S)"
  using assms by simp

lemma antimono_iff_mono_wrt_le_ge [iff]: "antimono f ⟷ ((≤) ⇛⇩m (≥)) 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) ⇛⇩m S x y))"
  by (intro antimonoI) blast

lemma antimono_dep_mono_wrt_pred_left: "antimono (λ(P :: 'a ⇒ bool). ((x : P) ⇛⇩m 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) ⇛⇩m S x y) f"
  and "R' ≤ R"
  shows "((x y ∷ R') ⇛⇩m 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) ⇛⇩m Q x) f"
  and "P' ≤ P"
  shows "((x : P') ⇛⇩m 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) ⇛⇩m S x y))"
  by (intro monoI) blast

lemma mono_dep_mono_wrt_pred_right: "mono (λ(Q :: 'a ⇒ 'b ⇒ bool). ((x : P) ⇛⇩m 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) ⇛⇩m 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) ⇛⇩m 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) ⇛⇩m Q x) f"
  and "⋀x. P x ⟹ Q x (f x) ⟹ T x (f x)"
  shows "((x : P) ⇛⇩m T x) f"
  using assms by blast


paragraph ‹Composition›

lemma dep_mono_wrt_rel_compI:
  assumes "((x y ∷ R) ⇛⇩m S x y) f"
  and "⋀x y. R x y ⟹ ((x' y' ∷ T x y) ⇛⇩m 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) ⇛⇩m 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) ⇛⇩m S x y) f"
  and "⋀x y. R x y ⟹ ((x' y' ∷ S x y) ⇛⇩m T x y x' y') f'"
  shows "((x y ∷ R) ⇛⇩m 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) ⇛⇩m Q x) f"
  and "⋀x. P x ⟹ ((x' y' ∷ R x) ⇛⇩m S x x' y') f'"
  and "⋀x. P x ⟹ Q x (f x) ⟹ R x (f x) (f x)"
  shows "((x : P) ⇛⇩m (λ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) ⇛⇩m Q x) f"
  and "⋀x. P x ⟹ ((x' : R x) ⇛⇩m S x x') f'"
  and "⋀x. P x ⟹ Q x (f x) ⟹ R x (f x)"
  shows "((x : P) ⇛⇩m 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) ⇛⇩m Q x) f"
  and "⋀x. P x ⟹ ((x' : Q x) ⇛⇩m S x x') f'"
  shows "((x : P) ⇛⇩m 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 ⇛⇩m (⊤ :: 'b ⇒ 'b ⇒ bool)) f"
  by auto

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

paragraph ‹Instantiations›

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

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

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: "((≤) ⇛⇩m (≤) ⇛ (≤)) (∘∘)" 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:
  "((≤) ⇛⇩m (≤) ⇛ (≤)) (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:
  "((≤) ⇛⇩m (≤) ⇛ (≤)) (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: "((≥) ⇛⇩m (≤) ⇛ (≤)) ball" by fast
lemma mono_bex: "((≤) ⇛⇩m (≤) ⇛ (≤)) bex" by fast

end