Theory Relations

theory Relations
imports Main
begin

type_synonym 'a Rel = "'a ⇒ 'a ⇒ bool"

abbreviation symmetric :: "'a Rel ⇒ bool" where 
  "symmetric  A ≡ ∀ x.  ∀ y. (A x y) ⟶ (A y x)"

abbreviation asymmetric :: "'a Rel ⇒ bool" where
 " asymmetric A ≡ ∀ x. ∀ y. (A x y) ⟶ ¬(A y x)"

abbreviation antisymmetric :: "'a Rel ⇒ bool" where
 " antisymmetric A ≡ ∀ x. ∀ y. (A x y ∧ A y x) ⟶ x = y" 

abbreviation reflexive :: "'a Rel ⇒ bool" where 
  "reflexive  A ≡ ∀ x. A x x"

abbreviation irreflexive :: "'a Rel ⇒ bool" where 
  "irreflexive  A ≡ ∀ x. ¬(A x x)"

abbreviation transitive :: "'a Rel ⇒ bool" where 
  "transitive  A ≡ ∀ x. ∀ y. ∀ z. (A x y) ∧ (A y z) ⟶ (A x z)"

abbreviation total :: "'a Rel ⇒ bool" where 
  "total  A ≡ ∀ x. ∀ y. A x y ∨ A y x"

abbreviation universal :: "'a Rel ⇒ bool" where 
  "universal  A ≡ ∀ x. ∀ y. A x y"

abbreviation serial :: "'a Rel ⇒ bool" where 
  "serial  A ≡ ∀ x. ∃ y. A x y"

abbreviation euclidean :: "'a Rel ⇒ bool" where 
  "euclidean  A ≡ ∀x y z. (A x y ∧ A x z) ⟶ A y z"

abbreviation preorder :: "'a Rel ⇒ bool" where
  "preorder A ≡ reflexive A ∧ transitive A"

abbreviation equivalence :: "'a Rel ⇒ bool" where
  "equivalence A ≡ preorder A ∧ symmetric A"

abbreviation partial_order :: "'a Rel ⇒ bool" where
  "partial_order A ≡  preorder A ∧ antisymmetric A"

abbreviation strict_partial_order :: "'a Rel ⇒ bool" where
  "strict_partial_order A ≡  irreflexive A ∧ asymmetric A ∧ transitive A" (* asymmetry is redundant *)

end