src/HOL/Integ/NatBin.thy

--- a/src/HOL/Integ/NatBin.thy	Wed Jan 23 16:57:33 2002 +0100
+++ b/src/HOL/Integ/NatBin.thy	Wed Jan 23 16:58:05 2002 +0100
@@ -2,23 +2,62 @@
     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
-*)
+header {* Binary arithmetic for the natural numbers *}
 
 theory NatBin = IntPower
 files ("nat_bin.ML"):
 
-instance  nat :: number ..
+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
 
-defs
-  nat_number_of_def:
-    "number_of v == nat (number_of v)"
-     (*::bin=>nat        ::bin=>int*)
+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
 
-use "nat_bin.ML"	setup nat_bin_arith_setup
+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_of =
+  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 *}