Theory ListGA

header {* \isaheader{Generic Algorithms for Sequences} *}
theory ListGA
imports "../spec/ListSpec" 
begin

subsection {* Iterators *}

subsubsection {* iteratei (by get, size) *}

locale idx_iteratei_loc = 
  list_size + list_get +
  constrains α :: "'s => 'a list"
  assumes [simp]: "!!s. invar s"
begin

  fun idx_iteratei_aux 
    :: "nat => nat => 's => ('σ=>bool) => ('a =>'σ => 'σ) => 'σ => 'σ"
  where
    "idx_iteratei_aux sz i l c f σ = (
      if i=0 ∨ ¬ c σ then σ
      else idx_iteratei_aux sz (i - 1) l c f (f (get l (sz-i)) σ)
    )"

  declare idx_iteratei_aux.simps[simp del]

  lemma idx_iteratei_aux_simps[simp]:
    "i=0 ==> idx_iteratei_aux sz i l c f σ = σ"
    "¬c σ ==> idx_iteratei_aux sz i l c f σ = σ"
    "[|i≠0; c σ|] ==> idx_iteratei_aux sz i l c f σ = idx_iteratei_aux sz (i - 1) l c f (f (get l (sz-i)) σ)"
    apply -
    apply (subst idx_iteratei_aux.simps, simp)+
    done

  definition idx_iteratei where 
    "idx_iteratei l c f σ ≡ idx_iteratei_aux (size l) (size l) l c f σ"

  lemma idx_iteratei_correct:
    shows "idx_iteratei s = foldli (α s)" 
  proof -
    {
      fix n l
      assume A: "Suc n ≤ length l"
      hence B: "length l - Suc n < length l" by simp
      from A have [simp]: "Suc (length l - Suc n) = length l - n" by simp
      from nth_drop'[OF B, simplified] have 
        "drop (length l - Suc n) l = l!(length l - Suc n)#drop (length l - n) l" 
        by simp
    } note drop_aux=this

    {
      fix s c f σ i
      assume "invar s" "i≤size s"
      hence "idx_iteratei_aux (size s) i s c f σ 
        = foldli (drop (size s - i) (α s)) c f σ"
      proof (induct i arbitrary: σ)
        case 0 with size_correct[of s] show ?case by simp
      next
        case (Suc n)
        note [simp, intro!] = Suc.prems(1)
        show ?case proof (cases "c σ")
          case False thus ?thesis by simp
        next
          case True[simp, intro!]
          show ?thesis using Suc by (simp add: get_correct size_correct drop_aux)
        qed
      qed
    } note aux=this

    show ?thesis
      unfolding idx_iteratei_def[abs_def]
      by (auto simp add: fun_eq_iff aux[of _ "size s", simplified])
  qed

  lemmas idx_iteratei_unfold[code_unfold] = idx_iteratei_correct[symmetric]

  subsubsection {* reverse\_iteratei (by get, size) *}

  fun idx_reverse_iteratei_aux 
    :: "nat => nat => 's => ('σ=>bool) => ('a =>'σ => 'σ) => 'σ => 'σ"
    where
    "idx_reverse_iteratei_aux sz i l c f σ = (
      if i=0 ∨ ¬ c σ then σ
      else idx_reverse_iteratei_aux sz (i - 1) l c f (f (get l (i - 1)) σ)
    )"

  declare idx_reverse_iteratei_aux.simps[simp del]

  lemma idx_reverse_iteratei_aux_simps[simp]:
    "i=0 ==> idx_reverse_iteratei_aux sz i l c f σ = σ"
    "¬c σ ==> idx_reverse_iteratei_aux sz i l c f σ = σ"
    "[|i≠0; c σ|] ==> idx_reverse_iteratei_aux sz i l c f σ 
    = idx_reverse_iteratei_aux sz (i - 1) l c f (f (get l (i - 1)) σ)"
    by (subst idx_reverse_iteratei_aux.simps, simp)+

  definition "idx_reverse_iteratei l c f σ 
    == idx_reverse_iteratei_aux (size l) (size l) l c f σ"

  lemma idx_reverse_iteratei_correct:
    shows "idx_reverse_iteratei s = foldri (α s)"
  proof -
    {
      fix s c f σ i
      assume "invar s" "i≤size s"
      hence "idx_reverse_iteratei_aux (size s) i s c f σ 
        = foldri (take i (α s)) c f σ"
      proof (induct i arbitrary: σ)
        case 0 with size_correct[of s] show ?case by simp
      next
        case (Suc n)
        note [simp, intro!] = Suc.prems(1)
        show ?case proof (cases "c σ")
          case False thus ?thesis by simp
        next
          case True[simp, intro!]
          show ?thesis using Suc 
            by (simp add: get_correct size_correct take_Suc_conv_app_nth)
        qed
      qed
    } note aux=this

    show ?thesis
      unfolding idx_reverse_iteratei_def[abs_def]
      apply (simp add: fun_eq_iff aux[of _ "size s", simplified])
      apply (simp add: size_correct)
    done
  qed

  lemmas idx_reverse_iteratei_unfold[code_unfold] 
    = idx_reverse_iteratei_correct[symmetric]

end

subsection {* Size (by iterator) *}

locale it_size_loc = poly_list_iteratei +
  constrains α :: "'s => 'a list"
begin

  definition it_size :: "'s => nat"
    where "it_size l == iterate l (λx res. Suc res) (0::nat)"

  lemma it_size_impl: shows "list_size α invar it_size"
    apply (unfold_locales)
    apply (unfold it_size_def)
    apply (simp add: iterate_correct foldli_foldl)
    done
end

subsubsection {* Size (by reverse\_iterator) *}

locale rev_it_size_loc = poly_list_rev_iteratei +
  constrains α :: "'s => 'a list"
begin

  definition rev_it_size :: "'s => nat"
    where "rev_it_size l == rev_iterate l (λx res. Suc res) (0::nat)"

  lemma rev_it_size_impl:
    shows "list_size α invar rev_it_size"
    apply (unfold_locales)
    apply (unfold rev_it_size_def)
    apply (simp add: rev_iterate_correct foldri_foldr)
    done

end

subsection {* Get (by iteratori) *}
locale it_get_loc = poly_list_iteratei + 
  constrains α :: "'s => 'a list"
begin

  definition it_get:: "'s => nat => 'a" 
    where "it_get s i ≡ 
      the (snd (iteratei s
                (λ(i,x). x=None) 
                (λx (i,_). if i=0 then (0,Some x) else (i - 1,None)) 
                (i,None)))"

  lemma it_get_correct:
    shows "list_get α invar it_get"
  proof 
    fix s i 
    assume "invar s" "i < length (α s)"

    def l ≡ "α s"
    from `i < length (α s)`
    show "it_get s i = α s ! i"
      unfolding it_get_def iteratei_correct l_def[symmetric]
    proof (induct i arbitrary: l)
      case 0
      then obtain x xs where l_eq[simp]: "l = x # xs" by (cases l, auto)
      thus ?case by simp
    next
      case (Suc i)
      note ind_hyp = Suc(1)
      note Suc_i_le = Suc(2)
      from Suc_i_le obtain x xs 
        where l_eq[simp]: "l = x # xs" by (cases l, auto)

      from ind_hyp [of xs] Suc_i_le
      show ?case by simp
    qed
  qed
end

end