Re: [isabelle] primcorec complains about invalid map function
> So, how should I write my definition of map_bar'?
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and