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.