[isabelle-dev] command value

[Christian Sternagel]

Sorry, something strange was going on... after loading the file with the 
below contents again, the results are different (but I swear that they 
have been as shown the first time).

Now the first 'value [simp] "revapp xs ys"' yields

   "fold op # xs [] @ ys" :: "'a list"

which is still strange, since rev_conv_fold is not a simplification rule 
but explains the latter three results (which are as expected after [code 
del] on rev_conv_fold {why does this have any effect on [simp]?}).

cheers

chris

PS: Sorry for the heavy traffic.

On 04/27/2012 02:33 PM, Christian Sternagel wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev