# Notes on Isabelle/HOL Simprocs

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}
```
• Groups.abel_cancel_sum:
```   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')
```

```    #(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
);
```
• 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)
```