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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
