# HG changeset patch
# User huffman
# Date 1319962022 -3600
# Node ID 2e84e5f0463bb0397ec54945a636237ce058cf33
# Parent  0e00bc1ad51ce1ebee0bd3191994519a6746d797
extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'

diff -r 0e00bc1ad51c -r 2e84e5f0463b src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Sun Oct 30 07:08:33 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Sun Oct 30 09:07:02 2011 +0100
@@ -113,7 +113,9 @@
   |"(l::'a::number_ring) - m = n"
   |"(l::'a::number_ring) = m - n"
   |"(l::'a::number_ring) * m = n"
-  |"(l::'a::number_ring) = m * n") =
+  |"(l::'a::number_ring) = m * n"
+  |"- (l::'a::number_ring) = m"
+  |"(l::'a::number_ring) = - m") =
   {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
 
 simproc_setup intless_cancel_numerals
@@ -122,7 +124,9 @@
   |"(l::'a::{linordered_idom,number_ring}) - m < n"
   |"(l::'a::{linordered_idom,number_ring}) < m - n"
   |"(l::'a::{linordered_idom,number_ring}) * m < n"
-  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
+  |"(l::'a::{linordered_idom,number_ring}) < m * n"
+  |"- (l::'a::{linordered_idom,number_ring}) < m"
+  |"(l::'a::{linordered_idom,number_ring}) < - m") =
   {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
 
 simproc_setup intle_cancel_numerals
@@ -131,7 +135,9 @@
   |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
   |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
   |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
-  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n") =
+  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n"
+  |"- (l::'a::{linordered_idom,number_ring}) \<le> m"
+  |"(l::'a::{linordered_idom,number_ring}) \<le> - m") =
   {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
 
 simproc_setup ring_eq_cancel_numeral_factor
diff -r 0e00bc1ad51c -r 2e84e5f0463b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Oct 30 07:08:33 2011 +0100
+++ b/src/HOL/Transcendental.thy	Sun Oct 30 09:07:02 2011 +0100
@@ -1589,10 +1589,7 @@
 by simp
 
 lemma m2pi_less_pi: "- (2 * pi) < pi"
-proof -
-  have "- (2 * pi) < 0" and "0 < pi" by auto
-  from order_less_trans[OF this] show ?thesis .
-qed
+by simp
 
 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
 apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
@@ -2351,7 +2348,7 @@
 proof -
   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
   have nonneg: "0 \<le> ?c"
-    by (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
+    by (simp add: cos_ge_zero)
   have "0 = cos (pi / 4 + pi / 4)"
     by simp
   also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>"