Re: [isabelle] primcorec complains about invalid map function



Am 05.02.2014 09:20, schrieb Andreas Lochbihler:
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' *)

The corecursive call to map_bar' is only allowed to be applied either directly of through the map function of foo (the one generated by the package, not your custom map_foo'). The solution is to modify the "abstract state" (here "un_Bar r") before applying the corecursive call. To obtain your original equations you will need a few helper lemmas (relating map_foo and map_foo').

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

lemma map_foo_map_foo': "map_foo f k foo = map_foo' f id k foo"
  by (induct foo) auto

lemma map_foo'_comp[simp]:
"map_foo' f h k (map_foo' f' h' k' foo) = map_foo' (f o f') (h' o h) (k o k') foo"
  by (induct foo) (auto simp: map_fun.compositionality o_def)

lemma map_bar': "un_Bar (map_bar' f h r) = map_foo' f h (map_bar' f h) (un_Bar r)"
  by (auto simp: map_foo_map_foo')

Dmitriy





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