|
61581
|
1 |
(* Author: Tobias Nipkow *)
|
|
|
2 |
|
|
|
3 |
section {* Three-Way Comparison *}
|
|
|
4 |
|
|
|
5 |
theory Cmp
|
|
|
6 |
imports Main
|
|
|
7 |
begin
|
|
|
8 |
|
|
|
9 |
datatype cmp = LT | EQ | GT
|
|
|
10 |
|
|
|
11 |
class cmp = linorder +
|
|
|
12 |
fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> cmp"
|
|
|
13 |
assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
|
|
|
14 |
assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
|
|
|
15 |
assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
|
|
|
16 |
|
|
|
17 |
lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) =
|
|
|
18 |
(if c = LT then l else if c = GT then g else e)"
|
|
|
19 |
by(simp split: cmp.split)
|
|
|
20 |
|
|
|
21 |
end
|