[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.