Re: [isabelle] primcorec complains about invalid map function



Hi Jasmin,

It would be nice if such basic type constructors like sum and product work with prim(co)rec. I tried to register sum with wrap_free_constructors, but that did not work.

Did you specify selectors?
I tried the following in Isabelle/8a53ee72e595.

wrap_free_constructors
  [Inl, Inr]
  case_sum
  [is_Inl, is_Inr]
  [[projl], [projr]]
sorry

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

It results in the following exception:

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

Best,
Andreas




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