[isabelle] coinduct_upto for coinductive predicates


I have a coinductive predicate P and I want to show that "P s" holds, where "s" is a corecursively-defined stream whose definition uses a friendly function, i.e. something like "s = 0 ## g s" where g is friendly. (see also attached theory)

The problem is that P.coinduct then only allows me to use "P s" in the coinduction proof, but I need "P (g s)". I suppose what I really need here is something like "coinduction up to friends for coinductive predicates"; from what I read, something like this is already available for "normal" coinduction w.r.t. equality.

How do I do something like this? (my actual coinductive predicate is, of course, much more complicated than this, so working with "normal" coinduction w.r.t. equality is not an option)



Attachment: Test.thy
Description: application/extension-thy

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