theory Iterator imports It_to_It SetIteratorOperations SetIteratorGA Proper_Iterator Gen_Iterator Idx_Iterator begin text {* Folding over a list created by a proper iterator can be replaced by a single iteration *} lemma proper_it_to_list_opt[refine_transfer_post_subst]: assumes PR: "proper_it' it it'" shows "foldli o it_to_list it ≡ it'" proof (rule eq_reflection, intro ext) fix s c f σ obtain l where "it s = foldli l" and "it' s = foldli l" by (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]]) thus "(foldli o it_to_list it) s c f σ = it' s c f σ" by (simp add: comp_def it_to_list_def) qed lemma iterator_cnv_to_comp[refine_transfer_post_simp]: "foldli (it_to_list it x) = (foldli o it_to_list it) x" by auto declare idx_iteratei_eq_foldli[autoref_rules] end