src/HOL/Numeral_Simprocs.thy
changeset 45284 ae78a4ffa81d
parent 37886 2f9d3fc1a8ac
child 45296 7a97b2bda137
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Thu Oct 27 22:37:19 2011 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Fri Oct 28 11:02:27 2011 +0200
     1.3 @@ -94,6 +94,106 @@
     1.4  
     1.5  use "Tools/numeral_simprocs.ML"
     1.6  
     1.7 +simproc_setup semiring_assoc_fold
     1.8 +  ("(a::'a::comm_semiring_1_cancel) * b") =
     1.9 +  {* fn phi => Numeral_Simprocs.assoc_fold *}
    1.10 +
    1.11 +simproc_setup int_combine_numerals
    1.12 +  ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") =
    1.13 +  {* fn phi => Numeral_Simprocs.combine_numerals *}
    1.14 +
    1.15 +simproc_setup field_combine_numerals
    1.16 +  ("(i::'a::{field_inverse_zero, number_ring}) + j"
    1.17 +  |"(i::'a::{field_inverse_zero, number_ring}) - j") =
    1.18 +  {* fn phi => Numeral_Simprocs.field_combine_numerals *}
    1.19 +
    1.20 +simproc_setup inteq_cancel_numerals
    1.21 +  ("(l::'a::number_ring) + m = n"
    1.22 +  |"(l::'a::number_ring) = m + n"
    1.23 +  |"(l::'a::number_ring) - m = n"
    1.24 +  |"(l::'a::number_ring) = m - n"
    1.25 +  |"(l::'a::number_ring) * m = n"
    1.26 +  |"(l::'a::number_ring) = m * n") =
    1.27 +  {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
    1.28 +
    1.29 +simproc_setup intless_cancel_numerals
    1.30 +  ("(l::'a::{linordered_idom,number_ring}) + m < n"
    1.31 +  |"(l::'a::{linordered_idom,number_ring}) < m + n"
    1.32 +  |"(l::'a::{linordered_idom,number_ring}) - m < n"
    1.33 +  |"(l::'a::{linordered_idom,number_ring}) < m - n"
    1.34 +  |"(l::'a::{linordered_idom,number_ring}) * m < n"
    1.35 +  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
    1.36 +  {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
    1.37 +
    1.38 +simproc_setup intle_cancel_numerals
    1.39 +  ("(l::'a::{linordered_idom,number_ring}) + m \<le> n"
    1.40 +  |"(l::'a::{linordered_idom,number_ring}) \<le> m + n"
    1.41 +  |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
    1.42 +  |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
    1.43 +  |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
    1.44 +  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n") =
    1.45 +  {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
    1.46 +
    1.47 +simproc_setup ring_eq_cancel_numeral_factor
    1.48 +  ("(l::'a::{idom,number_ring}) * m = n"
    1.49 +  |"(l::'a::{idom,number_ring}) = m * n") =
    1.50 +  {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
    1.51 +
    1.52 +simproc_setup ring_less_cancel_numeral_factor
    1.53 +  ("(l::'a::{linordered_idom,number_ring}) * m < n"
    1.54 +  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
    1.55 +  {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
    1.56 +
    1.57 +simproc_setup ring_le_cancel_numeral_factor
    1.58 +  ("(l::'a::{linordered_idom,number_ring}) * m <= n"
    1.59 +  |"(l::'a::{linordered_idom,number_ring}) <= m * n") =
    1.60 +  {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
    1.61 +
    1.62 +simproc_setup int_div_cancel_numeral_factors
    1.63 +  ("((l::'a::{semiring_div,number_ring}) * m) div n"
    1.64 +  |"(l::'a::{semiring_div,number_ring}) div (m * n)") =
    1.65 +  {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
    1.66 +
    1.67 +simproc_setup divide_cancel_numeral_factor
    1.68 +  ("((l::'a::{field_inverse_zero,number_ring}) * m) / n"
    1.69 +  |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)"
    1.70 +  |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") =
    1.71 +  {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
    1.72 +
    1.73 +simproc_setup ring_eq_cancel_factor
    1.74 +  ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
    1.75 +  {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
    1.76 +
    1.77 +simproc_setup linordered_ring_le_cancel_factor
    1.78 +  ("(l::'a::linordered_ring) * m <= n"
    1.79 +  |"(l::'a::linordered_ring) <= m * n") =
    1.80 +  {* fn phi => Numeral_Simprocs.le_cancel_factor *}
    1.81 +
    1.82 +simproc_setup linordered_ring_less_cancel_factor
    1.83 +  ("(l::'a::linordered_ring) * m < n"
    1.84 +  |"(l::'a::linordered_ring) < m * n") =
    1.85 +  {* fn phi => Numeral_Simprocs.less_cancel_factor *}
    1.86 +
    1.87 +simproc_setup int_div_cancel_factor
    1.88 +  ("((l::'a::semiring_div) * m) div n"
    1.89 +  |"(l::'a::semiring_div) div (m * n)") =
    1.90 +  {* fn phi => Numeral_Simprocs.div_cancel_factor *}
    1.91 +
    1.92 +simproc_setup int_mod_cancel_factor
    1.93 +  ("((l::'a::semiring_div) * m) mod n"
    1.94 +  |"(l::'a::semiring_div) mod (m * n)") =
    1.95 +  {* fn phi => Numeral_Simprocs.mod_cancel_factor *}
    1.96 +
    1.97 +simproc_setup dvd_cancel_factor
    1.98 +  ("((l::'a::idom) * m) dvd n"
    1.99 +  |"(l::'a::idom) dvd (m * n)") =
   1.100 +  {* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
   1.101 +
   1.102 +simproc_setup divide_cancel_factor
   1.103 +  ("((l::'a::field_inverse_zero) * m) / n"
   1.104 +  |"(l::'a::field_inverse_zero) / (m * n)") =
   1.105 +  {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
   1.106 +
   1.107  use "Tools/nat_numeral_simprocs.ML"
   1.108  
   1.109  declaration {* 
   1.110 @@ -110,9 +210,12 @@
   1.111       @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   1.112       @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
   1.113       @{thm if_True}, @{thm if_False}])
   1.114 -  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
   1.115 -      :: Numeral_Simprocs.combine_numerals
   1.116 -      :: Numeral_Simprocs.cancel_numerals)
   1.117 +  #> Lin_Arith.add_simprocs
   1.118 +      [@{simproc semiring_assoc_fold},
   1.119 +       @{simproc int_combine_numerals},
   1.120 +       @{simproc inteq_cancel_numerals},
   1.121 +       @{simproc intless_cancel_numerals},
   1.122 +       @{simproc intle_cancel_numerals}]
   1.123    #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
   1.124  *}
   1.125