src/HOL/Data_Structures/Cmp.thy
author haftmann
Sat, 11 Nov 2017 18:41:08 +0000
changeset 67051 e7e54a0b9197
parent 63437 b81a6bfa9c23
child 67406 23307fd33906
permissions -rw-r--r--
dedicated definition for coprimality
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
     2
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
     3
section {* Three-Way Comparison *}
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
     4
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
     5
theory Cmp
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
     6
imports Main
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
     7
begin
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
     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
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
    10
63437
b81a6bfa9c23 restored executability of cmp
nipkow
parents: 63411
diff changeset
    11
definition cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where
b81a6bfa9c23 restored executability of cmp
nipkow
parents: 63411
diff changeset
    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
b81a6bfa9c23 restored executability of cmp
nipkow
parents: 63411
diff changeset
    18
by (auto simp: cmp_def)
61640
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
    19
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
    20
lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) =
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
    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
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
    23
44c9198f210c no CRLF
nipkow
parents: 61581
diff changeset
    24
end