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



Dave,

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".

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





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