# 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
```