Theory ListGA

section ‹\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 Cons_nth_drop_Suc[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 [simp, intro!]: True
          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 [simp, intro!]: True
          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)"

    define l where "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