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