*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] nat_code Equation*From*: Brian Huffman <huffman at in.tum.de>*Date*: Tue, 4 Dec 2012 09:39:08 -0800*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <A2324240-A6DA-4BEE-A7A8-FB02771B3B53@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> <CAAMXsiYaGLygd6a_kE9efTsw_hd51nGjsjBpbCWsQMu56c5GgA@mail.gmail.com> <A2324240-A6DA-4BEE-A7A8-FB02771B3B53@uibk.ac.at>

On Tue, Dec 4, 2012 at 12:18 AM, René Thiemann <rene.thiemann at uibk.ac.at> wrote: > Thanks Brian, for the new version of Code_Nat. Unfortunately, it works for foo, > but not for other functions. A minimized example that fails is as follows: > > fun double :: "nat ⇒ nat" where > "double 0 = 0" > | "double n = n + n" > > export_code double in Haskell file - > > Constructor as head in equation: > nat_of_num ?n ≡ plus_nat_inst.plus_nat (pred_numeral ?n) (nat_of_num num.One) > > René This took me a minute to figure out! In this example double.simps actually contains the rule "double (Suc n) = Suc n + Suc n". Since the RHS mentions "Suc" we must also generate code for "Suc" as well, which is where the problem starts. In the code equation for Suc, "Suc n = n + 1", my code preprocessor incorrectly translates away the Suc on the LHS. I attach an updated version that fixes this. However, after some more thought I don't think that my general approach will work at all for patterns like "Suc (Suc n)"; in the long run we'll probably have to stay with a code preprocessor like the current one, which can combine multiple equations into single ones that use if-then-else or case. - Brian

**Attachment:
Code_Nat.thy**

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

**Re: [isabelle] nat_code Equation***From:*Brian Huffman

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

- Previous by Date: [isabelle] Proving set equality -- set-up question
- Next by Date: Re: [isabelle] Indexed Sum/Product Operator
- 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