[isabelle-dev] Problem with simproc enat_eq_cancel

[Makarius]

On Fri, 1 Mar 2013, Andreas Lochbihler wrote:

> theory Scratch imports
>  "~~/src/HOL/Library/Extended_Nat"
> begin
>
> definition epred :: "enat => enat"
> where "epred n = n - 1"
>
> lemma epred_iadd1: "a ~= 0 ==> epred (a + b) = epred a + b"
> apply(simp add: epred_def)
>
> I would have expected that the call to simp at least unfolds epred_def, but 
> it raises the following error:
>
> *** 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).  He did all these renovations of the old 
simprocs, and this one seems to be derived from the same tradition.

At the bottom of the ML sources, I recognize slightly odd things that I 
did myself in the mid 1990-ies, together with Larry.  So in the worst 
case, I will look again eventually.


> By the way, why does the failure in the simproc yield a proof error at all? 
> Usually, simp does not raise "Proof failed" if it gets stuck somewhere.

This plain ERROR stems from Goal.prove here:

  http://isabelle.in.tum.de/repos/isabelle/annotate/d5b5c9259afd/src/Provers/Arith/extract_common_term.ML#l71

There is already a (* FIXME avoid handling of generic exceptions *) that 
is not as general to include ERROR as well.  We used to have this odd odd 
catch-all programming style in the distant past, but you can never be sure 
if the patterns are sufficient or necessary.


 	Makarius