When working with Isabelle’s infinite stream data type, I need this obviously true lemma, but I am unable to figure out how to prove it (as I am not well versed with coinduction yet). How would I go about proving it?
lemma sset_cycle[simp]:
"xs ≠ [] ⟹ sset (cycle xs) = set xs"
Instead of induction over n
and using op !!
as proposed by Manuel Eberl you can also do induction directly over sset
(with rule sset_induct):
lemma sset_cycle [simp]:
assumes "xs ≠ []"
shows "sset (cycle xs) = set xs"
proof (intro set_eqI iffI)
fix x
assume "x ∈ sset (cycle xs)"
from this assms show "x ∈ set xs"
by (induction "cycle xs" arbitrary: xs rule: sset_induct) (case_tac xs; fastforce)+
next
fix x
assume "x ∈ set xs"
with assms show "x ∈ sset (cycle xs)"
by (metis UnI1 cycle_decomp sset_shift)
qed