Theory Binary_Relations_Reflexive

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Reflexive›
theory Binary_Relations_Reflexive
  imports
    Functions_Monotone
    ML_Unification.ML_Unification_HOL_Setup
    ML_Unification.Unify_Resolve_Tactics
begin

consts reflexive_on :: "'a ⇒ 'b ⇒ bool"

overloading
  reflexive_on_pred ≡ "reflexive_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "reflexive_on_pred P R ≡ ∀x. P x ⟶ R x x"
end

lemma reflexive_onI [intro]:
  assumes "⋀x. P x ⟹ R x x"
  shows "reflexive_on P R"
  using assms unfolding reflexive_on_pred_def by blast

lemma reflexive_onD [dest]:
  assumes "reflexive_on P R"
  and "P x"
  shows "R x x"
  using assms unfolding reflexive_on_pred_def by blast

context
  fixes R :: "'a ⇒ 'a ⇒ bool" and P :: "'a ⇒ bool"
begin

lemma le_in_dom_if_reflexive_on:
  assumes "reflexive_on P R"
  shows "P ≤ in_dom R"
  using assms by blast

lemma le_in_codom_if_reflexive_on:
  assumes "reflexive_on P R"
  shows "P ≤ in_codom R"
  using assms by blast

lemma in_codom_eq_in_dom_if_reflexive_on_in_field:
  assumes "reflexive_on (in_field R) R"
  shows "in_codom R = in_dom R"
  using assms by blast

lemma reflexive_on_rel_inv_iff_reflexive_on [iff]:
  "reflexive_on P R¯ ⟷ reflexive_on P R"
  by blast

lemma mono_reflexive_on:
  "((≥) ⇛⇩m (≤) ⇛ (≤)) (reflexive_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by fastforce

lemma reflexive_on_if_le_pred_if_reflexive_on:
  fixes P' :: "'a ⇒ bool"
  assumes "reflexive_on P R"
  and "P' ≤ P"
  shows "reflexive_on P' R"
  using assms by blast

end

lemma reflexive_on_sup_eq [simp]:
  "(reflexive_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool) (P ⊔ Q)
  = reflexive_on P ⊓ reflexive_on Q"
  by (intro ext iffI reflexive_onI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on)

lemma reflexive_on_iff_eq_restrict_le:
  "reflexive_on (P :: 'a ⇒ bool) (R :: 'a ⇒ _) ⟷ ((=)↾⇘P⇙ ≤ R)"
  by blast


consts reflexive :: "'a ⇒ bool"

overloading
  reflexive ≡ "reflexive :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "reflexive :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡ reflexive_on (⊤ :: 'a ⇒ bool)"
end

lemma reflexive_eq_reflexive_on:
  "(reflexive :: ('a ⇒ 'a ⇒ bool) ⇒ _) = reflexive_on (⊤ :: 'a ⇒ bool)"
  unfolding reflexive_def ..

lemma reflexive_eq_reflexive_on_uhint [uhint]:
  "P ≡ (⊤ :: 'a ⇒ bool) ⟹ (reflexive :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ reflexive_on P"
  by (simp add: reflexive_eq_reflexive_on)

lemma reflexiveI [intro]:
  assumes "⋀x. R x x"
  shows "reflexive R"
  using assms by (urule reflexive_onI)

lemma reflexiveD:
  assumes "reflexive R"
  shows "R x x"
  using assms by (urule (d) reflexive_onD where chained = insert) simp

lemma reflexive_on_if_reflexive:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "reflexive R"
  shows "reflexive_on P R"
  using assms by (intro reflexive_onI) (blast dest: reflexiveD)

lemma reflexive_rel_inv_iff_reflexive [iff]:
  "reflexive (R :: 'a ⇒ 'a ⇒ bool)¯ ⟷ reflexive R"
  by (blast dest: reflexiveD)

lemma reflexive_iff_eq_le: "reflexive R ⟷ ((=) ≤ R)"
  unfolding reflexive_eq_reflexive_on reflexive_on_iff_eq_restrict_le
  by auto

paragraph ‹Instantiations›

lemma reflexive_eq: "reflexive (=)"
  by (rule reflexiveI) (rule refl)

lemma reflexive_top: "reflexive (⊤ :: 'a ⇒ 'a ⇒ bool)"
  by (rule reflexiveI) auto


end