Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Client.thy Sprache: Isabelle

Original von: Isabelle^©

(* 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.17 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.