--- a/NEWS Fri Mar 30 10:41:27 2012 +0200
+++ b/NEWS Fri Mar 30 11:16:35 2012 +0200
@@ -162,6 +162,9 @@
mod_mult_distrib ~> mult_mod_left
mod_mult_distrib2 ~> mult_mod_right
+* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
+generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
+
* More default pred/set conversions on a couple of relation operations
and predicates. Added powers of predicate relations.
Consolidation of some relation theorems:
--- a/src/HOL/Divides.thy Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/Divides.thy Fri Mar 30 11:16:35 2012 +0200
@@ -1086,7 +1086,7 @@
by (simp add: numeral_2_eq_2 le_mod_geq)
lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: nat_mult_2 [symmetric])
+by (simp add: mult_2 [symmetric])
lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
proof -
--- a/src/HOL/Library/Code_Integer.thy Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy Fri Mar 30 11:16:35 2012 +0200
@@ -22,7 +22,7 @@
proof -
have "2 = nat 2" by simp
show ?thesis
- apply (subst nat_mult_2 [symmetric])
+ apply (subst mult_2 [symmetric])
apply (auto simp add: Let_def divmod_int_mod_div not_le
nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
apply (unfold `2 = nat 2`)
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Mar 30 11:16:35 2012 +0200
@@ -2781,7 +2781,7 @@
lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
using binomial_Vandermonde[of n n n,symmetric]
- unfolding nat_mult_2 apply (simp add: power2_eq_square)
+ unfolding mult_2 apply (simp add: power2_eq_square)
apply (rule setsum_cong2)
by (auto intro: binomial_symmetric)
@@ -3139,7 +3139,7 @@
moreover
{assume on: "odd n"
from on obtain m where m: "n = 2*m + 1"
- unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2)
+ unfolding odd_nat_equiv_def2 by (auto simp add: mult_2)
have "?l $n = ?r$n"
by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
power_mult power_minus)}
--- a/src/HOL/Library/Target_Numeral.thy Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy Fri Mar 30 11:16:35 2012 +0200
@@ -385,7 +385,7 @@
by simp
then have "num_of_nat (nat (int_of k)) =
num_of_nat (nat (int_of k) div 2 + nat (int_of k) div 2 + nat (int_of k) mod 2)"
- by (simp add: nat_mult_2)
+ by (simp add: mult_2)
with ** have "num_of_nat (nat (int_of k)) =
num_of_nat (nat (int_of k) div 2 + nat (int_of k) div 2 + 1)"
by simp
@@ -395,7 +395,7 @@
by (auto simp add: num_of_int_def nat_of_def Let_def prod_case_beta
not_le Target_Numeral.int_eq_iff less_eq_int_def
nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
- nat_mult_2 aux add_One)
+ mult_2 [where 'a=nat] aux add_One)
qed
hide_const (open) int_of nat_of Pos Neg sub dup divmod_abs num_of_int
--- a/src/HOL/NSA/HSeries.thy Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/NSA/HSeries.thy Fri Mar 30 11:16:35 2012 +0200
@@ -114,7 +114,7 @@
lemma sumhr_minus_one_realpow_zero [simp]:
"!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
unfolding sumhr_app
-by transfer (simp del: power_Suc add: nat_mult_2 [symmetric])
+by transfer (simp del: power_Suc add: mult_2 [symmetric])
lemma sumhr_interval_const:
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
--- a/src/HOL/Nat_Numeral.thy Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy Fri Mar 30 11:16:35 2012 +0200
@@ -114,13 +114,6 @@
text {*Evens and Odds, for Mutilated Chess Board*}
-text{*Lemmas for specialist use, NOT as default simprules*}
-lemma nat_mult_2: "2 * z = (z+z::nat)"
-by (rule mult_2) (* FIXME: duplicate *)
-
-lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (rule mult_2_right) (* FIXME: duplicate *)
-
text{*Case analysis on @{term "n<2"}*}
lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
by (auto simp add: numeral_2_eq_2)