src/HOL/Numeral_Simprocs.thy
 author wenzelm Thu May 24 17:25:53 2012 +0200 (2012-05-24) changeset 47988 e4b69e10b990 parent 47255 30a1692557b0 child 48891 c0eafbd55de3 permissions -rw-r--r--
tuned proofs;
 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` huffman@47255 ` 17` ```lemmas semiring_norm = ``` huffman@47255 ` 18` ``` Let_def arith_simps nat_arith rel_simps ``` huffman@47255 ` 19` ``` if_False if_True ``` huffman@47255 ` 20` ``` add_0 add_Suc add_numeral_left ``` huffman@47255 ` 21` ``` add_neg_numeral_left mult_numeral_left ``` huffman@47255 ` 22` ``` numeral_1_eq_1 [symmetric] Suc_eq_plus1 ``` huffman@47255 ` 23` ``` eq_numeral_iff_iszero not_iszero_Numeral1 ``` huffman@47255 ` 24` huffman@47108 ` 25` ```declare split_div [of _ _ "numeral k", arith_split] for k ``` huffman@47108 ` 26` ```declare split_mod [of _ _ "numeral k", arith_split] for k ``` haftmann@33366 ` 27` haftmann@33366 ` 28` ```text {* For @{text combine_numerals} *} ``` haftmann@33366 ` 29` haftmann@33366 ` 30` ```lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)" ``` haftmann@33366 ` 31` ```by (simp add: add_mult_distrib) ``` haftmann@33366 ` 32` haftmann@33366 ` 33` ```text {* For @{text cancel_numerals} *} ``` haftmann@33366 ` 34` haftmann@33366 ` 35` ```lemma nat_diff_add_eq1: ``` haftmann@33366 ` 36` ``` "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)" ``` haftmann@33366 ` 37` ```by (simp split add: nat_diff_split add: add_mult_distrib) ``` haftmann@33366 ` 38` haftmann@33366 ` 39` ```lemma nat_diff_add_eq2: ``` haftmann@33366 ` 40` ``` "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))" ``` haftmann@33366 ` 41` ```by (simp split add: nat_diff_split add: add_mult_distrib) ``` haftmann@33366 ` 42` haftmann@33366 ` 43` ```lemma nat_eq_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_eq_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_less_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_less_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` ```lemma nat_le_add_iff1: ``` haftmann@33366 ` 60` ``` "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)" ``` haftmann@33366 ` 61` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 62` haftmann@33366 ` 63` ```lemma nat_le_add_iff2: ``` haftmann@33366 ` 64` ``` "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)" ``` haftmann@33366 ` 65` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 66` haftmann@33366 ` 67` ```text {* For @{text cancel_numeral_factors} *} ``` haftmann@33366 ` 68` haftmann@33366 ` 69` ```lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)" ``` haftmann@33366 ` 70` ```by auto ``` haftmann@33366 ` 71` haftmann@33366 ` 72` ```lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m (k*m = k*n) = (m=n)" ``` haftmann@33366 ` 76` ```by auto ``` haftmann@33366 ` 77` haftmann@33366 ` 78` ```lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)" ``` haftmann@33366 ` 79` ```by auto ``` haftmann@33366 ` 80` haftmann@33366 ` 81` ```lemma nat_mult_dvd_cancel_disj[simp]: ``` haftmann@33366 ` 82` ``` "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))" ``` huffman@47159 ` 83` ```by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1) ``` haftmann@33366 ` 84` haftmann@33366 ` 85` ```lemma nat_mult_dvd_cancel1: "0 < k \ (k*m) dvd (k*n::nat) = (m dvd n)" ``` haftmann@33366 ` 86` ```by(auto) ``` haftmann@33366 ` 87` haftmann@33366 ` 88` ```text {* For @{text cancel_factor} *} ``` haftmann@33366 ` 89` haftmann@33366 ` 90` ```lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)" ``` haftmann@33366 ` 91` ```by auto ``` haftmann@33366 ` 92` haftmann@33366 ` 93` ```lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m Numeral_Simprocs.assoc_fold *} ``` huffman@45284 ` 108` huffman@47108 ` 109` ```(* TODO: see whether the type class can be generalized further *) ``` huffman@45284 ` 110` ```simproc_setup int_combine_numerals ``` huffman@47108 ` 111` ``` ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") = ``` huffman@45284 ` 112` ``` {* fn phi => Numeral_Simprocs.combine_numerals *} ``` huffman@45284 ` 113` huffman@45284 ` 114` ```simproc_setup field_combine_numerals ``` huffman@47108 ` 115` ``` ("(i::'a::{field_inverse_zero,ring_char_0}) + j" ``` huffman@47108 ` 116` ``` |"(i::'a::{field_inverse_zero,ring_char_0}) - j") = ``` huffman@45284 ` 117` ``` {* fn phi => Numeral_Simprocs.field_combine_numerals *} ``` huffman@45284 ` 118` huffman@45284 ` 119` ```simproc_setup inteq_cancel_numerals ``` huffman@47108 ` 120` ``` ("(l::'a::comm_ring_1) + m = n" ``` huffman@47108 ` 121` ``` |"(l::'a::comm_ring_1) = m + n" ``` huffman@47108 ` 122` ``` |"(l::'a::comm_ring_1) - m = n" ``` huffman@47108 ` 123` ``` |"(l::'a::comm_ring_1) = m - n" ``` huffman@47108 ` 124` ``` |"(l::'a::comm_ring_1) * m = n" ``` huffman@47108 ` 125` ``` |"(l::'a::comm_ring_1) = m * n" ``` huffman@47108 ` 126` ``` |"- (l::'a::comm_ring_1) = m" ``` huffman@47108 ` 127` ``` |"(l::'a::comm_ring_1) = - m") = ``` huffman@45284 ` 128` ``` {* fn phi => Numeral_Simprocs.eq_cancel_numerals *} ``` huffman@45284 ` 129` huffman@45284 ` 130` ```simproc_setup intless_cancel_numerals ``` huffman@47108 ` 131` ``` ("(l::'a::linordered_idom) + m < n" ``` huffman@47108 ` 132` ``` |"(l::'a::linordered_idom) < m + n" ``` huffman@47108 ` 133` ``` |"(l::'a::linordered_idom) - m < n" ``` huffman@47108 ` 134` ``` |"(l::'a::linordered_idom) < m - n" ``` huffman@47108 ` 135` ``` |"(l::'a::linordered_idom) * m < n" ``` huffman@47108 ` 136` ``` |"(l::'a::linordered_idom) < m * n" ``` huffman@47108 ` 137` ``` |"- (l::'a::linordered_idom) < m" ``` huffman@47108 ` 138` ``` |"(l::'a::linordered_idom) < - m") = ``` huffman@45284 ` 139` ``` {* fn phi => Numeral_Simprocs.less_cancel_numerals *} ``` huffman@45284 ` 140` huffman@45284 ` 141` ```simproc_setup intle_cancel_numerals ``` huffman@47108 ` 142` ``` ("(l::'a::linordered_idom) + m \ n" ``` huffman@47108 ` 143` ``` |"(l::'a::linordered_idom) \ m + n" ``` huffman@47108 ` 144` ``` |"(l::'a::linordered_idom) - m \ n" ``` huffman@47108 ` 145` ``` |"(l::'a::linordered_idom) \ m - n" ``` huffman@47108 ` 146` ``` |"(l::'a::linordered_idom) * m \ n" ``` huffman@47108 ` 147` ``` |"(l::'a::linordered_idom) \ m * n" ``` huffman@47108 ` 148` ``` |"- (l::'a::linordered_idom) \ m" ``` huffman@47108 ` 149` ``` |"(l::'a::linordered_idom) \ - m") = ``` huffman@45284 ` 150` ``` {* fn phi => Numeral_Simprocs.le_cancel_numerals *} ``` huffman@45284 ` 151` huffman@45284 ` 152` ```simproc_setup ring_eq_cancel_numeral_factor ``` huffman@47108 ` 153` ``` ("(l::'a::{idom,ring_char_0}) * m = n" ``` huffman@47108 ` 154` ``` |"(l::'a::{idom,ring_char_0}) = m * n") = ``` huffman@45284 ` 155` ``` {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *} ``` huffman@45284 ` 156` huffman@45284 ` 157` ```simproc_setup ring_less_cancel_numeral_factor ``` huffman@47108 ` 158` ``` ("(l::'a::linordered_idom) * m < n" ``` huffman@47108 ` 159` ``` |"(l::'a::linordered_idom) < m * n") = ``` huffman@45284 ` 160` ``` {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *} ``` huffman@45284 ` 161` huffman@45284 ` 162` ```simproc_setup ring_le_cancel_numeral_factor ``` huffman@47108 ` 163` ``` ("(l::'a::linordered_idom) * m <= n" ``` huffman@47108 ` 164` ``` |"(l::'a::linordered_idom) <= m * n") = ``` huffman@45284 ` 165` ``` {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *} ``` huffman@45284 ` 166` huffman@47108 ` 167` ```(* TODO: remove comm_ring_1 constraint if possible *) ``` huffman@45284 ` 168` ```simproc_setup int_div_cancel_numeral_factors ``` huffman@47108 ` 169` ``` ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n" ``` huffman@47108 ` 170` ``` |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") = ``` huffman@45284 ` 171` ``` {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *} ``` huffman@45284 ` 172` huffman@45284 ` 173` ```simproc_setup divide_cancel_numeral_factor ``` huffman@47108 ` 174` ``` ("((l::'a::{field_inverse_zero,ring_char_0}) * m) / n" ``` huffman@47108 ` 175` ``` |"(l::'a::{field_inverse_zero,ring_char_0}) / (m * n)" ``` huffman@47108 ` 176` ``` |"((numeral v)::'a::{field_inverse_zero,ring_char_0}) / (numeral w)") = ``` huffman@45284 ` 177` ``` {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *} ``` huffman@45284 ` 178` huffman@45284 ` 179` ```simproc_setup ring_eq_cancel_factor ``` huffman@45284 ` 180` ``` ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") = ``` huffman@45284 ` 181` ``` {* fn phi => Numeral_Simprocs.eq_cancel_factor *} ``` huffman@45284 ` 182` huffman@45284 ` 183` ```simproc_setup linordered_ring_le_cancel_factor ``` huffman@45296 ` 184` ``` ("(l::'a::linordered_idom) * m <= n" ``` huffman@45296 ` 185` ``` |"(l::'a::linordered_idom) <= m * n") = ``` huffman@45284 ` 186` ``` {* fn phi => Numeral_Simprocs.le_cancel_factor *} ``` huffman@45284 ` 187` huffman@45284 ` 188` ```simproc_setup linordered_ring_less_cancel_factor ``` huffman@45296 ` 189` ``` ("(l::'a::linordered_idom) * m < n" ``` huffman@45296 ` 190` ``` |"(l::'a::linordered_idom) < m * n") = ``` huffman@45284 ` 191` ``` {* fn phi => Numeral_Simprocs.less_cancel_factor *} ``` huffman@45284 ` 192` huffman@45284 ` 193` ```simproc_setup int_div_cancel_factor ``` huffman@45284 ` 194` ``` ("((l::'a::semiring_div) * m) div n" ``` huffman@45284 ` 195` ``` |"(l::'a::semiring_div) div (m * n)") = ``` huffman@45284 ` 196` ``` {* fn phi => Numeral_Simprocs.div_cancel_factor *} ``` huffman@45284 ` 197` huffman@45284 ` 198` ```simproc_setup int_mod_cancel_factor ``` huffman@45284 ` 199` ``` ("((l::'a::semiring_div) * m) mod n" ``` huffman@45284 ` 200` ``` |"(l::'a::semiring_div) mod (m * n)") = ``` huffman@45284 ` 201` ``` {* fn phi => Numeral_Simprocs.mod_cancel_factor *} ``` huffman@45284 ` 202` huffman@45284 ` 203` ```simproc_setup dvd_cancel_factor ``` huffman@45284 ` 204` ``` ("((l::'a::idom) * m) dvd n" ``` huffman@45284 ` 205` ``` |"(l::'a::idom) dvd (m * n)") = ``` huffman@45284 ` 206` ``` {* fn phi => Numeral_Simprocs.dvd_cancel_factor *} ``` huffman@45284 ` 207` huffman@45284 ` 208` ```simproc_setup divide_cancel_factor ``` huffman@45284 ` 209` ``` ("((l::'a::field_inverse_zero) * m) / n" ``` huffman@45284 ` 210` ``` |"(l::'a::field_inverse_zero) / (m * n)") = ``` huffman@45284 ` 211` ``` {* fn phi => Numeral_Simprocs.divide_cancel_factor *} ``` huffman@45284 ` 212` haftmann@33366 ` 213` ```use "Tools/nat_numeral_simprocs.ML" ``` haftmann@33366 ` 214` huffman@45462 ` 215` ```simproc_setup nat_combine_numerals ``` huffman@45462 ` 216` ``` ("(i::nat) + j" | "Suc (i + j)") = ``` huffman@45462 ` 217` ``` {* fn phi => Nat_Numeral_Simprocs.combine_numerals *} ``` huffman@45462 ` 218` huffman@45436 ` 219` ```simproc_setup nateq_cancel_numerals ``` huffman@45436 ` 220` ``` ("(l::nat) + m = n" | "(l::nat) = m + n" | ``` huffman@45436 ` 221` ``` "(l::nat) * m = n" | "(l::nat) = m * n" | ``` huffman@45436 ` 222` ``` "Suc m = n" | "m = Suc n") = ``` huffman@45436 ` 223` ``` {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals *} ``` huffman@45436 ` 224` huffman@45436 ` 225` ```simproc_setup natless_cancel_numerals ``` huffman@45436 ` 226` ``` ("(l::nat) + m < n" | "(l::nat) < m + n" | ``` huffman@45436 ` 227` ``` "(l::nat) * m < n" | "(l::nat) < m * n" | ``` huffman@45436 ` 228` ``` "Suc m < n" | "m < Suc n") = ``` huffman@45436 ` 229` ``` {* fn phi => Nat_Numeral_Simprocs.less_cancel_numerals *} ``` huffman@45436 ` 230` huffman@45436 ` 231` ```simproc_setup natle_cancel_numerals ``` huffman@45436 ` 232` ``` ("(l::nat) + m \ n" | "(l::nat) \ m + n" | ``` huffman@45436 ` 233` ``` "(l::nat) * m \ n" | "(l::nat) \ m * n" | ``` huffman@45436 ` 234` ``` "Suc m \ n" | "m \ Suc n") = ``` huffman@45436 ` 235` ``` {* fn phi => Nat_Numeral_Simprocs.le_cancel_numerals *} ``` huffman@45436 ` 236` huffman@45436 ` 237` ```simproc_setup natdiff_cancel_numerals ``` huffman@45436 ` 238` ``` ("((l::nat) + m) - n" | "(l::nat) - (m + n)" | ``` huffman@45436 ` 239` ``` "(l::nat) * m - n" | "(l::nat) - m * n" | ``` huffman@45436 ` 240` ``` "Suc m - n" | "m - Suc n") = ``` huffman@45436 ` 241` ``` {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *} ``` huffman@45436 ` 242` huffman@45463 ` 243` ```simproc_setup nat_eq_cancel_numeral_factor ``` huffman@45463 ` 244` ``` ("(l::nat) * m = n" | "(l::nat) = m * n") = ``` huffman@45463 ` 245` ``` {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *} ``` huffman@45463 ` 246` huffman@45463 ` 247` ```simproc_setup nat_less_cancel_numeral_factor ``` huffman@45463 ` 248` ``` ("(l::nat) * m < n" | "(l::nat) < m * n") = ``` huffman@45463 ` 249` ``` {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *} ``` huffman@45463 ` 250` huffman@45463 ` 251` ```simproc_setup nat_le_cancel_numeral_factor ``` huffman@45463 ` 252` ``` ("(l::nat) * m <= n" | "(l::nat) <= m * n") = ``` huffman@45463 ` 253` ``` {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *} ``` huffman@45463 ` 254` huffman@45463 ` 255` ```simproc_setup nat_div_cancel_numeral_factor ``` huffman@45463 ` 256` ``` ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = ``` huffman@45463 ` 257` ``` {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *} ``` huffman@45463 ` 258` huffman@45463 ` 259` ```simproc_setup nat_dvd_cancel_numeral_factor ``` huffman@45463 ` 260` ``` ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = ``` huffman@45463 ` 261` ``` {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *} ``` huffman@45463 ` 262` huffman@45462 ` 263` ```simproc_setup nat_eq_cancel_factor ``` huffman@45462 ` 264` ``` ("(l::nat) * m = n" | "(l::nat) = m * n") = ``` huffman@45462 ` 265` ``` {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *} ``` huffman@45462 ` 266` huffman@45462 ` 267` ```simproc_setup nat_less_cancel_factor ``` huffman@45462 ` 268` ``` ("(l::nat) * m < n" | "(l::nat) < m * n") = ``` huffman@45462 ` 269` ``` {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *} ``` huffman@45462 ` 270` huffman@45462 ` 271` ```simproc_setup nat_le_cancel_factor ``` huffman@45462 ` 272` ``` ("(l::nat) * m <= n" | "(l::nat) <= m * n") = ``` huffman@45462 ` 273` ``` {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *} ``` huffman@45462 ` 274` huffman@45463 ` 275` ```simproc_setup nat_div_cancel_factor ``` huffman@45462 ` 276` ``` ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = ``` huffman@45463 ` 277` ``` {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *} ``` huffman@45462 ` 278` huffman@45462 ` 279` ```simproc_setup nat_dvd_cancel_factor ``` huffman@45462 ` 280` ``` ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = ``` huffman@45462 ` 281` ``` {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *} ``` huffman@45462 ` 282` huffman@47108 ` 283` ```(* FIXME: duplicate rule warnings for: ``` huffman@47108 ` 284` ``` ring_distribs ``` huffman@47108 ` 285` ``` numeral_plus_numeral numeral_times_numeral ``` huffman@47108 ` 286` ``` numeral_eq_iff numeral_less_iff numeral_le_iff ``` huffman@47108 ` 287` ``` numeral_neq_zero zero_neq_numeral zero_less_numeral ``` huffman@47108 ` 288` ``` if_True if_False *) ``` haftmann@33366 ` 289` ```declaration {* ``` huffman@47108 ` 290` ``` K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}]) ``` huffman@47108 ` 291` ``` #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1}, ``` haftmann@33366 ` 292` ``` @{thm nat_0}, @{thm nat_1}, ``` huffman@47108 ` 293` ``` @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral}, ``` huffman@47108 ` 294` ``` @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff}, ``` huffman@47108 ` 295` ``` @{thm le_Suc_numeral}, @{thm le_numeral_Suc}, ``` huffman@47108 ` 296` ``` @{thm less_Suc_numeral}, @{thm less_numeral_Suc}, ``` huffman@47108 ` 297` ``` @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc}, ``` haftmann@33366 ` 298` ``` @{thm mult_Suc}, @{thm mult_Suc_right}, ``` haftmann@33366 ` 299` ``` @{thm add_Suc}, @{thm add_Suc_right}, ``` huffman@47108 ` 300` ``` @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral}, ``` huffman@47108 ` 301` ``` @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral}, ``` haftmann@33366 ` 302` ``` @{thm if_True}, @{thm if_False}]) ``` huffman@45284 ` 303` ``` #> Lin_Arith.add_simprocs ``` huffman@45284 ` 304` ``` [@{simproc semiring_assoc_fold}, ``` huffman@45284 ` 305` ``` @{simproc int_combine_numerals}, ``` huffman@45284 ` 306` ``` @{simproc inteq_cancel_numerals}, ``` huffman@45284 ` 307` ``` @{simproc intless_cancel_numerals}, ``` huffman@45284 ` 308` ``` @{simproc intle_cancel_numerals}] ``` huffman@45436 ` 309` ``` #> Lin_Arith.add_simprocs ``` huffman@45462 ` 310` ``` [@{simproc nat_combine_numerals}, ``` huffman@45436 ` 311` ``` @{simproc nateq_cancel_numerals}, ``` huffman@45436 ` 312` ``` @{simproc natless_cancel_numerals}, ``` huffman@45436 ` 313` ``` @{simproc natle_cancel_numerals}, ``` huffman@45436 ` 314` ``` @{simproc natdiff_cancel_numerals}]) ``` haftmann@33366 ` 315` ```*} ``` haftmann@33366 ` 316` haftmann@37886 ` 317` ```end ```