[isabelle-dev] Problem with simproc enat_eq_cancel

[Brian Huffman]

On Wed, Mar 6, 2013 at 7:18 AM, Makarius <makarius at sketis.net> wrote:
> On Fri, 1 Mar 2013, Andreas Lochbihler wrote:
>> *** Proof failed.
>> *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b))
>> ***  1. (a + b - 1 = b + (a - 1)) = (a + (b + - 1) = a + (b + - 1))
>> *** The error(s) above occurred for the goal statement:
>> *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b))
>> *** At command "apply"
>>
>> The simp trace with simp_debug enabled ends as follows:
>>
>> [1]Trying procedure "Extended_Nat.enat_eq_cancel" on:
>> a + b - 1 = a - 1 + b
>>
>> simp_trace_depth_limit exceeded!
>
>
> These simprocs were introduced by Brian Huffman here:
>
> changeset:   45775:6c340de26a0d
> user:        huffman
> date:        Wed Dec 07 10:50:30 2011 +0100
> files:       src/HOL/Library/Extended_Nat.thy
> description:
> add cancellation simprocs for type enat
>
>
> We should Brian give time to comment on it (there is no need for real-time
> reactivity on isabelle-dev).

I just pushed a changeset to testboard that should fix the problem
(abdcf1a7cabf). The issue was that the enat simprocs used the library
function Arith_Data.dest_sum : term -> term list to split sums; it
treats subtraction "x - y" as equivalent to "x + - y", which is not
valid for enat.

> He did all these renovations of the old
> simprocs, and this one seems to be derived from the same tradition.

Actually, the enat cancellation simprocs are not done in my new
conversion-based style; these are just new instances of Larry's old
extract-common-term simproc functor
(Provers/Arith/extract_common_term.ML).

- Brian