src/HOL/Numeral_Simprocs.thy
changeset 47108 2a1953f0d20d
parent 45607 16b4f5774621
child 47159 978c00c20a59
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -14,8 +14,8 @@
     1.4    ("Tools/nat_numeral_simprocs.ML")
     1.5  begin
     1.6  
     1.7 -declare split_div [of _ _ "number_of k", arith_split] for k
     1.8 -declare split_mod [of _ _ "number_of k", arith_split] for k
     1.9 +declare split_div [of _ _ "numeral k", arith_split] for k
    1.10 +declare split_mod [of _ _ "numeral k", arith_split] for k
    1.11  
    1.12  text {* For @{text combine_numerals} *}
    1.13  
    1.14 @@ -98,72 +98,74 @@
    1.15    ("(a::'a::comm_semiring_1_cancel) * b") =
    1.16    {* fn phi => Numeral_Simprocs.assoc_fold *}
    1.17  
    1.18 +(* TODO: see whether the type class can be generalized further *)
    1.19  simproc_setup int_combine_numerals
    1.20 -  ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") =
    1.21 +  ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
    1.22    {* fn phi => Numeral_Simprocs.combine_numerals *}
    1.23  
    1.24  simproc_setup field_combine_numerals
    1.25 -  ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j"
    1.26 -  |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") =
    1.27 +  ("(i::'a::{field_inverse_zero,ring_char_0}) + j"
    1.28 +  |"(i::'a::{field_inverse_zero,ring_char_0}) - j") =
    1.29    {* fn phi => Numeral_Simprocs.field_combine_numerals *}
    1.30  
    1.31  simproc_setup inteq_cancel_numerals
    1.32 -  ("(l::'a::number_ring) + m = n"
    1.33 -  |"(l::'a::number_ring) = m + n"
    1.34 -  |"(l::'a::number_ring) - m = n"
    1.35 -  |"(l::'a::number_ring) = m - n"
    1.36 -  |"(l::'a::number_ring) * m = n"
    1.37 -  |"(l::'a::number_ring) = m * n"
    1.38 -  |"- (l::'a::number_ring) = m"
    1.39 -  |"(l::'a::number_ring) = - m") =
    1.40 +  ("(l::'a::comm_ring_1) + m = n"
    1.41 +  |"(l::'a::comm_ring_1) = m + n"
    1.42 +  |"(l::'a::comm_ring_1) - m = n"
    1.43 +  |"(l::'a::comm_ring_1) = m - n"
    1.44 +  |"(l::'a::comm_ring_1) * m = n"
    1.45 +  |"(l::'a::comm_ring_1) = m * n"
    1.46 +  |"- (l::'a::comm_ring_1) = m"
    1.47 +  |"(l::'a::comm_ring_1) = - m") =
    1.48    {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
    1.49  
    1.50  simproc_setup intless_cancel_numerals
    1.51 -  ("(l::'a::{linordered_idom,number_ring}) + m < n"
    1.52 -  |"(l::'a::{linordered_idom,number_ring}) < m + n"
    1.53 -  |"(l::'a::{linordered_idom,number_ring}) - m < n"
    1.54 -  |"(l::'a::{linordered_idom,number_ring}) < m - n"
    1.55 -  |"(l::'a::{linordered_idom,number_ring}) * m < n"
    1.56 -  |"(l::'a::{linordered_idom,number_ring}) < m * n"
    1.57 -  |"- (l::'a::{linordered_idom,number_ring}) < m"
    1.58 -  |"(l::'a::{linordered_idom,number_ring}) < - m") =
    1.59 +  ("(l::'a::linordered_idom) + m < n"
    1.60 +  |"(l::'a::linordered_idom) < m + n"
    1.61 +  |"(l::'a::linordered_idom) - m < n"
    1.62 +  |"(l::'a::linordered_idom) < m - n"
    1.63 +  |"(l::'a::linordered_idom) * m < n"
    1.64 +  |"(l::'a::linordered_idom) < m * n"
    1.65 +  |"- (l::'a::linordered_idom) < m"
    1.66 +  |"(l::'a::linordered_idom) < - m") =
    1.67    {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
    1.68  
    1.69  simproc_setup intle_cancel_numerals
    1.70 -  ("(l::'a::{linordered_idom,number_ring}) + m \<le> n"
    1.71 -  |"(l::'a::{linordered_idom,number_ring}) \<le> m + n"
    1.72 -  |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
    1.73 -  |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
    1.74 -  |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
    1.75 -  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n"
    1.76 -  |"- (l::'a::{linordered_idom,number_ring}) \<le> m"
    1.77 -  |"(l::'a::{linordered_idom,number_ring}) \<le> - m") =
    1.78 +  ("(l::'a::linordered_idom) + m \<le> n"
    1.79 +  |"(l::'a::linordered_idom) \<le> m + n"
    1.80 +  |"(l::'a::linordered_idom) - m \<le> n"
    1.81 +  |"(l::'a::linordered_idom) \<le> m - n"
    1.82 +  |"(l::'a::linordered_idom) * m \<le> n"
    1.83 +  |"(l::'a::linordered_idom) \<le> m * n"
    1.84 +  |"- (l::'a::linordered_idom) \<le> m"
    1.85 +  |"(l::'a::linordered_idom) \<le> - m") =
    1.86    {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
    1.87  
    1.88  simproc_setup ring_eq_cancel_numeral_factor
    1.89 -  ("(l::'a::{idom,ring_char_0,number_ring}) * m = n"
    1.90 -  |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") =
    1.91 +  ("(l::'a::{idom,ring_char_0}) * m = n"
    1.92 +  |"(l::'a::{idom,ring_char_0}) = m * n") =
    1.93    {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
    1.94  
    1.95  simproc_setup ring_less_cancel_numeral_factor
    1.96 -  ("(l::'a::{linordered_idom,number_ring}) * m < n"
    1.97 -  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
    1.98 +  ("(l::'a::linordered_idom) * m < n"
    1.99 +  |"(l::'a::linordered_idom) < m * n") =
   1.100    {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
   1.101  
   1.102  simproc_setup ring_le_cancel_numeral_factor
   1.103 -  ("(l::'a::{linordered_idom,number_ring}) * m <= n"
   1.104 -  |"(l::'a::{linordered_idom,number_ring}) <= m * n") =
   1.105 +  ("(l::'a::linordered_idom) * m <= n"
   1.106 +  |"(l::'a::linordered_idom) <= m * n") =
   1.107    {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
   1.108  
   1.109 +(* TODO: remove comm_ring_1 constraint if possible *)
   1.110  simproc_setup int_div_cancel_numeral_factors
   1.111 -  ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n"
   1.112 -  |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") =
   1.113 +  ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
   1.114 +  |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
   1.115    {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
   1.116  
   1.117  simproc_setup divide_cancel_numeral_factor
   1.118 -  ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n"
   1.119 -  |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)"
   1.120 -  |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") =
   1.121 +  ("((l::'a::{field_inverse_zero,ring_char_0}) * m) / n"
   1.122 +  |"(l::'a::{field_inverse_zero,ring_char_0}) / (m * n)"
   1.123 +  |"((numeral v)::'a::{field_inverse_zero,ring_char_0}) / (numeral w)") =
   1.124    {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
   1.125  
   1.126  simproc_setup ring_eq_cancel_factor
   1.127 @@ -270,19 +272,25 @@
   1.128    ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
   1.129    {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
   1.130  
   1.131 +(* FIXME: duplicate rule warnings for:
   1.132 +  ring_distribs
   1.133 +  numeral_plus_numeral numeral_times_numeral
   1.134 +  numeral_eq_iff numeral_less_iff numeral_le_iff
   1.135 +  numeral_neq_zero zero_neq_numeral zero_less_numeral
   1.136 +  if_True if_False *)
   1.137  declaration {* 
   1.138 -  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
   1.139 -  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
   1.140 +  K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}])
   1.141 +  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
   1.142       @{thm nat_0}, @{thm nat_1},
   1.143 -     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
   1.144 -     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
   1.145 -     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
   1.146 -     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
   1.147 -     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
   1.148 +     @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral},
   1.149 +     @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff},
   1.150 +     @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
   1.151 +     @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
   1.152 +     @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
   1.153       @{thm mult_Suc}, @{thm mult_Suc_right},
   1.154       @{thm add_Suc}, @{thm add_Suc_right},
   1.155 -     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   1.156 -     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
   1.157 +     @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral},
   1.158 +     @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral},
   1.159       @{thm if_True}, @{thm if_False}])
   1.160    #> Lin_Arith.add_simprocs
   1.161        [@{simproc semiring_assoc_fold},