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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to