[isabelle-dev] Of lazy lists and friendly corecs

[Andreas Lochbihler]

Hi Manuel,

I've played around a bit with lmerge. It magically works if you replace the selectors with 
case statements (in Isabelle/5c2c559f01eb):

friend_of_corec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
   "lmerge xs ys =
    (case xs of LNil ⇒ (case ys of LNil ⇒ LNil | LCons y ys' ⇒ LCons y ys')
     | LCons x xs' ⇒ (case ys of LNil ⇒ LCons x xs' | LCons y ys' ⇒
        if x ≤ y then LCons x (lmerge xs' ys)
        else LCons y (lmerge xs ys')))"
   subgoal by(subst lmerge.code)(simp split: llist.split)
   subgoal by transfer_prover
   done

Hope this helps,
Andreas

On 07/10/16 14:22, Manuel Eberl wrote:
> 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
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>