Re: [isabelle] primcorec complains about invalid map function



Hi Jasmin and Dmitriy,

Thanks for the quick replies. Jasmin's description of how he found the decomposition into map functions and state transformation helped me to solve the next few definitions.

> Do you think it would make sense if the BNF package always defined the "map" function
> in the way you suggest?
It would certainly have saved me some work it the BNF package did not omit the dead variables in the map function (I have also generalised the relator, so that would be the next thing). But I need them only for the lifting package, I have not yet used them in other cases. So, if there will be some integration of BNF and lifting, then that's definitely worth thinking about; otherwise, I suggest that we need more evidence of this being useful before someone starts to implement special cases for dead type variables.

> 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.

It is (not yet) obvious to me how I have to decompose the transformations such that primcorec accepts them. In fact, I am already stuck again.


codatatype 'a foobar = AA 'a | BB "bool => 'a foobar"

primcorec fbind :: "'a foobar => ('a => 'b foobar) => 'b foobar"
where "fbind f g = (if is_AA f then g (un_AA f) else BB (%b. fbind (un_BB f b) g))"

datatype_new ('a, 'c, 'e) foo = A 'a | B "'c => 'e"

codatatype ('a, 'c) bar = Bar "('a, 'c, ('a, 'c) bar) foo foobar"

definition bbind  :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
  "bbind r f =
  corec_bar (%r. fbind (un_Bar r) (%foo. case foo of A x =>
     map_foobar (map_foo id Inl) (un_Bar (f x))
   | B c => AA (B (%input. Inr (c input))))) r"


The functions fbind and bbind are monadic bind operations for the two codatatypes. Following your suggestions, I thought that I transform the foobar first into "bar + (bar * ('a => bar)) foo foobar" and then in the map functions, the Inl part stops the corecursion and the right continues. The following attempt raises an exception that says something about Inr () (but there are no unit types anywhere in my spec ???).

*** exception TERM raised (line 366 of "~~/src/HOL/Tools/hologic.ML"):
*** mk_split: bad body type
*** Inr ()
*** At command "primcorec"

primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
  "un_Bar (bbind r f) =
   map_foobar (map_foo id (case_sum id (split bbind)))
     (fbind (un_Bar r)
      (case_foo
        (map_foobar (map_foo id Inl) o un_Bar o f)
        (%c. AA (B (%i. Inr (c i, f))))))"

Next, I tried to eta-expand split as follows, but in vain. This time, I am puzzled about the "Inr (r, f)" in the prod_case. Where does that come from?

primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
where
  "un_Bar (bbind r f) =
   map_foobar (map_foo id (%z. case z of Inl r => r | Inr (r, f) => bbind r f))
     (fbind (un_Bar r)
      (case_foo
        (map_foobar (map_foo id Inl) o un_Bar o f)
        (%c. AA (B (%i. Inr (c i, f))))))"

*** primcorec error:
***   Type unification failed: Clash of types "_ + _" and "(_, _) bar"
***
*** Type error in application: incompatible operand type
***
*** Operator:  sum_case (%r. r) ::
***   (('a, 'c) bar * ('a => ('b, 'c) bar) => ('b, 'c) bar)
***   => ('b, 'c) bar + ('a, 'c) bar * ('a => ('b, 'c) bar) => ('b, 'c) bar
*** Operand:   %a. case a of (r, f) => Inr (r, f) ::
***   ('a, 'c) bar * ('a => ('b, 'c) bar)
***   => ('b, 'c) bar + ('a, 'c) bar * ('a => ('b, 'c) bar)
***
*** At command "primcorec"

Could you please help me once more?

Andreas




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