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"
"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,
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
"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)
by (auto simp: map_foo_map_foo')
This archive was generated by a fusion of
Pipermail (Mailman edition) and