|
(* Author: Tobias Nipkow, Daniel Stüwe *)
section \<open>Three-Way Comparison\<close>
theory Cmp
imports Main
begin
datatype cmp_val = LT | EQ | GT
definition cmp :: "'a:: linorder \ 'a \ cmp_val" where
"cmp x y = (if x < y then LT else if x=y then EQ else GT)"
lemma
LT[simp]: "cmp x y = LT \ x < y"
and EQ[simp]: "cmp x y = EQ \ x = y"
and GT[simp]: "cmp x y = GT \ x > y"
by (auto simp: cmp_def)
lemma case_cmp_if[simp]: "(case c of EQ \ e | LT \ l | GT \ g) =
(if c = LT then l else if c = GT then g else e)"
by(simp split: cmp_val.split)
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
