1.1 --- a/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 11:24:54 2012 +0100
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 11:53:03 2012 +0100
     1.3 @@ -35,11 +35,11 @@
     1.4    using mod_div_equality [of w 2]
     1.5    by (cases "w mod 2 = 0", simp_all)
     1.6  
     1.7 -lemma bin_rest_BIT: "bin_rest (x BIT b) = x"
     1.8 +lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"
     1.9    unfolding bin_rest_def Bit_def
    1.10    by (cases b, simp_all)
    1.11  
    1.12 -lemma bin_last_BIT: "bin_last (x BIT b) = b"
    1.13 +lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b"
    1.14    unfolding bin_last_def Bit_def
    1.15    by (cases b, simp_all add: z1pmod2)
    1.16  
    1.17 @@ -209,7 +209,6 @@
    1.18    "bin_rest Int.Min = Int.Min"
    1.19    "bin_rest (Int.Bit0 w) = w"
    1.20    "bin_rest (Int.Bit1 w) = w"
    1.21 -  "bin_rest (w BIT b) = w"
    1.22    using bin_rl_simps bin_rl_def by auto
    1.23  
    1.24  lemma bin_last_simps [simp]: 
    1.25 @@ -217,30 +216,29 @@
    1.26    "bin_last Int.Min = (1::bit)"
    1.27    "bin_last (Int.Bit0 w) = (0::bit)"
    1.28    "bin_last (Int.Bit1 w) = (1::bit)"
    1.29 -  "bin_last (w BIT b) = b"
    1.30    using bin_rl_simps bin_rl_def by auto
    1.31  
    1.32  lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
    1.33 -  unfolding bin_rest_def [symmetric] by auto
    1.34 +  unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT)
    1.35  
    1.36  lemma bin_nth_lem [rule_format]:
    1.37    "ALL y. bin_nth x = bin_nth y --> x = y"
    1.38 -  apply (induct x rule: bin_induct)
    1.39 +  apply (induct x rule: bin_induct [unfolded Pls_def Min_def])
    1.40      apply safe
    1.41      apply (erule rev_mp)
    1.42 -    apply (induct_tac y rule: bin_induct)
    1.43 +    apply (induct_tac y rule: bin_induct [unfolded Pls_def Min_def])
    1.44        apply safe
    1.45        apply (drule_tac x=0 in fun_cong, force)
    1.46       apply (erule notE, rule ext, 
    1.47              drule_tac x="Suc x" in fun_cong, force)
    1.48 -    apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
    1.49 +    apply (drule_tac x=0 in fun_cong, force)
    1.50     apply (erule rev_mp)
    1.51 -   apply (induct_tac y rule: bin_induct)
    1.52 +   apply (induct_tac y rule: bin_induct [unfolded Pls_def Min_def])
    1.53       apply safe
    1.54       apply (drule_tac x=0 in fun_cong, force)
    1.55      apply (erule notE, rule ext, 
    1.56             drule_tac x="Suc x" in fun_cong, force)
    1.57 -   apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
    1.58 +   apply (drule_tac x=0 in fun_cong, force)
    1.59    apply (case_tac y rule: bin_exhaust)
    1.60    apply clarify
    1.61    apply (erule allE)
    1.62 @@ -453,7 +451,7 @@
    1.63    bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps]
    1.64  
    1.65  lemmas bintrunc_BIT  [simp] = 
    1.66 -  bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps] for w b
    1.67 +  bintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
    1.68  
    1.69  lemma bintrunc_Bit0 [simp]:
    1.70    "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
    1.71 @@ -474,7 +472,7 @@
    1.72    sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps]
    1.73  
    1.74  lemmas sbintrunc_Suc_BIT [simp] = 
    1.75 -  sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps] for w b
    1.76 +  sbintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
    1.77  
    1.78  lemma sbintrunc_Suc_Bit0 [simp]:
    1.79    "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"