1.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 16:46:43 2012 +0100
     1.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 16:53:59 2012 +0100
     1.3 @@ -743,26 +743,43 @@
     1.4  lemmas rbl_Nils =
     1.5    rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
     1.6  
     1.7 -lemma rbl_pred: 
     1.8 -  "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.pred bin))"
     1.9 -  apply (induct n, simp)
    1.10 +lemma pred_BIT_simps [simp]:
    1.11 +  "x BIT 0 - 1 = (x - 1) BIT 1"
    1.12 +  "x BIT 1 - 1 = x BIT 0"
    1.13 +  by (simp_all add: Bit_B0_2t Bit_B1_2t)
    1.14 +
    1.15 +lemma rbl_pred:
    1.16 +  "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
    1.17 +  apply (induct n arbitrary: bin, simp)
    1.18    apply (unfold bin_to_bl_def)
    1.19    apply clarsimp
    1.20    apply (case_tac bin rule: bin_exhaust)
    1.21    apply (case_tac b)
    1.22 -   apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
    1.23 +   apply (clarsimp simp: bin_to_bl_aux_alt)+
    1.24    done
    1.25  
    1.26 +lemma succ_BIT_simps [simp]:
    1.27 +  "x BIT 0 + 1 = x BIT 1"
    1.28 +  "x BIT 1 + 1 = (x + 1) BIT 0"
    1.29 +  by (simp_all add: Bit_B0_2t Bit_B1_2t)
    1.30 +
    1.31  lemma rbl_succ: 
    1.32 -  "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.succ bin))"
    1.33 -  apply (induct n, simp)
    1.34 +  "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
    1.35 +  apply (induct n arbitrary: bin, simp)
    1.36    apply (unfold bin_to_bl_def)
    1.37    apply clarsimp
    1.38    apply (case_tac bin rule: bin_exhaust)
    1.39    apply (case_tac b)
    1.40 -   apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
    1.41 +   apply (clarsimp simp: bin_to_bl_aux_alt)+
    1.42    done
    1.43  
    1.44 +lemma add_BIT_simps [simp]: (* FIXME: move *)
    1.45 +  "x BIT 0 + y BIT 0 = (x + y) BIT 0"
    1.46 +  "x BIT 0 + y BIT 1 = (x + y) BIT 1"
    1.47 +  "x BIT 1 + y BIT 0 = (x + y) BIT 1"
    1.48 +  "x BIT 1 + y BIT 1 = (x + y + 1) BIT 0"
    1.49 +  by (simp_all add: Bit_B0_2t Bit_B1_2t)
    1.50 +
    1.51  lemma rbl_add: 
    1.52    "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
    1.53      rev (bin_to_bl n (bina + binb))"
    1.54 @@ -773,7 +790,7 @@
    1.55    apply (case_tac binb rule: bin_exhaust)
    1.56    apply (case_tac b)
    1.57     apply (case_tac [!] "ba")
    1.58 -     apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac BIT_simps)
    1.59 +     apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac)
    1.60    done
    1.61  
    1.62  lemma rbl_add_app2: 
    1.63 @@ -847,7 +864,13 @@
    1.64    apply simp
    1.65    apply (simp add: bin_to_bl_aux_alt)
    1.66    done
    1.67 -  
    1.68 +
    1.69 +lemma mult_BIT_simps [simp]:
    1.70 +  "x BIT 0 * y = (x * y) BIT 0"
    1.71 +  "x * y BIT 0 = (x * y) BIT 0"
    1.72 +  "x BIT 1 * y = (x * y) BIT 0 + y"
    1.73 +  by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
    1.74 +
    1.75  lemma rbl_mult: "!!bina binb. 
    1.76      rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
    1.77      rev (bin_to_bl n (bina * binb))"
    1.78 @@ -859,8 +882,8 @@
    1.79    apply (case_tac binb rule: bin_exhaust)
    1.80    apply (case_tac b)
    1.81     apply (case_tac [!] "ba")
    1.82 -     apply (auto simp: bin_to_bl_aux_alt Let_def BIT_simps)
    1.83 -     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add BIT_simps)
    1.84 +     apply (auto simp: bin_to_bl_aux_alt Let_def)
    1.85 +     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
    1.86    done
    1.87  
    1.88  lemma rbl_add_split: