remove simp rules made redundant by the replacement of neg_numeral with negated numerals
authorhuffman
Tue Mar 04 15:26:12 2014 -0800 (2014-03-04)
changeset 55911d00023bd3554
parent 55910 0a756571c7a4
child 55912 e12a0ab9917c
remove simp rules made redundant by the replacement of neg_numeral with negated numerals
src/HOL/Int.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/StarDef.thy
     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