*To*: Manuel Eberl <eberlm at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>, Jasmin Blanchette <jasmin.blanchette at inria.fr>*Subject*: Re: [isabelle] Tactic failed for Friends*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 26 Sep 2016 14:05:10 +0200*In-reply-to*: <0d224229-1202-cf1b-0812-dcea78d11a40@in.tum.de>*References*: <0d224229-1202-cf1b-0812-dcea78d11a40@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

Dear Manuel,

corecursive (friend) and manually prove the parametricity: by(fold relator_eq) transfer_prover Hope this helps, Andreas On 26/09/16 13:17, Manuel Eberl wrote:

Hallo, I don't know awfully much about friends and corecursion, but in my naÃvetÃ, I simply added "(friend)" to a reasonably friendly-looking corecursive definition and expected it to work. Instead, it looped. A minimal non-working example is the following: type_synonym ae = "(real Ã real) stream" corec (friend) add_ae :: "ae â ae" where "add_ae f = ((fst (shd f), snd (shd f)) ## add_ae (stl f))" This runs for about 3 seconds and then returns with the following error: Tactic failed The error(s) above occurred for the goal statementâ: rel_fun (rel_prod R (rel_pre_stream op = R)) (rel_pre_stream op = (rel_ssig_stream_v1 R)) (Îf. ((fst (fst (snd f)), snd (fst (snd f))), stream.v1.Oper (stream.v1.Sig (Inr (case snd f of (x1, x2) â stream.v1.VLeaf x2))))) (Îf. ((fst (fst (snd f)), snd (fst (snd f))), stream.v1.Oper (stream.v1.Sig (Inr (case snd f of (x1, x2) â stream.v1.VLeaf x2))))) The problem does not occur if I replace "(fst (shd f), snd (shd f))" with the equivalent "shd f". A similar, slightly less vacuous definition that is closer to my original definition is the following: corec (friend) add_ae :: "ae â ae â ae" where "add_ae f g = ((fst (shd f) + fst (shd g), snd (shd f)) ## add_ae (stl f) (stl g))" That also causes a similar error, but it takes about 110 seconds to get there. The command defining the function I originally had in mind has not terminated yet. Cheers, Manuel

**Follow-Ups**:**Re: [isabelle] Tactic failed for Friends***From:*Manuel Eberl

**References**:**[isabelle] Tactic failed for Friends***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Tactic failed for Friends
- Next by Date: Re: [isabelle] Tactic failed for Friends
- Previous by Thread: Re: [isabelle] Tactic failed for Friends
- Next by Thread: Re: [isabelle] Tactic failed for Friends
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list