Re: [isabelle] primrec with mutual recursion over nat



Dear Henning,

> The tutorial for datatypes states that this works fine with new-style
> datatypes, but in my case I get the error:
> "nat" is an old-style datatype
> 
> Some minimal example would be:
> primrec foo:: "('a â 'a) â nat â 'a â 'a" and bar:: "('a â 'a) â nat â
> 'a â 'a" where
>  "foo f 0 a = a"
> | "foo f (Suc n) a = f (bar f n a)"
> | "bar f 0 b = b"
> | "bar f (Suc n) b = f (foo f n b)"
> 
> Is there some way to fix this problem? Is there some "new-style nat"?

The error message is misleading. If you try with a "new-style nat", you get a more informative message:

    datatype nat = Z | Suc nat

    primrec foo:: "('a â 'a) â nat â 'a â 'a" and bar:: "('a â 'a) â nat â 'a â 'a" where
     "foo f Z a = a"
    | "foo f (Suc n) a = f (bar f n a)"
    | "bar f Z b = b"
    | "bar f (Suc n) b = f (foo f n b)"

produces

    "Scratch.nat" is neither mutually recursive with "Scratch.nat" nor nested recursive through itself

The definition works fine if you use "fun" instead. Where did you read that "this works fine with new-style datatypes"? I'm not aware of any sentence to that effect in "datatypes.pdf" -- but maybe I'm wrong.

Cheers,

Jasmin





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