Theory Binary_Relations_Least

✐‹creator "Kevin Kappelmann"›
subsection ‹Least Element With Respect To Some Relation›
theory Binary_Relations_Least
  imports
    Binary_Relations_Antisymmetric
    Bounded_Definite_Description
begin

definition "is_minimal_wrt_rel R (P :: 'a ⇒ bool) x ≡ P x ∧ (∀y : P. R x y)"

lemma is_minimal_wrt_relI [intro]:
  assumes "P x"
  and "⋀y. P y ⟹ R x y"
  shows "is_minimal_wrt_rel R P x"
  unfolding is_minimal_wrt_rel_def using assms by blast

lemma is_minimal_wrt_relE [elim]:
  assumes "is_minimal_wrt_rel R P x"
  obtains "P x" "⋀y. P y ⟹ R x y"
  using assms unfolding is_minimal_wrt_rel_def by blast


definition "is_least_wrt_rel R (P :: 'a ⇒ bool) x ≡
  is_minimal_wrt_rel R P x ∧ (∀x'. is_minimal_wrt_rel R P x' ⟶ x' = x)"

lemma is_least_wrt_relI [intro]:
  assumes "is_minimal_wrt_rel R P x"
  and "⋀x'. is_minimal_wrt_rel R P x' ⟹ x' = x"
  shows "is_least_wrt_rel R P x"
  unfolding is_least_wrt_rel_def using assms by blast

lemma is_least_wrt_relE [elim]:
  assumes "is_least_wrt_rel R P x"
  obtains "is_minimal_wrt_rel R P x" "⋀x'. is_minimal_wrt_rel R P x' ⟹ x' = x"
  using assms unfolding is_least_wrt_rel_def by blast

lemma is_least_wrt_rel_if_antisymmetric_onI:
  assumes "antisymmetric_on P R"
  and "is_minimal_wrt_rel R P x"
  shows "is_least_wrt_rel R P x"
  using assms by (intro is_least_wrt_relI) (blast dest: antisymmetric_onD)+

corollary is_least_wrt_rel_eq_is_minimal_wrt_rel_if_antisymmetric_on [simp]:
  assumes "antisymmetric_on P R"
  shows "is_least_wrt_rel R P = is_minimal_wrt_rel R P"
  using assms is_least_wrt_rel_if_antisymmetric_onI by (intro ext iffI) auto


definition "least_wrt_rel R (P :: 'a ⇒ bool) ≡ THE x. is_least_wrt_rel R P x"

lemma least_wrt_rel_eqI:
  assumes "is_least_wrt_rel R P x"
  shows "least_wrt_rel R P = x"
  unfolding least_wrt_rel_def using assms by (intro the1_equality) blast

lemma least_wrt_rel_eq_if_antisymmetric_onI:
  assumes "antisymmetric_on P R"
  and "is_minimal_wrt_rel R P x"
  shows "least_wrt_rel R P = x"
  using assms by (intro least_wrt_rel_eqI) auto

lemma pred_least_wrt_relI:
  assumes "is_least_wrt_rel R P x"
  shows "P (least_wrt_rel R P)"
  unfolding least_wrt_rel_def by (rule the1I2) (use assms in auto)

lemma pred_least_wrt_rel_if_antisymmetric_onI:
  assumes "antisymmetric_on P R"
  and "is_minimal_wrt_rel R P x"
  shows "P (least_wrt_rel R P)"
  by (rule pred_least_wrt_relI) (use assms in auto)


end