products/Sources/formale Sprachen/VDM/VDMPP/BuslinesPP/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Cmp.thy   Sprache: Unknown

(* 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.1 Sekunden  (vorverarbeitet)  ]