Theory Idx_Iterator

header {* \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, op!) ∈ 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 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 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 True[simp, intro!]
        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 op ! (length xs) i xs c f σ = foldli (drop (length xs - i) xs) c f σ"
using assms
proof(induct get≡"op ! :: '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 op ! (length l) i l c f σ = idx_iteratei_aux op ! (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 nth_drop'[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