Theory It_to_It

theory It_to_It
imports 
  "Proper_Iterator"
begin

  lemma proper_it_fold: 
    "proper_it it it' ==> foldli (it (λ_. True) (λx l. l@[x]) []) = it'"
    unfolding proper_it_def by auto
  lemma proper_it_unfold: 
    "proper_it it it' ==> it' = foldli (it (λ_. True) (λx l. l@[x]) [])"
    unfolding proper_it_def by auto


  text {* The following constant converts an iterator over list-state
    to an iterator over arbitrary state *}
  definition it_to_it :: "('x,'x list) set_iterator => ('x,'σ) set_iterator"
    where [code del]: "it_to_it it 
    ≡ (foldli (it (λ_. True) (λx l. l@[x]) []))"

  lemma pi_it_to_it[icf_proper_iteratorI]: "proper_it (it_to_it I) (it_to_it I)"
    unfolding it_to_it_def by (rule pi_foldli)
  text {* In case of a proper iterator, it is equivalent to direct iteration *}
  lemma it_to_it_fold: "proper_it it (it'::('x,'σ) set_iterator) 
    ==> it_to_it it = it'"
    unfolding it_to_it_def
    by (simp add: proper_it_fold)

  lemma it_to_it_map_fold:
    assumes P: "proper_it it it'"
    shows "it_to_it (λc f. it c (f o f')) = (λc f. it' c (f o f'))"
    apply (rule proper_itE[OF P])
    unfolding it_to_it_def
    apply (intro ext)
    apply (simp add: foldli_foldl map_by_foldl foldli_map)
    done

  lemma it_to_it_fold': "proper_it' it (it'::'s => ('x,'σ) set_iterator) 
    ==> it_to_it (it s) = (it' s)"
    by (drule proper_it'D) (rule it_to_it_fold)

  lemma it_to_it_map_fold':
    assumes P: "proper_it' it it'"
    shows "it_to_it (λc f. it s c (f o f')) = (λc f. it' s c (f o f'))"
    using P[THEN proper_it'D] by (rule it_to_it_map_fold)

  text {* This locale wraps up the setup of a proper iterator for use
    with @{text "it_to_it"}. *}
  locale proper_it_loc =
    fixes it :: "'s => ('x,'x list) set_iterator"
    and it' :: "'s => ('x,'σ) set_iterator"
    assumes proper': "proper_it' it it'"
  begin
    lemma proper: "proper_it (it s) (it' s)"
      using proper' by (rule proper_it'D)

    lemmas it_to_it_code_unfold[code_unfold] = it_to_it_fold[OF proper]
  end

  subsubsection {* Correctness *}
  text {* The polymorphic iterator is a valid iterator again. *}
  lemma it_to_it_genord_correct: 
    assumes "set_iterator_genord (it::('x,'x list) set_iterator) S R" 
    shows "set_iterator_genord ((it_to_it it)::('x,'σ) set_iterator) S R"
  proof -
    interpret set_iterator_genord it S R by fact

    show ?thesis
      apply (unfold_locales)
      unfolding it_to_it_def
      using foldli_transform
      by auto
  qed

  lemma it_to_it_linord_correct: 
    assumes "set_iterator_linord (it::('x::linorder,'x list) set_iterator) S" 
    shows "set_iterator_linord ((it_to_it it)::('x,'σ) set_iterator) S"
    using assms
    unfolding set_iterator_linord_def
    by (rule it_to_it_genord_correct)

  lemma it_to_it_rev_linord_correct: 
    assumes "set_iterator_rev_linord (it::('x::linorder,'x list) set_iterator) S"
    shows "set_iterator_rev_linord ((it_to_it it)::('x,'σ) set_iterator) S"
    using assms
    unfolding set_iterator_rev_linord_def
    by (rule it_to_it_genord_correct)

  lemma it_to_it_correct: 
    assumes "set_iterator (it::('x,'x list) set_iterator) S" 
    shows "set_iterator ((it_to_it it)::('x,'σ) set_iterator) S"
    using assms
    unfolding set_iterator_def
    by (rule it_to_it_genord_correct)

  lemma it_to_it_map_genord_correct:
    assumes "map_iterator_genord (it::('u,'v,('u×'v) list) map_iterator) S R" 
    shows "map_iterator_genord ((it_to_it it)::('u,'v,'σ) map_iterator) S R"
    using assms by (rule it_to_it_genord_correct)

  lemma it_to_it_map_linord_correct:
    assumes "map_iterator_linord (it::('u::linorder,'v,('u×'v) list) map_iterator) S" 
    shows "map_iterator_linord ((it_to_it it)::('u,'v,'σ) map_iterator) S"
    using assms unfolding set_iterator_map_linord_def by (rule it_to_it_genord_correct)

  lemma it_to_it_map_rev_linord_correct:
    assumes 
      "map_iterator_rev_linord (it::('u::linorder,'v,('u×'v) list) map_iterator) S" 
    shows "map_iterator_rev_linord ((it_to_it it)::('u,'v,'σ) map_iterator) S"
    using assms unfolding set_iterator_map_rev_linord_def 
    by (rule it_to_it_genord_correct)

  lemma it_to_it_map_correct:
    assumes "map_iterator (it::('u,'v,('u×'v) list) map_iterator) S" 
    shows "map_iterator ((it_to_it it)::('u,'v,'σ) map_iterator) S"
    using assms by (rule it_to_it_correct)






end