Theory Iterator

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