1.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 11:38:55 2011 +0100
     1.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 12:05:03 2011 +0100
     1.3 @@ -132,14 +132,14 @@
     1.4    "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" 
     1.5    unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
     1.6  
     1.7 -lemma bin_to_bl_0: "bin_to_bl 0 bs = []"
     1.8 +lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
     1.9    unfolding bin_to_bl_def by auto
    1.10  
    1.11  lemma size_bin_to_bl_aux: 
    1.12    "size (bin_to_bl_aux n w bs) = n + length bs"
    1.13    by (induct n arbitrary: w bs) auto
    1.14  
    1.15 -lemma size_bin_to_bl: "size (bin_to_bl n w) = n" 
    1.16 +lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" 
    1.17    unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
    1.18  
    1.19  lemma bin_bl_bin': 
    1.20 @@ -147,7 +147,7 @@
    1.21      bl_to_bin_aux bs (bintrunc n w)"
    1.22    by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
    1.23  
    1.24 -lemma bin_bl_bin: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
    1.25 +lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
    1.26    unfolding bin_to_bl_def bin_bl_bin' by auto
    1.27  
    1.28  lemma bl_bin_bl':
    1.29 @@ -159,7 +159,7 @@
    1.30      apply (auto simp add : bin_to_bl_def)
    1.31    done
    1.32  
    1.33 -lemma bl_bin_bl: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
    1.34 +lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
    1.35    unfolding bl_to_bin_def
    1.36    apply (rule box_equals)
    1.37      apply (rule bl_bin_bl')
    1.38 @@ -168,12 +168,6 @@
    1.39    apply simp
    1.40    done
    1.41    
    1.42 -declare 
    1.43 -  bin_to_bl_0 [simp] 
    1.44 -  size_bin_to_bl [simp] 
    1.45 -  bin_bl_bin [simp] 
    1.46 -  bl_bin_bl [simp]
    1.47 -
    1.48  lemma bl_to_bin_inj:
    1.49    "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
    1.50    apply (rule_tac box_equals)
    1.51 @@ -183,10 +177,10 @@
    1.52    apply simp
    1.53    done
    1.54  
    1.55 -lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
    1.56 +lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
    1.57    unfolding bl_to_bin_def by (auto simp: BIT_simps)
    1.58 -  
    1.59 -lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
    1.60 +
    1.61 +lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = Int.Pls"
    1.62    unfolding bl_to_bin_def by auto
    1.63  
    1.64  lemma bin_to_bl_Pls_aux: 
    1.65 @@ -209,15 +203,10 @@
    1.66    apply (simp add: bl_to_bin_def)
    1.67    done
    1.68  
    1.69 -lemma bin_to_bl_trunc:
    1.70 +lemma bin_to_bl_trunc [simp]:
    1.71    "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
    1.72    by (auto intro: bl_to_bin_inj)
    1.73  
    1.74 -declare 
    1.75 -  bin_to_bl_trunc [simp] 
    1.76 -  bl_to_bin_False [simp] 
    1.77 -  bl_to_bin_Nil [simp]
    1.78 -
    1.79  lemma bin_to_bl_aux_bintr [rule_format] :
    1.80    "ALL m bin bl. bin_to_bl_aux n (bintrunc m bin) bl = 
    1.81      replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
    1.82 @@ -1036,8 +1025,6 @@
    1.83     in (w1, w2 BIT bin_last w))" 
    1.84    by (simp only: nobm1 bin_split_minus_simp)
    1.85  
    1.86 -declare bin_split_pred_simp [simp]
    1.87 -
    1.88  lemma bin_rsplit_aux_simp_alt:
    1.89    "bin_rsplit_aux n m c bs =
    1.90     (if m = 0 \<or> n = 0