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.

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

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