# HG changeset patch
# User wenzelm
# Date 1325106524 -3600
# Node ID 64a19ea435fc3ead864a327cba9c0d9af6bf6680
# Parent  b4dcefaa17211c53c5d373cd4561c7acafe1e049# Parent  c296c75f4cf40a5ac422b711f5dffd89a987517f
merged

diff -r c296c75f4cf4 -r 64a19ea435fc NEWS
--- a/NEWS	Wed Dec 28 20:03:13 2011 +0100
+++ b/NEWS	Wed Dec 28 22:08:44 2011 +0100
@@ -70,7 +70,7 @@
 it is often sufficent to prune any tinkering with former theorems mem_def
 and Collect_def.
 
-* Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPABILITY.
+* Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPATIBILITY.
 
 * 'datatype' specifications allow explicit sort constraints.
 
@@ -113,14 +113,22 @@
   word_order_linear ~> linorder_linear
   lenw1_zero_neq_one ~> zero_neq_one
   word_number_of_eq ~> number_of_eq
-
-* Clarified attribute "mono_set": pure declararation without modifying
+  word_of_int_add_hom ~> wi_hom_add
+  word_of_int_sub_hom ~> wi_hom_sub
+  word_of_int_mult_hom ~> wi_hom_mult
+  word_of_int_minus_hom ~> wi_hom_neg
+  word_of_int_succ_hom ~> wi_hom_succ
+  word_of_int_pred_hom ~> wi_hom_pred
+  word_of_int_0_hom ~> word_0_wi
+  word_of_int_1_hom ~> word_1_wi
+
+* Clarified attribute "mono_set": pure declaration without modifying
 the result of the fact expression.
 
 * "Transitive_Closure.ntrancl": bounded transitive closure on
 relations.
 
-* Constant "Set.not_member" now qualifed.  INCOMPATIBILITY.
+* Constant "Set.not_member" now qualified.  INCOMPATIBILITY.
 
 * "sublists" moved to theory More_List.  INCOMPATIBILITY.
 
diff -r c296c75f4cf4 -r 64a19ea435fc src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Wed Dec 28 22:08:44 2011 +0100
@@ -12,54 +12,6 @@
 imports Bit_Representation Bit_Operations
 begin
 
-subsection {* Recursion combinators for bitstrings *}
-
-function bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a" where 
-  "bin_rec f1 f2 f3 bin = (if bin = 0 then f1 
-    else if bin = - 1 then f2
-    else f3 (bin_rest bin) (bin_last bin) (bin_rec f1 f2 f3 (bin_rest bin)))"
-  by pat_completeness auto
-
-termination by (relation "measure (nat o abs o snd o snd o snd)")
-  (simp_all add: bin_last_def bin_rest_def)
-
-declare bin_rec.simps [simp del]
-
-lemma bin_rec_PM:
-  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
-  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
-  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
-  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Bit0:
-  "f3 Int.Pls (0::bit) f1 = f1 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)"
-  by (unfold Pls_def Min_def Bit0_def Bit1_def) (simp add: bin_rec.simps bin_last_def bin_rest_def)
-
-lemma bin_rec_Bit1:
-  "f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)"
-  apply (cases "w = Int.Min")
-  apply (simp add: bin_rec_Min)
-  apply (cases "w = Int.Pls")
-  apply (simp add: bin_rec_Pls number_of_is_id Pls_def [symmetric] bin_rec.simps)
-  apply (subst bin_rec.simps)
-  apply auto unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id apply auto
-  done
-  
-lemma bin_rec_Bit:
-  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls (0::bit) f1 = f1 ==> 
-    f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
-  by (cases b, simp add: bin_rec_Bit0 BIT_simps, simp add: bin_rec_Bit1 BIT_simps)
-
-lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
-  bin_rec_Bit0 bin_rec_Bit1
-
-
 subsection {* Logical operations *}
 
 text "bit-wise logical operations on the int type"
@@ -67,21 +19,25 @@
 instantiation int :: bit
 begin
 
-definition
-  int_not_def: "bitNOT = bin_rec (- 1) 0
-    (\<lambda>w b s. s BIT (NOT b))"
+definition int_not_def:
+  "bitNOT = (\<lambda>x::int. - x - 1)"
 
-definition
-  int_and_def: "bitAND = bin_rec (\<lambda>x. 0) (\<lambda>y. y) 
-    (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
+function bitAND_int where
+  "bitAND_int x y =
+    (if x = 0 then 0 else if x = -1 then y else
+      (bin_rest x AND bin_rest y) BIT (bin_last x AND bin_last y))"
+  by pat_completeness simp
 
-definition
-  int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. - 1) 
-    (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
+termination
+  by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
+
+declare bitAND_int.simps [simp del]
 
-definition
-  int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
-    (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
+definition int_or_def:
+  "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
+
+definition int_xor_def:
+  "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
 
 instance ..
 
@@ -89,33 +45,78 @@
 
 subsubsection {* Basic simplification rules *}
 
+lemma int_not_BIT [simp]:
+  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
+  unfolding int_not_def Bit_def by (cases b, simp_all)
+
 lemma int_not_simps [simp]:
   "NOT Int.Pls = Int.Min"
   "NOT Int.Min = Int.Pls"
   "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
   "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
-  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
-  unfolding int_not_def Pls_def [symmetric] Min_def [symmetric]
-  by (simp_all add: bin_rec_simps BIT_simps)
+  unfolding int_not_def Pls_def Min_def Bit0_def Bit1_def by simp_all
+
+lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
+  unfolding int_not_def by simp
+
+lemma int_and_0 [simp]: "(0::int) AND x = 0"
+  by (simp add: bitAND_int.simps)
+
+lemma int_and_m1 [simp]: "(-1::int) AND x = x"
+  by (simp add: bitAND_int.simps)
+
+lemma int_and_Pls [simp]: "Int.Pls AND x = Int.Pls"
+  unfolding Pls_def by simp
+
+lemma int_and_Min [simp]: "Int.Min AND x = x"
+  unfolding Min_def by simp
+
+lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
+  by (subst BIT_eq_iff [symmetric], simp)
+
+lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
+  by (subst BIT_eq_iff [symmetric], simp)
+
+lemma int_and_Bits [simp]: 
+  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
+  by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
 
-lemma int_xor_Pls [simp]: 
-  "Int.Pls XOR x = x"
-  unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
+lemma int_and_Bits2 [simp]: 
+  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
+  unfolding BIT_simps [symmetric] int_and_Bits by simp_all
+
+lemma int_or_Pls [simp]: "Int.Pls OR x = x"
+  unfolding int_or_def by simp
+
+lemma int_or_Min [simp]: "Int.Min OR x = Int.Min"
+  unfolding int_or_def by simp
+
+lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
+  by (induct b, simp_all) (* TODO: move *)
 
-lemma int_xor_Min [simp]: 
-  "Int.Min XOR x = NOT x"
-  unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
+lemma int_or_Bits [simp]: 
+  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
+  unfolding int_or_def bit_or_def by simp
+
+lemma int_or_Bits2 [simp]: 
+  "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
+  "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+  "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
+  "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+  unfolding int_or_def by simp_all
+
+lemma int_xor_Pls [simp]: "Int.Pls XOR x = x"
+  unfolding int_xor_def by simp
+
+lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
+  by (induct b, simp_all) (* TODO: move *)
 
 lemma int_xor_Bits [simp]: 
   "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
-  apply (unfold int_xor_def Pls_def [symmetric] Min_def [symmetric])
-  apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
-    apply (rule ext, simp)
-   prefer 2
-   apply simp
-  apply (rule ext)
-  apply (simp add: int_not_simps [symmetric])
-  done
+  unfolding int_xor_def bit_xor_def by simp
 
 lemma int_xor_Bits2 [simp]: 
   "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
@@ -124,46 +125,6 @@
   "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
   unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
 
-lemma int_or_Pls [simp]: 
-  "Int.Pls OR x = x"
-  by (unfold int_or_def) (simp add: bin_rec_PM)
-  
-lemma int_or_Min [simp]:
-  "Int.Min OR x = Int.Min"
-  by (unfold int_or_def Pls_def [symmetric] Min_def [symmetric]) (simp add: bin_rec_PM)
-
-lemma int_or_Bits [simp]: 
-  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
-  unfolding int_or_def Pls_def [symmetric] Min_def [symmetric]
-  by (simp add: bin_rec_simps BIT_simps)
-
-lemma int_or_Bits2 [simp]: 
-  "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
-  "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
-  "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
-  "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
-  unfolding BIT_simps [symmetric] int_or_Bits by simp_all
-
-lemma int_and_Pls [simp]:
-  "Int.Pls AND x = Int.Pls"
-  unfolding int_and_def Pls_def [symmetric] by (simp add: bin_rec_PM)
-
-lemma int_and_Min [simp]:
-  "Int.Min AND x = x"
-  unfolding int_and_def by (simp add: bin_rec_PM)
-
-lemma int_and_Bits [simp]: 
-  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
-  unfolding int_and_def Pls_def [symmetric] Min_def [symmetric]
-  by (simp add: bin_rec_simps BIT_simps)
-
-lemma int_and_Bits2 [simp]: 
-  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
-  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
-  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
-  "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
-  unfolding BIT_simps [symmetric] int_and_Bits by simp_all
-
 subsubsection {* Binary destructors *}
 
 lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
@@ -205,6 +166,9 @@
 
 subsubsection {* Derived properties *}
 
+lemma int_xor_Min [simp]: "Int.Min XOR x = NOT x"
+  by (auto simp add: bin_eq_iff bin_nth_ops)
+
 lemma int_xor_extra_simps [simp]:
   "w XOR Int.Pls = w"
   "w XOR Int.Min = NOT w"
@@ -234,9 +198,6 @@
   "(x::int) XOR x = Int.Pls"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
-lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
-  by (auto simp add: bin_eq_iff bin_nth_ops)
-
 lemmas bin_log_esimps = 
   int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
   int_and_Pls int_and_Min  int_or_Pls int_or_Min  int_xor_Pls int_xor_Min
@@ -617,8 +578,6 @@
   apply (induct n arbitrary: m)
    apply clarsimp
    apply safe
-     apply (case_tac m) 
-      apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq])
    apply (case_tac m) 
     apply (auto simp: Bit_B0_2t [symmetric])
   done
@@ -630,4 +589,3 @@
   by auto
 
 end
-
diff -r c296c75f4cf4 -r 64a19ea435fc src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 28 22:08:44 2011 +0100
@@ -269,14 +269,17 @@
 lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
   by (induct n) auto
 
+lemma bin_nth_1 [simp]: "bin_nth 1 n \<longleftrightarrow> n = 0"
+  by (cases n) simp_all
+
 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
-  by (induct n) auto
+  by (induct n) auto (* FIXME: delete *)
 
 lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
   by (induct n) auto
 
 lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
-  by (induct n) auto
+  by (induct n) auto (* FIXME: delete *)
 
 lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))"
   by auto
@@ -288,18 +291,18 @@
   by (cases n) auto
 
 lemma bin_nth_minus_Bit0 [simp]:
-  "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
-  using bin_nth_minus [where b="(0::bit)"] by (simp add: BIT_simps)
+  "0 < n ==> bin_nth (number_of (Int.Bit0 w)) n = bin_nth (number_of w) (n - 1)"
+  using bin_nth_minus [where w="number_of w" and b="(0::bit)"] by simp
 
 lemma bin_nth_minus_Bit1 [simp]:
-  "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
-  using bin_nth_minus [where b="(1::bit)"] by (simp add: BIT_simps)
+  "0 < n ==> bin_nth (number_of (Int.Bit1 w)) n = bin_nth (number_of w) (n - 1)"
+  using bin_nth_minus [where w="number_of w" and b="(1::bit)"] by simp
 
 lemmas bin_nth_0 = bin_nth.simps(1)
 lemmas bin_nth_Suc = bin_nth.simps(2)
 
 lemmas bin_nth_simps = 
-  bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
+  bin_nth_0 bin_nth_Suc bin_nth_zero bin_nth_minus1 bin_nth_minus
   bin_nth_minus_Bit0 bin_nth_minus_Bit1
 
 
@@ -416,12 +419,14 @@
   by (cases n) auto
 
 lemma bin_nth_Bit0:
-  "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
-  using bin_nth_Bit [where b="(0::bit)"] by (simp add: BIT_simps)
+  "bin_nth (number_of (Int.Bit0 w)) n \<longleftrightarrow>
+    (\<exists>m. n = Suc m \<and> bin_nth (number_of w) m)"
+  using bin_nth_Bit [where w="number_of w" and b="(0::bit)"] by simp
 
 lemma bin_nth_Bit1:
-  "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
-  using bin_nth_Bit [where b="(1::bit)"] by (simp add: BIT_simps)
+  "bin_nth (number_of (Int.Bit1 w)) n \<longleftrightarrow>
+    n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (number_of w) m)"
+  using bin_nth_Bit [where w="number_of w" and b="(1::bit)"] by simp
 
 lemma bintrunc_bintrunc_l:
   "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
diff -r c296c75f4cf4 -r 64a19ea435fc src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy	Wed Dec 28 22:08:44 2011 +0100
@@ -14,7 +14,7 @@
 type_synonym word8 = "8 word"
 type_synonym byte = word8
 
--- "modulus"
+text "modulus"
 
 lemma "(27 :: 4 word) = -5" by simp
 
@@ -22,10 +22,12 @@
 
 lemma "27 \<noteq> (11 :: 6 word)" by simp
 
--- "signed"
+text "signed"
+
 lemma "(127 :: 6 word) = -1" by simp
 
--- "number ring simps"
+text "number ring simps"
+
 lemma 
   "27 + 11 = (38::'a::len word)"
   "27 + 11 = (6::5 word)"
@@ -43,57 +45,70 @@
 lemma "23 \<le> (27::8 word)" by simp
 lemma "\<not> 23 < (27::2 word)" by simp
 lemma "0 < (4::3 word)" by simp
+lemma "1 < (4::3 word)" by simp
+lemma "0 < (1::3 word)" by simp
 
--- "ring operations"
+text "ring operations"
 
 lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
 
--- "casting"
+text "casting"
 
 lemma "uint (234567 :: 10 word) = 71" by simp
 lemma "uint (-234567 :: 10 word) = 953" by simp
 lemma "sint (234567 :: 10 word) = 71" by simp
 lemma "sint (-234567 :: 10 word) = -71" by simp
+lemma "uint (1 :: 10 word) = 1" by simp
 
 lemma "unat (-234567 :: 10 word) = 953" by simp
+lemma "unat (1 :: 10 word) = 1" by simp
 
 lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
+lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
 
--- "reducing goals to nat or int and arith:"
+text "reducing goals to nat or int and arith:"
 lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith
 lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith
 
--- "bool lists"
+text "bool lists"
 
 lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
 
 lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
 
--- "this is not exactly fast, but bearable"
+text "this is not exactly fast, but bearable"
 lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
 
--- "this works only for replicate n True"
+text "this works only for replicate n True"
 lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
   by (unfold mask_bl [symmetric]) (simp add: mask_def)
 
 
--- "bit operations"
+text "bit operations"
 
 lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
-
 lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
-
 lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
-
 lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
+lemma "0 AND 5 = (0 :: byte)" by simp
+lemma "1 AND 1 = (1 :: byte)" by simp
+lemma "1 AND 0 = (0 :: byte)" by simp
+lemma "1 AND 5 = (1 :: byte)" apply simp? oops
+lemma "1 OR 6 = (7 :: byte)" apply simp? oops
+lemma "1 OR 1 = (1 :: byte)" by simp
+lemma "1 XOR 7 = (6 :: byte)" apply simp? oops
+lemma "1 XOR 1 = (0 :: byte)" by simp
+lemma "NOT 1 = (254 :: byte)" apply simp? oops
+lemma "NOT 0 = (255 :: byte)" apply simp oops
 
 lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
 
 lemma "(0b0010 :: 4 word) !! 1" by simp
 lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
 lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
+lemma "\<not> (1 :: 3 word) !! 2" apply simp? oops
 
 lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" 
   by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
@@ -101,12 +116,18 @@
 lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
 lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
 lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
+lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" apply simp? oops
+lemma "set_bit 1 0 False = (0::'a::len0 word)" apply simp? oops
 
 lemma "lsb (0b0101::'a::len word)" by simp
 lemma "\<not> lsb (0b1000::'a::len word)" by simp
+lemma "lsb (1::'a::len word)" by simp
+lemma "\<not> lsb (0::'a::len word)" by simp
 
 lemma "\<not> msb (0b0101::4 word)" by simp
 lemma   "msb (0b1000::4 word)" by simp
+lemma "\<not> msb (1::4 word)" apply simp? oops
+lemma "\<not> msb (0::4 word)" apply simp? oops
 
 lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
 lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" 
@@ -115,13 +136,19 @@
 lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
 lemma "0b1011 >> 2 = (0b10::8 word)" by simp
 lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
+lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops
 
 lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
+lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops
 
 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
 lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
 lemma "word_roti -2 0b0110 = (0b1001::4 word)" by simp
+lemma "word_rotr 2 0 = (0::4 word)" by simp
+lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_roti -2 1 = (0b0100::4 word)" apply simp? oops
 
 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
 proof -
diff -r c296c75f4cf4 -r 64a19ea435fc src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 28 22:08:44 2011 +0100
@@ -132,9 +132,6 @@
 lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
   by (simp add: sints_def range_sbintrunc)
 
-lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
-  by auto
-
 lemma 
   uint_0:"0 <= uint x" and 
   uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
@@ -153,19 +150,17 @@
                    word.uint_inverse word.Abs_word_inverse int_mod_lem)
   done
 
-lemma int_word_uint:
-  "uint (word_of_int x::'a::len0 word) = x mod 2 ^ len_of TYPE('a)"
-  by (fact td_ext_uint [THEN td_ext.eq_norm])
-
 interpretation word_uint:
   td_ext "uint::'a::len0 word \<Rightarrow> int" 
          word_of_int 
          "uints (len_of TYPE('a::len0))"
          "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   by (rule td_ext_uint)
-  
+
 lemmas td_uint = word_uint.td_thm
 
+lemmas int_word_uint = word_uint.eq_norm
+
 lemmas td_ext_ubin = td_ext_uint 
   [unfolded len_gt_0 no_bintr_alt1 [symmetric]]
 
@@ -227,8 +222,8 @@
 definition
   word_number_of_def: "number_of w = word_of_int w"
 
-lemmas word_arith_wis = 
-  word_add_def word_mult_def word_minus_def 
+lemmas word_arith_wis =
+  word_add_def word_sub_wi word_mult_def word_minus_def 
   word_succ_def word_pred_def word_0_wi word_1_wi
 
 lemmas arths = 
@@ -237,6 +232,7 @@
 lemma wi_homs: 
   shows
   wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
+  wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" and
   wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
   wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
   wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and
@@ -245,29 +241,9 @@
 
 lemmas wi_hom_syms = wi_homs [symmetric]
 
-lemma word_of_int_sub_hom:
-  "(word_of_int a) - word_of_int b = word_of_int (a - b)"
-  by (simp add: word_sub_wi arths)
-
-lemmas new_word_of_int_homs = 
-  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
-
-lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric]
-
-lemmas word_of_int_hom_syms =
-  new_word_of_int_hom_syms (* FIXME: duplicate *)
-
-lemmas word_of_int_homs =
-  new_word_of_int_homs (* FIXME: duplicate *)
-
-(* FIXME: provide only one copy of these theorems! *)
-lemmas word_of_int_add_hom = wi_hom_add
-lemmas word_of_int_mult_hom = wi_hom_mult
-lemmas word_of_int_minus_hom = wi_hom_neg
-lemmas word_of_int_succ_hom = wi_hom_succ
-lemmas word_of_int_pred_hom = wi_hom_pred
-lemmas word_of_int_0_hom = word_0_wi
-lemmas word_of_int_1_hom = word_1_wi
+lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi
+
+lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
 
 instance
   by default (auto simp: split_word_all word_of_int_homs algebra_simps)
@@ -288,7 +264,7 @@
 lemma word_of_int: "of_int = word_of_int"
   apply (rule ext)
   apply (case_tac x rule: int_diff_cases)
-  apply (simp add: word_of_nat word_of_int_sub_hom)
+  apply (simp add: word_of_nat wi_hom_sub)
   done
 
 instance word :: (len) number_ring
@@ -462,6 +438,8 @@
 (* FIXME: only provide one theorem name *)
 lemmas of_nth_def = word_set_bits_def
 
+subsection {* Theorems about typedefs *}
+
 lemma sint_sbintrunc': 
   "sint (word_of_int bin :: 'a word) = 
     (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
@@ -670,6 +648,8 @@
   "x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"
   unfolding word_size by (rule order_trans [OF _ sint_ge])
 
+subsection {* Testing bits *}
+
 lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
   unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
 
@@ -680,17 +660,16 @@
   apply fast
   done
 
-lemma word_eqI [rule_format] : 
+lemma word_eq_iff:
+  fixes x y :: "'a::len0 word"
+  shows "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"
+  unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]
+  by (metis test_bit_size [unfolded word_size])
+
+lemma word_eqI [rule_format]:
   fixes u :: "'a::len0 word"
   shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
-  apply (rule test_bit_eq_iff [THEN iffD1])
-  apply (rule ext)
-  apply (erule allE)
-  apply (erule impCE)
-   prefer 2
-   apply assumption
-  apply (auto dest!: test_bit_size simp add: word_size)
-  done
+  by (simp add: word_size word_eq_iff)
 
 lemma word_eqD: "(u::'a::len0 word) = v \<Longrightarrow> u !! x = v !! x"
   by simp
@@ -810,8 +789,11 @@
 
 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   unfolding uint_bl by (simp add : word_size)
-  
-lemmas uint_bl_bin [simp] = trans [OF bin_bl_bin word_ubin.norm_Rep]
+
+lemma uint_bl_bin:
+  fixes x :: "'a::len0 word"
+  shows "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
+  by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
 
 (* FIXME: the next two lemmas should be unnecessary, because the lhs
 terms should never occur in practice *)
@@ -894,10 +876,21 @@
    word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (number_of w))"
   unfolding scast_def by simp
 
-lemmas source_size = source_size_def [unfolded Let_def word_size]
-lemmas target_size = target_size_def [unfolded Let_def word_size]
-lemmas is_down = is_down_def [unfolded source_size target_size]
-lemmas is_up = is_up_def [unfolded source_size target_size]
+lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = len_of TYPE('a)"
+  unfolding source_size_def word_size Let_def ..
+
+lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = len_of TYPE('b)"
+  unfolding target_size_def word_size Let_def ..
+
+lemma is_down:
+  fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+  shows "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"
+  unfolding is_down_def source_size target_size ..
+
+lemma is_up:
+  fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+  shows "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"
+  unfolding is_up_def source_size target_size ..
 
 lemmas is_up_down = trans [OF is_up is_down [symmetric]]
 
@@ -1041,7 +1034,6 @@
 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
 
 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
-lemmas word_log_bin_defs = word_log_defs
 
 text {* Executable equality *}
 
@@ -1060,9 +1052,7 @@
 subsection {* Word Arithmetic *}
 
 lemma word_less_alt: "(a < b) = (uint a < uint b)"
-  unfolding word_less_def word_le_def
-  by (auto simp del: word_uint.Rep_inject 
-           simp: word_uint.Rep_inject [symmetric])
+  unfolding word_less_def word_le_def by (simp add: less_le)
 
 lemma signed_linorder: "class.linorder word_sle word_sless"
 proof
@@ -1100,12 +1090,8 @@
 lemma word_0_no: "(0::'a::len0 word) = Numeral0"
   by (simp add: word_number_of_alt)
 
-lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
-  unfolding Pls_def Bit_def by auto
-
-lemma word_1_no: 
-  "(1 :: 'a :: len0 word) = number_of (Int.Pls BIT 1)"
-  unfolding word_1_wi word_number_of_def int_one_bin by auto
+lemma word_1_no: "(1::'a::len0 word) = Numeral1"
+  by (simp add: word_number_of_alt)
 
 lemma word_m1_wi: "-1 = word_of_int -1" 
   by (rule word_number_of_alt)
@@ -1204,7 +1190,7 @@
   by (rule word_uint.Abs_cases [of b],
       rule word_uint.Abs_cases [of a],
       simp add: add_commute mult_commute 
-                ring_distribs new_word_of_int_homs
+                ring_distribs word_of_int_homs
            del: word_of_int_0 word_of_int_1)+
 
 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
@@ -1237,11 +1223,11 @@
   "word_succ (number_of bin) = number_of (Int.succ bin) & 
     word_pred (number_of bin) = number_of (Int.pred bin)"
   unfolding word_number_of_def Int.succ_def Int.pred_def
-  by (simp add: new_word_of_int_homs)
+  by (simp add: word_of_int_homs)
 
 lemma word_sp_01 [simp] : 
   "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
-  by (unfold word_0_no word_1_no) (auto simp: BIT_simps)
+  unfolding word_0_no word_1_no by simp
 
 (* alternative approach to lifting arithmetic equalities *)
 lemma word_of_int_Ex:
@@ -1502,7 +1488,7 @@
 
 lemmas le_plus = le_plus' [rotated]
 
-lemmas le_minus = leD [THEN thin_rl, THEN le_minus']
+lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
 
 lemma word_plus_mono_right: 
   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
@@ -1774,11 +1760,11 @@
 
 lemma Abs_fnat_hom_mult:
   "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
-  by (simp add: word_of_nat word_of_int_mult_hom zmult_int)
+  by (simp add: word_of_nat wi_hom_mult zmult_int)
 
 lemma Abs_fnat_hom_Suc:
   "word_succ (of_nat a) = of_nat (Suc a)"
-  by (simp add: word_of_nat word_of_int_succ_hom add_ac)
+  by (simp add: word_of_nat wi_hom_succ add_ac)
 
 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
   by simp
@@ -2108,17 +2094,23 @@
   folded word_ubin.eq_norm, THEN eq_reflection]
 
 (* the binary operations only *)
+(* BH: why is this needed? *)
 lemmas word_log_binary_defs = 
   word_and_def word_or_def word_xor_def
 
-lemmas word_no_log_defs [simp] = 
-  word_not_def  [where a="number_of a", 
-                 unfolded word_no_wi wils1, folded word_no_wi]
-  word_log_binary_defs [where a="number_of a" and b="number_of b",
-                        unfolded word_no_wi wils1, folded word_no_wi]
-  for a b
-
-lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
+lemma word_wi_log_defs:
+  "NOT word_of_int a = word_of_int (NOT a)"
+  "word_of_int a AND word_of_int b = word_of_int (a AND b)"
+  "word_of_int a OR word_of_int b = word_of_int (a OR b)"
+  "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
+  unfolding word_log_defs wils1 by simp_all
+
+lemma word_no_log_defs [simp]:
+  "NOT number_of a = (number_of (NOT a) :: 'a::len0 word)"
+  "number_of a AND number_of b = (number_of (a AND b) :: 'a word)"
+  "number_of a OR number_of b = (number_of (a OR b) :: 'a word)"
+  "number_of a XOR number_of b = (number_of (a XOR b) :: 'a word)"
+  unfolding word_no_wi word_wi_log_defs by simp_all
 
 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   by (simp add: word_or_def word_wi_log_defs word_ubin.eq_norm
@@ -2147,11 +2139,24 @@
   apply (simp add : test_bit_bin word_size)
   done
 
+lemma test_bit_wi [simp]:
+  "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
+  unfolding word_test_bit_def
+  by (simp add: nth_bintr [symmetric] word_ubin.eq_norm)
+
+lemma test_bit_no [simp]:
+  "(number_of w :: 'a::len0 word) !! n \<longleftrightarrow>
+    n < len_of TYPE('a) \<and> bin_nth (number_of w) n"
+  unfolding word_number_of_alt test_bit_wi ..
+
+lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
+  unfolding word_test_bit_def by simp
+
 (* get from commutativity, associativity etc of int_and etc
   to same for word_and etc *)
 
 lemmas bwsimps = 
-  word_of_int_homs(2) 
+  wi_hom_add
   word_0_wi_Pls
   word_m1_wi_Min
   word_wi_log_defs
@@ -2162,10 +2167,7 @@
   "(x AND y) AND z = x AND y AND z"
   "(x OR y) OR z = x OR y OR z"
   "(x XOR y) XOR z = x XOR y XOR z"
-  using word_of_int_Ex [where x=x] 
-        word_of_int_Ex [where x=y] 
-        word_of_int_Ex [where x=z]
-  by (auto simp: bwsimps bbw_assocs)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
   
 lemma word_bw_comms:
   fixes x :: "'a::len0 word"
@@ -2173,9 +2175,7 @@
   "x AND y = y AND x"
   "x OR y = y OR x"
   "x XOR y = y XOR x"
-  using word_of_int_Ex [where x=x] 
-        word_of_int_Ex [where x=y] 
-  by (auto simp: bwsimps bin_ops_comm)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
   
 lemma word_bw_lcs:
   fixes x :: "'a::len0 word"
@@ -2183,10 +2183,7 @@
   "y AND x AND z = x AND y AND z"
   "y OR x OR z = x OR y OR z"
   "y XOR x XOR z = x XOR y XOR z"
-  using word_of_int_Ex [where x=x] 
-        word_of_int_Ex [where x=y] 
-        word_of_int_Ex [where x=z]
-  by (auto simp: bwsimps)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_log_esimps [simp]:
   fixes x :: "'a::len0 word"
@@ -2203,17 +2200,14 @@
   "-1 OR x = -1"
   "0 XOR x = x"
   "-1 XOR x = NOT x"
-  using word_of_int_Ex [where x=x] 
-  by (auto simp: bwsimps)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_not_dist:
   fixes x :: "'a::len0 word"
   shows
   "NOT (x OR y) = NOT x AND NOT y"
   "NOT (x AND y) = NOT x OR NOT y"
-  using word_of_int_Ex [where x=x] 
-        word_of_int_Ex [where x=y] 
-  by (auto simp: bwsimps bbw_not_dist)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_bw_same:
   fixes x :: "'a::len0 word"
@@ -2221,8 +2215,7 @@
   "x AND x = x"
   "x OR x = x"
   "x XOR x = 0"
-  using word_of_int_Ex [where x=x] 
-  by (auto simp: bwsimps)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_ao_absorbs [simp]:
   fixes x :: "'a::len0 word"
@@ -2235,30 +2228,21 @@
   "x OR x AND y = x"
   "(x OR y) AND x = x"
   "x AND y OR x = x"
-  using word_of_int_Ex [where x=x] 
-        word_of_int_Ex [where x=y] 
-  by (auto simp: bwsimps)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_not_not [simp]:
   "NOT NOT (x::'a::len0 word) = x"
-  using word_of_int_Ex [where x=x] 
-  by (auto simp: bwsimps)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_ao_dist:
   fixes x :: "'a::len0 word"
   shows "(x OR y) AND z = x AND z OR y AND z"
-  using word_of_int_Ex [where x=x] 
-        word_of_int_Ex [where x=y] 
-        word_of_int_Ex [where x=z]   
-  by (auto simp: bwsimps bbw_ao_dist)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_oa_dist:
   fixes x :: "'a::len0 word"
   shows "x AND y OR z = (x OR z) AND (y OR z)"
-  using word_of_int_Ex [where x=x] 
-        word_of_int_Ex [where x=y] 
-        word_of_int_Ex [where x=z]   
-  by (auto simp: bwsimps bbw_oa_dist)
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_add_not [simp]: 
   fixes x :: "'a::len0 word"
@@ -2328,15 +2312,13 @@
   by (simp add : sign_Min_lt_0 number_of_is_id)
 
 lemma word_msb_no [simp]:
-  "msb (number_of bin :: 'a::len word) = bin_nth bin (len_of TYPE('a) - 1)"
-  unfolding word_msb_def word_number_of_def
+  "msb (number_of w::'a::len word) = bin_nth (number_of w) (len_of TYPE('a) - 1)"
+  unfolding word_msb_def word_number_of_alt
   by (clarsimp simp add: word_sbin.eq_norm bin_sign_lem)
 
 lemma word_msb_nth:
   "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"
-  apply (rule trans [OF _ word_msb_no])
-  apply (simp add : word_number_of_def)
-  done
+  unfolding word_msb_def sint_uint by (simp add: bin_sign_lem)
 
 lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
   apply (unfold word_msb_nth uint_bl)
@@ -2442,19 +2424,6 @@
   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
   by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
 
-lemma test_bit_wi [simp]:
-  "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
-  unfolding word_test_bit_def
-  by (simp add: nth_bintr [symmetric] word_ubin.eq_norm)
-
-lemma test_bit_no [simp]:
-  "(number_of bin :: 'a::len0 word) !! n \<equiv> n < len_of TYPE('a) \<and> bin_nth bin n"
-  unfolding word_test_bit_def word_number_of_def word_size
-  by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
-
-lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
-  unfolding test_bit_no word_0_no by auto
-
 lemma nth_sint: 
   fixes w :: "'a::len word"
   defines "l \<equiv> len_of TYPE ('a)"
@@ -2463,7 +2432,7 @@
   by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
 
 lemma word_lsb_no [simp]:
-  "lsb (number_of bin :: 'a :: len word) = (bin_last bin = 1)"
+  "lsb (number_of bin :: 'a :: len word) = (bin_last (number_of bin) = 1)"
   unfolding word_lsb_alt test_bit_no by auto
 
 lemma word_set_no [simp]:
@@ -2928,15 +2897,15 @@
 
 lemma shiftr_no': 
   "w = number_of bin \<Longrightarrow> 
-  (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))"
+  (w::'a::len0 word) >> n = word_of_int ((bin_rest ^^ n) (bintrunc (size w) (number_of bin)))"
   apply clarsimp
   apply (rule word_eqI)
   apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
   done
 
 lemma sshiftr_no': 
-  "w = number_of bin \<Longrightarrow> w >>> n = number_of ((bin_rest ^^ n) 
-    (sbintrunc (size w - 1) bin))"
+  "w = number_of bin \<Longrightarrow> w >>> n = word_of_int ((bin_rest ^^ n) 
+    (sbintrunc (size w - 1) (number_of bin)))"
   apply clarsimp
   apply (rule word_eqI)
   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
@@ -3042,7 +3011,7 @@
 lemma mask_bl: "mask n = of_bl (replicate n True)"
   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
 
-lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
+lemma mask_bin: "mask n = word_of_int (bintrunc n -1)"
   by (auto simp add: nth_bintr word_size intro: word_eqI)
 
 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
@@ -3051,11 +3020,11 @@
   apply (auto simp add: test_bit_bin)
   done
 
-lemma and_mask_no: "number_of i AND mask n = number_of (bintrunc n i)" 
-  by (auto simp add : nth_bintr word_size word_ops_nth_size intro: word_eqI)
-
 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
-  by (fact and_mask_no [unfolded word_number_of_def])
+  by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
+
+lemma and_mask_no: "number_of i AND mask n = word_of_int (bintrunc n (number_of i))"
+  unfolding word_number_of_alt by (rule and_mask_wi)
 
 lemma bl_and_mask':
   "to_bl (w AND mask n :: 'a :: len word) = 
@@ -3152,7 +3121,7 @@
   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
-  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
+  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
 
 lemma mask_power_eq:
   "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
@@ -3448,7 +3417,7 @@
   "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
   apply (unfold of_bl_def)
   apply (simp add: bl_to_bin_app_cat bin_cat_num)
-  apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
+  apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
   done
 
 lemma of_bl_False [simp]:
@@ -3769,7 +3738,7 @@
   apply (clarsimp simp add : word_size)
   apply (rule nth_equalityI, assumption)
   apply clarsimp
-  apply (rule word_eqI)
+  apply (rule word_eqI [rule_format])
   apply (rule trans)
    apply (rule test_bit_rsplit_alt)
      apply (clarsimp simp: word_size)+
@@ -4141,7 +4110,7 @@
 declare word_roti_def [simp]
 
 
-subsection {* Miscellaneous  *}
+subsection {* Maximum machine word *}
 
 lemma word_int_cases:
   "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
@@ -4460,6 +4429,8 @@
   apply (case_tac "1+n = 0", auto)
   done
 
+subsection {* Recursion combinator for words *}
+
 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
   "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
 
@@ -4568,7 +4539,7 @@
 
 
 lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
-  by (fact word_1_no [symmetric, unfolded BIT_simps])
+  by (fact word_1_no [symmetric])
 
 lemma word_no_0 [simp]: "(Numeral0::'a::len0 word) = 0"
   by (fact word_0_no [symmetric])