Search code examples
liststreamproofisabellecoinduction

How to prove sset (cycle xs) = set xs

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"
Solution

  • 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