src/HOL/Library/Stream.thy
changeset 63192 a742d309afa2
parent 62093 bd73a2279fcd
child 63649 e690d6f2185b
equal deleted inserted replaced
63190:3e79279c10ca 63192:a742d309afa2
   338    stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
   338    stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
   339   by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
   339   by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
   340 
   340 
   341 lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
   341 lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
   342   by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
   342   by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
       
   343 
       
   344 lemma sset_cycle[simp]:
       
   345   assumes "xs \<noteq> []" 
       
   346   shows "sset (cycle xs) = set xs"
       
   347 proof (intro set_eqI iffI)
       
   348   fix x
       
   349   assume "x \<in> sset (cycle xs)"
       
   350   then show "x \<in> set xs" using assms
       
   351     by (induction "cycle xs" arbitrary: xs rule: sset_induct) (fastforce simp: neq_Nil_conv)+
       
   352 qed (metis assms UnI1 cycle_decomp sset_shift)
   343 
   353 
   344 
   354 
   345 subsection \<open>iterated application of a function\<close>
   355 subsection \<open>iterated application of a function\<close>
   346 
   356 
   347 primcorec siterate where
   357 primcorec siterate where