[isabelle] primcorec complains about invalid map function
Dear BNF experts,
I am trying to convert my manual definitions of primitively corecursive functions to use
primcorec. Unfortunately, I am having trouble as soon as my codatatype uses nested
recursion. Here's a minimal example. It runs with Isabelle2013-2, but the problem is the
same with a recent development version such as e872d196a73b. I want to define map_bar'
with primcorec, but primcorec rejects my attempt below with "Invalid map function in
"map_foo'". So, how should I write my definition of map_bar'?
datatype_new ('a, 'c, 'e) foo = A 'a | B "'c => 'e"
primrec_new map_foo' ::
"('a => 'b) => ('d => 'c) => ('e => 'f)
=> ('a, 'c, 'e) foo => ('b, 'd, 'f) foo"
"map_foo' f h k (A x) = A (f x)"
| "map_foo' f h k (B c) = B (map_fun h k c)"
codatatype ('a, 'c) bar = Bar "('a, 'c, ('a, 'c) bar) foo"
definition map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b, 'd) bar"
where "map_bar' f h = bar_unfold (map_foo' f h id o un_Bar)" (* works *)
primcorec map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b, 'd) bar"
where "un_Bar (map_bar' f h r) = map_foo' f h (map_bar' f h) (un_Bar r)"
(* invalid map function map_foo' *)
Here's some background info on what I am trying to achieve. The type variable 'c in foo is
dead, so map_foo as generated by datatype_new does not take a parameter for 'c. The
quotient and lifting packages, however, expect a map function that take one parameters for
each type variable. That's why I want to define map_foo' and map_bar'.
This archive was generated by a fusion of
Pipermail (Mailman edition) and