fpSemScript.sml

(*Generated by Lem from fpSem.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory libTheory machine_ieeeTheory;

val _ = numLib.prefer_num();



val _ = new_theory "fpSem"

(*open import Pervasives*)
(*open import Lib*)

(*open import {hol} `machine_ieeeTheory`*)
(*open import {isabelle} `IEEE_Floating_Point.FP64`*)

(*type rounding*)

val _ = Hol_datatype `
 fp_cmp = FP_Less | FP_LessEqual | FP_Greater | FP_GreaterEqual | FP_Equal`;

val _ = Hol_datatype `
 fp_uop = FP_Abs | FP_Neg | FP_Sqrt`;

val _ = Hol_datatype `
 fp_bop = FP_Add | FP_Sub | FP_Mul | FP_Div`;


(*val fp64_lessThan     : word64 -> word64 -> bool*)
(*val fp64_lessEqual    : word64 -> word64 -> bool*)
(*val fp64_greaterThan  : word64 -> word64 -> bool*)
(*val fp64_greaterEqual : word64 -> word64 -> bool*)
(*val fp64_equal        : word64 -> word64 -> bool*)

(*val fp64_abs    : word64 -> word64*)
(*val fp64_negate : word64 -> word64*)
(*val fp64_sqrt   : rounding -> word64 -> word64*)

(*val fp64_add : rounding -> word64 -> word64 -> word64*)
(*val fp64_sub : rounding -> word64 -> word64 -> word64*)
(*val fp64_mul : rounding -> word64 -> word64 -> word64*)
(*val fp64_div : rounding -> word64 -> word64 -> word64*)

(*val roundTiesToEven : rounding*)

(*val fp_cmp : fp_cmp -> word64 -> word64 -> bool*)
val _ = Define `
 (fp_cmp fop=  ((case fop of
    FP_Less => fp64_lessThan
  | FP_LessEqual => fp64_lessEqual
  | FP_Greater => fp64_greaterThan
  | FP_GreaterEqual => fp64_greaterEqual
  | FP_Equal => fp64_equal
)))`;


(*val fp_uop : fp_uop -> word64 -> word64*)
val _ = Define `
 (fp_uop fop=  ((case fop of
    FP_Abs => fp64_abs
  | FP_Neg => fp64_negate
  | FP_Sqrt => fp64_sqrt roundTiesToEven
)))`;


(*val fp_bop : fp_bop -> word64 -> word64 -> word64*)
val _ = Define `
 (fp_bop fop=  ((case fop of
    FP_Add => fp64_add roundTiesToEven
  | FP_Sub => fp64_sub roundTiesToEven
  | FP_Mul => fp64_mul roundTiesToEven
  | FP_Div => fp64_div roundTiesToEven
)))`;

val _ = export_theory()