1.1 --- a/src/HOL/Word/Bit_Int.thy	Tue Dec 27 13:16:22 2011 +0100
     1.2 +++ b/src/HOL/Word/Bit_Int.thy	Tue Dec 27 15:37:33 2011 +0100
     1.3 @@ -471,11 +471,7 @@
     1.4  subsection {* Splitting and concatenation *}
     1.5  
     1.6  definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
     1.7 -  "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
     1.8 -
     1.9 -lemma [code]:
    1.10    "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
    1.11 -  by (simp add: bin_rcat_def Pls_def)
    1.12  
    1.13  fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    1.14    "bin_rsplit_aux n m c bs =
    1.15 @@ -536,7 +532,7 @@
    1.16    done
    1.17  
    1.18  lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
    1.19 -  by (induct n arbitrary: w) (auto simp: Int.Pls_def)
    1.20 +  by (induct n arbitrary: w) auto
    1.21  
    1.22  lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w"
    1.23    unfolding Pls_def by (rule bin_cat_zero)
    1.24 @@ -570,7 +566,7 @@
    1.25    by (induct n arbitrary: w) auto
    1.26  
    1.27  lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
    1.28 -  by (induct n) (auto simp: Int.Pls_def)
    1.29 +  by (induct n) auto
    1.30  
    1.31  lemma bin_split_Pls [simp]:
    1.32    "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
    1.33 @@ -586,7 +582,7 @@
    1.34    apply (induct n arbitrary: m b c, clarsimp)
    1.35    apply (simp add: bin_rest_trunc Let_def split: ls_splits)
    1.36    apply (case_tac m)
    1.37 -   apply (auto simp: Let_def BIT_simps split: ls_splits)
    1.38 +   apply (auto simp: Let_def split: ls_splits)
    1.39    done
    1.40  
    1.41  lemma bin_split_trunc1:
    1.42 @@ -595,13 +591,13 @@
    1.43    apply (induct n arbitrary: m b c, clarsimp)
    1.44    apply (simp add: bin_rest_trunc Let_def split: ls_splits)
    1.45    apply (case_tac m)
    1.46 -   apply (auto simp: Let_def BIT_simps split: ls_splits)
    1.47 +   apply (auto simp: Let_def split: ls_splits)
    1.48    done
    1.49  
    1.50  lemma bin_cat_num:
    1.51    "bin_cat a n b = a * 2 ^ n + bintrunc n b"
    1.52    apply (induct n arbitrary: b, clarsimp)
    1.53 -  apply (simp add: Bit_def cong: number_of_False_cong)
    1.54 +  apply (simp add: Bit_def)
    1.55    done
    1.56  
    1.57  lemma bin_split_num:

     2.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 13:16:22 2011 +0100
     2.2 +++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 15:37:33 2011 +0100
     2.3 @@ -326,28 +326,19 @@
     2.4    by (cases w rule: bin_exhaust) auto
     2.5  
     2.6  primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where
     2.7 -  Z : "bintrunc 0 bin = Int.Pls"
     2.8 +  Z : "bintrunc 0 bin = 0"
     2.9  | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
    2.10  
    2.11  primrec sbintrunc :: "nat => int => int" where
    2.12 -  Z : "sbintrunc 0 bin = 
    2.13 -    (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)"
    2.14 +  Z : "sbintrunc 0 bin = (case bin_last bin of (1::bit) \<Rightarrow> -1 | (0::bit) \<Rightarrow> 0)"
    2.15  | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
    2.16  
    2.17 -lemma [code]:
    2.18 -  "sbintrunc 0 bin = 
    2.19 -    (case bin_last bin of (1::bit) => - 1 | (0::bit) => 0)"
    2.20 -  "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
    2.21 -  apply simp_all
    2.22 -  apply (simp only: Pls_def Min_def)
    2.23 -  done
    2.24 -
    2.25 -lemma sign_bintr: "bin_sign (bintrunc n w) = Int.Pls"
    2.26 +lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
    2.27    by (induct n arbitrary: w) auto
    2.28  
    2.29  lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)"
    2.30    apply (induct n arbitrary: w)
    2.31 -  apply (simp add: Pls_def)
    2.32 +  apply simp
    2.33    apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
    2.34    done
    2.35  
    2.36 @@ -356,10 +347,8 @@
    2.37     apply clarsimp
    2.38     apply (subst mod_add_left_eq)
    2.39     apply (simp add: bin_last_def)
    2.40 -   apply (simp add: number_of_eq)
    2.41 -  apply (simp add: Pls_def)
    2.42 -  apply (simp add: bin_last_def bin_rest_def Bit_def 
    2.43 -              cong: number_of_False_cong)
    2.44 +  apply simp
    2.45 +  apply (simp add: bin_last_def bin_rest_def Bit_def)
    2.46    apply (clarsimp simp: mod_mult_mult1 [symmetric] 
    2.47           zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
    2.48    apply (rule trans [symmetric, OF _ emep1])
    2.49 @@ -370,13 +359,13 @@
    2.50  subsection "Simplifications for (s)bintrunc"
    2.51  
    2.52  lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
    2.53 -  by (induct n) (auto simp add: Int.Pls_def)
    2.54 +  by (induct n) auto
    2.55  
    2.56  lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
    2.57 -  by (induct n) (auto simp add: Int.Pls_def)
    2.58 +  by (induct n) auto
    2.59  
    2.60  lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
    2.61 -  by (induct n) (auto, simp add: number_of_is_id)
    2.62 +  by (induct n) auto
    2.63  
    2.64  lemma bintrunc_Suc_numeral:
    2.65    "bintrunc (Suc n) 1 = 1"
    2.66 @@ -389,7 +378,7 @@
    2.67    "sbintrunc 0 1 = -1"
    2.68    "sbintrunc 0 (number_of (Int.Bit0 w)) = 0"
    2.69    "sbintrunc 0 (number_of (Int.Bit1 w)) = -1"
    2.70 -  by (simp_all, unfold Pls_def number_of_is_id, simp_all)
    2.71 +  by simp_all
    2.72  
    2.73  lemma sbintrunc_Suc_numeral:
    2.74    "sbintrunc (Suc n) 1 = 1"
    2.75 @@ -403,7 +392,7 @@
    2.76  
    2.77  lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
    2.78  
    2.79 -lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
    2.80 +lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
    2.81    apply (induct n arbitrary: bin)
    2.82     apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
    2.83    done
    2.84 @@ -516,10 +505,10 @@
    2.85    sbintrunc.Z [where bin="w BIT (1::bit)", 
    2.86                 simplified bin_last_simps bin_rest_simps bit.simps] for w
    2.87  
    2.88 -lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
    2.89 +lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = 0"
    2.90    using sbintrunc_0_BIT_B0 by simp
    2.91  
    2.92 -lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
    2.93 +lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = -1"
    2.94    using sbintrunc_0_BIT_B1 by simp
    2.95  
    2.96  lemmas sbintrunc_0_simps =
    2.97 @@ -544,12 +533,12 @@
    2.98  
    2.99  lemma bintrunc_n_Pls [simp]:
   2.100    "bintrunc n Int.Pls = Int.Pls"
   2.101 -  by (induct n) (auto simp: BIT_simps)
   2.102 +  unfolding Pls_def by simp
   2.103  
   2.104  lemma sbintrunc_n_PM [simp]:
   2.105    "sbintrunc n Int.Pls = Int.Pls"
   2.106    "sbintrunc n Int.Min = Int.Min"
   2.107 -  by (induct n) (auto simp: BIT_simps)
   2.108 +  unfolding Pls_def Min_def by simp_all
   2.109  
   2.110  lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
   2.111  
   2.112 @@ -823,7 +812,7 @@
   2.113  subsection {* Splitting and concatenation *}
   2.114  
   2.115  primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
   2.116 -  Z: "bin_split 0 w = (w, Int.Pls)"
   2.117 +  Z: "bin_split 0 w = (w, 0)"
   2.118    | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
   2.119          in (w1, w2 BIT bin_last w))"
   2.120  

     3.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 13:16:22 2011 +0100
     3.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 15:37:33 2011 +0100
     3.3 @@ -20,11 +20,7 @@
     3.4        bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
     3.5  
     3.6  definition bl_to_bin :: "bool list \<Rightarrow> int" where
     3.7 -  bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
     3.8 -
     3.9 -lemma [code]:
    3.10 -  "bl_to_bin bs = bl_to_bin_aux bs 0"
    3.11 -  by (simp add: bl_to_bin_def Pls_def)
    3.12 +  bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
    3.13  
    3.14  primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
    3.15    Z: "bin_to_bl_aux 0 w bl = bl"
    3.16 @@ -89,6 +85,11 @@
    3.17    "(butlast ^^ n) bl = take (length bl - n) bl"
    3.18    by (induct n) (auto simp: butlast_take)
    3.19  
    3.20 +lemma bin_to_bl_aux_zero_minus_simp [simp]:
    3.21 +  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = 
    3.22 +    bin_to_bl_aux (n - 1) 0 (False # bl)"
    3.23 +  by (cases n) auto
    3.24 +
    3.25  lemma bin_to_bl_aux_Pls_minus_simp [simp]:
    3.26    "0 < n ==> bin_to_bl_aux n Int.Pls bl = 
    3.27      bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
    3.28 @@ -178,11 +179,15 @@
    3.29    done
    3.30  
    3.31  lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
    3.32 -  unfolding bl_to_bin_def by (auto simp: BIT_simps)
    3.33 +  unfolding bl_to_bin_def by auto
    3.34  
    3.35 -lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = Int.Pls"
    3.36 +lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
    3.37    unfolding bl_to_bin_def by auto
    3.38  
    3.39 +lemma bin_to_bl_zero_aux: 
    3.40 +  "bin_to_bl_aux n 0 bl = replicate n False @ bl"
    3.41 +  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
    3.42 +
    3.43  lemma bin_to_bl_Pls_aux: 
    3.44    "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
    3.45    by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
    3.46 @@ -199,7 +204,7 @@
    3.47  
    3.48  lemma bl_to_bin_rep_F: 
    3.49    "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
    3.50 -  apply (simp add: bin_to_bl_Pls_aux [symmetric] bin_bl_bin')
    3.51 +  apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
    3.52    apply (simp add: bl_to_bin_def)
    3.53    done
    3.54  
    3.55 @@ -214,7 +219,7 @@
    3.56     apply clarsimp
    3.57    apply clarsimp
    3.58    apply (case_tac "m")
    3.59 -   apply (clarsimp simp: bin_to_bl_Pls_aux) 
    3.60 +   apply (clarsimp simp: bin_to_bl_zero_aux) 
    3.61     apply (erule thin_rl)
    3.62     apply (induct_tac n)   
    3.63      apply auto
    3.64 @@ -225,7 +230,7 @@
    3.65      replicate (n - m) False @ bin_to_bl (min n m) bin"
    3.66    unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
    3.67  
    3.68 -lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
    3.69 +lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
    3.70    by (induct n) auto
    3.71  
    3.72  lemma len_bin_to_bl_aux: 
    3.73 @@ -239,12 +244,12 @@
    3.74    "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
    3.75    by (induct bs arbitrary: w) auto
    3.76    
    3.77 -lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls"
    3.78 +lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
    3.79    unfolding bl_to_bin_def by (simp add : sign_bl_bin')
    3.80    
    3.81  lemma bl_sbin_sign_aux: 
    3.82    "hd (bin_to_bl_aux (Suc n) w bs) = 
    3.83 -    (bin_sign (sbintrunc n w) = Int.Min)"
    3.84 +    (bin_sign (sbintrunc n w) = -1)"
    3.85    apply (induct n arbitrary: w bs)
    3.86     apply clarsimp
    3.87     apply (cases w rule: bin_exhaust)
    3.88 @@ -253,7 +258,7 @@
    3.89    done
    3.90      
    3.91  lemma bl_sbin_sign: 
    3.92 -  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
    3.93 +  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
    3.94    unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
    3.95  
    3.96  lemma bin_nth_of_bl_aux:
    3.97 @@ -654,7 +659,7 @@
    3.98  
    3.99  lemma bl_to_bin_aux_alt:
   3.100    "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
   3.101 -  using bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls"]
   3.102 +  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
   3.103    unfolding bl_to_bin_def [symmetric] by simp
   3.104  
   3.105  lemma bin_to_bl_cat:
   3.106 @@ -685,7 +690,7 @@
   3.107      Int.succ (bl_to_bin (replicate n True))"
   3.108    apply (unfold bl_to_bin_def)
   3.109    apply (induct n)
   3.110 -   apply (simp add: BIT_simps)
   3.111 +   apply (simp add: Int.succ_def)
   3.112    apply (simp only: Suc_eq_plus1 replicate_add
   3.113                      append_Cons [symmetric] bl_to_bin_aux_append)
   3.114    apply (simp add: BIT_simps)

     4.1 --- a/src/HOL/Word/Word.thy	Tue Dec 27 13:16:22 2011 +0100
     4.2 +++ b/src/HOL/Word/Word.thy	Tue Dec 27 15:37:33 2011 +0100
     4.3 @@ -377,16 +377,12 @@
     4.4  
     4.5  definition
     4.6    word_msb_def: 
     4.7 -  "msb a \<longleftrightarrow> bin_sign (sint a) = Int.Min"
     4.8 +  "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
     4.9  
    4.10  instance ..
    4.11  
    4.12  end
    4.13  
    4.14 -lemma [code]:
    4.15 -  "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
    4.16 -  by (simp only: word_msb_def Min_def)
    4.17 -
    4.18  definition setBit :: "'a :: len0 word => nat => 'a word" where 
    4.19    "setBit w n = set_bit w n True"
    4.20  
    4.21 @@ -552,19 +548,17 @@
    4.22  
    4.23  lemma uint_bintrunc [simp]:
    4.24    "uint (number_of bin :: 'a word) =
    4.25 -    number_of (bintrunc (len_of TYPE ('a :: len0)) bin)"
    4.26 -  unfolding word_number_of_def number_of_eq
    4.27 -  by (auto intro: word_ubin.eq_norm) 
    4.28 +    bintrunc (len_of TYPE ('a :: len0)) (number_of bin)"
    4.29 +  unfolding word_number_of_alt by (rule word_ubin.eq_norm)
    4.30  
    4.31  lemma sint_sbintrunc [simp]:
    4.32    "sint (number_of bin :: 'a word) =
    4.33 -    number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" 
    4.34 -  unfolding word_number_of_def number_of_eq
    4.35 -  by (subst word_sbin.eq_norm) simp
    4.36 +    sbintrunc (len_of TYPE ('a :: len) - 1) (number_of bin)"
    4.37 +  unfolding word_number_of_alt by (rule word_sbin.eq_norm)
    4.38  
    4.39  lemma unat_bintrunc [simp]:
    4.40    "unat (number_of bin :: 'a :: len0 word) =
    4.41 -    number_of (bintrunc (len_of TYPE('a)) bin)"
    4.42 +    nat (bintrunc (len_of TYPE('a)) (number_of bin))"
    4.43    unfolding unat_def nat_number_of_def 
    4.44    by (simp only: uint_bintrunc)
    4.45  
    4.46 @@ -638,7 +632,7 @@
    4.47  
    4.48  lemma word_of_int_bin [simp] : 
    4.49    "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)"
    4.50 -  unfolding word_number_of_alt by auto
    4.51 +  unfolding word_number_of_alt ..
    4.52  
    4.53  lemma word_int_case_wi: 
    4.54    "word_int_case f (word_of_int i :: 'b word) = 
    4.55 @@ -774,7 +768,7 @@
    4.56  lemma length_bl_neq_0 [iff]: "length (to_bl (x::'a::len word)) \<noteq> 0"
    4.57    by (fact length_bl_gt_0 [THEN gr_implies_not0])
    4.58  
    4.59 -lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Int.Min)"
    4.60 +lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
    4.61    apply (unfold to_bl_def sint_uint)
    4.62    apply (rule trans [OF _ bl_sbin_sign])
    4.63    apply simp
    4.64 @@ -890,14 +884,14 @@
    4.65  
    4.66  (* for literal u(s)cast *)
    4.67  
    4.68 -lemma ucast_bintr [simp]: 
    4.69 +lemma ucast_bintr [simp]:
    4.70    "ucast (number_of w ::'a::len0 word) = 
    4.71 -   number_of (bintrunc (len_of TYPE('a)) w)"
    4.72 +   word_of_int (bintrunc (len_of TYPE('a)) (number_of w))"
    4.73    unfolding ucast_def by simp
    4.74  
    4.75 -lemma scast_sbintr [simp]: 
    4.76 +lemma scast_sbintr [simp]:
    4.77    "scast (number_of w ::'a::len word) = 
    4.78 -   number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)"
    4.79 +   word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (number_of w))"
    4.80    unfolding scast_def by simp
    4.81  
    4.82  lemmas source_size = source_size_def [unfolded Let_def word_size]
    4.83 @@ -1698,7 +1692,7 @@
    4.84  
    4.85  lemma iszero_word_no [simp] : 
    4.86    "iszero (number_of bin :: 'a :: len word) = 
    4.87 -    iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
    4.88 +    iszero (bintrunc (len_of TYPE('a)) (number_of bin))"
    4.89    apply (simp add: zero_bintrunc number_of_is_id)
    4.90    apply (unfold iszero_def Pls_def)
    4.91    apply (rule refl)
    4.92 @@ -2447,7 +2441,12 @@
    4.93    assumes "m ~= n"
    4.94    shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
    4.95    by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
    4.96 -    
    4.97 +
    4.98 +lemma test_bit_wi [simp]:
    4.99 +  "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
   4.100 +  unfolding word_test_bit_def
   4.101 +  by (simp add: nth_bintr [symmetric] word_ubin.eq_norm)
   4.102 +
   4.103  lemma test_bit_no [simp]:
   4.104    "(number_of bin :: 'a::len0 word) !! n \<equiv> n < len_of TYPE('a) \<and> bin_nth bin n"
   4.105    unfolding word_test_bit_def word_number_of_def word_size
   4.106 @@ -2469,19 +2468,18 @@
   4.107  
   4.108  lemma word_set_no [simp]:
   4.109    "set_bit (number_of bin::'a::len0 word) n b = 
   4.110 -    number_of (bin_sc n (if b then 1 else 0) bin)"
   4.111 -  apply (unfold word_set_bit_def word_number_of_def [symmetric])
   4.112 +    word_of_int (bin_sc n (if b then 1 else 0) (number_of bin))"
   4.113 +  unfolding word_set_bit_def
   4.114    apply (rule word_eqI)
   4.115 -  apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id 
   4.116 -                        nth_bintr)
   4.117 +  apply (simp add: word_size bin_nth_sc_gen nth_bintr)
   4.118    done
   4.119  
   4.120  lemma setBit_no [simp]:
   4.121 -  "setBit (number_of bin) n = number_of (bin_sc n 1 bin) "
   4.122 +  "setBit (number_of bin) n = word_of_int (bin_sc n 1 (number_of bin))"
   4.123    by (simp add: setBit_def)
   4.124  
   4.125  lemma clearBit_no [simp]:
   4.126 -  "clearBit (number_of bin) n = number_of (bin_sc n 0 bin)"
   4.127 +  "clearBit (number_of bin) n = word_of_int (bin_sc n 0 (number_of bin))"
   4.128    by (simp add: clearBit_def)
   4.129  
   4.130  lemma to_bl_n1: 
   4.131 @@ -2529,11 +2527,11 @@
   4.132    apply (case_tac "nat")
   4.133     apply clarsimp
   4.134     apply (case_tac "n")
   4.135 -    apply (clarsimp simp add : word_1_wi [symmetric])
   4.136 -   apply (clarsimp simp add : word_0_wi [symmetric] BIT_simps)
   4.137 +    apply clarsimp
   4.138 +   apply clarsimp
   4.139    apply (drule word_gt_0 [THEN iffD1])
   4.140    apply (safe intro!: word_eqI bin_nth_lem ext)
   4.141 -     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric] BIT_simps)
   4.142 +     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
   4.143    done
   4.144  
   4.145  lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
   4.146 @@ -2545,7 +2543,7 @@
   4.147     apply (rule box_equals) 
   4.148       apply (rule_tac [2] bintr_ariths (1))+ 
   4.149     apply (clarsimp simp add : number_of_is_id)
   4.150 -  apply (simp add: BIT_simps)
   4.151 +  apply simp
   4.152    done
   4.153  
   4.154  lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
   4.155 @@ -2577,24 +2575,26 @@
   4.156  
   4.157  subsection {* Shifting, Rotating, and Splitting Words *}
   4.158  
   4.159 -lemma shiftl1_number [simp] :
   4.160 -  "shiftl1 (number_of w) = number_of (w BIT 0)"
   4.161 -  apply (unfold shiftl1_def word_number_of_def)
   4.162 -  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
   4.163 -              del: BIT_simps)
   4.164 +lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT 0)"
   4.165 +  unfolding shiftl1_def
   4.166 +  apply (simp only: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
   4.167    apply (subst refl [THEN bintrunc_BIT_I, symmetric])
   4.168    apply (subst bintrunc_bintrunc_min)
   4.169    apply simp
   4.170    done
   4.171  
   4.172 +lemma shiftl1_number [simp] :
   4.173 +  "shiftl1 (number_of w) = number_of (Int.Bit0 w)"
   4.174 +  unfolding word_number_of_alt shiftl1_wi by simp
   4.175 +
   4.176  lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
   4.177 -  unfolding word_0_no shiftl1_number by (auto simp: BIT_simps)
   4.178 -
   4.179 -lemma shiftl1_def_u: "shiftl1 w = number_of (uint w BIT 0)"
   4.180 -  by (simp only: word_number_of_def shiftl1_def)
   4.181 -
   4.182 -lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
   4.183 -  by (rule trans [OF _ shiftl1_number]) simp
   4.184 +  unfolding shiftl1_def by simp
   4.185 +
   4.186 +lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT 0)"
   4.187 +  by (simp only: shiftl1_def) (* FIXME: duplicate *)
   4.188 +
   4.189 +lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT 0)"
   4.190 +  unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
   4.191  
   4.192  lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
   4.193    unfolding shiftr1_def by simp
   4.194 @@ -2603,7 +2603,7 @@
   4.195    unfolding sshiftr1_def by simp
   4.196  
   4.197  lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
   4.198 -  unfolding sshiftr1_def by auto
   4.199 +  unfolding sshiftr1_def by simp
   4.200  
   4.201  lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
   4.202    unfolding shiftl_def by (induct n) auto
   4.203 @@ -2741,8 +2741,7 @@
   4.204    unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
   4.205  
   4.206  lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
   4.207 -  unfolding uint_bl of_bl_no 
   4.208 -  by (simp add: bl_to_bin_aux_append bl_to_bin_def)
   4.209 +  by (simp add: of_bl_def bl_to_bin_append)
   4.210  
   4.211  lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
   4.212  proof -
   4.213 @@ -2906,16 +2905,10 @@
   4.214  (* note - the following results use 'a :: len word < number_ring *)
   4.215  
   4.216  lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
   4.217 -  apply (simp add: shiftl1_def_u BIT_simps)
   4.218 -  apply (simp only:  double_number_of_Bit0 [symmetric])
   4.219 -  apply simp
   4.220 -  done
   4.221 +  by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
   4.222  
   4.223  lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
   4.224 -  apply (simp add: shiftl1_def_u BIT_simps)
   4.225 -  apply (simp only: double_number_of_Bit0 [symmetric])
   4.226 -  apply simp
   4.227 -  done
   4.228 +  by (simp add: shiftl1_2t)
   4.229  
   4.230  lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   4.231    unfolding shiftl_def 
   4.232 @@ -3052,7 +3045,7 @@
   4.233  lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
   4.234    by (auto simp add: nth_bintr word_size intro: word_eqI)
   4.235  
   4.236 -lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
   4.237 +lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
   4.238    apply (rule word_eqI)
   4.239    apply (simp add: nth_bintr word_size word_ops_nth_size)
   4.240    apply (auto simp add: test_bit_bin)
   4.241 @@ -3076,10 +3069,11 @@
   4.242    done
   4.243  
   4.244  lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
   4.245 -  by (fact and_mask_bintr [unfolded word_number_of_alt no_bintr_alt])
   4.246 +  by (simp only: and_mask_bintr bintrunc_mod2p)
   4.247  
   4.248  lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
   4.249 -  apply (simp add : and_mask_bintr no_bintr_alt)
   4.250 +  apply (simp add: and_mask_bintr word_ubin.eq_norm)
   4.251 +  apply (simp add: bintrunc_mod2p)
   4.252    apply (rule xtr8)
   4.253     prefer 2
   4.254     apply (rule pos_mod_bound)
   4.255 @@ -3496,7 +3490,7 @@
   4.256    apply (unfold word_size)
   4.257    apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
   4.258     defer
   4.259 -   apply (simp add: word_0_wi_Pls)
   4.260 +   apply simp
   4.261    apply (simp add : of_bl_def to_bl_def)
   4.262    apply (subst bin_split_take1 [symmetric])
   4.263      prefer 2
   4.264 @@ -4586,7 +4580,4 @@
   4.265  
   4.266  setup {* SMT_Word.setup *}
   4.267  
   4.268 -text {* Legacy simp rules *}
   4.269 -declare BIT_simps [simp]
   4.270 -
   4.271  end