# [isabelle] Tactic failed for Friends

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*