[isabelle-dev] Of lazy lists and friendly corecs

[Manuel Eberl]

Hallo,

I've been playing around with corec and friends in combination with the 
lazy lists from "$AFP/Coinductive/Coinductive_List" and encountered the 
following problem:

Suppose I want a function that takes two (implicitly sorted) lazy lists 
and merges them in the following fashion:

primcorec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
   "lmerge xs ys = (if lnull xs then ys
                    else if lnull ys then xs
                    else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge 
(ltl xs) ys)
                    else LCons (lhd ys) (lmerge xs (ltl ys)))"

I've still not fully understood what ‘friendly’ means, but I should be 
very surprised if this function were not friendly. So I tried this:

friend_of_corec lmerge where
   "lmerge xs ys = (if lnull xs ∧ lnull ys then LNil
                    else if lnull xs then LCons (lhd ys) (ltl ys)
                    else if lnull ys then LCons (lhd xs) (ltl xs)
                    else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge 
(ltl xs) ys)
                    else LCons (lhd ys) (lmerge xs (ltl ys)))"

Unfortunately, I get the following error:

exception TYPE raised (line 168 of "consts.ML"): Illegal type for 
constant "Coinductive_List.llist.LNil" :: 'b

I now have the following questions:
1. Something like "if lnull xs then ys" works in primcorec, but in corec 
and friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl 
ys)". Is that a known limitation?
2. What is the relationship between primcorec and friendliness? If I 
have a function defined by primcorec, is the additional step with 
friend_of_corec fundamentally necessary or is that just a technical 
issue? (I would have naïvely assumed that primitively-corecursive 
functions are always friendly or something like that)
3. What causes the above error and how do I get around it?


Cheers,

Manuel


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20161007/98d225c4/attachment.html>