Theory Binary_Relations_Irreflexive

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Irreflexive›
theory Binary_Relations_Irreflexive
  imports
    Functions_Monotone
begin

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

overloading
  irreflexive_on_pred ≡ "irreflexive_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "irreflexive_on_pred P R ≡ ∀x : P. ¬(R x x)"
end

lemma irreflexive_onI [intro]:
  assumes "⋀x. P x ⟹ ¬(R x x)"
  shows "irreflexive_on P R"
  using assms unfolding irreflexive_on_pred_def by blast

lemma irreflexive_onD [dest]:
  assumes "irreflexive_on P R"
  and "P x"
  shows "¬(R x x)"
  using assms unfolding irreflexive_on_pred_def by blast

lemma antimono_irreflexive_on:
  "((≤) ⇒ (≤) ⇛ (≥)) (irreflexive_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by blast


consts irreflexive :: "'a ⇒ bool"

overloading
  irreflexive ≡ "irreflexive :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(irreflexive :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ irreflexive_on (⊤ :: 'a ⇒ bool)"
end

lemma irreflexive_eq_irreflexive_on:
  "(irreflexive :: ('a ⇒ 'a ⇒ bool) ⇒ _) = irreflexive_on (⊤ :: 'a ⇒ bool)"
  unfolding irreflexive_def ..

lemma irreflexive_eq_irreflexive_on_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "irreflexive :: ('a ⇒ 'a ⇒ bool) ⇒ _ ≡ irreflexive_on P"
  using assms by (simp add: irreflexive_eq_irreflexive_on)

lemma irreflexiveI [intro]:
  assumes "⋀x. ¬(R x x)"
  shows "irreflexive R"
  using assms by (urule irreflexive_onI)

lemma irreflexiveD:
  assumes "irreflexive R"
  shows "¬(R x x)"
  using assms by (urule (d) irreflexive_onD where chained = insert) simp

lemma irreflexive_on_if_irreflexive:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "irreflexive R"
  shows "irreflexive_on P R"
  using assms by (intro irreflexive_onI) (blast dest: irreflexiveD)


end