src/HOL/Library/Dlist.thy

   "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
 
 qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
   "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
 
+qualified definition rotate :: "nat \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+  "rotate n dxs = Dlist (List.rotate n (list_of_dlist dxs))"
+
 end
 
 
 text \<open>Derived operations:\<close>
 

   by (simp add: Dlist.map_def)
 
 lemma list_of_dlist_filter [simp, code abstract]:
   "list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)"
   by (simp add: Dlist.filter_def)
+
+lemma list_of_dlist_rotate [simp, code abstract]:
+  "list_of_dlist (Dlist.rotate n dxs) = List.rotate n (list_of_dlist dxs)"
+  by (simp add: Dlist.rotate_def)
 
 
 text \<open>Explicit executable conversion\<close>
 
 definition dlist_of_list [simp]: