Theory Binary_Relations_Antisymmetric

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Antisymmetric›
theory Binary_Relations_Antisymmetric
  imports
    Binary_Relation_Functions
    Functions_Monotone
begin

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

overloading
  antisymmetric_on_pred ≡ "antisymmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "antisymmetric_on_pred P R ≡ ∀x y : P. R x y ∧ R y x ⟶ x = y"
end

lemma antisymmetric_onI [intro]:
  assumes "⋀x y. P x ⟹ P y ⟹ R x y ⟹ R y x ⟹ x = y"
  shows "antisymmetric_on P R"
  unfolding antisymmetric_on_pred_def using assms by blast

lemma antisymmetric_onD:
  assumes "antisymmetric_on P R"
  and "P x" "P y"
  and "R x y" "R y x"
  shows "x = y"
  using assms unfolding antisymmetric_on_pred_def by blast

lemma antisymmetric_onE:
  assumes "antisymmetric_on P R"
  obtains "⋀x y. P x ⟹ P y ⟹ R x y ⟹ R y x ⟹ x = y"
  using assms unfolding antisymmetric_on_pred_def by blast

lemma antimono_antisymmetric_on:
  "((≤) ⇒ (≤) ⇛ (≥)) (antisymmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by (blast intro!: antisymmetric_onI dest: antisymmetric_onD)

consts antisymmetric :: "'a ⇒ bool"

overloading
  antisymmetric ≡ "antisymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "antisymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _ ≡ antisymmetric_on (⊤ :: 'a ⇒ bool)"
end

lemma antisymmetric_eq_antisymmetric_on:
  "(antisymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) = antisymmetric_on (⊤ :: 'a ⇒ bool)"
  unfolding antisymmetric_def ..

lemma antisymmetric_eq_antisymmetric_on_uhint [uhint]:
  "P ≡ (⊤ :: 'a ⇒ bool) ⟹ (antisymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ antisymmetric_on P"
  by (simp add: antisymmetric_eq_antisymmetric_on)

lemma antisymmetricI [intro]:
  assumes "⋀x y. R x y ⟹ R y x ⟹ x = y"
  shows "antisymmetric R"
  using assms by (urule antisymmetric_onI)

lemma antisymmetricD:
  assumes "antisymmetric R"
  and "R x y" "R y x"
  shows "x = y"
  using assms by (urule (d) antisymmetric_onD where chained = insert) simp_all

lemma antisymmetricE:
  assumes "antisymmetric R"
  obtains "⋀x y. R x y ⟹ R y x ⟹ x = y"
  using assms by (urule (e) antisymmetric_onE where chained = insert) simp_all

lemma antisymmetric_on_if_antisymmetric:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "antisymmetric R"
  shows "antisymmetric_on P R"
  using assms by (intro antisymmetric_onI) (blast dest: antisymmetricD)

lemma antisymmetric_if_antisymmetric_on_in_field:
  assumes "antisymmetric_on (in_field R) R"
  shows "antisymmetric R"
  using assms by (intro antisymmetricI) (blast dest: antisymmetric_onD)

corollary antisymmetric_on_in_field_iff_antisymmetric [iff]:
  "antisymmetric_on (in_field R) R ⟷ antisymmetric R"
  using antisymmetric_if_antisymmetric_on_in_field antisymmetric_on_if_antisymmetric
  by blast


end