[isabelle-dev] Problem with simproc enat_eq_cancel

[Andreas Lochbihler]

Dear all,

in the repository (8a635bf2c86c) and in Isabelle2013, there seems to be 
something wrong with the enat_eq_cancel simproc in Extended_Nat. Can 
someone please look into this? Here's a minimal example:

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!


When I disable the simproc, I am able to prove the lemma:

using [[simproc del:enat_eq_cancel]]
apply(cases a b rule: enat.exhaust[case_product enat.exhaust])
apply(simp_all add: epred_def eSuc_def one_enat_def zero_enat_def split: 
enat.splits)
done

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.

Best,
Andreas