1(* Author: Tobias Nipkow, Daniel St��we *) 2 3section \<open>Three-Way Comparison\<close> 4 5theory Cmp 6imports Main 7begin 8 9datatype cmp_val = LT | EQ | GT 10 11definition cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where 12"cmp x y = (if x < y then LT else if x=y then EQ else GT)" 13 14lemma 15 LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y" 16and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y" 17and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y" 18by (auto simp: cmp_def) 19 20lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) = 21 (if c = LT then l else if c = GT then g else e)" 22by(simp split: cmp_val.split) 23 24end 25