Theory Preorders

✐‹creator "Kevin Kappelmann"›
subsection ‹Preorders›
theory Preorders
  imports
    Binary_Relations_Reflexive
    Binary_Relations_Transitive
begin

definition "preorder_on ≡ reflexive_on ⊓ transitive_on"

lemma preorder_onI [intro]:
  assumes "reflexive_on P R"
  and "transitive_on P R"
  shows "preorder_on P R"
  unfolding preorder_on_def using assms by auto

lemma preorder_onE [elim]:
  assumes "preorder_on P R"
  obtains "reflexive_on P R" "transitive_on P R"
  using assms unfolding preorder_on_def by auto

lemma reflexive_on_if_preorder_on:
  assumes "preorder_on P R"
  shows "reflexive_on P R"
  using assms by (elim preorder_onE)

lemma transitive_on_if_preorder_on:
  assumes "preorder_on P R"
  shows "transitive_on P R"
  using assms by (elim preorder_onE)

lemma transitive_if_preorder_on_in_field:
  assumes "preorder_on (in_field R) R"
  shows "transitive R"
  using assms by (elim preorder_onE) (rule transitive_if_transitive_on_in_field)

corollary preorder_on_in_fieldE [elim]:
  assumes "preorder_on (in_field R) R"
  obtains "reflexive_on (in_field R) R" "transitive R"
  using assms
  by (blast dest: reflexive_on_if_preorder_on transitive_if_preorder_on_in_field)

lemma preorder_on_rel_inv_if_preorder_on [iff]:
  "preorder_on P R¯ ⟷ preorder_on (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool)"
  by auto

lemma rel_if_all_rel_if_rel_if_reflexive_on:
  assumes "reflexive_on P R"
  and "⋀z. P z ⟹ R x z ⟹ R y z"
  and "P x"
  shows "R y x"
  using assms by blast

lemma rel_if_all_rel_if_rel_if_reflexive_on':
  assumes "reflexive_on P R"
  and "⋀z. P z ⟹ R z x ⟹ R z y"
  and "P x"
  shows "R x y"
  using assms by blast

consts preorder :: "'a ⇒ bool"

overloading
  preorder ≡ "preorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(preorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ preorder_on (⊤ :: 'a ⇒ bool)"
end

lemma preorder_eq_preorder_on:
  "(preorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = preorder_on (⊤ :: 'a ⇒ bool)"
  unfolding preorder_def ..

lemma preorder_eq_preorder_on_uhint [uhint]:
  assumes "P ≡ ⊤ :: 'a ⇒ bool"
  shows "(preorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ preorder_on P"
  using assms by (simp add: preorder_eq_preorder_on)

context
  fixes R :: "'a ⇒ 'a ⇒ bool"
begin

lemma preorderI [intro]:
  assumes "reflexive R"
  and "transitive R"
  shows "preorder R"
  using assms by (urule preorder_onI)

lemma preorderE [elim]:
  assumes "preorder R"
  obtains "reflexive R" "transitive R"
  using assms by (urule (e) preorder_onE)

lemma preorder_on_if_preorder:
  fixes P :: "'a ⇒ bool"
  assumes "preorder R"
  shows "preorder_on P R"
  using assms by (elim preorderE)
  (intro preorder_onI reflexive_on_if_reflexive transitive_on_if_transitive)

end

paragraph ‹Instantiations›

lemma preorder_eq: "preorder (=)"
  using reflexive_eq transitive_eq by (rule preorderI)


end