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:
  "((≥)  (≤)  (≤)) (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