Re: [isabelle] primcorec complains about invalid map function



Hi Andreas,

> So, how should I write my definition of map_bar'?

Try

    primcorec map_bar' :: "('a => 'b) => ('d => 'c) => ('a, 'c) bar => ('b, 'd) bar" where
    "un_Bar (map_bar' f h r) = map_foo id (map_bar' f h) ((map_foo' f h id \<circ> un_Bar) r)"

I arrived at it by looking at the characteristic theorem

    thm bar.unfold[of "map_foo' f h id o un_Bar" for f h, folded map_bar'_def]

associated with your definition

    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 *)

I'm sorry if this is a bit tedious each time. If this is a major hurdle for you, we might look into ways to make "primcorec" work more smoothly for such cases. Do you think it would make sense if the BNF package always defined the "map" function in the way you suggest?

Cheers,

Jasmin





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