src/HOL/Int.thy
changeset 54230 b1d955791529
parent 54223 85705ba18add
child 54249 ce00f2fef556
     1.1 --- a/src/HOL/Int.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Int.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -220,7 +220,7 @@
     1.4    by (transfer fixing: uminus) clarsimp
     1.5  
     1.6  lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
     1.7 -by (simp add: diff_minus Groups.diff_minus)
     1.8 +  using of_int_add [of w "- z"] by simp
     1.9  
    1.10  lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
    1.11    by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
    1.12 @@ -749,7 +749,7 @@
    1.13  
    1.14  lemmas int_arith_rules =
    1.15    neg_le_iff_le numeral_One
    1.16 -  minus_zero diff_minus left_minus right_minus
    1.17 +  minus_zero left_minus right_minus
    1.18    mult_zero_left mult_zero_right mult_1_left mult_1_right
    1.19    mult_minus_left mult_minus_right
    1.20    minus_add_distrib minus_minus mult_assoc
    1.21 @@ -793,7 +793,6 @@
    1.22  subsection{*The functions @{term nat} and @{term int}*}
    1.23  
    1.24  text{*Simplify the term @{term "w + - z"}*}
    1.25 -lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp]
    1.26  
    1.27  lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
    1.28  apply (insert zless_nat_conj [of 1 z])
    1.29 @@ -1510,10 +1509,13 @@
    1.30    "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
    1.31    "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
    1.32    "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
    1.33 -  unfolding sub_def dup_def numeral.simps Pos_def Neg_def
    1.34 -    neg_numeral_def numeral_BitM
    1.35 -  by (simp_all only: algebra_simps)
    1.36 -
    1.37 +  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def
    1.38 +    neg_numeral_def numeral_BitM)
    1.39 +  apply (simp_all only: algebra_simps minus_diff_eq)
    1.40 +  apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
    1.41 +  apply (simp_all only: minus_add add.assoc left_minus)
    1.42 +  apply (simp_all only: algebra_simps right_minus)
    1.43 +  done
    1.44  
    1.45  text {* Implementations *}
    1.46