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 
    License:     LGPL
*)
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"
  by (simp add: 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