src/HOL/Num.thy
changeset 57512 cc97b347b301
parent 55974 c835a9379026
child 58112 8081087096ad
     1.1 --- a/src/HOL/Num.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -254,8 +254,8 @@
     1.4  lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
     1.5    apply (induct x)
     1.6    apply simp
     1.7 -  apply (simp add: add_assoc [symmetric], simp add: add_assoc)
     1.8 -  apply (simp add: add_assoc [symmetric], simp add: add_assoc)
     1.9 +  apply (simp add: add.assoc [symmetric], simp add: add.assoc)
    1.10 +  apply (simp add: add.assoc [symmetric], simp add: add.assoc)
    1.11    done
    1.12  
    1.13  lemma numeral_inc: "numeral (inc x) = numeral x + 1"
    1.14 @@ -264,7 +264,7 @@
    1.15    have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1"
    1.16      by (simp only: one_plus_numeral_commute)
    1.17    with Bit1 show ?case
    1.18 -    by (simp add: add_assoc)
    1.19 +    by (simp add: add.assoc)
    1.20  qed simp_all
    1.21  
    1.22  declare numeral.simps [simp del]
    1.23 @@ -350,7 +350,7 @@
    1.24  
    1.25  lemma numeral_add: "numeral (m + n) = numeral m + numeral n"
    1.26    by (induct n rule: num_induct)
    1.27 -     (simp_all only: numeral_One add_One add_inc numeral_inc add_assoc)
    1.28 +     (simp_all only: numeral_One add_One add_inc numeral_inc add.assoc)
    1.29  
    1.30  lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)"
    1.31    by (rule numeral_add [symmetric])
    1.32 @@ -397,20 +397,20 @@
    1.33    apply simp
    1.34    apply (rule_tac a=x in add_left_imp_eq)
    1.35    apply (rule_tac a=x in add_right_imp_eq)
    1.36 -  apply (simp add: add_assoc)
    1.37 -  apply (simp add: add_assoc [symmetric], simp add: add_assoc)
    1.38 +  apply (simp add: add.assoc)
    1.39 +  apply (simp add: add.assoc [symmetric], simp add: add.assoc)
    1.40    apply (rule_tac a=x in add_left_imp_eq)
    1.41    apply (rule_tac a=x in add_right_imp_eq)
    1.42 -  apply (simp add: add_assoc)
    1.43 -  apply (simp add: add_assoc, simp add: add_assoc [symmetric])
    1.44 +  apply (simp add: add.assoc)
    1.45 +  apply (simp add: add.assoc, simp add: add.assoc [symmetric])
    1.46    done
    1.47  
    1.48  lemma is_num_add_left_commute:
    1.49    "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + (y + z) = y + (x + z)"
    1.50 -  by (simp only: add_assoc [symmetric] is_num_add_commute)
    1.51 +  by (simp only: add.assoc [symmetric] is_num_add_commute)
    1.52  
    1.53  lemmas is_num_normalize =
    1.54 -  add_assoc is_num_add_commute is_num_add_left_commute
    1.55 +  add.assoc is_num_add_commute is_num_add_left_commute
    1.56    is_num.intros is_num_numeral
    1.57    minus_add
    1.58  
    1.59 @@ -1172,7 +1172,7 @@
    1.60    minus_zero left_minus right_minus
    1.61    mult_1_left mult_1_right
    1.62    mult_minus_left mult_minus_right
    1.63 -  minus_add_distrib minus_minus mult_assoc
    1.64 +  minus_add_distrib minus_minus mult.assoc
    1.65  
    1.66  lemmas of_nat_simps =
    1.67    of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    1.68 @@ -1225,20 +1225,20 @@
    1.69  
    1.70  lemma add_numeral_left [simp]:
    1.71    "numeral v + (numeral w + z) = (numeral(v + w) + z)"
    1.72 -  by (simp_all add: add_assoc [symmetric])
    1.73 +  by (simp_all add: add.assoc [symmetric])
    1.74  
    1.75  lemma add_neg_numeral_left [simp]:
    1.76    "numeral v + (- numeral w + y) = (sub v w + y)"
    1.77    "- numeral v + (numeral w + y) = (sub w v + y)"
    1.78    "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
    1.79 -  by (simp_all add: add_assoc [symmetric])
    1.80 +  by (simp_all add: add.assoc [symmetric])
    1.81  
    1.82  lemma mult_numeral_left [simp]:
    1.83    "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
    1.84    "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
    1.85    "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
    1.86    "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
    1.87 -  by (simp_all add: mult_assoc [symmetric])
    1.88 +  by (simp_all add: mult.assoc [symmetric])
    1.89  
    1.90  hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
    1.91