author huffman Tue Mar 04 15:26:12 2014 -0800 (2014-03-04) changeset 55911 d00023bd3554 parent 55910 0a756571c7a4 child 55912 e12a0ab9917c
remove simp rules made redundant by the replacement of neg_numeral with negated numerals
 src/HOL/Int.thy file | annotate | diff | revisions src/HOL/NSA/HyperDef.thy file | annotate | diff | revisions src/HOL/NSA/StarDef.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Int.thy	Tue Mar 04 14:14:28 2014 -0800
1.2 +++ b/src/HOL/Int.thy	Tue Mar 04 15:26:12 2014 -0800
1.3 @@ -766,13 +766,6 @@
1.4    {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
1.5
1.6
1.7 -subsection{*Lemmas About Small Numerals*}
1.8 -
1.9 -lemma abs_power_minus_one [simp]:
1.10 -  "abs(-1 ^ n) = (1::'a::linordered_idom)"
1.11 -by (simp add: power_abs)
1.12 -
1.13 -
1.14  subsection{*More Inequality Reasoning*}
1.15
1.16  lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
1.17 @@ -1226,9 +1219,6 @@
1.18    unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
1.19    by simp
1.20
1.21 -lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
1.22 -  by (fact divide_minus_left)
1.23 -
1.24  lemma half_gt_zero_iff:
1.25    "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
1.26    by auto
```
```     2.1 --- a/src/HOL/NSA/HyperDef.thy	Tue Mar 04 14:14:28 2014 -0800
2.2 +++ b/src/HOL/NSA/HyperDef.thy	Tue Mar 04 15:26:12 2014 -0800
2.3 @@ -346,7 +346,7 @@
2.4    K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
2.5      @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
2.6    #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
2.7 -      @{thm star_of_numeral}, @{thm star_of_neg_numeral}, @{thm star_of_add},
2.8 +      @{thm star_of_numeral}, @{thm star_of_add},
2.9        @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
2.10    #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
2.11  *}
2.12 @@ -496,9 +496,9 @@
2.13    "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
2.14  by transfer (rule power_one)
2.15
2.16 -lemma hrabs_hyperpow_minus_one [simp]:
2.17 -  "\<And>n. abs(-1 pow n) = (1::'a::{linordered_idom} star)"
2.18 -by transfer (rule abs_power_minus_one)
2.19 +lemma hrabs_hyperpow_minus [simp]:
2.20 +  "\<And>(a::'a::{linordered_idom} star) n. abs((-a) pow n) = abs (a pow n)"
2.21 +by transfer (rule abs_power_minus)
2.22
2.23  lemma hyperpow_mult:
2.24    "\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n
```
```     3.1 --- a/src/HOL/NSA/StarDef.thy	Tue Mar 04 14:14:28 2014 -0800
3.2 +++ b/src/HOL/NSA/StarDef.thy	Tue Mar 04 15:26:12 2014 -0800
3.3 @@ -967,16 +967,6 @@
3.4  lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k"
3.5  by transfer (rule refl)
3.6
3.7 -lemma star_neg_numeral_def [transfer_unfold]:
3.8 -  "- numeral k = star_of (- numeral k)"
3.9 -by (simp only: star_of_minus star_of_numeral)
3.10 -
3.11 -lemma Standard_neg_numeral [simp]: "- numeral k \<in> Standard"
3.12 -  using star_neg_numeral_def [of k] by simp
3.13 -
3.14 -lemma star_of_neg_numeral [simp]: "star_of (- numeral k) = - numeral k"
3.15 -by transfer (rule refl)
3.16 -
3.17  lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
3.18  by (induct n, simp_all)
3.19
```