[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"
where
  "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'.

Best,
Andreas




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