Re: [isabelle] nat_code Equation

On Mon, Dec 3, 2012 at 1:18 AM, René Thiemann <rene.thiemann at> wrote:
> Unfortunately, HOL/Library/Code_Nat.thy does not fully work in my case.
> The following short example shows the problem:
> theory Test
>  imports "~~/src/HOL/Library/Code_Nat"
> begin
> fun foo where
>   "foo xs 0 = True"
> | "foo [] (Suc _) = False"
> | "foo (x # xs) (Suc n) = foo xs n"
> export_code foo in Haskell file -
> complains about
> "Nat.Suc" is not a constructor, on left hand side of equation, in theorem:
> foo [] (Suc ?uu) ≡ False
> Of course, I can drop the pattern matching on Suc, but I do not want to do that
> manually for all my functions.

Hi René,

The ML setup in Code_Nat.thy is intended to automatically translate
away patterns involving Suc, so that you don't have to do it yourself.
Unfortunately the translation is kind of picky; it only works if for
each rule with a "Suc n" pattern, there is a matching rule with a "0"
pattern in its place. E.g. the following modification works with
Code_Nat.thy in Isabelle2012:

fun foo where
  "foo [] 0 = True"
| "foo (x # xs) 0 = True"
| "foo [] (Suc _) = False"
| "foo (x # xs) (Suc n) = foo xs n"

But instead of changing your code, please try out the attached version
of Code_Nat.thy, where I have modified the code preprocessor.

Florian: Perhaps you could look at my code and see whether it would be
suitable to check in to the development repo. It might still contain
some bugs; I haven't tested it on nested patterns like "Suc (Suc n)"
for example.

- Brian

Attachment: Code_Nat.thy
Description: Binary data

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