# HG changeset patch
# User huffman
# Date 1333098995 -7200
# Node ID 501b9bbd0d6e6ef55bda12ab21e6dd1a3caa90aa
# Parent  4d0878d54ca5d688ea780428c0ca42fa5f3a9b0e
removed redundant nat-specific copies of theorems

diff -r 4d0878d54ca5 -r 501b9bbd0d6e NEWS
--- 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:
diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/Divides.thy
--- 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 -
diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/Library/Code_Integer.thy
--- 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`)
diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/Library/Formal_Power_Series.thy
--- 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)}
diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/Library/Target_Numeral.thy
--- 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
diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/NSA/HSeries.thy
--- 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  
diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/Nat_Numeral.thy
--- 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)