Theory HOL-Data_Structures.Cmp

(* Author: Tobias Nipkow, Daniel Stüwe *)

section ‹Three-Way Comparison›

theory Cmp
imports Main
begin

datatype cmp_val = LT | EQ | GT

definition cmp :: "'a:: linorder  'a  cmp_val" where
"cmp x y = (if x < y then LT else if x=y then EQ else GT)"

lemma 
    LT[simp]: "cmp x y = LT  x < y"
and EQ[simp]: "cmp x y = EQ  x = y"
and GT[simp]: "cmp x y = GT  x > y"
by (auto simp: cmp_def)

lemma case_cmp_if[simp]: "(case c of EQ  e | LT  l | GT  g) =
  (if c = LT then l else if c = GT then g else e)"
by(simp split: cmp_val.split)

end