# HG changeset patch
# User huffman
# Date 1393975572 28800
# Node ID d00023bd3554044dc85dc5f9654d048153718515
# Parent  0a756571c7a4bab8ff06eb3917f5d755a22a8ec9
remove simp rules made redundant by the replacement of neg_numeral with negated numerals

diff -r 0a756571c7a4 -r d00023bd3554 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Mar 04 14:14:28 2014 -0800
+++ b/src/HOL/Int.thy	Tue Mar 04 15:26:12 2014 -0800
@@ -766,13 +766,6 @@
   {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
 
 
-subsection{*Lemmas About Small Numerals*}
-
-lemma abs_power_minus_one [simp]:
-  "abs(-1 ^ n) = (1::'a::linordered_idom)"
-by (simp add: power_abs)
-
-
 subsection{*More Inequality Reasoning*}
 
 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
@@ -1226,9 +1219,6 @@
   unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
   by simp
 
-lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
-  by (fact divide_minus_left)
-
 lemma half_gt_zero_iff:
   "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
   by auto
diff -r 0a756571c7a4 -r d00023bd3554 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Tue Mar 04 14:14:28 2014 -0800
+++ b/src/HOL/NSA/HyperDef.thy	Tue Mar 04 15:26:12 2014 -0800
@@ -346,7 +346,7 @@
   K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
     @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
   #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
-      @{thm star_of_numeral}, @{thm star_of_neg_numeral}, @{thm star_of_add},
+      @{thm star_of_numeral}, @{thm star_of_add},
       @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
   #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
 *}
@@ -496,9 +496,9 @@
   "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
 by transfer (rule power_one)
 
-lemma hrabs_hyperpow_minus_one [simp]:
-  "\<And>n. abs(-1 pow n) = (1::'a::{linordered_idom} star)"
-by transfer (rule abs_power_minus_one)
+lemma hrabs_hyperpow_minus [simp]:
+  "\<And>(a::'a::{linordered_idom} star) n. abs((-a) pow n) = abs (a pow n)"
+by transfer (rule abs_power_minus)
 
 lemma hyperpow_mult:
   "\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n
diff -r 0a756571c7a4 -r d00023bd3554 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Mar 04 14:14:28 2014 -0800
+++ b/src/HOL/NSA/StarDef.thy	Tue Mar 04 15:26:12 2014 -0800
@@ -967,16 +967,6 @@
 lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k"
 by transfer (rule refl)
 
-lemma star_neg_numeral_def [transfer_unfold]:
-  "- numeral k = star_of (- numeral k)"
-by (simp only: star_of_minus star_of_numeral)
-
-lemma Standard_neg_numeral [simp]: "- numeral k \<in> Standard"
-  using star_neg_numeral_def [of k] by simp
-
-lemma star_of_neg_numeral [simp]: "star_of (- numeral k) = - numeral k"
-by transfer (rule refl)
-
 lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
 by (induct n, simp_all)