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.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)"])