# HG changeset patch
# User traytel
# Date 1464699411 -7200
# Node ID a742d309afa2b7ea9d6b83a780f2bfb2453d81c9
# Parent  3e79279c10ca0032d9173bed0edec29aa4bc7274
moved lemma from afp

diff -r 3e79279c10ca -r a742d309afa2 src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Tue May 31 12:24:43 2016 +0200
+++ b/src/HOL/Library/Stream.thy	Tue May 31 14:56:51 2016 +0200
@@ -341,6 +341,16 @@
 lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
   by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
 
+lemma sset_cycle[simp]:
+  assumes "xs \<noteq> []" 
+  shows "sset (cycle xs) = set xs"
+proof (intro set_eqI iffI)
+  fix x
+  assume "x \<in> sset (cycle xs)"
+  then show "x \<in> set xs" using assms
+    by (induction "cycle xs" arbitrary: xs rule: sset_induct) (fastforce simp: neq_Nil_conv)+
+qed (metis assms UnI1 cycle_decomp sset_shift)
+
 
 subsection \<open>iterated application of a function\<close>