summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | traytel |

Tue, 31 May 2016 21:06:46 +0200 | |

changeset 63193 | 53ca45d39130 |

parent 63192 | a742d309afa2 (diff) |

parent 63191 | c3896c385c3e (current diff) |

child 63196 | 82552b478356 |

merged

--- a/src/HOL/Library/Stream.thy Tue May 31 18:31:33 2016 +0200 +++ b/src/HOL/Library/Stream.thy Tue May 31 21:06:46 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>