src/HOL/Word/Word.thy
changeset 41550 efa734d9b221
parent 41413 64cd30d6b0b8
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/Word/Word.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -2171,7 +2171,7 @@
     1.4  
     1.5  lemma word_of_int_power_hom: 
     1.6    "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
     1.7 -  by (induct n) (simp_all add : word_of_int_hom_syms power_Suc)
     1.8 +  by (induct n) (simp_all add: word_of_int_hom_syms)
     1.9  
    1.10  lemma word_arith_power_alt: 
    1.11    "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
    1.12 @@ -2367,7 +2367,7 @@
    1.13    using word_of_int_Ex [where x=x] 
    1.14          word_of_int_Ex [where x=y] 
    1.15          word_of_int_Ex [where x=z]   
    1.16 -  by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm)
    1.17 +  by (auto simp: bwsimps bbw_ao_dist)
    1.18  
    1.19  lemma word_oa_dist:
    1.20    fixes x :: "'a::len0 word"
    1.21 @@ -2375,7 +2375,7 @@
    1.22    using word_of_int_Ex [where x=x] 
    1.23          word_of_int_Ex [where x=y] 
    1.24          word_of_int_Ex [where x=z]   
    1.25 -  by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm)
    1.26 +  by (auto simp: bwsimps bbw_oa_dist)
    1.27  
    1.28  lemma word_add_not [simp]: 
    1.29    fixes x :: "'a::len0 word"
    1.30 @@ -2571,7 +2571,7 @@
    1.31    fixes w :: "'a::len0 word"
    1.32    assumes "m ~= n"
    1.33    shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
    1.34 -  by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems)
    1.35 +  by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
    1.36      
    1.37  lemma test_bit_no': 
    1.38    fixes w :: "'a::len0 word"
    1.39 @@ -2623,7 +2623,7 @@
    1.40    done
    1.41  
    1.42  lemma word_msb_n1: "msb (-1::'a::len word)"
    1.43 -  unfolding word_msb_alt word_msb_alt to_bl_n1 by simp
    1.44 +  unfolding word_msb_alt to_bl_n1 by simp
    1.45  
    1.46  declare word_set_set_same [simp] word_set_nth [simp]
    1.47    test_bit_no [simp] word_set_no [simp] nth_0 [simp]
    1.48 @@ -3047,7 +3047,7 @@
    1.49  
    1.50  lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
    1.51    unfolding shiftl_def 
    1.52 -  by (induct n) (auto simp: shiftl1_2t power_Suc)
    1.53 +  by (induct n) (auto simp: shiftl1_2t)
    1.54  
    1.55  lemma shiftr1_bintr [simp]:
    1.56    "(shiftr1 (number_of w) :: 'a :: len0 word) = 
    1.57 @@ -3940,12 +3940,12 @@
    1.58       apply (clarsimp simp: word_size)+
    1.59    apply (rule trans)
    1.60    apply (rule test_bit_rcat [OF refl refl])
    1.61 -  apply (simp add : word_size msrevs)
    1.62 +  apply (simp add: word_size msrevs)
    1.63    apply (subst nth_rev)
    1.64     apply arith
    1.65 -  apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
    1.66 +  apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
    1.67    apply safe
    1.68 -  apply (simp add : diff_mult_distrib)
    1.69 +  apply (simp add: diff_mult_distrib)
    1.70    apply (rule mpl_lem)
    1.71    apply (cases "size ws")
    1.72     apply simp_all