author | haftmann |
Sat, 11 Nov 2017 18:41:08 +0000 | |
changeset 67051 | e7e54a0b9197 |
parent 63437 | b81a6bfa9c23 |
child 67406 | 23307fd33906 |
permissions | -rw-r--r-- |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
1 |
(* Author: Tobias Nipkow, Daniel Stüwe *) |
61640 | 2 |
|
3 |
section {* Three-Way Comparison *} |
|
4 |
||
5 |
theory Cmp |
|
6 |
imports Main |
|
7 |
begin |
|
8 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
9 |
datatype cmp_val = LT | EQ | GT |
61640 | 10 |
|
63437 | 11 |
definition 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)" |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
13 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
14 |
lemma |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
15 |
LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
16 |
and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
17 |
and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y" |
63437 | 18 |
by (auto simp: cmp_def) |
61640 | 19 |
|
20 |
lemma 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)" |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61640
diff
changeset
|
22 |
by(simp split: cmp_val.split) |
61640 | 23 |
|
24 |
end |