Theory Cmp

(* Author: Tobias Nipkow *)

section {* Three-Way Comparison *}

theory Cmp
imports Main
begin

datatype cmp = LT | EQ | GT

class cmp = linorder +
fixes cmp :: "'a ⇒ 'a ⇒ cmp"
assumes LT[simp]: "cmp x y = LT ⟷ x < y"
assumes EQ[simp]: "cmp x y = EQ ⟷ x = y"
assumes GT[simp]: "cmp x y = GT ⟷ x > y"

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.split)

end