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