# 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 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 \ hypreal"})) *} @@ -496,9 +496,9 @@ "\n. 1 pow n = (1::'a::monoid_mult star)" by transfer (rule power_one) -lemma hrabs_hyperpow_minus_one [simp]: - "\n. abs(-1 pow n) = (1::'a::{linordered_idom} star)" -by transfer (rule abs_power_minus_one) +lemma hrabs_hyperpow_minus [simp]: + "\(a::'a::{linordered_idom} star) n. abs((-a) pow n) = abs (a pow n)" +by transfer (rule abs_power_minus) lemma hyperpow_mult: "\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 \ 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)