Re: [isabelle] coinduct_upto for coinductive predicates

Hi Manuel,

You can use Andreas's rule to prove that fact for any xs:

lemma P_s: assumes "P xs" shows "P( g xs)"
using assms apply(coinduction arbitrary: xs rule: P_coinduct_upto_g)
by (smt P.cases embed g.code stream.sel(1) stream.sel(2))

(and, of course, you can also use it to immediately prove P(s), your original motivation)


From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Manuel Eberl <eberlm at>
Sent: 07 November 2016 17:08
To: cl-isabelle-users at
Cc: Andreas Lochbihler
Subject: Re: [isabelle] coinduct_upto for coinductive predicates


thanks for the explanation. I think I now managed to define the closure
that I need and prove the corresponding coinduct_upto rule.

I noticed that during the proof of this rule, I essentially needed to
prove that all the friendly functions in the closure preserve the
inductive predicate, i.e. in terms of the example theory from earlier, I
needed to prove some generalised version of "P s ==> P (g s)".

I then thought that once I have proven the coinduct_upto rule, I should
be able to easily derive the fact "P s ==> P (g s)" from that, but I
cannot see how. If I want to prove "P s ==> P (g s)", do I really have
to do all the proof work again?



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