src/HOL/Numeral_Simprocs.thy
changeset 47108 2a1953f0d20d
parent 45607 16b4f5774621
child 47159 978c00c20a59
equal deleted inserted replaced
47107:35807a5d8dc2 47108:2a1953f0d20d
    12   "~~/src/Provers/Arith/extract_common_term.ML"
    12   "~~/src/Provers/Arith/extract_common_term.ML"
    13   ("Tools/numeral_simprocs.ML")
    13   ("Tools/numeral_simprocs.ML")
    14   ("Tools/nat_numeral_simprocs.ML")
    14   ("Tools/nat_numeral_simprocs.ML")
    15 begin
    15 begin
    16 
    16 
    17 declare split_div [of _ _ "number_of k", arith_split] for k
    17 declare split_div [of _ _ "numeral k", arith_split] for k
    18 declare split_mod [of _ _ "number_of k", arith_split] for k
    18 declare split_mod [of _ _ "numeral k", arith_split] for k
    19 
    19 
    20 text {* For @{text combine_numerals} *}
    20 text {* For @{text combine_numerals} *}
    21 
    21 
    22 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
    22 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
    23 by (simp add: add_mult_distrib)
    23 by (simp add: add_mult_distrib)
    96 
    96 
    97 simproc_setup semiring_assoc_fold
    97 simproc_setup semiring_assoc_fold
    98   ("(a::'a::comm_semiring_1_cancel) * b") =
    98   ("(a::'a::comm_semiring_1_cancel) * b") =
    99   {* fn phi => Numeral_Simprocs.assoc_fold *}
    99   {* fn phi => Numeral_Simprocs.assoc_fold *}
   100 
   100 
       
   101 (* TODO: see whether the type class can be generalized further *)
   101 simproc_setup int_combine_numerals
   102 simproc_setup int_combine_numerals
   102   ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") =
   103   ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
   103   {* fn phi => Numeral_Simprocs.combine_numerals *}
   104   {* fn phi => Numeral_Simprocs.combine_numerals *}
   104 
   105 
   105 simproc_setup field_combine_numerals
   106 simproc_setup field_combine_numerals
   106   ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j"
   107   ("(i::'a::{field_inverse_zero,ring_char_0}) + j"
   107   |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") =
   108   |"(i::'a::{field_inverse_zero,ring_char_0}) - j") =
   108   {* fn phi => Numeral_Simprocs.field_combine_numerals *}
   109   {* fn phi => Numeral_Simprocs.field_combine_numerals *}
   109 
   110 
   110 simproc_setup inteq_cancel_numerals
   111 simproc_setup inteq_cancel_numerals
   111   ("(l::'a::number_ring) + m = n"
   112   ("(l::'a::comm_ring_1) + m = n"
   112   |"(l::'a::number_ring) = m + n"
   113   |"(l::'a::comm_ring_1) = m + n"
   113   |"(l::'a::number_ring) - m = n"
   114   |"(l::'a::comm_ring_1) - m = n"
   114   |"(l::'a::number_ring) = m - n"
   115   |"(l::'a::comm_ring_1) = m - n"
   115   |"(l::'a::number_ring) * m = n"
   116   |"(l::'a::comm_ring_1) * m = n"
   116   |"(l::'a::number_ring) = m * n"
   117   |"(l::'a::comm_ring_1) = m * n"
   117   |"- (l::'a::number_ring) = m"
   118   |"- (l::'a::comm_ring_1) = m"
   118   |"(l::'a::number_ring) = - m") =
   119   |"(l::'a::comm_ring_1) = - m") =
   119   {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
   120   {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
   120 
   121 
   121 simproc_setup intless_cancel_numerals
   122 simproc_setup intless_cancel_numerals
   122   ("(l::'a::{linordered_idom,number_ring}) + m < n"
   123   ("(l::'a::linordered_idom) + m < n"
   123   |"(l::'a::{linordered_idom,number_ring}) < m + n"
   124   |"(l::'a::linordered_idom) < m + n"
   124   |"(l::'a::{linordered_idom,number_ring}) - m < n"
   125   |"(l::'a::linordered_idom) - m < n"
   125   |"(l::'a::{linordered_idom,number_ring}) < m - n"
   126   |"(l::'a::linordered_idom) < m - n"
   126   |"(l::'a::{linordered_idom,number_ring}) * m < n"
   127   |"(l::'a::linordered_idom) * m < n"
   127   |"(l::'a::{linordered_idom,number_ring}) < m * n"
   128   |"(l::'a::linordered_idom) < m * n"
   128   |"- (l::'a::{linordered_idom,number_ring}) < m"
   129   |"- (l::'a::linordered_idom) < m"
   129   |"(l::'a::{linordered_idom,number_ring}) < - m") =
   130   |"(l::'a::linordered_idom) < - m") =
   130   {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
   131   {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
   131 
   132 
   132 simproc_setup intle_cancel_numerals
   133 simproc_setup intle_cancel_numerals
   133   ("(l::'a::{linordered_idom,number_ring}) + m \<le> n"
   134   ("(l::'a::linordered_idom) + m \<le> n"
   134   |"(l::'a::{linordered_idom,number_ring}) \<le> m + n"
   135   |"(l::'a::linordered_idom) \<le> m + n"
   135   |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
   136   |"(l::'a::linordered_idom) - m \<le> n"
   136   |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
   137   |"(l::'a::linordered_idom) \<le> m - n"
   137   |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
   138   |"(l::'a::linordered_idom) * m \<le> n"
   138   |"(l::'a::{linordered_idom,number_ring}) \<le> m * n"
   139   |"(l::'a::linordered_idom) \<le> m * n"
   139   |"- (l::'a::{linordered_idom,number_ring}) \<le> m"
   140   |"- (l::'a::linordered_idom) \<le> m"
   140   |"(l::'a::{linordered_idom,number_ring}) \<le> - m") =
   141   |"(l::'a::linordered_idom) \<le> - m") =
   141   {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
   142   {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
   142 
   143 
   143 simproc_setup ring_eq_cancel_numeral_factor
   144 simproc_setup ring_eq_cancel_numeral_factor
   144   ("(l::'a::{idom,ring_char_0,number_ring}) * m = n"
   145   ("(l::'a::{idom,ring_char_0}) * m = n"
   145   |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") =
   146   |"(l::'a::{idom,ring_char_0}) = m * n") =
   146   {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
   147   {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
   147 
   148 
   148 simproc_setup ring_less_cancel_numeral_factor
   149 simproc_setup ring_less_cancel_numeral_factor
   149   ("(l::'a::{linordered_idom,number_ring}) * m < n"
   150   ("(l::'a::linordered_idom) * m < n"
   150   |"(l::'a::{linordered_idom,number_ring}) < m * n") =
   151   |"(l::'a::linordered_idom) < m * n") =
   151   {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
   152   {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
   152 
   153 
   153 simproc_setup ring_le_cancel_numeral_factor
   154 simproc_setup ring_le_cancel_numeral_factor
   154   ("(l::'a::{linordered_idom,number_ring}) * m <= n"
   155   ("(l::'a::linordered_idom) * m <= n"
   155   |"(l::'a::{linordered_idom,number_ring}) <= m * n") =
   156   |"(l::'a::linordered_idom) <= m * n") =
   156   {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
   157   {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
   157 
   158 
       
   159 (* TODO: remove comm_ring_1 constraint if possible *)
   158 simproc_setup int_div_cancel_numeral_factors
   160 simproc_setup int_div_cancel_numeral_factors
   159   ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n"
   161   ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
   160   |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") =
   162   |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
   161   {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
   163   {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
   162 
   164 
   163 simproc_setup divide_cancel_numeral_factor
   165 simproc_setup divide_cancel_numeral_factor
   164   ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n"
   166   ("((l::'a::{field_inverse_zero,ring_char_0}) * m) / n"
   165   |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)"
   167   |"(l::'a::{field_inverse_zero,ring_char_0}) / (m * n)"
   166   |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") =
   168   |"((numeral v)::'a::{field_inverse_zero,ring_char_0}) / (numeral w)") =
   167   {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
   169   {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
   168 
   170 
   169 simproc_setup ring_eq_cancel_factor
   171 simproc_setup ring_eq_cancel_factor
   170   ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
   172   ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
   171   {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
   173   {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
   268 
   270 
   269 simproc_setup nat_dvd_cancel_factor
   271 simproc_setup nat_dvd_cancel_factor
   270   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
   272   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
   271   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
   273   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
   272 
   274 
       
   275 (* FIXME: duplicate rule warnings for:
       
   276   ring_distribs
       
   277   numeral_plus_numeral numeral_times_numeral
       
   278   numeral_eq_iff numeral_less_iff numeral_le_iff
       
   279   numeral_neq_zero zero_neq_numeral zero_less_numeral
       
   280   if_True if_False *)
   273 declaration {* 
   281 declaration {* 
   274   K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
   282   K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}])
   275   #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
   283   #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
   276      @{thm nat_0}, @{thm nat_1},
   284      @{thm nat_0}, @{thm nat_1},
   277      @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
   285      @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral},
   278      @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
   286      @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff},
   279      @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
   287      @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
   280      @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
   288      @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
   281      @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
   289      @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
   282      @{thm mult_Suc}, @{thm mult_Suc_right},
   290      @{thm mult_Suc}, @{thm mult_Suc_right},
   283      @{thm add_Suc}, @{thm add_Suc_right},
   291      @{thm add_Suc}, @{thm add_Suc_right},
   284      @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   292      @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral},
   285      @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
   293      @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral},
   286      @{thm if_True}, @{thm if_False}])
   294      @{thm if_True}, @{thm if_False}])
   287   #> Lin_Arith.add_simprocs
   295   #> Lin_Arith.add_simprocs
   288       [@{simproc semiring_assoc_fold},
   296       [@{simproc semiring_assoc_fold},
   289        @{simproc int_combine_numerals},
   297        @{simproc int_combine_numerals},
   290        @{simproc inteq_cancel_numerals},
   298        @{simproc inteq_cancel_numerals},