src/HOL/Numeral_Simprocs.thy
changeset 45308 2e84e5f0463b
parent 45296 7a97b2bda137
child 45435 d660c4b9daa6
     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