src/HOL/Integ/NatBin.thy

Improved efficiency of code generated for functions int and nat.

(*  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

(* Enable arith to deal with div/mod k where k is a numeral: *)
declare split_div[of _ _ "number_of k", standard, arith_split]
declare split_mod[of _ _ "number_of k", standard, arith_split]

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

lemma nat_number_of_Min: "number_of bin.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")

constdefs
  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
  "int_aux i n == (i + int n)"
  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
  "nat_aux n i == (n + nat i)"

lemma [code]:
  "int_aux i 0 = i"
  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
  "int n = int_aux 0 n"
  by (simp add: int_aux_def)+

lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
  by (simp add: nat_aux_def Suc_nat_eq_nat_zadd1) -- {* tail recursive *}
lemma [code]: "nat i = nat_aux 0 i"
  by (simp add: nat_aux_def)

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

end