[isabelle-dev] command value

[Christian Sternagel]

Hi all,

after

   fun revapp :: "'a list ⇒ 'a list ⇒ 'a list" where
     "revapp [] ys = ys" |
     "revapp (x#xs) ys = revapp xs (x#ys)"

   lemma revapp [simp, code]: "revapp xs ys = rev xs @ ys"
     by (induct xs arbitrary: ys) auto

   value [simp] "revapp xs ys"

what would you expect as the result of calling value?

I expected "rev xs @ ys", but obtained "revapp xs ys". What's the reason?

Moreover the outcome of

   declare rev.simps [code del, simp del]
   declare revapp.simps [code del, simp del]
   declare append.simps [code del, simp del]

   value [code] "revapp [1::nat] [2]"
   value [simp] "revapp [1::nat] [2]"
   value [nbe]  "revapp [1::nat] [2]"

seems also strange to me. I get

   "[1, 2]" :: "nat list"
   "[Suc 0] @ [Suc (Suc 0)]" :: "nat list"
   "[Suc 0] @ [Suc (Suc 0)]" :: "nat list"

but would expect

   an error message about missing code equations
   rev [Suc 0] @ [Suc (Suc 0)]
   I have no clue what "nbe" actually does ;)

cheers

chris