Re: [isabelle-dev] Of lazy lists and friendly corecs
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
Re: [isabelle-dev] Of lazy lists and friendly corecs
Hi Manuel, a function is friendly if it produces at least one constructor after applying at most one constructor to the codatatype argument. This does not have anything to do with primitive corecursion, because the codatatype result type need not be a argument type---and even if it is, there are primcorec functions which are not friendly, e.g., primcorec odds :: "'a stream => 'a stream" where "odds xs = SCons (shd xs) (odds (stl (stl xs)))" I leave it to Dmitriy and Jasmin to reply to your problem with the error message about lmerge. But in theory this should work (and in fact I've already done it for streams). > 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? Yes, this is known to us, but we currently don't have the time to implement all the preprocessing features of primcorec for friend_of_corec. Best, 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
[isabelle-dev] Of lazy lists and friendly corecs
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
