src/HOL/Data_Structures/Cmp.thy
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61640 44c9198f210c
child 63411 e051eea34990
permissions -rw-r--r--
proper syntax;

(* Author: Tobias Nipkow *)

section {* Three-Way Comparison *}

theory Cmp
imports Main
begin

datatype cmp = LT | EQ | GT

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

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

end