*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] nat_code Equation*From*: Brian Huffman <huffman at in.tum.de>*Date*: Mon, 3 Dec 2012 11:02:35 -0800*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <E23D8E77-94CA-4689-BA23-971780FC34DB@uibk.ac.at>*References*: <FB64BADF-227D-4ED8-988B-57680C25BB73@uibk.ac.at> <50B8CDE9.3070807@in.tum.de> <50B8D5FC.8040009@in.tum.de> <CAAMXsiagmLap6eB1tpjB8F-Lk3DV9jeZcxvbNRNcEbO1M7NVVQ@mail.gmail.com> <E23D8E77-94CA-4689-BA23-971780FC34DB@uibk.ac.at>

On Mon, Dec 3, 2012 at 1:18 AM, René Thiemann <rene.thiemann at uibk.ac.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**

**Follow-Ups**:**Re: [isabelle] nat_code Equation***From:*Florian Haftmann

**Re: [isabelle] nat_code Equation***From:*René Thiemann

**References**:**Re: [isabelle] nat_code Equation***From:*René Thiemann

- Previous by Date: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Next by Date: Re: [isabelle] nat_code Equation
- Previous by Thread: Re: [isabelle] nat_code Equation
- Next by Thread: Re: [isabelle] nat_code Equation
- Cl-isabelle-users December 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list