Theory Deriving.Compare

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
subsection ‹Compare›

theory Compare
imports Comparator
keywords "compare_code" :: thy_decl

text ‹This introduces a type class for having a proper comparator, similar to @{class linorder}.
  Since most of the Isabelle/HOL algorithms work on the latter, we also provide a method which 
  turns linear-order based algorithms into comparator-based algorithms, where two consecutive 
  invocations of linear orders and equality are merged into one comparator invocation.
  We further define a class which both define a linear order and a comparator, and where the
  induces orders coincide.›

class compare =
  fixes compare :: "'a comparator"
  assumes comparator_compare: "comparator compare"

lemma compare_Eq_is_eq [simp]:
  "compare x y = Eq  x = y"
  by (rule comparator.eq [OF comparator_compare])
lemma compare_refl [simp]:
  "compare x x = Eq"
  by simp


lemma (in linorder) le_lt_comparator_of:
  "le_of_comp comparator_of = (≤)" "lt_of_comp comparator_of = (<)"
  by (intro ext, auto simp: comparator_of_def le_of_comp_def lt_of_comp_def)+

class compare_order = ord + compare +
  assumes ord_defs: "le_of_comp compare = (≤) " "lt_of_comp compare = (<)"

text @{class compare_order} is @{class compare} and @{class linorder}, where comparator and orders 
  define the same ordering.›

subclass (in compare_order) linorder
  by (unfold ord_defs[symmetric], rule comparator.linorder, rule comparator_compare)

context compare_order

lemma compare_is_comparator_of: 
  "compare = comparator_of" 
proof (intro ext)
  fix x y :: 'a
  show "compare x y = comparator_of x y"
    by  (unfold comparator_of_def, unfold ord_defs[symmetric] lt_of_comp_def, 
      cases "compare x y", auto)

lemmas two_comparisons_into_compare = 
  comparator.two_comparisons_into_case_order[OF comparator_compare, unfolded ord_defs]
thm two_comparisons_into_compare

ML_file ‹compare_code.ML›

text Compare_Code.change_compare_code const ty-vars› changes the code equations of some constant such that
  two consecutive comparisons via @{term "(<=)"}, @{term "(<)"}", or @{term "(=)"} are turned into one
  invocation of @{const compare}. 
  The difference to a standard code_unfold› is that here we change the code-equations
  where an additional sort-constraint on @{class compare_order} can be added. Otherwise, there would
  be no @{const compare}-function.›