1.1 --- a/src/HOL/Integ/NatBin.thy	Wed Jan 23 16:57:33 2002 +0100
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Wed Jan 23 16:58:05 2002 +0100
     1.3 @@ -2,23 +2,62 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1999  University of Cambridge
     1.7 +*)
     1.8  
     1.9 -Binary arithmetic for the natural numbers
    1.10 -
    1.11 -This case is simply reduced to that for the non-negative integers
    1.12 -*)
    1.13 +header {* Binary arithmetic for the natural numbers *}
    1.14  
    1.15  theory NatBin = IntPower
    1.16  files ("nat_bin.ML"):
    1.17  
    1.18 -instance  nat :: number ..
    1.19 +text {*
    1.20 +  This case is simply reduced to that for the non-negative integers.
    1.21 +*}
    1.22  
    1.23 -defs
    1.24 -  nat_number_of_def:
    1.25 -    "number_of v == nat (number_of v)"
    1.26 -     (*::bin=>nat        ::bin=>int*)
    1.27  
    1.28 -use "nat_bin.ML"	setup nat_bin_arith_setup
    1.29 +instance nat :: number ..
    1.30 +
    1.31 +defs (overloaded)
    1.32 +  nat_number_of_def: "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
    1.33 +
    1.34 +use "nat_bin.ML"
    1.35 +setup nat_bin_arith_setup
    1.36 +
    1.37 +lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
    1.38 +  by (simp add: number_of_Pls nat_number_of_def)
    1.39 +
    1.40 +lemma nat_number_of_Min: "number_of Min = (0::nat)"
    1.41 +  apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
    1.42 +  apply (simp add: neg_nat)
    1.43 +  done
    1.44 +
    1.45 +lemma nat_number_of_BIT_True:
    1.46 +  "number_of (w BIT True) =
    1.47 +    (if neg (number_of w) then 0
    1.48 +     else let n = number_of w in Suc (n + n))"
    1.49 +  apply (simp only: nat_number_of_def Let_def split: split_if)
    1.50 +  apply (intro conjI impI)
    1.51 +   apply (simp add: neg_nat neg_number_of_BIT)
    1.52 +  apply (rule int_int_eq [THEN iffD1])
    1.53 +  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
    1.54 +  apply (simp only: number_of_BIT if_True zadd_assoc)
    1.55 +  done
    1.56 +
    1.57 +lemma nat_number_of_BIT_False:
    1.58 +    "number_of (w BIT False) = (let n::nat = number_of w in n + n)"
    1.59 +  apply (simp only: nat_number_of_def Let_def)
    1.60 +  apply (cases "neg (number_of w)")
    1.61 +   apply (simp add: neg_nat neg_number_of_BIT)
    1.62 +  apply (rule int_int_eq [THEN iffD1])
    1.63 +  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
    1.64 +  apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc)
    1.65 +  done
    1.66 +
    1.67 +lemmas nat_number_of =
    1.68 +  nat_number_of_Pls nat_number_of_Min
    1.69 +  nat_number_of_BIT_True nat_number_of_BIT_False
    1.70 +
    1.71 +lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    1.72 +  by (simp add: Let_def)
    1.73  
    1.74  
    1.75  subsection {* Configuration of the code generator *}