src/HOL/Num.thy
changeset 54230 b1d955791529
parent 53064 7e3f39bc41df
child 54249 ce00f2fef556
     1.1 --- a/src/HOL/Num.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Num.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -407,7 +407,7 @@
     1.4    apply (simp add: add_assoc [symmetric], simp add: add_assoc)
     1.5    apply (rule_tac a=x in add_left_imp_eq)
     1.6    apply (rule_tac a=x in add_right_imp_eq)
     1.7 -  apply (simp add: add_assoc minus_add_cancel add_minus_cancel)
     1.8 +  apply (simp add: add_assoc)
     1.9    apply (simp add: add_assoc, simp add: add_assoc [symmetric])
    1.10    done
    1.11  
    1.12 @@ -418,7 +418,7 @@
    1.13  lemmas is_num_normalize =
    1.14    add_assoc is_num_add_commute is_num_add_left_commute
    1.15    is_num.intros is_num_numeral
    1.16 -  diff_minus minus_add add_minus_cancel minus_add_cancel
    1.17 +  minus_add
    1.18  
    1.19  definition dbl :: "'a \<Rightarrow> 'a" where "dbl x = x + x"
    1.20  definition dbl_inc :: "'a \<Rightarrow> 'a" where "dbl_inc x = x + x + 1"
    1.21 @@ -435,24 +435,21 @@
    1.22    "dbl 0 = 0"
    1.23    "dbl 1 = 2"
    1.24    "dbl (numeral k) = numeral (Bit0 k)"
    1.25 -  unfolding dbl_def neg_numeral_def numeral.simps
    1.26 -  by (simp_all add: minus_add)
    1.27 +  by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
    1.28  
    1.29  lemma dbl_inc_simps [simp]:
    1.30    "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
    1.31    "dbl_inc 0 = 1"
    1.32    "dbl_inc 1 = 3"
    1.33    "dbl_inc (numeral k) = numeral (Bit1 k)"
    1.34 -  unfolding dbl_inc_def neg_numeral_def numeral.simps numeral_BitM
    1.35 -  by (simp_all add: is_num_normalize)
    1.36 +  by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
    1.37  
    1.38  lemma dbl_dec_simps [simp]:
    1.39    "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
    1.40    "dbl_dec 0 = -1"
    1.41    "dbl_dec 1 = 1"
    1.42    "dbl_dec (numeral k) = numeral (BitM k)"
    1.43 -  unfolding dbl_dec_def neg_numeral_def numeral.simps numeral_BitM
    1.44 -  by (simp_all add: is_num_normalize)
    1.45 +  by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
    1.46  
    1.47  lemma sub_num_simps [simp]:
    1.48    "sub One One = 0"
    1.49 @@ -464,38 +461,35 @@
    1.50    "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
    1.51    "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
    1.52    "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
    1.53 -  unfolding dbl_def dbl_dec_def dbl_inc_def sub_def
    1.54 -  unfolding neg_numeral_def numeral.simps numeral_BitM
    1.55 -  by (simp_all add: is_num_normalize)
    1.56 +  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
    1.57 +    numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
    1.58  
    1.59  lemma add_neg_numeral_simps:
    1.60    "numeral m + neg_numeral n = sub m n"
    1.61    "neg_numeral m + numeral n = sub n m"
    1.62    "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
    1.63 -  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
    1.64 -  by (simp_all add: is_num_normalize)
    1.65 +  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
    1.66 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
    1.67  
    1.68  lemma add_neg_numeral_special:
    1.69    "1 + neg_numeral m = sub One m"
    1.70    "neg_numeral m + 1 = sub One m"
    1.71 -  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
    1.72 -  by (simp_all add: is_num_normalize)
    1.73 +  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
    1.74  
    1.75  lemma diff_numeral_simps:
    1.76    "numeral m - numeral n = sub m n"
    1.77    "numeral m - neg_numeral n = numeral (m + n)"
    1.78    "neg_numeral m - numeral n = neg_numeral (m + n)"
    1.79    "neg_numeral m - neg_numeral n = sub n m"
    1.80 -  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
    1.81 -  by (simp_all add: is_num_normalize)
    1.82 +  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
    1.83 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
    1.84  
    1.85  lemma diff_numeral_special:
    1.86    "1 - numeral n = sub One n"
    1.87    "1 - neg_numeral n = numeral (One + n)"
    1.88    "numeral m - 1 = sub m One"
    1.89    "neg_numeral m - 1 = neg_numeral (m + One)"
    1.90 -  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
    1.91 -  by (simp_all add: is_num_normalize)
    1.92 +  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
    1.93  
    1.94  lemma minus_one: "- 1 = -1"
    1.95    unfolding neg_numeral_def numeral.simps ..