src/HOL/Num.thy

   apply (rule_tac a=x in add_right_imp_eq)
   apply (simp add: add_assoc minus_add_cancel)
   apply (simp add: add_assoc [symmetric], simp add: add_assoc)
   apply (rule_tac a=x in add_left_imp_eq)
   apply (rule_tac a=x in add_right_imp_eq)
-  apply (simp add: add_assoc minus_add_cancel add_minus_cancel)
+  apply (simp add: add_assoc)
   apply (simp add: add_assoc, simp add: add_assoc [symmetric])
   done
 
 lemma is_num_add_left_commute:
   "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + (y + z) = y + (x + z)"
   by (simp only: add_assoc [symmetric] is_num_add_commute)
 
 lemmas is_num_normalize =
   add_assoc is_num_add_commute is_num_add_left_commute
   is_num.intros is_num_numeral
-  diff_minus minus_add add_minus_cancel minus_add_cancel
+  minus_add
 
 definition dbl :: "'a \<Rightarrow> 'a" where "dbl x = x + x"
 definition dbl_inc :: "'a \<Rightarrow> 'a" where "dbl_inc x = x + x + 1"
 definition dbl_dec :: "'a \<Rightarrow> 'a" where "dbl_dec x = x + x - 1"
 

 lemma dbl_simps [simp]:
   "dbl (neg_numeral k) = neg_numeral (Bit0 k)"
   "dbl 0 = 0"
   "dbl 1 = 2"
   "dbl (numeral k) = numeral (Bit0 k)"
-  unfolding dbl_def neg_numeral_def numeral.simps
-  by (simp_all add: minus_add)
+  by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
 
 lemma dbl_inc_simps [simp]:
   "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
   "dbl_inc 0 = 1"
   "dbl_inc 1 = 3"
   "dbl_inc (numeral k) = numeral (Bit1 k)"
-  unfolding dbl_inc_def neg_numeral_def numeral.simps numeral_BitM
-  by (simp_all add: is_num_normalize)
+  by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
 
 lemma dbl_dec_simps [simp]:
   "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
   "dbl_dec 0 = -1"
   "dbl_dec 1 = 1"
   "dbl_dec (numeral k) = numeral (BitM k)"
-  unfolding dbl_dec_def neg_numeral_def numeral.simps numeral_BitM
-  by (simp_all add: is_num_normalize)
+  by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
 
 lemma sub_num_simps [simp]:
   "sub One One = 0"
   "sub One (Bit0 l) = neg_numeral (BitM l)"
   "sub One (Bit1 l) = neg_numeral (Bit0 l)"

   "sub (Bit1 k) One = numeral (Bit0 k)"
   "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
   "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
   "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
   "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
-  unfolding dbl_def dbl_dec_def dbl_inc_def sub_def
-  unfolding neg_numeral_def numeral.simps numeral_BitM
-  by (simp_all add: is_num_normalize)
+  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
+    numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 lemma add_neg_numeral_simps:
   "numeral m + neg_numeral n = sub m n"
   "neg_numeral m + numeral n = sub n m"
   "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
-  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
-  by (simp_all add: is_num_normalize)
+  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
+    del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 lemma add_neg_numeral_special:
   "1 + neg_numeral m = sub One m"
   "neg_numeral m + 1 = sub One m"
-  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
-  by (simp_all add: is_num_normalize)
+  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
 
 lemma diff_numeral_simps:
   "numeral m - numeral n = sub m n"
   "numeral m - neg_numeral n = numeral (m + n)"
   "neg_numeral m - numeral n = neg_numeral (m + n)"
   "neg_numeral m - neg_numeral n = sub n m"
-  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
-  by (simp_all add: is_num_normalize)
+  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
+    del: add_uminus_conv_diff add: diff_conv_add_uminus)
 
 lemma diff_numeral_special:
   "1 - numeral n = sub One n"
   "1 - neg_numeral n = numeral (One + n)"
   "numeral m - 1 = sub m One"
   "neg_numeral m - 1 = neg_numeral (m + One)"
-  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
-  by (simp_all add: is_num_normalize)
+  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
 
 lemma minus_one: "- 1 = -1"
   unfolding neg_numeral_def numeral.simps ..
 
 lemma minus_numeral: "- numeral n = neg_numeral n"