[isabelle-dev] Problem with simproc enat_eq_cancel
Makarius
makarius at sketis.net
Wed Mar 6 16:18:52 CET 2013
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
More information about the isabelle-dev
mailing list