Isabelle/HOL provides a large collection of arithmetic simplification procedures (simprocs). The purpose of this page is to list existing simprocs, describe what they are supposed to do, and show how they work. This page will also contain notes on some planned changes to the cancellation simprocs.

Groups.thy

Abelian group simprocs

[ Tools/abel_cancel.ML ]

Groups.abel_cancel_relation:

   a <= b {ordered_ab_group_add}
   a < b  {ordered_ab_group_add}
   c = d  {ab_group_add}

Groups.abel_cancel_sum:

   a - b  {ab_group_add}
   a + b  {ab_group_add}

Decompose each side into a sum of terms with signs:

 (bool * term) list

If a common term is found (with opposite signs, if op is "+") then those terms will be replaced with 0.

Proof step 1. Apply one of these rules, if one matches:

 diff_eq_diff_less: "a - b = c - d ==> (a < b) = (c < d)"
 diff_eq_diff_less_eq: "a - b = c - d ==> (a <= b) = (c <= d)"
 diff_eq_diff_eq: "a - b = c - d ==> (a = b) = (c = d)"

Proof step 2. Simplify with custom simpset to normalize equations. (push negations, use permutative ac rewriting on +)

Numeral_Simprocs.thy

Associative folding of numerals

[ Provers/Arith/assoc_fold.ML ]

semiring_assoc_fold: {comm_semiring_1_cancel}

   a * b

If terms "a" and "b" both contain numerals, the simproc regroups all the numerals at the front.

Numeral-cancellation simprocs

[ Provers/Arith/cancel_numeral_factor.ML ] functor CancelNumeralFactorFun

Cancel common coefficients in balanced expressions:

    u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'

where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) and d = gcd(m,m') and n=m/d and n'=m'/d.

It works by (a) massaging both sides to bring gcd(m,m') to the front:

    u*#m ~~ u'*#m'  ==  #d*(#n*u) ~~ #d*(#n'*u')

(b) then using the rule "cancel" to reach #n*u ~~ #n'*u'.

int_div_cancel_numeral_factors: {semiring_div,number_ring}

   l div (m * n),  (l * m) div n
 div_mult_mult1: "c ~= 0 ==> (c * a) div (c * b) = a div b"

divide_cancel_numeral_factor: {field_inverse_zero,number_ring}

   l / (m * n),  number_of v / number_of w,  (l * m) / n
 mult_divide_mult_cancel_left: "c ~= 0 ==> (c * a) / (c * b) = a / b"

ring_eq_cancel_numeral_factor: {number_ring,idom}

   l = m * n,  l * m = n
 mult_cancel_left: "(c * a = c * b) = (c = 0 \/ a = b)

ring_less_cancel_numeral_factor: {number_ring,linordered_idom}

   l < m * n,  l * m < n
 mult_less_cancel_left:
   "(c * a < c * b) = ((0 <= c --> a < b) /\ (c <= 0 --> b < a))"

ring_le_cancel_numeral_factor: {number_ring,linordered_idom}

   l <= m * n,  l * m <= n
 mult_le_cancel_left:
   "(c * a <= c * b) = ((0 < c --> a <= b) /\ (c < 0 --> b <= a))"

Extract common term

[ Provers/Arith/extract_common_term.ML ] functor ExtractCommonTermFun

Extract common terms in balanced expressions:

    i + u + j ~~ i' + u + j'  ==  u + (i + j) ~~ u + (i' + j')
    i + u     ~~ u            ==  u + i       ~~ u + 0

where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a suitable identity for +.

This massaged formula is then simplified in a user-specified way.

ring_eq_cancel_factor: {idom}

   l = m * n,   l * m = n
 mult_cancel_left: "(c * a = c * b) = (c = 0 \/ a = b)

linordered_ring_le_cancel_factor: {linordered_idom}

   l <= m * n,  l * m <= n
 mult_le_cancel_left_pos: "0 < c ==> (c * a <= c * b) = (a <= b)"
 mult_le_cancel_left_neg: "c < 0 ==> (c * a <= c * b) = (b <= a)"

linordered_ring_less_cancel_factor: {linordered_idom}

   l < m * n,   l * m < n
 mult_less_cancel_left_pos: "0 < c ==> (c * a < c * b) = (a < b)"
 mult_less_cancel_left_neg: "c < 0 ==> (c * a < c * b) = (b < a)"

int_div_cancel_factor: {semiring_div}

   l div (m * n),  (l * m) div n
 div_mult_mult1_if: "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"

int_mod_cancel_factor: {semiring_div}

   l mod (m * n),  (l * m) mod n
 mod_mult_mult1: "(c * a) mod (c * b) = c * (a mod b)"

dvd_cancel_factor: {idom}

   l dvd (m * n),  (l * m) dvd n
 dvd_mult_cancel_left: "(c * a dvd c * b) = (c = 0 \/ a dvd b)"

divide_cancel_factor: {field_inverse_zero}

   l / (m * n),  (l * m) / n
 mult_divide_mult_cancel_left_if:
   "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"

TODO: Data.prove_conv and Data.norm_tac are each only used once, in "Data.prove_conv [Data.norm_tac ss]". Why not combine these?

Proof step 1: Prove cancellation rule "simp_th" of the form "(u + _ ~~ u + _) = ..." using Data.simp_conv (may depend on the value of "u").

Proof step 2: Prove reshaping rule "reshape" of the form "(i + u + j ~~ i' + u + j') = (u + (i + j) ~~ u + (i' + j'))" using Data.prove_conv/Data.norm_tac. (Arith_Data.prove_conv)

Proof step 2:

Numeral cancellation

[ Provers/Arith/cancel_numerals.ML ] functor CancelNumeralsFun

Cancel common coefficients in balanced expressions:

    i + #m*u + j ~~ i' + #m'*u + j'  ==  #(m-m')*u + i + j ~~ i' + j'

where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).

It works by (a) massaging both sides to bring the selected term to the front:

    #m*u + (i + j) ~~ #m'*u + (i' + j')

(b) then using bal_add1 or bal_add2 to reach

    #(m-m')*u + i + j ~~ i' + j'       (if m'<=m)

or

    i + j ~~ #(m'-m)*u + i' + j'       (otherwise)

inteq_cancel_numerals: {number_ring}

   l = m * n,  l = m - n,  l = m + n
   l * m = n,  l - m = n,  l + m = n
 eq_add_iff1: "(a * e + c = b * e + d) = ((a - b) * e + c = d)"
 eq_add_iff2: "(a * e + c = b * e + d) = (c = (b - a) * e + d)"

intless_cancel_numerals: {number_ring,linordered_idom}

   l < m * n,  l < m - n,  l < m + n
   l * m < n,  l - m < n,  l + m < n
 less_add_iff1: "(a * e + c < b * e + d) = ((a - b) * e + c < d)"
 less_add_iff2: "(a * e + c < b * e + d) = (c < (b - a) * e + d)"

intle_cancel_numerals: {number_ring,linordered_idom}

   l <= m * n,  l <= m - n,  l <= m + n
   l * m <= n,  l - m <= n,  l + m <= n
 le_add_iff1: "(a * e + c <= b * e + d) = ((a - b) * e + c <= d)"
 le_add_iff2: "(a * e + c <= b * e + d) = (c <= (b - a) * e + d)"

Combining numerals

[ Provers/Arith/combine_numerals.ML ] functor CombineNumeralsFun

Combine coefficients in expressions:

    i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))

It works by (a) massaging the sum to bring the selected terms to the front:

    #m*u + (#n*u + (i + (j + k)))

(b) then using left_distrib to reach

    #(m+n)*u + (i + (j + k))

field_combine_numerals: {field_inverse_zero,number_ring}

   i - j,  i + j

int_combine_numerals: {number_ring}

   i - j,  i + j

Cancel numerals

structure LeCancelNumerals = CancelNumeralsFun
 (open CancelNumeralsCommon
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
  val bal_add1 = @{thm le_add_iff1} RS trans
  val bal_add2 = @{thm le_add_iff2} RS trans
);

nat_combine_numerals:

   Suc ((i) + (j))
   (i) + (j)

nat_divide_cancel_factor:

   (l) div ((m) * (n))
   (l) * (m) div (n)

nat_dvd_cancel_factor:

   (l) dvd (m) * (n)
   (l) * (m) dvd (n)

nat_eq_cancel_factor:

   (l) = (m) * (n)
   (l) * (m) = (n)

nat_le_cancel_factor:

   (l) <= (m) * (n)
   (l) * (m) <= (n)

nat_less_cancel_factor:

   (l) < (m) * (n)
   (l) * (m) < (n)

natdiff_cancel_numerals:

   (m) - Suc (n)
   (l) - (m) * (n)
   (l) - ((m) + (n))
   Suc (m) - (n)
   (l) * (m) - (n)
   (l) + (m) - (n)

natdiff_cancel_sums:

   (m) - Suc (n)
   (l) - ((m) + (n))
   Suc (m) - (n)
   (l) + (m) - (n)

natdiv_cancel_numeral_factors:

   (l) div ((m) * (n))
   (l) * (m) div (n)

natdvd_cancel_numeral_factors:

   (l) dvd (m) * (n)
   (l) * (m) dvd (n)

nateq_cancel_numeral_factors:

   (l) = (m) * (n)
   (l) * (m) = (n)

nateq_cancel_numerals:

   (m) = Suc (n)
   (l) = (m) * (n)
   (l) = (m) + (n)
   Suc (m) = (n)
   (l) * (m) = (n)
   (l) + (m) = (n)

nateq_cancel_sums:

   (m) = Suc (n)
   (l) = (m) + (n)
   Suc (m) = (n)
   (l) + (m) = (n)

natle_cancel_numeral_factors:

   (l) <= (m) * (n)
   (l) * (m) <= (n)

natle_cancel_numerals:

   (m) <= Suc (n)
   (l) <= (m) * (n)
   (l) <= (m) + (n)
   Suc (m) <= (n)
   (l) * (m) <= (n)
   (l) + (m) <= (n)

natle_cancel_sums:

   (m) <= Suc (n)
   (l) <= (m) + (n)
   Suc (m) <= (n)
   (l) + (m) <= (n)

natless_cancel_numeral_factors:

   (l) < (m) * (n)
   (l) * (m) < (n)

natless_cancel_numerals:

   (m) < Suc (n)
   (l) < (m) * (n)
   (l) < (m) + (n)
   Suc (m) < (n)
   (l) * (m) < (n)
   (l) + (m) < (n)

natless_cancel_sums:

   (m) < Suc (n)
   (l) < (m) + (n)
   Suc (m) < (n)
   (l) + (m) < (n)

Notes on Isabelle/HOL Simprocs

Contents