# Re: [isabelle] recdef error message talks about :000

`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:

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.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*