1.1 --- a/src/HOL/Word/Bit_Int.thy	Fri Dec 23 15:24:22 2011 +0100
     1.2 +++ b/src/HOL/Word/Bit_Int.thy	Fri Dec 23 15:34:18 2011 +0100
     1.3 @@ -535,8 +535,11 @@
     1.4    apply (case_tac m, auto)
     1.5    done
     1.6  
     1.7 +lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
     1.8 +  by (induct n arbitrary: w) (auto simp: Int.Pls_def)
     1.9 +
    1.10  lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w"
    1.11 -  by (induct n arbitrary: w) auto
    1.12 +  unfolding Pls_def by (rule bin_cat_zero)
    1.13  
    1.14  lemma bintr_cat1: 
    1.15    "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
    1.16 @@ -566,9 +569,12 @@
    1.17    "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
    1.18    by (induct n arbitrary: w) auto
    1.19  
    1.20 +lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
    1.21 +  by (induct n) (auto simp: Int.Pls_def)
    1.22 +
    1.23  lemma bin_split_Pls [simp]:
    1.24    "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
    1.25 -  by (induct n) (auto simp: Let_def BIT_simps split: ls_splits)
    1.26 +  unfolding Pls_def by (rule bin_split_zero)
    1.27  
    1.28  lemma bin_split_Min [simp]:
    1.29    "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"