--- a/src/HOL/Word/BinGeneral.thy Wed Aug 22 21:09:21 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy Thu Aug 23 15:47:42 2007 +0200
@@ -158,11 +158,6 @@
bin_last :: "int => bit"
bin_rest :: "int => int"
bin_sign :: "int => int"
- bin_nth :: "int => nat => bool"
-
-primrec
- Z : "bin_nth w 0 = (bin_last w = bit.B1)"
- Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
defs
bin_rest_def : "bin_rest w == fst (bin_rl w)"
@@ -228,6 +223,15 @@
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
unfolding bin_rest_div [symmetric] by auto
+subsection {* Testing bit positions *}
+
+consts
+ bin_nth :: "int => nat => bool"
+
+primrec
+ Z : "bin_nth w 0 = (bin_last w = bit.B1)"
+ Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
+
lemma bin_nth_lem [rule_format]:
"ALL y. bin_nth x = bin_nth y --> x = y"
apply (induct x rule: bin_induct)