src/HOL/Integ/NatBin.thy

registered directly executable version with the code generator

(*  Title:      HOL/NatBin.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1999  University of Cambridge

Binary arithmetic for the natural numbers

This case is simply reduced to that for the non-negative integers
*)

theory NatBin = IntPower
files ("nat_bin.ML"):

instance  nat :: number ..

defs
  nat_number_of_def:
    "number_of v == nat (number_of v)"
     (*::bin=>nat        ::bin=>int*)

use "nat_bin.ML"	setup nat_bin_arith_setup


subsection {* Configuration of the code generator *}

types_code
  "int" ("int")

lemmas [code] = int_0 int_Suc

lemma [code]: "nat x = (if x <= 0 then 0 else Suc (nat (x - 1)))"
  by (simp add: Suc_nat_eq_nat_zadd1)

consts_code
  "0" :: "int"                  ("0")
  "1" :: "int"                  ("1")
  "uminus" :: "int => int"      ("~")
  "op +" :: "int => int => int" ("(_ +/ _)")
  "op *" :: "int => int => int" ("(_ */ _)")
  "neg"                         ("(_ < 0)")

end