--- a/src/HOL/Num.thy Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Num.thy Fri Nov 01 18:51:14 2013 +0100
@@ -407,7 +407,7 @@
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
@@ -418,7 +418,7 @@
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"
@@ -435,24 +435,21 @@
"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"
@@ -464,38 +461,35 @@
"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 ..