# HG changeset patch
# User huffman
# Date 1324996653 -3600
# Node ID 0b562d564d5f6d1241473a4425ed63b874065bb6
# Parent  871bdab23f5c9d36dd3510ac68d45cc72ba13a2c
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min

diff -r 871bdab23f5c -r 0b562d564d5f src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Tue Dec 27 13:16:22 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Tue Dec 27 15:37:33 2011 +0100
@@ -471,11 +471,7 @@
 subsection {* Splitting and concatenation *}
 
 definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
-  "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
-
-lemma [code]:
   "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
-  by (simp add: bin_rcat_def Pls_def)
 
 fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   "bin_rsplit_aux n m c bs =
@@ -536,7 +532,7 @@
   done
 
 lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
-  by (induct n arbitrary: w) (auto simp: Int.Pls_def)
+  by (induct n arbitrary: w) auto
 
 lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w"
   unfolding Pls_def by (rule bin_cat_zero)
@@ -570,7 +566,7 @@
   by (induct n arbitrary: w) auto
 
 lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
-  by (induct n) (auto simp: Int.Pls_def)
+  by (induct n) auto
 
 lemma bin_split_Pls [simp]:
   "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
@@ -586,7 +582,7 @@
   apply (induct n arbitrary: m b c, clarsimp)
   apply (simp add: bin_rest_trunc Let_def split: ls_splits)
   apply (case_tac m)
-   apply (auto simp: Let_def BIT_simps split: ls_splits)
+   apply (auto simp: Let_def split: ls_splits)
   done
 
 lemma bin_split_trunc1:
@@ -595,13 +591,13 @@
   apply (induct n arbitrary: m b c, clarsimp)
   apply (simp add: bin_rest_trunc Let_def split: ls_splits)
   apply (case_tac m)
-   apply (auto simp: Let_def BIT_simps split: ls_splits)
+   apply (auto simp: Let_def split: ls_splits)
   done
 
 lemma bin_cat_num:
   "bin_cat a n b = a * 2 ^ n + bintrunc n b"
   apply (induct n arbitrary: b, clarsimp)
-  apply (simp add: Bit_def cong: number_of_False_cong)
+  apply (simp add: Bit_def)
   done
 
 lemma bin_split_num:
diff -r 871bdab23f5c -r 0b562d564d5f src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 13:16:22 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 15:37:33 2011 +0100
@@ -326,28 +326,19 @@
   by (cases w rule: bin_exhaust) auto
 
 primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where
-  Z : "bintrunc 0 bin = Int.Pls"
+  Z : "bintrunc 0 bin = 0"
 | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
 
 primrec sbintrunc :: "nat => int => int" where
-  Z : "sbintrunc 0 bin = 
-    (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)"
+  Z : "sbintrunc 0 bin = (case bin_last bin of (1::bit) \<Rightarrow> -1 | (0::bit) \<Rightarrow> 0)"
 | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
 
-lemma [code]:
-  "sbintrunc 0 bin = 
-    (case bin_last bin of (1::bit) => - 1 | (0::bit) => 0)"
-  "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
-  apply simp_all
-  apply (simp only: Pls_def Min_def)
-  done
-
-lemma sign_bintr: "bin_sign (bintrunc n w) = Int.Pls"
+lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
   by (induct n arbitrary: w) auto
 
 lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)"
   apply (induct n arbitrary: w)
-  apply (simp add: Pls_def)
+  apply simp
   apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
   done
 
@@ -356,10 +347,8 @@
    apply clarsimp
    apply (subst mod_add_left_eq)
    apply (simp add: bin_last_def)
-   apply (simp add: number_of_eq)
-  apply (simp add: Pls_def)
-  apply (simp add: bin_last_def bin_rest_def Bit_def 
-              cong: number_of_False_cong)
+  apply simp
+  apply (simp add: bin_last_def bin_rest_def Bit_def)
   apply (clarsimp simp: mod_mult_mult1 [symmetric] 
          zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   apply (rule trans [symmetric, OF _ emep1])
@@ -370,13 +359,13 @@
 subsection "Simplifications for (s)bintrunc"
 
 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
-  by (induct n) (auto simp add: Int.Pls_def)
+  by (induct n) auto
 
 lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
-  by (induct n) (auto simp add: Int.Pls_def)
+  by (induct n) auto
 
 lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
-  by (induct n) (auto, simp add: number_of_is_id)
+  by (induct n) auto
 
 lemma bintrunc_Suc_numeral:
   "bintrunc (Suc n) 1 = 1"
@@ -389,7 +378,7 @@
   "sbintrunc 0 1 = -1"
   "sbintrunc 0 (number_of (Int.Bit0 w)) = 0"
   "sbintrunc 0 (number_of (Int.Bit1 w)) = -1"
-  by (simp_all, unfold Pls_def number_of_is_id, simp_all)
+  by simp_all
 
 lemma sbintrunc_Suc_numeral:
   "sbintrunc (Suc n) 1 = 1"
@@ -403,7 +392,7 @@
 
 lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
 
-lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
+lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
   apply (induct n arbitrary: bin)
    apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
   done
@@ -516,10 +505,10 @@
   sbintrunc.Z [where bin="w BIT (1::bit)", 
                simplified bin_last_simps bin_rest_simps bit.simps] for w
 
-lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
+lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = 0"
   using sbintrunc_0_BIT_B0 by simp
 
-lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
+lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = -1"
   using sbintrunc_0_BIT_B1 by simp
 
 lemmas sbintrunc_0_simps =
@@ -544,12 +533,12 @@
 
 lemma bintrunc_n_Pls [simp]:
   "bintrunc n Int.Pls = Int.Pls"
-  by (induct n) (auto simp: BIT_simps)
+  unfolding Pls_def by simp
 
 lemma sbintrunc_n_PM [simp]:
   "sbintrunc n Int.Pls = Int.Pls"
   "sbintrunc n Int.Min = Int.Min"
-  by (induct n) (auto simp: BIT_simps)
+  unfolding Pls_def Min_def by simp_all
 
 lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
 
@@ -823,7 +812,7 @@
 subsection {* Splitting and concatenation *}
 
 primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
-  Z: "bin_split 0 w = (w, Int.Pls)"
+  Z: "bin_split 0 w = (w, 0)"
   | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
         in (w1, w2 BIT bin_last w))"
 
diff -r 871bdab23f5c -r 0b562d564d5f src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 13:16:22 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 15:37:33 2011 +0100
@@ -20,11 +20,7 @@
       bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
 
 definition bl_to_bin :: "bool list \<Rightarrow> int" where
-  bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
-
-lemma [code]:
-  "bl_to_bin bs = bl_to_bin_aux bs 0"
-  by (simp add: bl_to_bin_def Pls_def)
+  bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
 
 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
   Z: "bin_to_bl_aux 0 w bl = bl"
@@ -89,6 +85,11 @@
   "(butlast ^^ n) bl = take (length bl - n) bl"
   by (induct n) (auto simp: butlast_take)
 
+lemma bin_to_bl_aux_zero_minus_simp [simp]:
+  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = 
+    bin_to_bl_aux (n - 1) 0 (False # bl)"
+  by (cases n) auto
+
 lemma bin_to_bl_aux_Pls_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n Int.Pls bl = 
     bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
@@ -178,11 +179,15 @@
   done
 
 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
-  unfolding bl_to_bin_def by (auto simp: BIT_simps)
+  unfolding bl_to_bin_def by auto
 
-lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = Int.Pls"
+lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
   unfolding bl_to_bin_def by auto
 
+lemma bin_to_bl_zero_aux: 
+  "bin_to_bl_aux n 0 bl = replicate n False @ bl"
+  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
+
 lemma bin_to_bl_Pls_aux: 
   "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
@@ -199,7 +204,7 @@
 
 lemma bl_to_bin_rep_F: 
   "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
-  apply (simp add: bin_to_bl_Pls_aux [symmetric] bin_bl_bin')
+  apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
   apply (simp add: bl_to_bin_def)
   done
 
@@ -214,7 +219,7 @@
    apply clarsimp
   apply clarsimp
   apply (case_tac "m")
-   apply (clarsimp simp: bin_to_bl_Pls_aux) 
+   apply (clarsimp simp: bin_to_bl_zero_aux) 
    apply (erule thin_rl)
    apply (induct_tac n)   
     apply auto
@@ -225,7 +230,7 @@
     replicate (n - m) False @ bin_to_bl (min n m) bin"
   unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
 
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
+lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
   by (induct n) auto
 
 lemma len_bin_to_bl_aux: 
@@ -239,12 +244,12 @@
   "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
   by (induct bs arbitrary: w) auto
   
-lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls"
+lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
   unfolding bl_to_bin_def by (simp add : sign_bl_bin')
   
 lemma bl_sbin_sign_aux: 
   "hd (bin_to_bl_aux (Suc n) w bs) = 
-    (bin_sign (sbintrunc n w) = Int.Min)"
+    (bin_sign (sbintrunc n w) = -1)"
   apply (induct n arbitrary: w bs)
    apply clarsimp
    apply (cases w rule: bin_exhaust)
@@ -253,7 +258,7 @@
   done
     
 lemma bl_sbin_sign: 
-  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
+  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
 
 lemma bin_nth_of_bl_aux:
@@ -654,7 +659,7 @@
 
 lemma bl_to_bin_aux_alt:
   "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
-  using bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls"]
+  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
   unfolding bl_to_bin_def [symmetric] by simp
 
 lemma bin_to_bl_cat:
@@ -685,7 +690,7 @@
     Int.succ (bl_to_bin (replicate n True))"
   apply (unfold bl_to_bin_def)
   apply (induct n)
-   apply (simp add: BIT_simps)
+   apply (simp add: Int.succ_def)
   apply (simp only: Suc_eq_plus1 replicate_add
                     append_Cons [symmetric] bl_to_bin_aux_append)
   apply (simp add: BIT_simps)
diff -r 871bdab23f5c -r 0b562d564d5f src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Dec 27 13:16:22 2011 +0100
+++ b/src/HOL/Word/Word.thy	Tue Dec 27 15:37:33 2011 +0100
@@ -377,16 +377,12 @@
 
 definition
   word_msb_def: 
-  "msb a \<longleftrightarrow> bin_sign (sint a) = Int.Min"
+  "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
 
 instance ..
 
 end
 
-lemma [code]:
-  "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
-  by (simp only: word_msb_def Min_def)
-
 definition setBit :: "'a :: len0 word => nat => 'a word" where 
   "setBit w n = set_bit w n True"
 
@@ -552,19 +548,17 @@
 
 lemma uint_bintrunc [simp]:
   "uint (number_of bin :: 'a word) =
-    number_of (bintrunc (len_of TYPE ('a :: len0)) bin)"
-  unfolding word_number_of_def number_of_eq
-  by (auto intro: word_ubin.eq_norm) 
+    bintrunc (len_of TYPE ('a :: len0)) (number_of bin)"
+  unfolding word_number_of_alt by (rule word_ubin.eq_norm)
 
 lemma sint_sbintrunc [simp]:
   "sint (number_of bin :: 'a word) =
-    number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" 
-  unfolding word_number_of_def number_of_eq
-  by (subst word_sbin.eq_norm) simp
+    sbintrunc (len_of TYPE ('a :: len) - 1) (number_of bin)"
+  unfolding word_number_of_alt by (rule word_sbin.eq_norm)
 
 lemma unat_bintrunc [simp]:
   "unat (number_of bin :: 'a :: len0 word) =
-    number_of (bintrunc (len_of TYPE('a)) bin)"
+    nat (bintrunc (len_of TYPE('a)) (number_of bin))"
   unfolding unat_def nat_number_of_def 
   by (simp only: uint_bintrunc)
 
@@ -638,7 +632,7 @@
 
 lemma word_of_int_bin [simp] : 
   "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)"
-  unfolding word_number_of_alt by auto
+  unfolding word_number_of_alt ..
 
 lemma word_int_case_wi: 
   "word_int_case f (word_of_int i :: 'b word) = 
@@ -774,7 +768,7 @@
 lemma length_bl_neq_0 [iff]: "length (to_bl (x::'a::len word)) \<noteq> 0"
   by (fact length_bl_gt_0 [THEN gr_implies_not0])
 
-lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Int.Min)"
+lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
   apply (unfold to_bl_def sint_uint)
   apply (rule trans [OF _ bl_sbin_sign])
   apply simp
@@ -890,14 +884,14 @@
 
 (* for literal u(s)cast *)
 
-lemma ucast_bintr [simp]: 
+lemma ucast_bintr [simp]:
   "ucast (number_of w ::'a::len0 word) = 
-   number_of (bintrunc (len_of TYPE('a)) w)"
+   word_of_int (bintrunc (len_of TYPE('a)) (number_of w))"
   unfolding ucast_def by simp
 
-lemma scast_sbintr [simp]: 
+lemma scast_sbintr [simp]:
   "scast (number_of w ::'a::len word) = 
-   number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)"
+   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]
@@ -1698,7 +1692,7 @@
 
 lemma iszero_word_no [simp] : 
   "iszero (number_of bin :: 'a :: len word) = 
-    iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
+    iszero (bintrunc (len_of TYPE('a)) (number_of bin))"
   apply (simp add: zero_bintrunc number_of_is_id)
   apply (unfold iszero_def Pls_def)
   apply (rule refl)
@@ -2447,7 +2441,12 @@
   assumes "m ~= n"
   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
@@ -2469,19 +2468,18 @@
 
 lemma word_set_no [simp]:
   "set_bit (number_of bin::'a::len0 word) n b = 
-    number_of (bin_sc n (if b then 1 else 0) bin)"
-  apply (unfold word_set_bit_def word_number_of_def [symmetric])
+    word_of_int (bin_sc n (if b then 1 else 0) (number_of bin))"
+  unfolding word_set_bit_def
   apply (rule word_eqI)
-  apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id 
-                        nth_bintr)
+  apply (simp add: word_size bin_nth_sc_gen nth_bintr)
   done
 
 lemma setBit_no [simp]:
-  "setBit (number_of bin) n = number_of (bin_sc n 1 bin) "
+  "setBit (number_of bin) n = word_of_int (bin_sc n 1 (number_of bin))"
   by (simp add: setBit_def)
 
 lemma clearBit_no [simp]:
-  "clearBit (number_of bin) n = number_of (bin_sc n 0 bin)"
+  "clearBit (number_of bin) n = word_of_int (bin_sc n 0 (number_of bin))"
   by (simp add: clearBit_def)
 
 lemma to_bl_n1: 
@@ -2529,11 +2527,11 @@
   apply (case_tac "nat")
    apply clarsimp
    apply (case_tac "n")
-    apply (clarsimp simp add : word_1_wi [symmetric])
-   apply (clarsimp simp add : word_0_wi [symmetric] BIT_simps)
+    apply clarsimp
+   apply clarsimp
   apply (drule word_gt_0 [THEN iffD1])
   apply (safe intro!: word_eqI bin_nth_lem ext)
-     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric] BIT_simps)
+     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
   done
 
 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
@@ -2545,7 +2543,7 @@
    apply (rule box_equals) 
      apply (rule_tac [2] bintr_ariths (1))+ 
    apply (clarsimp simp add : number_of_is_id)
-  apply (simp add: BIT_simps)
+  apply simp
   done
 
 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
@@ -2577,24 +2575,26 @@
 
 subsection {* Shifting, Rotating, and Splitting Words *}
 
-lemma shiftl1_number [simp] :
-  "shiftl1 (number_of w) = number_of (w BIT 0)"
-  apply (unfold shiftl1_def word_number_of_def)
-  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
-              del: BIT_simps)
+lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT 0)"
+  unfolding shiftl1_def
+  apply (simp only: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
   apply (subst bintrunc_bintrunc_min)
   apply simp
   done
 
+lemma shiftl1_number [simp] :
+  "shiftl1 (number_of w) = number_of (Int.Bit0 w)"
+  unfolding word_number_of_alt shiftl1_wi by simp
+
 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
-  unfolding word_0_no shiftl1_number by (auto simp: BIT_simps)
-
-lemma shiftl1_def_u: "shiftl1 w = number_of (uint w BIT 0)"
-  by (simp only: word_number_of_def shiftl1_def)
-
-lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
-  by (rule trans [OF _ shiftl1_number]) simp
+  unfolding shiftl1_def by simp
+
+lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT 0)"
+  by (simp only: shiftl1_def) (* FIXME: duplicate *)
+
+lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT 0)"
+  unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
 
 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
   unfolding shiftr1_def by simp
@@ -2603,7 +2603,7 @@
   unfolding sshiftr1_def by simp
 
 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
-  unfolding sshiftr1_def by auto
+  unfolding sshiftr1_def by simp
 
 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
   unfolding shiftl_def by (induct n) auto
@@ -2741,8 +2741,7 @@
   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
 
 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
-  unfolding uint_bl of_bl_no 
-  by (simp add: bl_to_bin_aux_append bl_to_bin_def)
+  by (simp add: of_bl_def bl_to_bin_append)
 
 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
 proof -
@@ -2906,16 +2905,10 @@
 (* note - the following results use 'a :: len word < number_ring *)
 
 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
-  apply (simp add: shiftl1_def_u BIT_simps)
-  apply (simp only:  double_number_of_Bit0 [symmetric])
-  apply simp
-  done
+  by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
 
 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
-  apply (simp add: shiftl1_def_u BIT_simps)
-  apply (simp only: double_number_of_Bit0 [symmetric])
-  apply simp
-  done
+  by (simp add: shiftl1_2t)
 
 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   unfolding shiftl_def 
@@ -3052,7 +3045,7 @@
 lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
   by (auto simp add: nth_bintr word_size intro: word_eqI)
 
-lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
+lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
   apply (rule word_eqI)
   apply (simp add: nth_bintr word_size word_ops_nth_size)
   apply (auto simp add: test_bit_bin)
@@ -3076,10 +3069,11 @@
   done
 
 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
-  by (fact and_mask_bintr [unfolded word_number_of_alt no_bintr_alt])
+  by (simp only: and_mask_bintr bintrunc_mod2p)
 
 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
-  apply (simp add : and_mask_bintr no_bintr_alt)
+  apply (simp add: and_mask_bintr word_ubin.eq_norm)
+  apply (simp add: bintrunc_mod2p)
   apply (rule xtr8)
    prefer 2
    apply (rule pos_mod_bound)
@@ -3496,7 +3490,7 @@
   apply (unfold word_size)
   apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
    defer
-   apply (simp add: word_0_wi_Pls)
+   apply simp
   apply (simp add : of_bl_def to_bl_def)
   apply (subst bin_split_take1 [symmetric])
     prefer 2
@@ -4586,7 +4580,4 @@
 
 setup {* SMT_Word.setup *}
 
-text {* Legacy simp rules *}
-declare BIT_simps [simp]
-
 end