src/HOL/Numeral_Simprocs.thy
changeset 45435 d660c4b9daa6
parent 45308 2e84e5f0463b
child 45436 62bc9474d04b
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 14:47:38 2011 +1100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 10:58:08 2011 +0100
     1.3 @@ -103,8 +103,8 @@
     1.4    {* fn phi => Numeral_Simprocs.combine_numerals *}
     1.5  
     1.6  simproc_setup field_combine_numerals
     1.7 -  ("(i::'a::{field_inverse_zero, number_ring}) + j"
     1.8 -  |"(i::'a::{field_inverse_zero, number_ring}) - j") =
     1.9 +  ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j"
    1.10 +  |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") =
    1.11    {* fn phi => Numeral_Simprocs.field_combine_numerals *}
    1.12  
    1.13  simproc_setup inteq_cancel_numerals
    1.14 @@ -141,8 +141,8 @@
    1.15    {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
    1.16  
    1.17  simproc_setup ring_eq_cancel_numeral_factor
    1.18 -  ("(l::'a::{idom,number_ring}) * m = n"
    1.19 -  |"(l::'a::{idom,number_ring}) = m * n") =
    1.20 +  ("(l::'a::{idom,ring_char_0,number_ring}) * m = n"
    1.21 +  |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") =
    1.22    {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
    1.23  
    1.24  simproc_setup ring_less_cancel_numeral_factor
    1.25 @@ -156,14 +156,14 @@
    1.26    {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
    1.27  
    1.28  simproc_setup int_div_cancel_numeral_factors
    1.29 -  ("((l::'a::{semiring_div,number_ring}) * m) div n"
    1.30 -  |"(l::'a::{semiring_div,number_ring}) div (m * n)") =
    1.31 +  ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n"
    1.32 +  |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") =
    1.33    {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
    1.34  
    1.35  simproc_setup divide_cancel_numeral_factor
    1.36 -  ("((l::'a::{field_inverse_zero,number_ring}) * m) / n"
    1.37 -  |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)"
    1.38 -  |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") =
    1.39 +  ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n"
    1.40 +  |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)"
    1.41 +  |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") =
    1.42    {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
    1.43  
    1.44  simproc_setup ring_eq_cancel_factor