src/HOL/Numeral_Simprocs.thy
 author wenzelm Sun Nov 20 21:07:10 2011 +0100 (2011-11-20) changeset 45607 16b4f5774621 parent 45463 9a588a835c1e child 47108 2a1953f0d20d permissions -rw-r--r--
eliminated obsolete "standard";
 haftmann@33366 ` 1` ```(* Author: Various *) ``` haftmann@33366 ` 2` haftmann@33366 ` 3` ```header {* Combination and Cancellation Simprocs for Numeral Expressions *} ``` haftmann@33366 ` 4` haftmann@33366 ` 5` ```theory Numeral_Simprocs ``` haftmann@33366 ` 6` ```imports Divides ``` haftmann@33366 ` 7` ```uses ``` haftmann@33366 ` 8` ``` "~~/src/Provers/Arith/assoc_fold.ML" ``` haftmann@33366 ` 9` ``` "~~/src/Provers/Arith/cancel_numerals.ML" ``` haftmann@33366 ` 10` ``` "~~/src/Provers/Arith/combine_numerals.ML" ``` haftmann@33366 ` 11` ``` "~~/src/Provers/Arith/cancel_numeral_factor.ML" ``` haftmann@33366 ` 12` ``` "~~/src/Provers/Arith/extract_common_term.ML" ``` haftmann@33366 ` 13` ``` ("Tools/numeral_simprocs.ML") ``` haftmann@33366 ` 14` ``` ("Tools/nat_numeral_simprocs.ML") ``` haftmann@33366 ` 15` ```begin ``` haftmann@33366 ` 16` wenzelm@45607 ` 17` ```declare split_div [of _ _ "number_of k", arith_split] for k ``` wenzelm@45607 ` 18` ```declare split_mod [of _ _ "number_of k", arith_split] for k ``` haftmann@33366 ` 19` haftmann@33366 ` 20` ```text {* For @{text combine_numerals} *} ``` haftmann@33366 ` 21` haftmann@33366 ` 22` ```lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)" ``` haftmann@33366 ` 23` ```by (simp add: add_mult_distrib) ``` haftmann@33366 ` 24` haftmann@33366 ` 25` ```text {* For @{text cancel_numerals} *} ``` haftmann@33366 ` 26` haftmann@33366 ` 27` ```lemma nat_diff_add_eq1: ``` haftmann@33366 ` 28` ``` "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)" ``` haftmann@33366 ` 29` ```by (simp split add: nat_diff_split add: add_mult_distrib) ``` haftmann@33366 ` 30` haftmann@33366 ` 31` ```lemma nat_diff_add_eq2: ``` haftmann@33366 ` 32` ``` "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))" ``` haftmann@33366 ` 33` ```by (simp split add: nat_diff_split add: add_mult_distrib) ``` haftmann@33366 ` 34` haftmann@33366 ` 35` ```lemma nat_eq_add_iff1: ``` haftmann@33366 ` 36` ``` "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)" ``` haftmann@33366 ` 37` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 38` haftmann@33366 ` 39` ```lemma nat_eq_add_iff2: ``` haftmann@33366 ` 40` ``` "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)" ``` haftmann@33366 ` 41` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 42` haftmann@33366 ` 43` ```lemma nat_less_add_iff1: ``` haftmann@33366 ` 44` ``` "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)" ``` haftmann@33366 ` 45` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 46` haftmann@33366 ` 47` ```lemma nat_less_add_iff2: ``` haftmann@33366 ` 48` ``` "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)" ``` haftmann@33366 ` 49` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 50` haftmann@33366 ` 51` ```lemma nat_le_add_iff1: ``` haftmann@33366 ` 52` ``` "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)" ``` haftmann@33366 ` 53` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 54` haftmann@33366 ` 55` ```lemma nat_le_add_iff2: ``` haftmann@33366 ` 56` ``` "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)" ``` haftmann@33366 ` 57` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 58` haftmann@33366 ` 59` ```text {* For @{text cancel_numeral_factors} *} ``` haftmann@33366 ` 60` haftmann@33366 ` 61` ```lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)" ``` haftmann@33366 ` 62` ```by auto ``` haftmann@33366 ` 63` haftmann@33366 ` 64` ```lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m (k*m = k*n) = (m=n)" ``` haftmann@33366 ` 68` ```by auto ``` haftmann@33366 ` 69` haftmann@33366 ` 70` ```lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)" ``` haftmann@33366 ` 71` ```by auto ``` haftmann@33366 ` 72` haftmann@33366 ` 73` ```lemma nat_mult_dvd_cancel_disj[simp]: ``` haftmann@33366 ` 74` ``` "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))" ``` haftmann@33366 ` 75` ```by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric]) ``` haftmann@33366 ` 76` haftmann@33366 ` 77` ```lemma nat_mult_dvd_cancel1: "0 < k \ (k*m) dvd (k*n::nat) = (m dvd n)" ``` haftmann@33366 ` 78` ```by(auto) ``` haftmann@33366 ` 79` haftmann@33366 ` 80` ```text {* For @{text cancel_factor} *} ``` haftmann@33366 ` 81` haftmann@33366 ` 82` ```lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)" ``` haftmann@33366 ` 83` ```by auto ``` haftmann@33366 ` 84` haftmann@33366 ` 85` ```lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m Numeral_Simprocs.assoc_fold *} ``` huffman@45284 ` 100` huffman@45284 ` 101` ```simproc_setup int_combine_numerals ``` huffman@45284 ` 102` ``` ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") = ``` huffman@45284 ` 103` ``` {* fn phi => Numeral_Simprocs.combine_numerals *} ``` huffman@45284 ` 104` huffman@45284 ` 105` ```simproc_setup field_combine_numerals ``` huffman@45435 ` 106` ``` ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j" ``` huffman@45435 ` 107` ``` |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") = ``` huffman@45284 ` 108` ``` {* fn phi => Numeral_Simprocs.field_combine_numerals *} ``` huffman@45284 ` 109` huffman@45284 ` 110` ```simproc_setup inteq_cancel_numerals ``` huffman@45284 ` 111` ``` ("(l::'a::number_ring) + m = n" ``` huffman@45284 ` 112` ``` |"(l::'a::number_ring) = m + n" ``` huffman@45284 ` 113` ``` |"(l::'a::number_ring) - m = n" ``` huffman@45284 ` 114` ``` |"(l::'a::number_ring) = m - n" ``` huffman@45284 ` 115` ``` |"(l::'a::number_ring) * m = n" ``` huffman@45308 ` 116` ``` |"(l::'a::number_ring) = m * n" ``` huffman@45308 ` 117` ``` |"- (l::'a::number_ring) = m" ``` huffman@45308 ` 118` ``` |"(l::'a::number_ring) = - m") = ``` huffman@45284 ` 119` ``` {* fn phi => Numeral_Simprocs.eq_cancel_numerals *} ``` huffman@45284 ` 120` huffman@45284 ` 121` ```simproc_setup intless_cancel_numerals ``` huffman@45284 ` 122` ``` ("(l::'a::{linordered_idom,number_ring}) + m < n" ``` huffman@45284 ` 123` ``` |"(l::'a::{linordered_idom,number_ring}) < m + n" ``` huffman@45284 ` 124` ``` |"(l::'a::{linordered_idom,number_ring}) - m < n" ``` huffman@45284 ` 125` ``` |"(l::'a::{linordered_idom,number_ring}) < m - n" ``` huffman@45284 ` 126` ``` |"(l::'a::{linordered_idom,number_ring}) * m < n" ``` huffman@45308 ` 127` ``` |"(l::'a::{linordered_idom,number_ring}) < m * n" ``` huffman@45308 ` 128` ``` |"- (l::'a::{linordered_idom,number_ring}) < m" ``` huffman@45308 ` 129` ``` |"(l::'a::{linordered_idom,number_ring}) < - m") = ``` huffman@45284 ` 130` ``` {* fn phi => Numeral_Simprocs.less_cancel_numerals *} ``` huffman@45284 ` 131` huffman@45284 ` 132` ```simproc_setup intle_cancel_numerals ``` huffman@45284 ` 133` ``` ("(l::'a::{linordered_idom,number_ring}) + m \ n" ``` huffman@45284 ` 134` ``` |"(l::'a::{linordered_idom,number_ring}) \ m + n" ``` huffman@45284 ` 135` ``` |"(l::'a::{linordered_idom,number_ring}) - m \ n" ``` huffman@45284 ` 136` ``` |"(l::'a::{linordered_idom,number_ring}) \ m - n" ``` huffman@45284 ` 137` ``` |"(l::'a::{linordered_idom,number_ring}) * m \ n" ``` huffman@45308 ` 138` ``` |"(l::'a::{linordered_idom,number_ring}) \ m * n" ``` huffman@45308 ` 139` ``` |"- (l::'a::{linordered_idom,number_ring}) \ m" ``` huffman@45308 ` 140` ``` |"(l::'a::{linordered_idom,number_ring}) \ - m") = ``` huffman@45284 ` 141` ``` {* fn phi => Numeral_Simprocs.le_cancel_numerals *} ``` huffman@45284 ` 142` huffman@45284 ` 143` ```simproc_setup ring_eq_cancel_numeral_factor ``` huffman@45435 ` 144` ``` ("(l::'a::{idom,ring_char_0,number_ring}) * m = n" ``` huffman@45435 ` 145` ``` |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") = ``` huffman@45284 ` 146` ``` {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *} ``` huffman@45284 ` 147` huffman@45284 ` 148` ```simproc_setup ring_less_cancel_numeral_factor ``` huffman@45284 ` 149` ``` ("(l::'a::{linordered_idom,number_ring}) * m < n" ``` huffman@45284 ` 150` ``` |"(l::'a::{linordered_idom,number_ring}) < m * n") = ``` huffman@45284 ` 151` ``` {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *} ``` huffman@45284 ` 152` huffman@45284 ` 153` ```simproc_setup ring_le_cancel_numeral_factor ``` huffman@45284 ` 154` ``` ("(l::'a::{linordered_idom,number_ring}) * m <= n" ``` huffman@45284 ` 155` ``` |"(l::'a::{linordered_idom,number_ring}) <= m * n") = ``` huffman@45284 ` 156` ``` {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *} ``` huffman@45284 ` 157` huffman@45284 ` 158` ```simproc_setup int_div_cancel_numeral_factors ``` huffman@45435 ` 159` ``` ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n" ``` huffman@45435 ` 160` ``` |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") = ``` huffman@45284 ` 161` ``` {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *} ``` huffman@45284 ` 162` huffman@45284 ` 163` ```simproc_setup divide_cancel_numeral_factor ``` huffman@45435 ` 164` ``` ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n" ``` huffman@45435 ` 165` ``` |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)" ``` huffman@45435 ` 166` ``` |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") = ``` huffman@45284 ` 167` ``` {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *} ``` huffman@45284 ` 168` huffman@45284 ` 169` ```simproc_setup ring_eq_cancel_factor ``` huffman@45284 ` 170` ``` ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") = ``` huffman@45284 ` 171` ``` {* fn phi => Numeral_Simprocs.eq_cancel_factor *} ``` huffman@45284 ` 172` huffman@45284 ` 173` ```simproc_setup linordered_ring_le_cancel_factor ``` huffman@45296 ` 174` ``` ("(l::'a::linordered_idom) * m <= n" ``` huffman@45296 ` 175` ``` |"(l::'a::linordered_idom) <= m * n") = ``` huffman@45284 ` 176` ``` {* fn phi => Numeral_Simprocs.le_cancel_factor *} ``` huffman@45284 ` 177` huffman@45284 ` 178` ```simproc_setup linordered_ring_less_cancel_factor ``` huffman@45296 ` 179` ``` ("(l::'a::linordered_idom) * m < n" ``` huffman@45296 ` 180` ``` |"(l::'a::linordered_idom) < m * n") = ``` huffman@45284 ` 181` ``` {* fn phi => Numeral_Simprocs.less_cancel_factor *} ``` huffman@45284 ` 182` huffman@45284 ` 183` ```simproc_setup int_div_cancel_factor ``` huffman@45284 ` 184` ``` ("((l::'a::semiring_div) * m) div n" ``` huffman@45284 ` 185` ``` |"(l::'a::semiring_div) div (m * n)") = ``` huffman@45284 ` 186` ``` {* fn phi => Numeral_Simprocs.div_cancel_factor *} ``` huffman@45284 ` 187` huffman@45284 ` 188` ```simproc_setup int_mod_cancel_factor ``` huffman@45284 ` 189` ``` ("((l::'a::semiring_div) * m) mod n" ``` huffman@45284 ` 190` ``` |"(l::'a::semiring_div) mod (m * n)") = ``` huffman@45284 ` 191` ``` {* fn phi => Numeral_Simprocs.mod_cancel_factor *} ``` huffman@45284 ` 192` huffman@45284 ` 193` ```simproc_setup dvd_cancel_factor ``` huffman@45284 ` 194` ``` ("((l::'a::idom) * m) dvd n" ``` huffman@45284 ` 195` ``` |"(l::'a::idom) dvd (m * n)") = ``` huffman@45284 ` 196` ``` {* fn phi => Numeral_Simprocs.dvd_cancel_factor *} ``` huffman@45284 ` 197` huffman@45284 ` 198` ```simproc_setup divide_cancel_factor ``` huffman@45284 ` 199` ``` ("((l::'a::field_inverse_zero) * m) / n" ``` huffman@45284 ` 200` ``` |"(l::'a::field_inverse_zero) / (m * n)") = ``` huffman@45284 ` 201` ``` {* fn phi => Numeral_Simprocs.divide_cancel_factor *} ``` huffman@45284 ` 202` haftmann@33366 ` 203` ```use "Tools/nat_numeral_simprocs.ML" ``` haftmann@33366 ` 204` huffman@45462 ` 205` ```simproc_setup nat_combine_numerals ``` huffman@45462 ` 206` ``` ("(i::nat) + j" | "Suc (i + j)") = ``` huffman@45462 ` 207` ``` {* fn phi => Nat_Numeral_Simprocs.combine_numerals *} ``` huffman@45462 ` 208` huffman@45436 ` 209` ```simproc_setup nateq_cancel_numerals ``` huffman@45436 ` 210` ``` ("(l::nat) + m = n" | "(l::nat) = m + n" | ``` huffman@45436 ` 211` ``` "(l::nat) * m = n" | "(l::nat) = m * n" | ``` huffman@45436 ` 212` ``` "Suc m = n" | "m = Suc n") = ``` huffman@45436 ` 213` ``` {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals *} ``` huffman@45436 ` 214` huffman@45436 ` 215` ```simproc_setup natless_cancel_numerals ``` huffman@45436 ` 216` ``` ("(l::nat) + m < n" | "(l::nat) < m + n" | ``` huffman@45436 ` 217` ``` "(l::nat) * m < n" | "(l::nat) < m * n" | ``` huffman@45436 ` 218` ``` "Suc m < n" | "m < Suc n") = ``` huffman@45436 ` 219` ``` {* fn phi => Nat_Numeral_Simprocs.less_cancel_numerals *} ``` huffman@45436 ` 220` huffman@45436 ` 221` ```simproc_setup natle_cancel_numerals ``` huffman@45436 ` 222` ``` ("(l::nat) + m \ n" | "(l::nat) \ m + n" | ``` huffman@45436 ` 223` ``` "(l::nat) * m \ n" | "(l::nat) \ m * n" | ``` huffman@45436 ` 224` ``` "Suc m \ n" | "m \ Suc n") = ``` huffman@45436 ` 225` ``` {* fn phi => Nat_Numeral_Simprocs.le_cancel_numerals *} ``` huffman@45436 ` 226` huffman@45436 ` 227` ```simproc_setup natdiff_cancel_numerals ``` huffman@45436 ` 228` ``` ("((l::nat) + m) - n" | "(l::nat) - (m + n)" | ``` huffman@45436 ` 229` ``` "(l::nat) * m - n" | "(l::nat) - m * n" | ``` huffman@45436 ` 230` ``` "Suc m - n" | "m - Suc n") = ``` huffman@45436 ` 231` ``` {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *} ``` huffman@45436 ` 232` huffman@45463 ` 233` ```simproc_setup nat_eq_cancel_numeral_factor ``` huffman@45463 ` 234` ``` ("(l::nat) * m = n" | "(l::nat) = m * n") = ``` huffman@45463 ` 235` ``` {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *} ``` huffman@45463 ` 236` huffman@45463 ` 237` ```simproc_setup nat_less_cancel_numeral_factor ``` huffman@45463 ` 238` ``` ("(l::nat) * m < n" | "(l::nat) < m * n") = ``` huffman@45463 ` 239` ``` {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *} ``` huffman@45463 ` 240` huffman@45463 ` 241` ```simproc_setup nat_le_cancel_numeral_factor ``` huffman@45463 ` 242` ``` ("(l::nat) * m <= n" | "(l::nat) <= m * n") = ``` huffman@45463 ` 243` ``` {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *} ``` huffman@45463 ` 244` huffman@45463 ` 245` ```simproc_setup nat_div_cancel_numeral_factor ``` huffman@45463 ` 246` ``` ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = ``` huffman@45463 ` 247` ``` {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *} ``` huffman@45463 ` 248` huffman@45463 ` 249` ```simproc_setup nat_dvd_cancel_numeral_factor ``` huffman@45463 ` 250` ``` ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = ``` huffman@45463 ` 251` ``` {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *} ``` huffman@45463 ` 252` huffman@45462 ` 253` ```simproc_setup nat_eq_cancel_factor ``` huffman@45462 ` 254` ``` ("(l::nat) * m = n" | "(l::nat) = m * n") = ``` huffman@45462 ` 255` ``` {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *} ``` huffman@45462 ` 256` huffman@45462 ` 257` ```simproc_setup nat_less_cancel_factor ``` huffman@45462 ` 258` ``` ("(l::nat) * m < n" | "(l::nat) < m * n") = ``` huffman@45462 ` 259` ``` {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *} ``` huffman@45462 ` 260` huffman@45462 ` 261` ```simproc_setup nat_le_cancel_factor ``` huffman@45462 ` 262` ``` ("(l::nat) * m <= n" | "(l::nat) <= m * n") = ``` huffman@45462 ` 263` ``` {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *} ``` huffman@45462 ` 264` huffman@45463 ` 265` ```simproc_setup nat_div_cancel_factor ``` huffman@45462 ` 266` ``` ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = ``` huffman@45463 ` 267` ``` {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *} ``` huffman@45462 ` 268` huffman@45462 ` 269` ```simproc_setup nat_dvd_cancel_factor ``` huffman@45462 ` 270` ``` ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = ``` huffman@45462 ` 271` ``` {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *} ``` huffman@45462 ` 272` haftmann@33366 ` 273` ```declaration {* ``` haftmann@33366 ` 274` ``` K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]) ``` haftmann@33366 ` 275` ``` #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, ``` haftmann@33366 ` 276` ``` @{thm nat_0}, @{thm nat_1}, ``` haftmann@33366 ` 277` ``` @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of}, ``` haftmann@33366 ` 278` ``` @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less}, ``` haftmann@33366 ` 279` ``` @{thm le_Suc_number_of}, @{thm le_number_of_Suc}, ``` haftmann@33366 ` 280` ``` @{thm less_Suc_number_of}, @{thm less_number_of_Suc}, ``` haftmann@33366 ` 281` ``` @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, ``` haftmann@33366 ` 282` ``` @{thm mult_Suc}, @{thm mult_Suc_right}, ``` haftmann@33366 ` 283` ``` @{thm add_Suc}, @{thm add_Suc_right}, ``` haftmann@33366 ` 284` ``` @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, ``` haftmann@33366 ` 285` ``` @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, ``` haftmann@33366 ` 286` ``` @{thm if_True}, @{thm if_False}]) ``` huffman@45284 ` 287` ``` #> Lin_Arith.add_simprocs ``` huffman@45284 ` 288` ``` [@{simproc semiring_assoc_fold}, ``` huffman@45284 ` 289` ``` @{simproc int_combine_numerals}, ``` huffman@45284 ` 290` ``` @{simproc inteq_cancel_numerals}, ``` huffman@45284 ` 291` ``` @{simproc intless_cancel_numerals}, ``` huffman@45284 ` 292` ``` @{simproc intle_cancel_numerals}] ``` huffman@45436 ` 293` ``` #> Lin_Arith.add_simprocs ``` huffman@45462 ` 294` ``` [@{simproc nat_combine_numerals}, ``` huffman@45436 ` 295` ``` @{simproc nateq_cancel_numerals}, ``` huffman@45436 ` 296` ``` @{simproc natless_cancel_numerals}, ``` huffman@45436 ` 297` ``` @{simproc natle_cancel_numerals}, ``` huffman@45436 ` 298` ``` @{simproc natdiff_cancel_numerals}]) ``` haftmann@33366 ` 299` ```*} ``` haftmann@33366 ` 300` haftmann@37886 ` 301` ```end ```