# Theory SWA

(*<*)
theory SWA
imports Main
begin
(*>*)

section ‹Sliding Window Algorithm›

datatype 'a tree =
Leaf
| Node (l: nat) (r: nat) (val: "'a option") (lchild: "'a tree") (rchild: "'a tree")
where
"l Leaf = 0"
| "r Leaf = 0"
| "val Leaf = None"
| "lchild Leaf = Leaf"
| "rchild Leaf = Leaf"

lemma neq_Leaf_if_l_gt0: "0 < l t ⟹ t ≠ Leaf"
by auto

primrec discharge :: "'a tree ⇒ 'a tree" where
"discharge Leaf = Leaf"
| "discharge (Node i j _ t u) = Node i j None t u"

fun plus_option :: "'a option ⇒ 'a option ⇒ 'a option" where
"plus_option None _ = None"
| "plus_option _ None = None"
| "plus_option (Some a) (Some b) = Some (a + b)"

instance proof
fix a b c :: "'a option"
show "a + b + c = a + (b + c)"
by (induct a b rule: plus_option.induct; cases c)
(auto simp: algebra_simps)
qed

end

fun combine :: "'a :: semigroup_add tree ⇒ 'a tree ⇒ 'a tree" where
"combine t Leaf = t"
| "combine Leaf t = t"
| "combine t u = Node (l t) (r u) (val t + val u) (discharge t) u"

lemma combine_non_Leaves: "⟦t ≠ Leaf; u ≠ Leaf⟧ ⟹ combine t u = Node (l t) (r u) (val t + val u) (discharge t) u"
proof -
assume assms: "t ≠ Leaf" "u ≠ Leaf"
from assms have "combine t u = Node (l (Node (l t) (r t) (val t) (lchild t) (rchild t))) (r (Node (l u) (r u) (val u) (lchild u) (rchild u))) (val (Node (l t) (r t) (val t) (lchild t) (rchild t)) + val (Node (l u) (r u) (val u) (lchild u) (rchild u))) (discharge (Node (l t) (r t) (val t) (lchild t) (rchild t))) (Node (l u) (r u) (val u) (lchild u) (rchild u))"
by (metis (no_types) combine.simps(3) tree.exhaust_sel)
with assms show ?thesis
by simp
qed

lemma r_combine_non_Leaves: "⟦t ≠ Leaf; u ≠ Leaf⟧ ⟹ r (combine t u) = r u"

type_synonym window = "nat × nat"

definition window :: "'a list ⇒ window ⇒ bool" where
"window as = (λ(l, r). 0 < l ∧ l ≤ r ∧ r ≤ length as)"

definition windows :: "'a list ⇒ window list ⇒ bool" where
"windows as ws = ((∀w ∈ set ws. window as w) ∧
sorted (map fst ws) ∧ sorted (map snd ws))"

function reusables :: "'a tree ⇒ window ⇒ 'a tree list" where
"reusables t w = (if fst w > r t then [] else if fst w = l t then [t]
else let v = lchild t; u = rchild t in if fst w ≥ l u then
reusables u w else u # reusables v w)"
by auto
termination
by (relation "measure (λp. size (fst p))")
(auto simp: lchild_def rchild_def split: tree.splits)

declare reusables.simps[simp del]

lemma reusables_Leaf[simp]: "0 < fst w ⟹ reusables Leaf w = []"

primrec well_shaped :: "'a tree ⇒ bool" where
"well_shaped Leaf = True"
| "well_shaped (Node i j _ t u) = (i ≤ j ∧ (i = j ⟶ t = Leaf ∧ u = Leaf) ∧
(i < j ⟶ t ≠ Leaf ∧ u ≠ Leaf ∧ well_shaped t ∧ well_shaped u ∧
i = l t ∧ j = r u ∧ Suc (r t) = l u))"

lemma l_lchild_eq_l_if_well_shaped[simp]:
"⟦well_shaped t; l t < r t⟧ ⟹ l (lchild t) = l t"
by (induct t) auto

lemma r_rchild_eq_r_if_well_shaped[simp]:
"⟦well_shaped t; l t < r t⟧ ⟹ r (rchild t) = r t"
by (induct t) auto

lemma r_lchild_eq_l_rchild_if_well_shaped:
"⟦well_shaped t; l t < r t⟧ ⟹ r (lchild t) = l (rchild t) - 1"
by (induct t) auto

lemma r_lchild_le_r: "well_shaped t ⟹ r (lchild t) ≤ r t"
proof (induct t)
case (Node i j a t1 t2)
then show ?case
by auto
(metis Suc_eq_plus1_left order.trans le_add2 tree.exhaust_sel well_shaped.simps(2))
qed simp

lemma well_shaped_lchild[simp]: "well_shaped t ⟹ well_shaped (lchild t)"
by (induct t) auto

lemma well_shaped_rchild[simp]: "well_shaped t ⟹ well_shaped (rchild t)"
by (induct t) auto

"adjacent w ts = (Leaf ∉ set ts ∧
list_all2 (λt u. l t = Suc (r u)) (butlast ts) (tl ts) ∧
(ts = [] ∨ (l (last ts) = fst w ∧ r (hd ts) = snd w)))"

(t ≠ Leaf ∧ r t = snd w ∧ (case ts of [] ⇒ l t = fst w
| u # us ⇒ adjacent (fst w, r u) ts ∧ l t = Suc (r u)))"
unfolding adjacent_def by (auto split: list.splits)

lemma adjacent_ConsI: "⟦t ≠ Leaf; r t = snd w;
(case ts of [] ⇒ l t = fst w
| u # us ⇒ adjacent (fst w, r u) ts ∧ l t = Suc (r u))⟧ ⟹

lemma adjacent_singleton: "t ≠ Leaf ⟹ adjacent (l t, r t) [t]"

lemma append_Cons_eq_append_append: "xs @ y # ys = xs @ [y] @ ys"
by simp

lemma list_all2_append_singletonI: "⟦list_all2 P xs ys; P x y⟧ ⟹ list_all2 P (xs @ [x]) (ys @ [y])"

lemma list_all2_Cons_append_singletonI: "⟦xs ≠ []; list_all2 P (x # butlast xs) ys; P (last xs) y⟧ ⟹ list_all2 P (x # xs) (ys @ [y])"
using list_all2_append_singletonI by fastforce

lemma adjacent_appendI: "⟦0 < fst w; fst w ≤ snd w;
(case us of [] ⇒ adjacent w ts
| u # us' ⇒ adjacent (Suc (r u), snd w) ts ∧ adjacent (fst w, (case ts of [] ⇒ snd w | ts ⇒ r u)) (u # us'))⟧ ⟹
by (auto simp: intro: list_all2_Cons_append_singletonI
list_all2_appendI[OF list_all2_Cons_append_singletonI, simplified] split: list.splits if_splits)

lemma (in semigroup_add) fold_add_add: "fold (+) xs (x + y) = fold (+) xs x + y"
by (induct xs arbitrary: x) (auto simp: add_assoc[symmetric])

context
fixes as :: "'a :: semigroup_add list"
and ws :: "window list"
begin

abbreviation atomic where
"atomic i ≡ Node i i (Some (nth as (i - 1))) Leaf Leaf"

definition atomics :: "nat ⇒ nat ⇒ 'a tree list" where
"atomics i j ≡ map atomic (rev [i ..< Suc j])"

definition slide :: "'a tree ⇒ window ⇒ 'a tree" where
"slide t w =
(let
ts = atomics (max (fst w) (Suc (r t))) (snd w);
ts' = reusables t w
in fold combine (ts @ ts') Leaf)"

primrec iterate :: "'a tree ⇒ window list ⇒ 'a list" where
"iterate t [] = []"
| "iterate t (w # xs) = (let t' = slide t w in the (val t') # iterate t' xs)"

definition sliding_window :: "'a list" where
"sliding_window = iterate Leaf ws"

section ‹Correctness›

abbreviation sum where
"sum i j ≡ fold (+) (rev (map (nth as) [i - 1 ..< j - 1])) (nth as (j - 1))"

primrec well_valued0 :: "'a tree ⇒ bool" where
"well_valued0 Leaf = True"
| "well_valued0 (Node i j a t u) = (0 < i ∧ j ≤ length as ∧ (a ≠ None ⟶ a = Some (sum i j)) ∧
well_valued0 t ∧ well_valued0 u ∧ (u = Leaf ∨ val u ≠ None))"

abbreviation well_valued :: "'a tree ⇒ bool" where
"well_valued t ≡ (well_valued0 t ∧ (t ≠ Leaf ⟶ val t ≠ None))"

definition valid :: "'a tree ⇒ bool" where
"valid t = (well_shaped t ∧ well_valued t)"

lemma valid_Leaf: "valid Leaf"
unfolding valid_def by auto

assumes "i > 0" "j ≥ i" "k > j"
shows "sum i j + sum (Suc j) k = sum i k"
proof -
have *: "[i - 1 ..< k - 1] = [i - 1..< j] @ [j..< k - 1]"
using assms upt_add_eq_append[of "i - 1" "j - 1" "k - j"]
by (cases j) (auto simp: upt_conv_Cons)
then show ?thesis using assms
qed

lemma well_valued0_rchild_if_well_valued0[simp]: "well_valued0 t ⟹ well_valued0 (rchild t)"
by (induct t) auto

lemma well_valued0_lchild_if_well_valued0[simp]: "well_valued0 t ⟹ well_valued0 (lchild t)"
by (induct t) auto

lemma valid_rchild_if_valid: "valid t ⟹ valid (rchild t)"
by (metis tree.exhaust_sel tree.sel(9) valid_def well_shaped_rchild well_valued0.simps(2))

lemma val_eq_Some_sum_if_valid_neq_Leaf: "⟦valid t; t ≠ Leaf⟧ ⟹ val t = Some (sum (l t) (r t))"
by (auto simp: valid_def foldr_conv_fold)
(metis One_nat_def option.distinct(1) option.inject tree.exhaust_sel well_valued0.simps(2))

subsection ‹Correctness of the Slide Function›

(* fact (b) part 1 *)
by (auto 0 1 simp: last_map last_rev nth_tl
map_butlast[symmetric] list_all2_conv_all_nth nth_Cons' rev_nth nth_append)

(* fact (b) part 2 *)
lemma valid_atomics: "⟦t ∈ set (atomics i j); 0 < i; j ≤ length as⟧ ⟹ valid t"
unfolding atomics_def
by (auto simp: valid_def)

lemma reusables_neq_Nil_if_well_shaped_and_overlapping:
"⟦well_shaped t; l t ≤ fst w; r t ≤ snd w; fst w ≤ r t⟧ ⟹ reusables t w ≠ []"
by (induction t w rule: reusables.induct) (simp add: reusables.simps Let_def)

lemma reusables_lchild_neq_Nil_under_some_conditions:
"⟦well_shaped t; l t ≤ fst w; r t ≤ snd w; fst w ≠ l t; r t ≥ fst w; l (rchild t) > fst w⟧ ⟹
reusables (lchild t) w ≠ []"
using r_lchild_eq_l_rchild_if_well_shaped[of "t"] r_lchild_le_r[of t]
by (intro reusables_neq_Nil_if_well_shaped_and_overlapping) auto

(* fact (a) part 1 *)
lemma adjacent_reusables: "⟦0 < fst w; well_shaped t; l t ≤ fst w; r t ≤ snd w⟧ ⟹
adjacent (fst w, r t) (reusables t w)"
proof (induction t w rule: reusables.induct)
case (1 t w)
show ?case
proof (cases "fst w > r t")
case False
with 1 show ?thesis
proof (cases "fst w = l t")
case False
then show ?thesis
proof (cases "fst w ≥ l (rchild t)")
case True
with 1 ‹fst w ≠ l t› show ?thesis by (subst reusables.simps) auto
next
case False
with 1 ‹fst w ≠ l t› ‹¬ fst w > r t› obtain x xs where *: "reusables (lchild t) w = x # xs"
by (cases "reusables (lchild t) w") (auto simp: reusables_lchild_neq_Nil_under_some_conditions)
with 1(2-6) ‹fst w ≠ l t› ‹¬ fst w > r t› ‹¬ l (rchild t) ≤ fst w›
have "adjacent (fst w, r (lchild t)) (x # xs)"
with 1 ‹fst w ≠ l t› ‹¬ fst w > r t› * show ?thesis
by (subst reusables.simps)
qed
qed (auto simp: reusables.simps intro!: adjacent_singleton)
qed (auto simp: reusables.simps)
qed

lemma valid_rchild_if_well_valued0: "⟦well_shaped t; well_valued0 t⟧ ⟹ valid (rchild t)"
by (metis tree.exhaust_sel tree.sel(9) valid_def well_shaped_rchild well_valued0.simps(2))

lemma valid_reusables_under_some_conditions:
"⟦0 < fst w; well_valued0 t; well_shaped t; l t < fst w; r t ≤ snd w⟧ ⟹
∀t' ∈ set (reusables t w). valid t'"
proof (induction t w rule: reusables.induct)
case (1 t w)
show ?case
proof (cases "fst w > r t")
case False
with 1 show ?thesis
proof (cases "fst w = l t")
next
case False
then show ?thesis
proof (cases "fst w ≥ l (rchild t)")
case True
with 1 ‹fst w ≠ l t› ‹¬ fst w > r t› have *: "Ball (set (reusables (rchild t) w)) valid"
by (metis (no_types, lifting) ball_empty dual_order.strict_trans2 leI le_neq_implies_less list.set(1) r_rchild_eq_r_if_well_shaped reusables.simps set_ConsD valid_rchild_if_well_valued0 well_shaped_rchild well_valued0_rchild_if_well_valued0)
from 1 ‹fst w ≠ l t› ‹¬ fst w > r t› True have "reusables t w = reusables (rchild t) w"
by (subst reusables.simps)
simp
with 1 * show ?thesis
by simp
next
case False
with 1 ‹fst w ≠ l t› ‹¬ fst w > r t› have *: "Ball (set (reusables (lchild t) w)) valid"
by (metis dual_order.strict_trans2 l_lchild_eq_l_if_well_shaped leI order_trans r_lchild_le_r well_shaped_lchild well_valued0_lchild_if_well_valued0)
with 1 have valid_rchild: "valid (rchild t)"
with 1 ‹fst w ≠ l t› ‹¬ fst w > r t› False have "reusables t w = rchild t # reusables (lchild t) w"
by (subst reusables.simps) presburger
with 1 ‹fst w ≠ l t› ‹¬ fst w > r t› False * valid_rchild show ?thesis
by (metis set_ConsD)
qed
qed (auto simp: reusables.simps)
qed (auto simp: reusables.simps)
qed

(* fact (a) part 2 *)
lemma valid_reusables:
assumes "0 < fst w" "valid t" "l t ≤ fst w" "r t ≤ snd w"
shows "∀t' ∈ set (reusables t w). valid t'"
proof (cases "l t < fst w")
case True
with assms show ?thesis
using valid_def valid_reusables_under_some_conditions by blast
next
case False
with assms show ?thesis
qed

lemma combine_valid_Nodes_aux:
assumes prems: "0 < l a" "a ≠ Leaf" "z ≠ Leaf" "l z = Suc (r a)" "well_shaped a" "well_shaped z"
"well_valued0 a" "val a = Some va" "well_valued0 z" "val z = Some vz"
shows "va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))"
proof -
from prems have "l a > 0" by simp
moreover from prems have "r a ≥ l a"
by (metis tree.collapse well_shaped.simps(2))
moreover have "r z > r a"
by (metis Suc_le_lessD prems(3) prems(4) prems(6) tree.collapse well_shaped.simps(2))
ultimately have *: "sum (l a) (r a) + sum (Suc (r a)) (r z) = sum (l a) (r z)"
from prems have "va = sum (l a) (r a)"
by (metis option.discI option.inject tree.collapse well_valued0.simps(2))
moreover from prems have "vz = sum (Suc (r a)) (r z)"
by (metis option.discI option.inject prems(2) prems(3) prems(8) prems(9) tree.collapse well_valued0.simps(2))
moreover have "fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0)) = sum (l a) (r z)"
by simp
ultimately show ?thesis
using * by (auto simp: add_sum)
qed

lemma discharge_is_Leaf[simp]: "discharge a = Leaf ⟷ a = Leaf"
by (cases a) auto

lemma well_shaped_discharge[simp]: "well_shaped a ⟹ well_shaped (discharge a)"
by (cases a) auto

lemma well_valued0_discharge[simp]: "well_valued0 a ⟹ well_valued0 (discharge a)"
by (cases a) auto

lemma l_discharge[simp]: "l (discharge a) = l a"
by (cases a) auto

lemma r_discharge[simp]: "r (discharge a) = r a"
by (cases a) auto

lemma well_shaped_lr: "well_shaped a ⟹ l a ≤ r a"
by (cases a) auto

lemma well_valued0_r: "well_valued0 a ⟹ a ≠ Leaf ⟹ r a ≤ length as"
by (cases a) auto

lemma valid_combine_if_valid: "⟦0 < l a; valid a; valid z; a ≠ Leaf; z ≠ Leaf; l z = Suc (r a)⟧ ⟹
valid (combine a z)"
by (force simp add: valid_def combine_non_Leaves combine_valid_Nodes_aux
dest: well_shaped_lr well_valued0_r)

lemma combine_neq_Leaf_if_both_non_Leaf: "⟦a ≠ Leaf; z ≠ Leaf⟧ ⟹
combine a z ≠ Leaf"

(* generalized version of fact (c) *)
lemma valid_fold_combine: "⟦0 < fst w; ts = h # ts'; ∀t ∈ set ts. valid t; adjacent (fst w, l h - 1) ts';
valid z; z ≠ Leaf; l z = (case ts' of [] ⇒ fst w | t⇩1 # ts'' ⇒ Suc (r t⇩1)); r z = snd w⟧ ⟹
valid (fold combine ts' z) ∧
l (fold combine ts' z) = fst w ∧ r (fold combine ts' z) = snd w"
proof (induction ts' arbitrary: z ts h)
case Nil
then show ?case by simp
next
case (Cons a ts')
moreover from Cons(3-4) have "valid a" by simp
moreover from Cons(5) have "adjacent (fst w, l a - Suc 0) ts'"
unfolding adjacent_Cons by (auto split: list.splits)
moreover from Cons(2-6,8) have "valid (combine a z)"
by (intro valid_combine_if_valid) (auto split: list.splits)
moreover from Cons(5,7) have "combine a z ≠ Leaf"
moreover from Cons(5,7) have "l (combine a z) = (case ts' of [] ⇒ fst w | t⇩1 # ts'' ⇒ Suc (r t⇩1))"
moreover from Cons(5,7,9) have "r (combine a z) = snd w"
ultimately show ?case
by simp
qed

(* fact (c) *)
lemma valid_fold_combine_Leaf:
assumes "0 < fst w" "ts = h # ts'" "∀t ∈ set ts. valid t" "adjacent w ts"
shows "valid (fold combine ts Leaf) ∧
l (fold combine ts Leaf) = fst w ∧ r (fold combine ts Leaf) = snd w"
proof -
from assms(2) have "fold combine ts Leaf = fold combine ts' h"
by simp
moreover have "valid (fold combine ts' h) ∧
l (fold combine ts' h) = fst w ∧ r (fold combine ts' h) = snd w"
proof (rule valid_fold_combine)
from assms show "0 < fst w" "ts = h # ts'" "∀t ∈ set ts. valid t" "valid h" "h ≠ Leaf" "r h = snd w"
"l h = (case ts' of [] ⇒ fst w | t⇩1 # ts'' ⇒ Suc (r t⇩1))"
from assms show "adjacent (fst w, l h - 1) ts'"
qed
ultimately show ?thesis by simp
qed

fixes x :: "'a tree" and xs :: "'a tree list"
assumes a1: "0 < fst w"
and a2: "l t ≤ fst w"
and a3: "r t ≤ snd w"
and a4: "valid t"
and a5: "reusables t w = x # xs"
shows "adjacent (Suc (r x), snd w) (atomics (max (fst w) (Suc (r t))) (snd w))"
proof -
have f6: "∀p ts. adjacent p ts = ((Leaf::'a tree) ∉ set ts ∧ list_all2 (λt ta. l t = Suc (r ta)) (butlast ts) (tl ts) ∧ (ts = [] ∨ l (last ts) = fst p ∧ r (hd ts) = snd p))"
then have f7: "Leaf ∉ set (atomics (max (fst w) (Suc (r t))) (snd w)) ∧ list_all2 (λt ta. l t = Suc (r ta)) (butlast (atomics (max (fst w) (Suc (r t))) (snd w))) (tl (atomics (max (fst w) (Suc (r t))) (snd w))) ∧ (atomics (max (fst w) (Suc (r t))) (snd w) = [] ∨ l (last (atomics (max (fst w) (Suc (r t))) (snd w))) = fst (max (fst w) (Suc (r t)), snd w) ∧ r (hd (atomics (max (fst w) (Suc (r t))) (snd w))) = snd (max (fst w) (Suc (r t)), snd w))"
have "adjacent (fst w, r t) (reusables t w)"
then have f8: "r x = r t"
have "max (fst w) (Suc (r t)) = Suc (r t)"
using a5 by (metis (no_types) Suc_n_not_le_n list.simps(3) max.bounded_iff max_def_raw not_le_imp_less reusables.simps)
then show ?thesis
using f8 f7 f6 by presburger
qed

lemma adjacent_Cons_r: "adjacent (a, r t) (x # xs) ⟹ adjacent (a, r x) (x # xs)"

"adjacent (fst w, r t) (x # xs) ⟹ 0 < fst w ⟹ fst w ≤ snd w ⟹ r t ≤ snd w ⟹
atomics (max (fst w) (Suc (r t))) (snd w) = [] ⟹
by (metis (no_types, lifting) atomics_def adjacent_def append_is_Nil_conv diff_Suc_Suc diff_zero le_Suc_eq list.simps(3) map_is_Nil_conv max_Suc_Suc max_def_raw prod.sel(1) prod.sel(2) rev_is_Nil_conv upt.simps(2))

"⟦0 < fst w; fst w ≤ snd w; valid t; l t ≤ fst w; r t ≤ snd w⟧ ⟹
adjacent w (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)"
using adjacent_atomics_nonempty_reusables[of w t] reusables_neq_Nil_if_well_shaped_and_overlapping[of t w]
by (intro adjacent_appendI) (auto simp: valid_def max.absorb1 atomize_not

lemma valid_append_atomics_reusables: "⟦0 < fst w; valid t; l t ≤ fst w; r t ≤ snd w; snd w ≤ length as⟧ ⟹
∀t ∈ set (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w). valid t"
by (auto simp only: set_append valid_reusables dest: valid_atomics split: if_splits)

lemma append_atomics_reusables_neq_Nil: "⟦0 < fst w; fst w ≤ snd w; valid t; l t ≤ fst w; r t ≤ snd w⟧ ⟹
atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w ≠ []"
by (simp add: reusables_neq_Nil_if_well_shaped_and_overlapping valid_def atomics_def)

(* lemma 1 *)
lemma valid_slide:
assumes "0 < fst w" "fst w ≤ snd w" "valid t" "l t ≤ fst w" "r t ≤ snd w" "snd w ≤ length as"
shows "valid (slide t w) ∧ l (slide t w) = fst w ∧ r (slide t w) = snd w"
proof -
from assms have non_empty: "atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w ≠ []"
using append_atomics_reusables_neq_Nil by blast
from assms have adjacent: "adjacent w (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w)"
from assms have valid: "∀t ∈ set (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w). valid t"
using valid_append_atomics_reusables by blast
have *: "slide t w = fold combine (atomics (max (fst w) (Suc (r t))) (snd w) @ reusables t w) Leaf"
from assms(1) non_empty adjacent valid show "valid (slide t w) ∧ l (slide t w) = fst w ∧ r (slide t w) = snd w"
unfolding * neq_Nil_conv using valid_fold_combine_Leaf by blast
qed

subsection ‹Correctness of the Sliding Window Algorithm›

lemma iterate_eq_map_sum: "⟦valid t; windows as xs; (case xs of [] ⇒ True | x # xs' ⇒ l t ≤ fst x ∧ r t ≤ snd x)⟧ ⟹
iterate t xs = map (λw. sum (fst w) (snd w)) xs"
by (induction xs arbitrary: t)
(auto simp: valid_slide windows_def window_def val_eq_Some_sum_if_valid_neq_Leaf neq_Leaf_if_l_gt0 split: list.split)

(* theorem 2: functional correctness *)
theorem correctness: "windows as ws ⟹ sliding_window = map (λw. sum (fst w) (snd w)) ws"
by (auto simp only: sliding_window_def intro!: iterate_eq_map_sum)
(auto simp: valid_def split: list.split)

end

(*<*)
value[code] "sliding_window [2,4,5,2 :: nat] [(1, 3), (1, 4), (2, 4)]"
value[code] "slide [2,4,5,2 :: nat] Leaf (1, 3)"
(*>*)

subsection ‹Summary of the Correctness Proof›

text ‹We closely follow Basin et al.'s proof outline~\<^cite>‹"BASIN2015186"›.
\begin{enumerate}
\item Lemma 1, the correctness result about the function @{term SWA.slide}, is formalized
by @{thm[source] SWA.valid_slide}. It follows from the following auxiliary facts:
\begin{itemize}
\item Fact (a) is formalized by @{thm[source] SWA.adjacent_reusables} and @{thm[source] SWA.valid_reusables}.
\item Fact (b) is formalized by @{thm[source] SWA.adjacent_atomics} and @{thm[source] SWA.valid_atomics}.
\item Fact (c) is formalized by @{thm[source] SWA.valid_fold_combine_Leaf}.
\end{itemize}
\item Theorem 2, the correctness result about the function @{term SWA.sliding_window}, is formalized
by @{thm[source] SWA.correctness}.
\end{enumerate}
›

section ‹Alternative Slide Interface and Additional Operations›

subsection ‹Alternative Slide Interface›

text ‹
The slide operation above takes the \emph{entire} input sequence as a parameter. This is often
impractical. We provide an alternative interface to the slide operation that takes only the
\emph{new} elements as a parameter.
›

abbreviation atomic' where
"atomic' as b idx ≡ Node b b (Some (nth as idx)) Leaf Leaf"

abbreviation atomics' :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ 'a tree list" where
"atomics' as i j sidx ≡ map (λb. atomic' as b (b - sidx)) (rev [i ..< Suc j])"

definition slide' :: "'a :: semigroup_add list ⇒ 'a tree ⇒ window ⇒ 'a tree" where
"slide' as t w =
(let
ts = atomics' as (max (fst w) (Suc (r t))) (snd w) (Suc (r t));
ts' = reusables t w
in fold combine (ts @ ts') Leaf)"

(* examples from paper *)
(*<*)
value[code] "slide' [2,4,5,2 :: nat] Leaf (1, 3)"
value[code] "slide' [2,4,5,2 :: nat] Leaf (1, 4)"
value[code] "slide' [2,4,5,2 :: nat] Leaf (2, 4)"
value[code] "slide' [2 :: nat] (slide' [2,4,5 :: nat] Leaf (1, 3)) (1, 4)"
value[code] "slide' [] (slide' [2 :: nat] (slide' [2,4,5 :: nat] Leaf (1, 3)) (1, 4)) (2, 4)"
value[code] "slide' [2,4,5 :: nat] Leaf (1, 3)"
value[code] "slide' [2 :: nat] (slide' [2,4,5 :: nat] Leaf (1, 3)) (2, 4)"
(*>*)

lemma slide_eq_slide':
assumes "0 < fst w" "fst w ≤ snd w" "valid as t" "r t = length as" "l t ≤ fst w" "r t ≤ snd w" "snd w ≤ length (as @ as')"
shows "slide (as @ as') t w = slide' as' t w"
proof (cases "r t = snd w")
case True
with assms have *: "atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = []"
by simp
from True assms have "atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t)) = []"
by simp
with * show ?thesis
unfolding slide_def slide'_def atomics_def by simp
next
case False
with assms have "r t < snd w"
by simp
with assms have "atomic' (as @ as') (snd w) (snd w - Suc 0) = atomic' as' (snd w) (snd w - Suc (length as))"
with assms have *: "∀i. i ∈ set ([max (fst w) (Suc (length as))..<snd w]) ⟶ atomic' (as @ as') i (i - Suc 0) = atomic' as' i (i - Suc (length as))"
by (auto simp: nth_append)
then have "map (λi. atomic' (as @ as') i (i - Suc 0)) (rev [max (fst w) (Suc (length as))..<snd w]) = map (λb. atomic' as' b (b - Suc (r t))) (rev [max (fst w) (Suc (r t))..<snd w])"
with assms have "atomics' (as @ as') (max (fst w) (Suc (r t))) (snd w) 1 = atomics' as' (max (fst w) (Suc (r t))) (snd w) (Suc (r t))"
by (auto simp: nth_append)
then show ?thesis
unfolding slide_def slide'_def atomics_def
by presburger
qed

lemma sum_eq_sum_append: "⟦0 < i; i ≤ j; j ≤ length as⟧ ⟹ sum as i j = sum (as @ as') i j"
proof -
assume assms: "0 < i" "i ≤ j" "j ≤ length as"
then have *: "rev (map ((!) as) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (as@as')) [i - Suc 0..<j - Suc 0])"
by (auto simp: nth_append)
from assms have "as ! (j - Suc 0) = (as @ as') ! (j - Suc 0)"
by (auto simp: nth_append)
then show ?thesis
qed

lemma well_valued0_append: "⟦well_shaped t; well_valued0 as t⟧ ⟹ well_valued0 (as @ as') t"
proof (induction t)
case (Node i j a t1 t2)
then show ?case
using sum_eq_sum_append
by (auto 4 0)
qed simp

lemma valid_append: "valid as t ⟹ valid (as @ as') t"
unfolding valid_def
by (auto intro: well_valued0_append)

lemma valid_slide_append: "⟦0 < fst w; fst w ≤ snd w; valid as t; l t ≤ fst w; r t ≤ snd w; snd w ≤ length as + length as'⟧ ⟹
valid (as @ as') (slide (as @ as') t w) ∧ l (slide (as @ as') t w) = fst w ∧ r (slide (as @ as') t w) = snd w"
by (auto simp: valid_append valid_slide)

(* correctness of alternative slide interface *)
theorem valid_slide':
assumes "0 < fst w" "fst w ≤ snd w" "valid as t" "length as = r t" "length as' ≥ snd w - r t" "l t ≤ fst w" "r t ≤ snd w"
shows "valid (as @ as') (slide' as' t w) ∧ l (slide' as' t w) = fst w ∧ r (slide' as' t w) = snd w"
proof -
from assms have "valid (as @ as') (slide (as @ as') t w) ∧ l (slide (as @ as') t w) = fst w ∧ r (slide (as @ as') t w) = snd w"
with assms show ?thesis
qed

subsection ‹Updating all Values in the Tree›

text ‹
So far, we have assumed that the sequence is fixed. However, under certain conditions,
SWA can be applied even if the sequence changes. In particular, if a function that distributes
over the associative operation is mapped onto the sequence, validity of the tree can be preserved
by mapping the same function onto the tree using @{term map_tree}.
›

lemma map_tree_eq_Leaf_iff: "map_tree f t = Leaf ⟷ t = Leaf"
by simp

lemma l_map_tree_eq_l[simp]: "l (map_tree f t) = l t"
by (cases t)
(auto split: option.splits)

lemma r_map_tree_eq_r[simp]: "r (map_tree f t) = r t"
by (cases t)
(auto split: option.splits)

lemma val_map_tree_neq_None: "val t ≠ None ⟹ val (map_tree f t) ≠ None"
by (cases t) auto

lemma well_shaped_map_tree: "well_shaped t ⟹ well_shaped (map_tree f t)"
by (induction t)
(auto split: option.split)

lemma fold_distr: "(∀x y. f (x + y) = f x + f y) ⟹ f (fold (+) list e) = fold (+) (map f list) (f e)"
by (induction list arbitrary: e) auto

lemma map_rev_map_nth_eq: "∀x ∈ set xs. x < length as ⟹ map f (rev (map ((!) as) xs)) = rev (map ((!) (map f as)) xs)"

lemma f_nth_eq_map_f_nth: "⟦as ≠ []; length as ≥ n⟧ ⟹ f (as ! (n - Suc 0)) = map f as ! (n - Suc 0)"
by (cases "n = length as") auto

lemma well_valued0_map_map_tree:
"⟦∀x y. f (x + y) = f x + f y; well_shaped t; well_valued0 as t; r t ≤ length as; as ≠ []⟧ ⟹
well_shaped (map_tree f t) ∧ well_valued0 (map f as) (map_tree f t)"
proof (rule conjI[OF well_shaped_map_tree], assumption, induction t)
case (Node i j a t1 t2)
then have "map f (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) =
rev (map ((!) (map f as)) [l t1 - Suc 0..<r t2 - Suc 0])"
by (subst map_rev_map_nth_eq) auto
moreover from Node have "r t1 ≤ length as"
by (cases t1) auto
ultimately show ?case using Node(3-7)
by (auto simp: fold_distr[of f] val_map_tree_neq_None
well_shaped_map_tree intro!: Node(1,2))
qed simp

lemma valid_map_map_tree:
assumes "∀x y. f (x + y) = f x + f y" "valid as t" "r t ≤ length as"
shows "valid (map f as) (map_tree f t)"
proof (cases "as ≠ []")
case True
with assms show ?thesis
by (metis map_tree_eq_Leaf_iff val_map_tree_neq_None valid_def well_valued0_map_map_tree)
next
case False
with assms show ?thesis
by (metis le_zero_eq list.size(3) tree.exhaust_sel map_tree_eq_Leaf_iff valid_Leaf valid_def well_shaped.simps(2) well_valued0.simps(2))
qed

lemma valid_Nil_iff: "valid [] t ⟷ t = Leaf"
unfolding valid_def
proof
assume "well_shaped t ∧ well_valued [] t"
then show "t = Leaf"
by (metis le_neq_implies_less list.size(3) not_less_zero tree.collapse well_shaped.simps(2) well_valued0.simps(2))
qed simp

subsection ‹Updating the Rightmost Leaf of the Tree›

text ‹
We provide a function to update the rightmost leaf of the tree. This may be used in an online
setting where the input sequence is not known in advance to update the latest observed element
using the same associative operation used in SWA. We show that validity of the tree is preserved
in this case.
›

fun update_rightmost :: "('a ⇒ 'a) ⇒ 'a tree ⇒ 'a tree" where
"update_rightmost _ Leaf = Leaf"
| "update_rightmost f (Node i j a t u) = Node i j (map_option f a) t (update_rightmost f u)"

lemma update_rightmost_eq_Leaf_iff: "update_rightmost f t = Leaf ⟷ t = Leaf"
by (cases t)
(auto split: option.splits)

lemma l_update_rightmost_eq_l[simp]: "l (update_rightmost f t) = l t"
by (cases t)
(auto split: option.splits)

lemma r_update_rightmost_eq_r[simp]: "r (update_rightmost f t) = r t"
by (cases t)
(auto split: option.splits)

lemma val_update_rightmost_neq_None: "val t ≠ None ⟹ val (update_rightmost f t) ≠ None"
by (cases t) auto

lemma well_shaped_update_rightmost: "well_shaped t ⟹ well_shaped (update_rightmost f t)"
by (induction t)
(auto simp: update_rightmost_eq_Leaf_iff split: option.split)

lemma sum_eq_sum_prepend: "⟦0 < i; i ≤ j; length xs < i; length ys = length xs⟧ ⟹ sum (xs @ as) i j = sum (ys @ as) i j"
proof -
assume assms: "0 < i" "i ≤ j" "length xs < i" "length ys = length xs"
then have *: "rev (map ((!) (xs @ as)) [i - Suc 0..<j - Suc 0]) = rev (map ((!) (ys @ as)) [i - Suc 0..<j - Suc 0])"
by (auto simp: nth_append)
from assms have "(xs @ as) ! (j - Suc 0) = (ys @ as) ! (j - Suc 0)"
by (auto simp: nth_append)
then show ?thesis
qed

lemma well_valued0_prepend: "⟦length xs ≤ l t - 1; length ys = length xs; well_shaped t; well_valued0 (xs @ as) t⟧ ⟹ well_valued0 (ys @ as) t"
proof (induction t)
case (Node i j a t1 t2)
then have well_valued0_t1: "well_valued0 (ys @ as) t1"
by auto
from Node have "well_valued0 (ys @ as) t2"
proof (cases a)
case None
with Node show ?thesis
by auto
(metis One_nat_def Suc_pred diff_Suc_1 le_Suc_eq le_Suc_ex trans_le_add1 tree.exhaust_sel well_shaped.simps(2))
next
case (Some a')
with Node show ?thesis
by auto
(metis One_nat_def diff_Suc_1 diff_le_self le_trans tree.exhaust_sel well_shaped.simps(2))
qed
with Node well_valued0_t1 show ?case
proof -
have f1: "0 < i ∧ j ≤ length (xs @ as) ∧ (a = None ∨ a = Some (SWA.sum (xs @ as) i j)) ∧ well_valued0 (xs @ as) t1 ∧ well_valued0 (xs @ as) t2 ∧ (t2 = Leaf ∨ val t2 ≠ None)"
by (meson ‹well_valued0 (xs @ as) (Node i j a t1 t2)› well_valued0.simps(2))
then have f2: "j ≤ length (ys @ as)"
by (simp add: ‹length ys = length xs›)
have "a = None ∨ a = Some (SWA.sum (ys @ as) i j)"
using f1 by (metis Node.prems(1) Node.prems(2) Node.prems(3) One_nat_def Suc_pred le_imp_less_Suc sum_eq_sum_prepend tree.sel(2) well_shaped.simps(2))
then show ?thesis
using f2 f1 ‹well_valued0 (ys @ as) t2› well_valued0.simps(2) well_valued0_t1 by blast
qed
qed simp

lemma valid_prepend: "⟦length xs ≤ l t - 1; length ys = length xs; valid (xs @ as) t⟧ ⟹ valid (ys @ as) t"
unfolding valid_def
by (auto intro: well_valued0_prepend)

lemma take_eq_append_take_take_drop: "m ≤ n ⟹ take n xs = take m xs @ take (n-m) (drop m xs)"
proof (induction xs)
case (Cons a xs)
then show ?case
qed simp

lemma well_valued0_take_r: "⟦well_shaped t; well_valued0 as t⟧ ⟹ well_valued0 (take (r t) as) t"
proof (induction t)
case (Node i j a t1 t2)
from Node have well_valued0_t1: "well_valued0 (take j as) t1"
proof -
from Node have "r t1 ≤ j"
using r_lchild_le_r by (metis tree.sel(4) tree.sel(8))
with Node have "take j as = take (r t1) as @ take (j - r t1) (drop (r t1) as)"
using take_eq_append_take_take_drop[of "r t1" j as] by simp
with Node show ?thesis
by (auto intro!: well_valued0_append)
qed
from Node have well_valued0_t2: "well_valued0 (take j as) t2"
by auto
from Node have sum_eq: "fold (+) (rev (map ((!) as) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0)) =
fold (+) (rev (map ((!) (take (r t2) as)) [l t1 - Suc 0..<r t2 - Suc 0])) (as ! (r t2 - Suc 0))"
by (intro arg_cong[where f="λxs. fold _ xs _"]) auto
from Node well_valued0_t1 well_valued0_t2 sum_eq show ?case
by auto
qed simp

lemma valid_take_r: "valid as t ⟹ valid (take (r t) as) t"
unfolding valid_def
by (auto intro: well_valued0_take_r)

lemma well_valued0_butlast: "⟦well_shaped t; well_valued0 as t; r t < length as⟧ ⟹ well_valued0 (butlast as) t"
proof (induction t)
case (Node i j a t1 t2)
then  have r_le_length: "j ≤ length (butlast as)"
by simp
from Node have "i > 0"
by simp
with r_le_length Node have sum_eq: "sum as i j = sum (butlast as) i j"
by (metis append_butlast_last_id le_zero_eq less_imp_le_nat list.size(3) neq_iff
sum_eq_sum_append well_shaped.simps(2))
from Node have "r t1 < length as"
by (metis dual_order.strict_trans2 r_lchild_le_r tree.sel(8))
with Node r_le_length show ?case
by (metis (no_types, lifting) dual_order.strict_iff_order sum_eq tree.sel(10) tree.sel(4)
well_shaped.simps(2) well_shaped_rchild well_valued0.simps(2))
qed simp

lemma well_valued0_append_butlast_lchild: "⟦well_shaped t; well_valued0 as t⟧ ⟹
well_valued0 (butlast as @ [last as + x]) (lchild t)"
proof (cases t)
case (Node i j a t1 t2)
assume assms: "well_shaped t" "well_valued0 as t"
from Node assms have "r t1 < length as"
by (fastforce dest: well_shaped_lr)
with Node assms show ?thesis
by (auto simp: well_valued0_butlast well_valued0_append)
qed simp

lemma sum_update_rightmost: "⟦0 < i; i ≤ j; length as = j⟧ ⟹
sum as i j + x = sum (butlast as @ [last as + x]) i j"
by (cases as)
intro!: arg_cong2[where f="(+)"] arg_cong[where f="λxs. fold _ xs _"])

lemma well_valued0_update_rightmost: "⟦well_shaped t; well_valued0 as t; length as = r t⟧ ⟹
well_valued0 (butlast as @ [last as + x]) (update_rightmost (λa. a + x) t)"
proof (induction t)
case Leaf
then show ?case
next
case (Node i j a t1 t2)
moreover
from Node have well_valued0_t1: "well_valued0 (butlast as @ [last as + x]) t1"
using well_valued0_append_butlast_lchild by (metis tree.sel(8))
moreover
from Node have well_valued0_t2:
"well_valued0 (butlast as @ [last as + x]) (update_rightmost ((λa. a + x)) t2)"
by (metis ‹well_valued0 (butlast as @ [last as + x]) t1› dual_order.strict_iff_order
tree.sel(4) update_rightmost.simps(1) well_shaped.simps(2) well_valued0.simps(2))
ultimately show ?case
using sum_update_rightmost
by (cases a) (auto simp: val_update_rightmost_neq_None)
qed

(* correctness of update_rightmost *)
lemma valid_update_rightmost: "⟦valid as t; length as = r t⟧ ⟹
valid (butlast as @ [last as + x]) (update_rightmost (λa. a + x) t)"
unfolding valid_def
using well_valued0_update_rightmost
by (metis update_rightmost.simps(1) val_update_rightmost_neq_None well_shaped_update_rightmost)

(*<*)
end
(*>*)