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"