# Theory Deriving.Comparator

```(*  Title:       Deriving class instances for datatypes
Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
Maintainer:  Christian Sternagel and René Thiemann
*)
section ‹Comparisons›

subsection ‹Comparators and Linear Orders›

theory Comparator
imports Main
begin

text ‹Instead of having to define a strict and a weak linear order, @{term "((<), (≤))"},
one can alternative use a comparator to define the linear order, which may deliver
three possible outcomes when comparing two values.›

datatype order = Eq | Lt | Gt

type_synonym 'a comparator = "'a ⇒ 'a ⇒ order"

text ‹In the following, we provide the obvious definitions how to switch between
linear orders and comparators.›

definition lt_of_comp :: "'a comparator ⇒ 'a ⇒ 'a ⇒ bool" where
"lt_of_comp acomp x y = (case acomp x y of Lt ⇒ True | _ ⇒ False)"

definition le_of_comp :: "'a comparator ⇒ 'a ⇒ 'a ⇒ bool" where
"le_of_comp acomp x y = (case acomp x y of Gt ⇒ False | _ ⇒ True)"

definition comp_of_ords :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a comparator" where
"comp_of_ords le lt x y = (if lt x y then Lt else if le x y then Eq else Gt)"

lemma comp_of_ords_of_le_lt[simp]: "comp_of_ords (le_of_comp c) (lt_of_comp c) = c"
by (intro ext, auto simp: comp_of_ords_def le_of_comp_def lt_of_comp_def split: order.split)

lemma lt_of_comp_of_ords: "lt_of_comp (comp_of_ords le lt) = lt"
by (intro ext, auto simp: comp_of_ords_def le_of_comp_def lt_of_comp_def split: order.split)

lemma le_of_comp_of_ords_gen: "(⋀ x y. lt x y ⟹ le x y) ⟹ le_of_comp (comp_of_ords le lt) = le"
by (intro ext, auto simp: comp_of_ords_def le_of_comp_def lt_of_comp_def split: order.split)

lemma le_of_comp_of_ords_linorder: assumes "class.linorder le lt"
shows "le_of_comp (comp_of_ords le lt) = le"
proof -
interpret linorder le lt by fact
show ?thesis by (rule le_of_comp_of_ords_gen) simp
qed

fun invert_order:: "order ⇒ order" where
"invert_order Lt = Gt" |
"invert_order Gt = Lt" |
"invert_order Eq = Eq"

locale comparator =
fixes comp :: "'a comparator"
assumes sym: "invert_order (comp x y) = comp y x"
and weak_eq: "comp x y = Eq ⟹ x = y"
and comp_trans: "comp x y = Lt ⟹ comp y z = Lt ⟹ comp x z = Lt"
begin

lemma eq: "(comp x y = Eq) = (x = y)"
proof
assume "x = y"
with sym [of y y] show "comp x y = Eq" by (cases "comp x y") auto
qed (rule weak_eq)

lemma comp_same [simp]:
"comp x x = Eq"

abbreviation "lt ≡ lt_of_comp comp"
abbreviation "le ≡ le_of_comp comp"

sublocale ordering le lt
proof
note [simp] = lt_of_comp_def le_of_comp_def
fix x y z :: 'a
show "le x x" using eq [of x x] by (simp)
show "le x y ⟹ le y z ⟹ le x z"
by (cases "comp x y" "comp y z" rule: order.exhaust [case_product order.exhaust])
(auto dest: comp_trans simp: eq)
show "le x y ⟹ le y x ⟹ x = y"
using sym [of x y] by (cases "comp x y") (simp_all add: eq)
show "lt x y ⟷ le x y ∧ x ≠ y"
using eq [of x y] by (cases "comp x y") (simp_all)
qed

lemma linorder: "class.linorder le lt"
proof (rule class.linorder.intro)
interpret order le lt
using ordering_axioms by (rule ordering_orderI)
show ‹class.order le lt›
by (fact order_axioms)
show ‹class.linorder_axioms le›
proof
note [simp] = lt_of_comp_def le_of_comp_def
fix x y :: 'a
show "le x y ∨ le y x"
using sym [of x y] by (cases "comp x y") (simp_all)
qed
qed

sublocale linorder le lt
by (rule linorder)

lemma Gt_lt_conv: "comp x y = Gt ⟷ lt y x"
unfolding lt_of_comp_def sym[of x y, symmetric]
by (cases "comp x y", auto)
lemma Lt_lt_conv: "comp x y = Lt ⟷ lt x y"
unfolding lt_of_comp_def by (cases "comp x y", auto)
lemma eq_Eq_conv: "comp x y = Eq ⟷ x = y"
by (rule eq)
lemma nGt_le_conv: "comp x y ≠ Gt ⟷ le x y"
unfolding le_of_comp_def by (cases "comp x y", auto)
lemma nLt_le_conv: "comp x y ≠ Lt ⟷ le y x"
unfolding le_of_comp_def sym[of x y, symmetric] by (cases "comp x y", auto)
lemma nEq_neq_conv: "comp x y ≠ Eq ⟷ x ≠ y"
using eq_Eq_conv[of x y] by simp

lemmas le_lt_convs =  nLt_le_conv nGt_le_conv Gt_lt_conv Lt_lt_conv eq_Eq_conv nEq_neq_conv

lemma two_comparisons_into_case_order:
"(if le x y then (if x = y then P else Q) else R) = (case_order P Q R (comp x y))"
"(if le x y then (if y = x then P else Q) else R) = (case_order P Q R (comp x y))"
"(if le x y then (if le y x then P else Q) else R) = (case_order P Q R (comp x y))"
"(if le x y then (if lt x y then Q else P) else R) = (case_order P Q R (comp x y))"
"(if lt x y then Q else (if le x y then P else R)) = (case_order P Q R (comp x y))"
"(if lt x y then Q else (if lt y x then R else P)) = (case_order P Q R (comp x y))"
"(if lt x y then Q else (if x = y then P else R)) = (case_order P Q R (comp x y))"
"(if lt x y then Q else (if y = x then P else R)) = (case_order P Q R (comp x y))"
"(if x = y then P else (if lt y x then R else Q)) = (case_order P Q R (comp x y))"
"(if x = y then P else (if lt x y then Q else R)) = (case_order P Q R (comp x y))"
"(if x = y then P else (if le y x then R else Q)) = (case_order P Q R (comp x y))"
"(if x = y then P else (if le x y then Q else R)) = (case_order P Q R (comp x y))"
by (auto simp: le_lt_convs split: order.splits)

end

lemma comp_of_ords: assumes "class.linorder le lt"
shows "comparator (comp_of_ords le lt)"
proof -
interpret linorder le lt by fact
show ?thesis
by (unfold_locales, auto simp: comp_of_ords_def split: if_splits)
qed

definition (in linorder) comparator_of :: "'a comparator" where
"comparator_of x y = (if x < y then Lt else if x = y then Eq else Gt)"

lemma comparator_of: "comparator comparator_of"
by unfold_locales (auto split: if_splits simp: comparator_of_def)

end
```