src/HOL/Integ/NatBin.thy

tuned;

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

header {* Binary arithmetic for the natural numbers *}

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

text {*
  This case is simply reduced to that for the non-negative integers.
*}


instance nat :: number ..

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

use "nat_bin.ML"
setup nat_bin_arith_setup

lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
  by (simp add: number_of_Pls nat_number_of_def)

lemma nat_number_of_Min: "number_of Min = (0::nat)"
  apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
  apply (simp add: neg_nat)
  done

lemma nat_number_of_BIT_True:
  "number_of (w BIT True) =
    (if neg (number_of w) then 0
     else let n = number_of w in Suc (n + n))"
  apply (simp only: nat_number_of_def Let_def split: split_if)
  apply (intro conjI impI)
   apply (simp add: neg_nat neg_number_of_BIT)
  apply (rule int_int_eq [THEN iffD1])
  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
  apply (simp only: number_of_BIT if_True zadd_assoc)
  done

lemma nat_number_of_BIT_False:
    "number_of (w BIT False) = (let n::nat = number_of w in n + n)"
  apply (simp only: nat_number_of_def Let_def)
  apply (cases "neg (number_of w)")
   apply (simp add: neg_nat neg_number_of_BIT)
  apply (rule int_int_eq [THEN iffD1])
  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
  apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc)
  done

lemmas nat_number =
  nat_number_of_Pls nat_number_of_Min
  nat_number_of_BIT_True nat_number_of_BIT_False

lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
  by (simp add: Let_def)


subsection {* Configuration of the code generator *}

ML {*
infix 7 `*;
infix 6 `+;

val op `* = op * : int * int -> int;
val op `+ = op + : int * int -> int;
val `~ = ~ : int -> int;
*}

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