extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
authorhuffman
Sun Oct 30 09:07:02 2011 +0100 (2011-10-30)
changeset 453082e84e5f0463b
parent 45307 0e00bc1ad51c
child 45309 5885ec8eb6b0
extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
src/HOL/Numeral_Simprocs.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Oct 30 07:08:33 2011 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sun Oct 30 09:07:02 2011 +0100
     1.3 @@ -113,7 +113,9 @@
     1.4    |"(l::'a::number_ring) - m = n"
     1.5    |"(l::'a::number_ring) = m - n"
     1.6    |"(l::'a::number_ring) * m = n"
     1.7 -  |"(l::'a::number_ring) = m * n") =
     1.8 +  |"(l::'a::number_ring) = m * n"
     1.9 +  |"- (l::'a::number_ring) = m"
    1.10 +  |"(l::'a::number_ring) = - m") =
    1.11    {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
    1.12  
    1.13  simproc_setup intless_cancel_numerals
    1.14 @@ -122,7 +124,9 @@
    1.15    |"(l::'a::{linordered_idom,number_ring}) - m < n"
    1.16    |"(l::'a::{linordered_idom,number_ring}) < m - n"
    1.17    |"(l::'a::{linordered_idom,number_ring}) * m < n"
    1.18 -  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
    1.19 +  |"(l::'a::{linordered_idom,number_ring}) < m * n"
    1.20 +  |"- (l::'a::{linordered_idom,number_ring}) < m"
    1.21 +  |"(l::'a::{linordered_idom,number_ring}) < - m") =
    1.22    {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
    1.23  
    1.24  simproc_setup intle_cancel_numerals
    1.25 @@ -131,7 +135,9 @@
    1.26    |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
    1.27    |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
    1.28    |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
    1.29 -  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n") =
    1.30 +  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n"
    1.31 +  |"- (l::'a::{linordered_idom,number_ring}) \<le> m"
    1.32 +  |"(l::'a::{linordered_idom,number_ring}) \<le> - m") =
    1.33    {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
    1.34  
    1.35  simproc_setup ring_eq_cancel_numeral_factor
     2.1 --- a/src/HOL/Transcendental.thy	Sun Oct 30 07:08:33 2011 +0100
     2.2 +++ b/src/HOL/Transcendental.thy	Sun Oct 30 09:07:02 2011 +0100
     2.3 @@ -1589,10 +1589,7 @@
     2.4  by simp
     2.5  
     2.6  lemma m2pi_less_pi: "- (2 * pi) < pi"
     2.7 -proof -
     2.8 -  have "- (2 * pi) < 0" and "0 < pi" by auto
     2.9 -  from order_less_trans[OF this] show ?thesis .
    2.10 -qed
    2.11 +by simp
    2.12  
    2.13  lemma sin_pi_half [simp]: "sin(pi/2) = 1"
    2.14  apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
    2.15 @@ -2351,7 +2348,7 @@
    2.16  proof -
    2.17    let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
    2.18    have nonneg: "0 \<le> ?c"
    2.19 -    by (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
    2.20 +    by (simp add: cos_ge_zero)
    2.21    have "0 = cos (pi / 4 + pi / 4)"
    2.22      by simp
    2.23    also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>"