Theory Binary_Relations_Asymmetric

✐‹creator "Kevin Kappelmann"›
✐‹creator "Niklas Krofta"›
theory Binary_Relations_Asymmetric
  imports
    Binary_Relations_Irreflexive
    Binary_Relations_Antisymmetric
    Functions_Monotone
begin

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

overloading
  asymmetric_on_pred ≡ "asymmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "asymmetric_on_pred (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool)
    ≡ ∀x y : P. R x y ⟶ ¬(R y x)"
end

lemma asymmetric_onI [intro]:
  assumes "⋀x y. P x ⟹ P y ⟹ R x y ⟹ ¬(R y x)"
  shows "asymmetric_on P R"
  using assms unfolding asymmetric_on_pred_def by blast

lemma asymmetric_onD [dest]:
  assumes "asymmetric_on P R"
  and "P x" "P y"
  and "R x y"
  shows "¬(R y x)"
  using assms unfolding asymmetric_on_pred_def by blast

lemma asymmetric_onE:
  assumes "asymmetric_on P R"
  obtains "⋀x y. P x ⟹ P y ⟹ R x y ⟹ ¬(R y x)"
  using assms unfolding asymmetric_on_pred_def by blast

lemma asymmetric_on_le_irreflexive_on:
  "(asymmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ _) ≤ irreflexive_on"
  by blast

lemma asymmetric_on_le_antisymmetric_on:
  "(asymmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ _) ≤ antisymmetric_on"
  by blast

lemma antimono_asymmetric_on:
  "((≤) ⇒ (≤) ⇛ (≥)) (asymmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by blast

lemma asymmetric_on_rel_map_if_mono_wrt_pred_if_asymmetric_on:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "asymmetric_on P R"
  and "(Q ⇒ P) f"
  shows "asymmetric_on Q (rel_map f R)"
  using assms by fastforce

consts asymmetric :: "'a ⇒ bool"

overloading
  asymmetric ≡ "asymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "asymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _ ≡ asymmetric_on (⊤ :: 'a ⇒ bool)"
end

lemma asymmetric_eq_asymmetric_on:
  "(asymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) = asymmetric_on (⊤ :: 'a ⇒ bool)"
  unfolding asymmetric_def ..

lemma asymmetric_eq_asymmetric_on_uhint [uhint]:
  "P ≡ (⊤ :: 'a ⇒ bool) ⟹ (asymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ asymmetric_on P"
  by (simp add: asymmetric_eq_asymmetric_on)

lemma asymmetricI [intro]:
  assumes "⋀x y. R x y ⟹ ¬(R y x)"
  shows "asymmetric R"
  using assms by (urule asymmetric_onI)

lemma asymmetricD [dest]:
  assumes "asymmetric R"
  and "R x y"
  shows "¬(R y x)"
  using assms by (urule (d) asymmetric_onD where chained = insert) simp_all

lemma asymmetricE:
  assumes "asymmetric R"
  obtains "⋀x y. R x y ⟹ ¬(R y x)"
  using assms by (urule (e) asymmetric_onE where chained = insert) simp_all

lemma asymmetric_on_if_asymmetric:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "asymmetric R"
  shows "asymmetric_on P R"
  using assms by (intro asymmetric_onI) blast

lemma asymmetric_if_asymmetric_on_in_field:
  assumes "asymmetric_on (in_field R) R"
  shows "asymmetric R"
  using assms by (intro asymmetricI) blast

corollary asymmetric_on_in_field_iff_asymmetric [iff]:
  "asymmetric_on (in_field R) R ⟷ asymmetric R"
  using asymmetric_if_asymmetric_on_in_field asymmetric_on_if_asymmetric by blast

lemma asymmetric_on_if_asymmetric_restrict:
  assumes "asymmetric R↑⇘P⇙"
  shows "asymmetric_on P R"
  using assms by blast

lemma asymmetric_restrict_if_asymmetric_on:
  assumes "asymmetric_on P R"
  shows "asymmetric R↑⇘P⇙"
  using assms by blast

corollary asymmetric_restrict_iff_asymmetric_on [iff]: "asymmetric R↑⇘P⇙ ⟷ asymmetric_on P R"
  using asymmetric_on_if_asymmetric_restrict asymmetric_restrict_if_asymmetric_on by blast

lemma asymmetric_le_irreflexive:
  "(asymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≤ irreflexive"
  by blast

lemma asymmetric_le_antisymmetric:
  "(asymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≤ antisymmetric"
  by blast

lemma antimono_asymmetric: "antimono (asymmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _)"
  by blast


end