isabelle: src/HOL/Data_Structures/Cmp.thy@dc85b5b3a532 (annotated)

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
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 63437 diff changeset	3	section \<open>Three-Way Comparison\<close>
61640 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

author	paulson <lp15@cam.ac.uk>
	Tue, 22 Jan 2019 12:00:16 +0000
changeset 69712	dc85b5b3a532
parent 67406	23307fd33906
permissions	-rw-r--r--