author huffman Fri, 30 Mar 2012 11:16:35 +0200 changeset 47217 501b9bbd0d6e parent 47216 4d0878d54ca5 child 47218 2b652cbadde1
removed redundant nat-specific copies of theorems
 NEWS file | annotate | diff | comparison | revisions src/HOL/Divides.thy file | annotate | diff | comparison | revisions src/HOL/Library/Code_Integer.thy file | annotate | diff | comparison | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions src/HOL/Library/Target_Numeral.thy file | annotate | diff | comparison | revisions src/HOL/NSA/HSeries.thy file | annotate | diff | comparison | revisions src/HOL/Nat_Numeral.thy file | annotate | diff | comparison | revisions
```--- 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 @@

lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"

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)"
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
+       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"