Hallo Andrei,yes, but the new coinduction rule doesn't help with that; I can do the same proof using the old one:
lemma P_s: assumes "P xs" shows "P( g xs)" using assms apply(coinduction arbitrary: xs) by (smt P.cases embed g.code stream.sel(1) stream.sel(2))It is a bit difficult to illustrate my problem because my actual predicate is quite complicated, but the above minimal example is so trivial that it is difficult to see what my point is.
Anyway, I attached my theory. The relevant coinductive predicate is "is_expansion_aux". The corresponding closure predicate is "ms_closure". The coinduct_upto theorem is "is_expansion_aux_coinduct_upto".
Note that the coinduct_upto theorem contains a lengthy proof for the ms_closure_add case involving the friendly ms_plus_aux function. Later, when I want to prove "is_expansion_aux_add", I have to do pretty much the same proof again. I wonder if there is some way to get rid of that duplication.