Theory Idx_Iterator

section ‹\isaheader{Iterator by get and size }›
theory Idx_Iterator
imports
  SetIterator
  Automatic_Refinement.Automatic_Refinement
begin

fun idx_iteratei_aux 
  :: "('s ⇒ nat ⇒ 'a) ⇒ nat ⇒ nat ⇒ 's ⇒ ('σ⇒bool) ⇒ ('a ⇒'σ ⇒ 'σ) ⇒ 'σ ⇒ 'σ"
where
  "idx_iteratei_aux get sz i l c f σ = (
    if i=0 ∨ ¬ c σ then σ
    else idx_iteratei_aux get 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 get sz i l c f σ = σ"
  "¬c σ ⟹ idx_iteratei_aux get sz i l c f σ = σ"
  "⟦i≠0; c σ⟧ ⟹ idx_iteratei_aux get sz i l c f σ = idx_iteratei_aux get sz (i - 1) l c f (f (get l (sz-i)) σ)"
  apply -
  apply (subst idx_iteratei_aux.simps, simp)+
  done

definition "idx_iteratei get sz l c f σ == idx_iteratei_aux get (sz l) (sz l) l c f σ"

lemma idx_iteratei_eq_foldli:
  assumes sz: "(sz, length) ∈ arel → nat_rel"
  assumes get: "(get, (!)) ∈ arel → nat_rel → Id"
  assumes "(s,s') ∈ arel"
  shows "(idx_iteratei get sz s, foldli s') ∈ Id" 
proof-
  have size_correct: "⋀s s'. (s,s') ∈ arel ⟹ sz s = length s'"
      using sz[param_fo] by simp
  have get_correct: "⋀s s' n. (s,s') ∈ arel ⟹ get s n = s' ! n"
      using get[param_fo] by simp
  {
    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 s' c f σ i
    assume "(s,s') ∈ arel" "i≤sz s"
    hence "idx_iteratei_aux get (sz s) i s c f σ = foldli (drop (sz 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 S = 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: size_correct[OF S] get_correct[OF S] drop_aux)
      qed
    qed
  } note aux=this

  show ?thesis
    unfolding idx_iteratei_def[abs_def]
    by (simp, intro ext, simp add: aux[OF ‹(s,s') ∈ arel›])
qed


text ‹Misc.›

lemma idx_iteratei_aux_nth_conv_foldli_drop:
  fixes xs :: "'b list"
  assumes "i ≤ length xs"
  shows "idx_iteratei_aux (!) (length xs) i xs c f σ = foldli (drop (length xs - i) xs) c f σ"
using assms
proof(induct get≡"(!) :: 'b list ⇒ nat ⇒ 'b" sz≡"length xs" i xs c f σ rule: idx_iteratei_aux.induct)
  case (1 i l c f σ)
  show ?case
  proof(cases "i = 0 ∨ ¬ c σ")
    case True thus ?thesis
      by(subst idx_iteratei_aux.simps)(auto)
  next
    case False
    hence i: "i > 0" and c: "c σ" by auto
    hence "idx_iteratei_aux (!) (length l) i l c f σ = idx_iteratei_aux (!) (length l) (i - 1) l c f (f (l ! (length l - i)) σ)"
      by(subst idx_iteratei_aux.simps) simp
    also have "… = foldli (drop (length l - (i - 1)) l) c f (f (l ! (length l - i)) σ)"
      using ‹i ≤ length l› i c by -(rule 1, auto)
    also from ‹i ≤ length l› i
    have "drop (length l - i) l = (l ! (length l - i)) # drop (length l - (i - 1)) l"
      apply (subst Cons_nth_drop_Suc[symmetric])
      apply simp_all
      done
    hence "foldli (drop (length l - (i - 1)) l) c f (f (l ! (length l - i)) σ) = foldli (drop (length l - i) l) c f σ"
      using c by simp
    finally show ?thesis .
  qed
qed

lemma idx_iteratei_nth_length_conv_foldli: "idx_iteratei nth length = foldli"
by(rule ext)+(simp add: idx_iteratei_def idx_iteratei_aux_nth_conv_foldli_drop)
end