Email Gateway (Aug 18 2022 at 11:45): Email Gateway (Aug 18 2022 at 11:45):From: Dave Cunningham <dc04@doc.ic.ac.uk>
I'm trying to use recdef for the first time and I'm getting error
messages I don't understand. Here is my problem boiled down as small as
I can make it:
consts test :: "nat list => bool"
recdef test "measure(length)"
"test ([]) = True"
"test ((discard#L)) = (EX L'. (L=L') /\ test L')"
*** Proof failed.
*** ALL:000 L. length :000 < Suc (length L)
*** 1. ALL:000 L. length :000 < Suc (length L)
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** ALL:000 L. length :000 < Suc (length L)
*** At command "recdef".
Have no idea what :000 is, or how to make this work. Any help
appreciated.
Email Gateway (Aug 18 2022 at 11:45):From: Amine Chaieb <chaieb@in.tum.de>
The :000 is a variable introduced by recdef to prove termination of
test. The definition looks unnecessarily complicated. Here is an
alternative:
consts test :: "nat list => bool"
recdef test "measure(length)"
"test ([]) = True"
"test ((discard#L)) = test L"
You could then derive your second clause:
lemma test_Cons: "test ((discard#L)) = (EX L'. (L = L') & test L')"
by simp
and prove that test is the constant True function, so you could have
defined test = (%x. True).
lemma "test xs" by (induct xs, simp_all)
You could alternatively use the function package to separate function
definition and termination proofs.
Hope it helps.
Amine
Dave Cunningham wrote:
Email Gateway (Aug 18 2022 at 11:45):From: Alexander Krauss <krauss@in.tum.de>
Dave,
First of all you should read the internal variable :000 as L'.
Recdef fails in proving the termination of the function and shows you
the goal it could not prove, which is indeed unprovable. The problem is
that it does not know that it can use the equality on the left of the
conjunction for simplifying the right hand side. You can tell it to do
so by adding
(hints recdef_cong: conj_cong)
at the end of the recdef command.
Also note that using the old recdef package is now discouraged in favour
of the new functinon package, which will often make your life easier.
See http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf for
documentation.
Hope this helps,
Alex
Last updated: May 03 2024 at 04:19 UTC