Re: [isabelle] nat_code Equation



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
Description: Binary data



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