[isabelle-dev] command value

Christian Sternagel c-sterna at jaist.ac.jp
Fri Apr 27 07:33:32 CEST 2012

Hi all,


   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 ;)



More information about the isabelle-dev mailing list