Theory Deriving.Compare_Generator

(*  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
*)
subsection ‹Compare Generator›

theory Compare_Generator
imports 
  Comparator_Generator
  Compare
begin

text ‹We provide a generator which takes the comparators of the comparator generator
  to synthesize suitable @{const compare}-functions from the @{class compare}-class.

One can further also use these comparison functions to derive an instance of the
@{class compare_order}-class, and therefore also for @{class linorder}. In total, we provide the three
derive›-methods where the example type @{type prod} can be replaced by any other datatype.

\begin{itemize}
\item derive compare prod› creates an instance @{type prod} :: (@{class compare}, @{class compare}) @{class compare}.
\item derive compare_order prod› creates an instance @{type prod} :: (@{class compare}, @{class compare}) @{class compare_order}.
\item derive linorder prod› creates an instance @{type prod} :: (@{class linorder}, @{class linorder}) @{class linorder}.
\end{itemize}

Usually, the use of derive linorder› is not recommended if there are comparators available:
Internally, the linear orders will directly be converted into comparators, so a direct use of the
comparators will result in more efficient generated code. This command is mainly provided as a convenience method
where comparators are not yet present. For example, at the time of writing, the Container Framework
has partly been adapted to internally use comparators, whereas in other AFP-entries, we did not
integrate comparators.
›

lemma linorder_axiomsD: assumes "class.linorder le lt"
  shows 
  "lt x y = (le x y  ¬ le y x)" (is ?a)
  "le x x" (is ?b)
  "le x y  le y z  le x z" (is "?c1  ?c2  ?c3") 
  "le x y  le y x  x = y" (is "?d1  ?d2  ?d3")
  "le x y  le y x" (is ?e)
proof -
  interpret linorder le lt by fact
  show ?a ?b "?c1  ?c2  ?c3" "?d1  ?d2  ?d3" ?e by auto
qed
 
named_theorems compare_simps "simp theorems to derive \"compare = comparator_of\""

ML_file ‹compare_generator.ML›

end