# Theory Window

```theory Window
imports "HOL-Library.AList" "HOL-Library.Mapping" "HOL-Library.While_Combinator" Timestamp
begin

type_synonym ('a, 'b) mmap = "('a × 'b) list"

(* 'b is a polymorphic input symbol; 'c is a polymorphic DFA state;
'd is a timestamp; 'e is a submonitor state *)

inductive chain_le :: "'d :: timestamp list ⇒ bool" where
chain_le_Nil: "chain_le []"
| chain_le_singleton: "chain_le [x]"
| chain_le_cons: "chain_le (y # xs) ⟹ x ≤ y ⟹ chain_le (x # y # xs)"

lemma chain_le_app: "chain_le (zs @ [z]) ⟹ z ≤ w ⟹ chain_le ((zs @ [z]) @ [w])"
apply (induction "zs @ [z]" arbitrary: zs rule: chain_le.induct)
apply (auto intro: chain_le.intros)[2]
subgoal for y xs x zs
apply (cases zs)
apply (auto)
apply (metis append.assoc append_Cons append_Nil chain_le_cons)
done
done

inductive reaches_on :: "('e ⇒ ('e × 'f) option) ⇒ 'e ⇒ 'f list ⇒ 'e ⇒ bool"
for run :: "'e ⇒ ('e × 'f) option" where
"reaches_on run s [] s"
| "run s = Some (s', v) ⟹ reaches_on run s' vs s'' ⟹ reaches_on run s (v # vs) s''"

lemma reaches_on_init_Some: "reaches_on r s xs s' ⟹ r s' ≠ None ⟹ r s ≠ None"
by (auto elim: reaches_on.cases)

lemma reaches_on_split: "reaches_on run s vs s' ⟹ i < length vs ⟹
∃s'' s'''. reaches_on run s (take i vs) s'' ∧ run s'' = Some (s''', vs ! i) ∧ reaches_on run s''' (drop (Suc i) vs) s'"
proof (induction s vs s' arbitrary: i rule: reaches_on.induct)
case (2 s s' v vs s'')
show ?case
using 2(1,2)
proof (cases i)
case (Suc n)
show ?thesis
using 2
by (fastforce simp: Suc intro: reaches_on.intros)
qed (auto intro: reaches_on.intros)
qed auto

lemma reaches_on_split': "reaches_on run s vs s' ⟹ i ≤ length vs ⟹
∃s'' . reaches_on run s (take i vs) s'' ∧ reaches_on run s'' (drop i vs) s'"
proof (induction s vs s' arbitrary: i rule: reaches_on.induct)
case (2 s s' v vs s'')
show ?case
using 2(1,2)
proof (cases i)
case (Suc n)
show ?thesis
using 2
by (fastforce simp: Suc intro: reaches_on.intros)
qed (auto intro: reaches_on.intros)
qed (auto intro: reaches_on.intros)

lemma reaches_on_split_app: "reaches_on run s (vs @ vs') s' ⟹
∃s''. reaches_on run s vs s'' ∧ reaches_on run s'' vs' s'"
using reaches_on_split'[where i="length vs", of run s "vs @ vs'" s']
by auto

lemma reaches_on_inj: "reaches_on run s vs t ⟹ reaches_on run s vs' t' ⟹
length vs = length vs' ⟹ vs = vs' ∧ t = t'"
apply (induction s vs t arbitrary: vs' t' rule: reaches_on.induct)
apply (auto elim: reaches_on.cases)[1]
subgoal for s s' v vs s'' vs' t'
apply (rule reaches_on.cases[of run s' vs s'']; rule reaches_on.cases[of run s vs' t'])
apply assumption+
apply auto[2]
apply fastforce
apply (metis length_0_conv list.discI)
apply (metis Pair_inject length_Cons nat.inject option.inject)
done
done

lemma reaches_on_split_last: "reaches_on run s (xs @ [x]) s'' ⟹
∃s'. reaches_on run s xs s' ∧ run s' = Some (s'', x)"
apply (induction s "xs @ [x]" s'' arbitrary: xs x rule: reaches_on.induct)
apply simp
subgoal for s s' v vs s'' xs x
by (cases vs rule: rev_cases) (fastforce elim: reaches_on.cases intro: reaches_on.intros)+
done

lemma reaches_on_rev_induct[consumes 1]: "reaches_on run s vs s' ⟹
(⋀s. P s [] s) ⟹
(⋀s s' v vs s''. reaches_on run s vs s' ⟹ P s vs s' ⟹ run s' = Some (s'', v) ⟹
P s (vs @ [v]) s'') ⟹
P s vs s'"
proof (induction vs arbitrary: s s' rule: rev_induct)
case (snoc x xs)
from snoc(2) obtain s'' where s''_def: "reaches_on run s xs s''" "run s'' = Some (s', x)"
using reaches_on_split_last
by fast
show ?case
using snoc(4)[OF s''_def(1) _ s''_def(2)] snoc(1)[OF s''_def(1) snoc(3,4)]
by auto
qed (auto elim: reaches_on.cases)

lemma reaches_on_app: "reaches_on run s vs s' ⟹ run s' = Some (s'', v) ⟹
reaches_on run s (vs @ [v]) s''"
by (induction s vs s' rule: reaches_on.induct) (auto intro: reaches_on.intros)

lemma reaches_on_trans: "reaches_on run s vs s' ⟹ reaches_on run s' vs' s'' ⟹
reaches_on run s (vs @ vs') s''"
by (induction s vs s' rule: reaches_on.induct) (auto intro: reaches_on.intros)

lemma reaches_onD: "reaches_on run s ((t, b) # vs) s' ⟹
∃s''. run s = Some (s'', (t, b)) ∧ reaches_on run s'' vs s'"
by (auto elim: reaches_on.cases)

lemma reaches_on_setD: "reaches_on run s vs s' ⟹ x ∈ set vs ⟹
∃vs' vs'' s''. reaches_on run s (vs' @ [x]) s'' ∧ reaches_on run s'' vs'' s' ∧ vs = vs' @ x # vs''"
proof (induction s vs s' rule: reaches_on_rev_induct)
case (2 s s' v vs s'')
show ?case
proof (cases "x ∈ set vs")
case True
obtain vs' vs'' s''' where split_def: "reaches_on run s (vs' @ [x]) s'''"
"reaches_on run s''' vs'' s'" "vs = vs' @ x # vs''"
using 2(3)[OF True]
by auto
show ?thesis
using split_def(1,3) reaches_on_app[OF split_def(2) 2(2)]
by auto
next
case False
have x_v: "x = v"
using 2(4) False
by auto
show ?thesis
unfolding x_v
using reaches_on_app[OF 2(1,2)] reaches_on.intros(1)[of run s'']
by auto
qed
qed auto

lemma reaches_on_len: "∃vs s'. reaches_on run s vs s' ∧ (length vs = n ∨ run s' = None)"
proof (induction n arbitrary: s)
case (Suc n)
show ?case
proof (cases "run s")
case (Some x)
obtain s' v where x_def: "x = (s', v)"
by (cases x) auto
obtain vs s'' where s''_def: "reaches_on run s' vs s''" "length vs = n ∨ run s'' = None"
using Suc[of s']
by auto
show ?thesis
using reaches_on.intros(2)[OF Some[unfolded x_def] s''_def(1)] s''_def(2)
by fastforce
qed (auto intro: reaches_on.intros)
qed (auto intro: reaches_on.intros)

lemma reaches_on_NilD: "reaches_on run q [] q' ⟹ q = q'"
by (auto elim: reaches_on.cases)

lemma reaches_on_ConsD: "reaches_on run q (x # xs) q' ⟹ ∃q''. run q = Some (q'', x) ∧ reaches_on run q'' xs q'"
by (auto elim: reaches_on.cases)

inductive reaches :: "('e ⇒ ('e × 'f) option) ⇒ 'e ⇒ nat ⇒ 'e ⇒ bool"
for run :: "'e ⇒ ('e × 'f) option" where
"reaches run s 0 s"
| "run s = Some (s', v) ⟹ reaches run s' n s'' ⟹ reaches run s (Suc n) s''"

lemma reaches_Suc_split_last: "reaches run s (Suc n) s' ⟹ ∃s'' x. reaches run s n s'' ∧ run s'' = Some (s', x)"
proof (induction n arbitrary: s)
case (Suc n)
obtain s'' x where s''_def: "run s = Some (s'', x)" "reaches run s'' (Suc n) s'"
using Suc(2)
by (auto elim: reaches.cases)
show ?case
using s''_def(1) Suc(1)[OF s''_def(2)]
by (auto intro: reaches.intros)
qed (auto elim!: reaches.cases intro: reaches.intros)

lemma reaches_invar: "reaches f x n y ⟹ P x ⟹ (⋀z z' v. P z ⟹ f z = Some (z', v) ⟹ P z') ⟹ P y"
by (induction x n y rule: reaches.induct) auto

lemma reaches_cong: "reaches f x n y ⟹ P x ⟹ (⋀z z' v. P z ⟹ f z = Some (z', v) ⟹ P z') ⟹ (⋀z. P z ⟹ f' (g z) = map_option (apfst g) (f z)) ⟹ reaches f' (g x) n (g y)"
by (induction x n y rule: reaches.induct) (auto intro: reaches.intros)

lemma reaches_on_n: "reaches_on run s vs s' ⟹ reaches run s (length vs) s'"
by (induction s vs s' rule: reaches_on.induct) (auto intro: reaches.intros)

lemma reaches_on: "reaches run s n s' ⟹ ∃vs. reaches_on run s vs s' ∧ length vs = n"
by (induction s n s' rule: reaches.induct) (auto intro: reaches_on.intros)

definition ts_at :: "('d × 'b) list ⇒ nat ⇒ 'd" where
"ts_at rho i = fst (rho ! i)"

definition bs_at :: "('d × 'b) list ⇒ nat ⇒ 'b" where
"bs_at rho i = snd (rho ! i)"

fun sub_bs :: "('d × 'b) list ⇒ nat × nat ⇒ 'b list" where
"sub_bs rho (i, j) = map (bs_at rho) [i..<j]"

definition steps :: "('c ⇒ 'b ⇒ 'c) ⇒ ('d × 'b) list ⇒ 'c ⇒ nat × nat ⇒ 'c" where
"steps step rho q ij = foldl step q (sub_bs rho ij)"

definition acc :: "('c ⇒ 'b ⇒ 'c) ⇒ ('c ⇒ bool) ⇒ ('d × 'b) list ⇒
'c ⇒ nat × nat ⇒ bool" where
"acc step accept rho q ij = accept (steps step rho q ij)"

definition sup_acc :: "('c ⇒ 'b ⇒ 'c) ⇒ ('c ⇒ bool) ⇒ ('d × 'b) list ⇒
'c ⇒ nat ⇒ nat ⇒ ('d × nat) option" where
"sup_acc step accept rho q i j =
(let L' = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}; m = Max L' in
if L' = {} then None else Some (ts_at rho m, m))"

definition sup_leadsto :: "'c ⇒ ('c ⇒ 'b ⇒ 'c) ⇒ ('d × 'b) list ⇒
nat ⇒ nat ⇒ 'c ⇒ 'd option" where
"sup_leadsto init step rho i j q =
(let L' = {l. l < i ∧ steps step rho init (l, j) = q}; m = Max L' in
if L' = {} then None else Some (ts_at rho m))"

definition mmap_keys :: "('a, 'b) mmap ⇒ 'a set" where
"mmap_keys kvs = set (map fst kvs)"

definition mmap_lookup :: "('a, 'b) mmap ⇒ 'a ⇒ 'b option" where
"mmap_lookup = map_of"

definition valid_s :: "'c ⇒ ('c ⇒ 'b ⇒ 'c) ⇒ ('c × 'b, 'c) mapping ⇒ ('c ⇒ bool) ⇒
('d × 'b) list ⇒ nat ⇒ nat ⇒ nat ⇒ ('c, 'c × ('d × nat) option) mmap ⇒ bool" where
"valid_s init step st accept rho u i j s ≡
(∀q bs. case Mapping.lookup st (q, bs) of None ⇒ True | Some v ⇒ step q bs = v) ∧
(mmap_keys s = {q. (∃l ≤ u. steps step rho init (l, i) = q)} ∧ distinct (map fst s) ∧
(∀q. case mmap_lookup s q of None ⇒ True
| Some (q', tstp) ⇒ steps step rho q (i, j) = q' ∧ tstp = sup_acc step accept rho q i j))"

record ('b, 'c, 'd, 't, 'e) args =
w_init :: 'c
w_step :: "'c ⇒ 'b ⇒ 'c"
w_accept :: "'c ⇒ bool"
w_run_t :: "'t ⇒ ('t × 'd) option"
w_read_t :: "'t ⇒ 'd option"
w_run_sub :: "'e ⇒ ('e × 'b) option"

record ('b, 'c, 'd, 't, 'e) window =
w_st :: "('c × 'b, 'c) mapping"
w_ac :: "('c, bool) mapping"
w_i :: nat
w_ti :: 't
w_si :: 'e
w_j :: nat
w_tj :: 't
w_sj :: 'e
w_s :: "('c, 'c × ('d × nat) option) mmap"
w_e :: "('c, 'd) mmap"

fun reach_window :: "('b, 'c, 'd, 't, 'e) args ⇒ 't ⇒ 'e ⇒
('d × 'b) list ⇒ nat × 't × 'e × nat × 't × 'e ⇒ bool" where
"reach_window args t0 sub rho (i, ti, si, j, tj, sj) ⟷ i ≤ j ∧ length rho = j ∧
reaches_on (w_run_t args) t0 (take i (map fst rho)) ti ∧
reaches_on (w_run_t args) ti (drop i (map fst rho)) tj ∧
reaches_on (w_run_sub args) sub (take i (map snd rho)) si ∧
reaches_on (w_run_sub args) si (drop i (map snd rho)) sj"

lemma reach_windowI: "reaches_on (w_run_t args) t0 (take i (map fst rho)) ti ⟹
reaches_on (w_run_sub args) sub (take i (map snd rho)) si ⟹
reaches_on (w_run_t args) t0 (map fst rho) tj ⟹
reaches_on (w_run_sub args) sub (map snd rho) sj ⟹
i ≤ length rho ⟹ length rho = j ⟹
reach_window args t0 sub rho (i, ti, si, j, tj, sj)"
by auto (metis reaches_on_split'[of _ _ _ _ i] length_map reaches_on_inj)+

lemma reach_window_shift:
assumes "reach_window args t0 sub rho (i, ti, si, j, tj, sj)" "i < j"
"w_run_t args ti = Some (ti', t)" "w_run_sub args si = Some (si', s)"
shows "reach_window args t0 sub rho (Suc i, ti', si', j, tj, sj)"
using reaches_on_app[of "w_run_t args" t0 "take i (map fst rho)" ti ti' t]
reaches_on_app[of "w_run_sub args" sub "take i (map snd rho)" si si' s] assms
apply (auto)
apply (smt append_take_drop_id id_take_nth_drop length_map list.discI list.inject
option.inject reaches_on.cases same_append_eq snd_conv take_Suc_conv_app_nth)
apply (smt Cons_nth_drop_Suc fst_conv length_map list.discI list.inject option.inject
reaches_on.cases)
apply (smt append_take_drop_id id_take_nth_drop length_map list.discI list.inject
option.inject reaches_on.cases same_append_eq snd_conv take_Suc_conv_app_nth)
apply (smt Cons_nth_drop_Suc fst_conv length_map list.discI list.inject option.inject
reaches_on.cases)
done

lemma reach_window_run_ti: "reach_window args t0 sub rho (i, ti, si, j, tj, sj) ⟹
i < j ⟹ ∃ti'. reaches_on (w_run_t args) t0 (take i (map fst rho)) ti ∧
w_run_t args ti = Some (ti', ts_at rho i) ∧
reaches_on (w_run_t args) ti' (drop (Suc i) (map fst rho)) tj"
apply (auto simp: ts_at_def elim!: reaches_on.cases[of "w_run_t args" ti "drop i (map fst rho)"])
using nth_via_drop apply fastforce
by (metis Cons_nth_drop_Suc length_map list.inject)

lemma reach_window_run_si: "reach_window args t0 sub rho (i, ti, si, j, tj, sj) ⟹
i < j ⟹ ∃si'. reaches_on (w_run_sub args) sub (take i (map snd rho)) si ∧
w_run_sub args si = Some (si', bs_at rho i) ∧
reaches_on (w_run_sub args) si' (drop (Suc i) (map snd rho)) sj"
apply (auto simp: bs_at_def elim!: reaches_on.cases[of "w_run_sub args" si "drop i (map snd rho)"])
using nth_via_drop apply fastforce
by (metis Cons_nth_drop_Suc length_map list.inject)

lemma reach_window_run_tj: "reach_window args t0 sub rho (i, ti, si, j, tj, sj) ⟹
reaches_on (w_run_t args) t0 (map fst rho) tj"
using reaches_on_trans
by fastforce

lemma reach_window_run_sj: "reach_window args t0 sub rho (i, ti, si, j, tj, sj) ⟹
reaches_on (w_run_sub args) sub (map snd rho) sj"
using reaches_on_trans
by fastforce

lemma reach_window_shift_all: "reach_window args t0 sub rho (i, si, ti, j, sj, tj) ⟹
reach_window args t0 sub rho (j, sj, tj, j, sj, tj)"
using reach_window_run_tj[of args t0 sub rho] reach_window_run_sj[of args t0 sub rho]
by (auto intro: reaches_on.intros)

lemma reach_window_app: "reach_window args t0 sub rho (i, si, ti, j, tj, sj) ⟹
w_run_t args tj = Some (tj', x) ⟹ w_run_sub args sj = Some (sj', y) ⟹
reach_window args t0 sub (rho @ [(x, y)]) (i, si, ti, Suc j, tj', sj')"

fun init_args :: "('c × ('c ⇒ 'b ⇒ 'c) × ('c ⇒ bool)) ⇒
(('t ⇒ ('t × 'd) option) × ('t ⇒ 'd option)) ⇒
('e ⇒ ('e × 'b) option) ⇒ ('b, 'c, 'd, 't, 'e) args" where
"init_args (init, step, accept) (run_t, read_t) run_sub =
⦇w_init = init, w_step = step, w_accept = accept, w_run_t = run_t, w_read_t = read_t, w_run_sub = run_sub⦈"

fun init_window :: "('b, 'c, 'd, 't, 'e) args ⇒ 't ⇒ 'e ⇒ ('b, 'c, 'd, 't, 'e) window" where
"init_window args t0 sub = ⦇w_st = Mapping.empty, w_ac = Mapping.empty,
w_i = 0, w_ti = t0, w_si = sub, w_j = 0, w_tj = t0, w_sj = sub,
w_s =[(w_init args, (w_init args, None))], w_e = []⦈"

definition valid_window :: "('b, 'c, 'd :: timestamp, 't, 'e) args ⇒ 't ⇒ 'e ⇒ ('d × 'b) list ⇒
('b, 'c, 'd, 't, 'e) window ⇒ bool" where
"valid_window args t0 sub rho w ⟷
(let init = w_init args; step = w_step args; accept = w_accept args;
run_t = w_run_t args; run_sub = w_run_sub args;
st = w_st w; ac = w_ac w;
i = w_i w; ti = w_ti w; si = w_si w; j = w_j w; tj = w_tj w; sj = w_sj w;
s = w_s w; e = w_e w in
(reach_window args t0 sub rho (i, ti, si, j, tj, sj) ∧
(∀i j. i ≤ j ∧ j < length rho ⟶ ts_at rho i ≤ ts_at rho j) ∧
(∀q. case Mapping.lookup ac q of None ⇒ True | Some v ⇒ accept q = v) ∧
(∀q. mmap_lookup e q = sup_leadsto init step rho i j q) ∧ distinct (map fst e) ∧
valid_s init step st accept rho i i j s))"

lemma valid_init_window: "valid_window args t0 sub [] (init_window args t0 sub)"
by (auto simp: valid_window_def mmap_keys_def mmap_lookup_def sup_leadsto_def
valid_s_def steps_def sup_acc_def intro: reaches_on.intros split: option.splits)

lemma steps_app_cong: "j ≤ length rho ⟹ steps step (rho @ [x]) q (i, j) =
steps step rho q (i, j)"
proof -
assume "j ≤ length rho"
then have map_cong: "map (bs_at (rho @ [x])) [i..<j] = map (bs_at rho) [i..<j]"
by (auto simp: bs_at_def nth_append)
show ?thesis
by (auto simp: steps_def map_cong)
qed

lemma acc_app_cong: "j < length rho ⟹ acc step accept (rho @ [x]) q (i, j) =
acc step accept rho q (i, j)"
by (auto simp: acc_def bs_at_def nth_append steps_app_cong)

lemma sup_acc_app_cong: "j ≤ length rho ⟹ sup_acc step accept (rho @ [x]) q i j =
sup_acc step accept rho q i j"
apply (auto simp: sup_acc_def Let_def ts_at_def nth_append acc_def)
apply (metis (mono_tags, opaque_lifting) less_eq_Suc_le order_less_le_trans steps_app_cong)+
done

lemma sup_acc_concat_cong: "j ≤ length rho ⟹ sup_acc step accept (rho @ rho') q i j =
sup_acc step accept rho q i j"
apply (induction rho' rule: rev_induct)
apply auto
apply (smt append.assoc le_add1 le_trans length_append sup_acc_app_cong)
done

lemma sup_leadsto_app_cong: "i ≤ j ⟹ j ≤ length rho ⟹
sup_leadsto init step (rho @ [x]) i j q = sup_leadsto init step rho i j q"
proof -
assume assms: "i ≤ j" "j ≤ length rho"
define L' where "L' = {l. l < i ∧ steps step rho init (l, j) = q}"
define L'' where "L'' = {l. l < i ∧ steps step (rho @ [x]) init (l, j) = q}"
show ?thesis
using assms
by (cases "L' = {}")
(auto simp: sup_leadsto_def L'_def L''_def ts_at_def nth_append steps_app_cong)
qed

lemma chain_le:
fixes xs :: "'d :: timestamp list"
shows "chain_le xs ⟹ i ≤ j ⟹ j < length xs ⟹ xs ! i ≤ xs ! j"
proof (induction xs arbitrary: i j rule: chain_le.induct)
case (chain_le_cons y xs x)
then show ?case
proof (cases i)
case 0
then show ?thesis
using chain_le_cons
apply (cases j)
apply auto
done
qed auto
qed auto

lemma steps_refl[simp]: "steps step rho q (i, i) = q"
unfolding steps_def by auto

lemma steps_split: "i < j ⟹ steps step rho q (i, j) =
steps step rho (step q (bs_at rho i)) (Suc i, j)"
unfolding steps_def by (simp add: upt_rec)

lemma steps_app: "i ≤ j ⟹ steps step rho q (i, j + 1) =
step (steps step rho q (i, j)) (bs_at rho j)"
unfolding steps_def by auto

lemma steps_appE: "i ≤ j ⟹ steps step rho q (i, Suc j) = q' ⟹
∃q''. steps step rho q (i, j) = q'' ∧ q' = step q'' (bs_at rho j)"
unfolding steps_def sub_bs.simps by auto

lemma steps_comp: "i ≤ l ⟹ l ≤ j ⟹ steps step rho q (i, l) = q' ⟹
steps step rho q' (l, j) = q'' ⟹ steps step rho q (i, j) = q''"
proof -
assume assms: "i ≤ l" "l ≤ j" "steps step rho q (i, l) = q'" "steps step rho q' (l, j) = q''"
have range_app: "[i..<l] @ [l..<j] = [i..<j]"
using assms(1,2)
have "q' = foldl step q (map (bs_at rho) [i..<l])"
using assms(3) unfolding steps_def by auto
moreover have "q'' = foldl step q' (map (bs_at rho) [l..<j])"
using assms(4) unfolding steps_def by auto
ultimately have "q'' = foldl step q (map (bs_at rho) ([i..<l] @ [l..<j]))"
by auto
then show ?thesis
unfolding steps_def range_app by auto
qed

lemma sup_acc_SomeI: "acc step accept rho q (i, Suc l) ⟹ l ∈ {i..<j} ⟹
∃tp. sup_acc step accept rho q i j = Some (ts_at rho tp, tp) ∧ l ≤ tp ∧ tp < j"
proof -
assume assms: "acc step accept rho q (i, Suc l)" "l ∈ {i..<j}"
define L where "L = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
have L_props: "finite L" "L ≠ {}" "l ∈ L"
using assms unfolding L_def by auto
then show "∃tp. sup_acc step accept rho q i j = Some (ts_at rho tp, tp) ∧ l ≤ tp ∧ tp < j"
using L_def L_props
(smt L_props(1) L_props(2) Max_ge Max_in mem_Collect_eq)
qed

lemma sup_acc_Some_ts: "sup_acc step accept rho q i j = Some (ts, tp) ⟹ ts = ts_at rho tp"
by (auto simp add: sup_acc_def Let_def split: if_splits)

lemma sup_acc_SomeE: "sup_acc step accept rho q i j = Some (ts, tp) ⟹
tp ∈ {i..<j} ∧ acc step accept rho q (i, Suc tp)"
proof -
assume assms: "sup_acc step accept rho q i j = Some (ts, tp)"
define L where "L  = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
have L_props: "finite L" "L ≠ {}" "Max L = tp"
unfolding L_def using assms
by (auto simp add: sup_acc_def Let_def split: if_splits)
show ?thesis
using Max_in[OF L_props(1,2)] unfolding L_props(3) unfolding L_def by auto
qed

lemma sup_acc_NoneE: "l ∈ {i..<j} ⟹ sup_acc step accept rho q i j = None ⟹
¬acc step accept rho q (i, Suc l)"
by (auto simp add: sup_acc_def Let_def split: if_splits)

lemma sup_acc_same: "sup_acc step accept rho q i i = None"

lemma sup_acc_None_restrict: "i ≤ j ⟹ sup_acc step accept rho q i j = None ⟹
sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j = None"
using steps_split
apply (auto simp add: sup_acc_def Let_def acc_def split: if_splits)
apply (smt (z3) lessI less_imp_le_nat order_less_le_trans steps_split)
done

lemma sup_acc_ext_idle: "i ≤ j ⟹ ¬acc step accept rho q (i, Suc j) ⟹
sup_acc step accept rho q i (Suc j) = sup_acc step accept rho q i j"
proof -
assume assms: "i ≤ j" "¬acc step accept rho q (i, Suc j)"
define L where "L = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
define L' where "L' = {l ∈ {i..<Suc j}. acc step accept rho q (i, Suc l)}"
have L_L': "L = L'"
unfolding L_def L'_def using assms(2) less_antisym by fastforce
show "sup_acc step accept rho q i (Suc j) = sup_acc step accept rho q i j"
using L_def L'_def L_L' by (auto simp add: sup_acc_def)
qed

lemma sup_acc_comp_Some_ge: "i ≤ l ⟹ l ≤ j ⟹ tp ≥ l ⟹
sup_acc step accept rho (steps step rho q (i, l)) l j = Some (ts, tp) ⟹
sup_acc step accept rho q i j = sup_acc step accept rho (steps step rho q (i, l)) l j"
proof -
assume assms: "i ≤ l" "l ≤ j" "sup_acc step accept rho (steps step rho q (i, l)) l j =
Some (ts, tp)" "tp ≥ l"
define L where "L = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
define L' where "L' = {l' ∈ {l..<j}. acc step accept rho (steps step rho q (i, l)) (l, Suc l')}"
have L'_props: "finite L'" "L' ≠ {}" "tp = Max L'" "ts = ts_at rho tp"
using assms(3) unfolding L'_def
by (auto simp add: sup_acc_def Let_def split: if_splits)
have tp_in_L': "tp ∈ L'"
using Max_in[OF L'_props(1,2)] unfolding L'_props(3) .
then have tp_in_L: "tp ∈ L"
unfolding L_def L'_def using assms(1) steps_comp[OF assms(1,2), of step rho]
using steps_comp
by (metis le_SucI)
have L_props: "finite L" "L ≠ {}"
using L_def tp_in_L by auto
have "⋀l'. l' ∈ L ⟹ l' ≤ tp"
proof -
fix l'
assume assm: "l' ∈ L"
show "l' ≤ tp"
proof (cases "l' < l")
case True
then show ?thesis
using assms(4) by auto
next
case False
then have "l' ∈ L'"
using assm
unfolding L_def L'_def
by (auto simp add: acc_def) (metis assms(1) less_imp_le_nat not_less_eq steps_comp)
then show ?thesis
using Max_eq_iff[OF L'_props(1,2)] L'_props(3) by auto
qed
qed
then have "Max L = tp"
using Max_eq_iff[OF L_props] tp_in_L by auto
then have "sup_acc step accept rho q i j = Some (ts, tp)"
using L_def L_props(2) unfolding L'_props(4)
then show "sup_acc step accept rho q i j = sup_acc step accept rho (steps step rho q (i, l)) l j"
using assms(3) by auto
qed

lemma sup_acc_comp_None: "i ≤ l ⟹ l ≤ j ⟹
sup_acc step accept rho (steps step rho q (i, l)) l j = None ⟹
sup_acc step accept rho q i j = sup_acc step accept rho q i l"
proof (induction "j - l" arbitrary: l)
case (Suc n)
have i_lt_j: "i < j"
using Suc by auto
have l_lt_j: "l < j"
using Suc by auto
have "¬acc step accept rho q (i, Suc l)"
using sup_acc_NoneE[of l l j step accept rho "steps step rho q (i, l)"] Suc(2-)
by (auto simp add: acc_def steps_def)
then have "sup_acc step accept rho q i (l + 1) = sup_acc step accept rho q i l"
using sup_acc_ext_idle[OF Suc(3)] by auto
moreover have "sup_acc step accept rho (steps step rho q (i, l + 1)) (l + 1) j = None"
using sup_acc_None_restrict[OF Suc(4,5)] steps_app[OF Suc(3), of step rho]
by auto
ultimately show ?case
using Suc(1)[of "l + 1"] Suc(2,3,4,5)
by auto

lemma sup_acc_ext: "i ≤ j ⟹ acc step accept rho q (i, Suc j) ⟹
sup_acc step accept rho q i (Suc j) = Some (ts_at rho j, j)"
proof -
assume assms: "i ≤ j" "acc step accept rho q (i, Suc j)"
define L' where "L' = {l ∈ {i..<j + 1}. acc step accept rho q (i, Suc l)}"
have j_in_L': "finite L'" "L' ≠ {}" "j ∈ L'"
using assms unfolding L'_def by auto
have j_is_Max: "Max L' = j"
using Max_eq_iff[OF j_in_L'(1,2)] j_in_L'(3)
show "sup_acc step accept rho q i (Suc j) = Some (ts_at rho j, j)"
using L'_def j_is_Max j_in_L'(2)
qed

lemma sup_acc_None: "i < j ⟹ sup_acc step accept rho q i j = None ⟹
sup_acc step accept rho (step q (bs_at rho i)) (i + 1) j = None"
using steps_split[of _ _ step rho]
by (auto simp add: sup_acc_def Let_def acc_def split: if_splits)

lemma sup_acc_i: "i < j ⟹ sup_acc step accept rho q i j = Some (ts, i) ⟹
sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j = None"
proof (rule ccontr)
assume assms: "i < j" "sup_acc step accept rho q i j = Some (ts, i)"
"sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j ≠ None"
from assms(3) obtain l where l_def: "l ∈ {Suc i..<j}"
"acc step accept rho (step q (bs_at rho i)) (Suc i, Suc l)"
by (auto simp add: sup_acc_def Let_def split: if_splits)
define L' where "L' = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
from assms(2) have L'_props: "finite L'" "L' ≠ {}" "Max L' = i"
by (auto simp add: sup_acc_def L'_def Let_def split: if_splits)
have i_lt_l: "i < l"
using l_def(1) by auto
from l_def have "l ∈ L'"
unfolding L'_def acc_def using steps_split[OF i_lt_l, of step rho] by (auto simp: steps_def)
then show "False"
using l_def(1) L'_props Max_ge i_lt_l not_le by auto
qed

lemma sup_acc_l: "i < j ⟹ i ≠ l ⟹ sup_acc step accept rho q i j = Some (ts, l) ⟹
sup_acc step accept rho q i j = sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j"
proof -
assume assms: "i < j" "i ≠ l" "sup_acc step accept rho q i j = Some (ts, l)"
define L where "L = {l ∈ {i..<j}. acc step accept rho q (i, Suc l)}"
define L' where "L' = {l ∈ {Suc i..<j}. acc step accept rho (step q (bs_at rho i)) (Suc i, Suc l)}"
from assms(3) have L_props: "finite L" "L ≠ {}" "l = Max L"
"sup_acc step accept rho q i j = Some (ts_at rho l, l)"
by (auto simp add: sup_acc_def L_def Let_def split: if_splits)
have l_in_L: "l ∈ L"
using Max_in[OF L_props(1,2)] L_props(3) by auto
then have i_lt_l: "i < l"
unfolding L_def using assms(2) by auto
have l_in_L': "finite L'" "L' ≠ {}" "l ∈ L'"
using steps_split[OF i_lt_l, of step rho q] l_in_L assms(2)
unfolding L_def L'_def acc_def by (auto simp: steps_def)
have "⋀l'. l' ∈ L' ⟹ l' ≤ l"
proof -
fix l'
assume assms: "l' ∈ L'"
have i_lt_l': "i < l'"
using assms unfolding L'_def by auto
have "l' ∈ L"
using steps_split[OF i_lt_l', of step rho] assms unfolding L_def L'_def acc_def by (auto simp: steps_def)
then show "l' ≤ l"
using L_props by simp
qed
then have l_sup_L': "Max L' = l"
using Max_eq_iff[OF l_in_L'(1,2)] l_in_L'(3) by auto
then show "sup_acc step accept rho q i j =
sup_acc step accept rho (step q (bs_at rho i)) (Suc i) j"
unfolding L_props(4)
unfolding sup_acc_def Let_def
using L'_def l_in_L'(2,3) L_props
unfolding Suc_eq_plus1 by auto
qed

lemma sup_leadsto_idle: "i < j ⟹ steps step rho init (i, j) ≠ q ⟹
sup_leadsto init step rho i j q = sup_leadsto init step rho (i + 1) j q"
proof -
assume assms: "i < j" "steps step rho init (i, j) ≠ q"
define L where "L = {l. l < i ∧ steps step rho init (l, j) = q}"
define L' where "L' = {l. l < i + 1 ∧ steps step rho init (l, j) = q}"
have L_L': "L = L'"
unfolding L_def L'_def using assms(2) less_antisym
by fastforce
show "sup_leadsto init step rho i j q = sup_leadsto init step rho (i + 1) j q"
using L_def L'_def L_L'
qed

lemma sup_leadsto_SomeI: "l < i ⟹ steps step rho init (l, j) = q ⟹
∃l'. sup_leadsto init step rho i j q = Some (ts_at rho l') ∧ l ≤ l' ∧ l' < i"
proof -
assume assms: "l < i" "steps step rho init (l, j) = q"
define L' where "L' = {l. l < i ∧ steps step rho init (l, j) = q}"
have fin_L': "finite L'"
unfolding L'_def by auto
moreover have L_nonempty: "L' ≠ {}"
using assms unfolding L'_def
ultimately have "Max L' ∈ L'"
using Max_in by auto
then show "∃l'. sup_leadsto init step rho i j q = Some (ts_at rho l') ∧ l ≤ l' ∧ l' < i"
using L'_def L_nonempty assms
qed

lemma sup_leadsto_SomeE: "i ≤ j ⟹ sup_leadsto init step rho i j q = Some ts ⟹
∃l < i. steps step rho init (l, j) = q ∧ ts_at rho l = ts"
proof -
assume assms: "i ≤ j" "sup_leadsto init step rho i j q = Some ts"
define L' where "L' = {l. l < i ∧ steps step rho init (l, j) = q}"
have fin_L': "finite L'"
unfolding L'_def by auto
moreover have L_nonempty: "L' ≠ {}"
using assms(2) unfolding L'_def
ultimately have "Max L' ∈ L'"
using Max_in by auto
then show "∃l < i. steps step rho init (l, j) = q ∧ ts_at rho l = ts"
using assms(2) L'_def
using ‹Max L' ∈ L'› by blast
qed

lemma Mapping_keys_dest: "x ∈ mmap_keys f ⟹ ∃y. mmap_lookup f x = Some y"
by (auto simp add: mmap_keys_def mmap_lookup_def weak_map_of_SomeI)

lemma Mapping_keys_intro: "mmap_lookup f x ≠ None ⟹ x ∈ mmap_keys f"
by (auto simp add: mmap_keys_def mmap_lookup_def)
(metis map_of_eq_None_iff option.distinct(1))

lemma Mapping_not_keys_intro: "mmap_lookup f x = None ⟹ x ∉ mmap_keys f"
unfolding mmap_lookup_def mmap_keys_def
using weak_map_of_SomeI by force

lemma Mapping_lookup_None_intro: "x ∉ mmap_keys f ⟹ mmap_lookup f x = None"
unfolding mmap_lookup_def mmap_keys_def

primrec mmap_combine :: "'key ⇒ 'val ⇒ ('val ⇒ 'val ⇒ 'val) ⇒ ('key × 'val) list ⇒
('key × 'val) list"
where
"mmap_combine k v c [] = [(k, v)]"
| "mmap_combine k v c (p # ps) = (case p of (k', v') ⇒
if k = k' then (k, c v' v) # ps else p # mmap_combine k v c ps)"

lemma mmap_combine_distinct_set: "distinct (map fst r) ⟹
distinct (map fst (mmap_combine k v c r)) ∧
set (map fst (mmap_combine k v c r)) = set (map fst r) ∪ {k}"
by (induction r) force+

lemma mmap_combine_lookup: "distinct (map fst r) ⟹ mmap_lookup (mmap_combine k v c r) z =
(if k = z then (case mmap_lookup r k of None ⇒ Some v | Some v' ⇒ Some (c v' v))
else mmap_lookup r z)"
using eq_key_imp_eq_value
by (induction r) (fastforce simp: mmap_lookup_def split: option.splits)+

definition mmap_fold :: "('c, 'd) mmap ⇒ (('c × 'd) ⇒ ('c × 'd)) ⇒ ('d ⇒ 'd ⇒ 'd) ⇒
('c, 'd) mmap ⇒ ('c, 'd) mmap" where
"mmap_fold m f c r = foldl (λr p. case f p of (k, v) ⇒ mmap_combine k v c r) r m"

definition mmap_fold' :: "('c, 'd) mmap ⇒ 'e ⇒ (('c × 'd) × 'e ⇒ ('c × 'd) × 'e) ⇒
('d ⇒ 'd ⇒ 'd) ⇒ ('c, 'd) mmap ⇒ ('c, 'd) mmap × 'e" where
"mmap_fold' m e f c r = foldl (λ(r, e) p. case f (p, e) of ((k, v), e') ⇒
(mmap_combine k v c r, e')) (r, e) m"

lemma mmap_fold'_eq: "mmap_fold' m e f' c r = (m', e') ⟹ P e ⟹
(⋀p e p' e'. P e ⟹ f' (p, e) = (p', e') ⟹ p' = f p ∧ P e') ⟹
m' = mmap_fold m f c r ∧ P e'"
proof (induction m arbitrary: e r m' e')
case (Cons p m)
obtain k v e'' where kv_def: "f' (p, e) = ((k, v), e'')" "P e''"
using Cons
by (cases "f' (p, e)") fastforce
have mmap_fold: "mmap_fold m f c (mmap_combine k v c r) = mmap_fold (p # m) f c r"
using Cons(1)[OF _ kv_def(2), where ?r="mmap_combine k v c r"] Cons(2,3,4)
by (simp add: mmap_fold_def mmap_fold'_def kv_def(1))
have mmap_fold': "mmap_fold' m e'' f' c (mmap_combine k v c r) = (m', e')"
using Cons(2)
by (auto simp: mmap_fold'_def kv_def)
show ?case
using Cons(1)[OF mmap_fold' kv_def(2) Cons(4)]
unfolding mmap_fold
by auto
qed (auto simp: mmap_fold_def mmap_fold'_def)

lemma foldl_mmap_combine_distinct_set: "distinct (map fst r) ⟹
distinct (map fst (mmap_fold m f c r)) ∧
set (map fst (mmap_fold m f c r)) = set (map fst r) ∪ set (map (fst ∘ f) m)"
apply (induction m arbitrary: r)
using mmap_combine_distinct_set
apply (auto simp: mmap_fold_def split: prod.splits)
apply force
apply (smt Un_iff fst_conv imageI insert_iff)
using mk_disjoint_insert
apply fastforce+
done

lemma mmap_fold_lookup_rec: "distinct (map fst r) ⟹ mmap_lookup (mmap_fold m f c r) z =
(case map (snd ∘ f) (filter (λ(k, v). fst (f (k, v)) = z) m) of [] ⇒ mmap_lookup r z
| v # vs ⇒ (case mmap_lookup r z of None ⇒ Some (foldl c v vs)
| Some w ⇒ Some (foldl c w (v # vs))))"
proof (induction m arbitrary: r)
case (Cons p ps)
obtain k v where kv_def: "f p = (k, v)"
by fastforce
have distinct: "distinct (map fst (mmap_combine k v c r))"
using mmap_combine_distinct_set[OF Cons(2)]
by auto
show ?case
using Cons(1)[OF distinct, unfolded mmap_combine_lookup[OF Cons(2)]]
by (auto simp: mmap_lookup_def kv_def mmap_fold_def split: list.splits option.splits)
qed (auto simp: mmap_fold_def)

lemma mmap_fold_distinct: "distinct (map fst m) ⟹ distinct (map fst (mmap_fold m f c []))"
using foldl_mmap_combine_distinct_set[of "[]"]
by auto

lemma mmap_fold_set: "distinct (map fst m) ⟹
set (map fst (mmap_fold m f c [])) = (fst ∘ f) ` set m"
using foldl_mmap_combine_distinct_set[of "[]"]
by force

lemma mmap_lookup_empty: "mmap_lookup [] z = None"
by (auto simp: mmap_lookup_def)

lemma mmap_fold_lookup: "distinct (map fst m) ⟹ mmap_lookup (mmap_fold m f c []) z =
(case map (snd ∘ f) (filter (λ(k, v). fst (f (k, v)) = z) m) of [] ⇒ None
| v # vs ⇒ Some (foldl c v vs))"
using mmap_fold_lookup_rec[of "[]" _ f c]
by (auto simp: mmap_lookup_empty split: list.splits)

definition fold_sup :: "('c, 'd :: timestamp) mmap ⇒ ('c ⇒ 'c) ⇒ ('c, 'd) mmap" where
"fold_sup m f = mmap_fold m (λ(x, y). (f x, y)) sup []"

lemma mmap_lookup_distinct: "distinct (map fst m) ⟹ (k, v) ∈ set m ⟹
mmap_lookup m k = Some v"
by (auto simp: mmap_lookup_def)

lemma fold_sup_distinct: "distinct (map fst m) ⟹ distinct (map fst (fold_sup m f))"
using mmap_fold_distinct
by (auto simp: fold_sup_def)

lemma fold_sup:
fixes v :: "'d :: timestamp"
shows "foldl sup v vs = fold sup vs v"
by (induction vs arbitrary: v) (auto simp: sup.commute)

lemma lookup_fold_sup:
assumes distinct: "distinct (map fst m)"
shows "mmap_lookup (fold_sup m f) z =
(let Z = {x ∈ mmap_keys m. f x = z} in
if Z = {} then None else Some (Sup_fin ((the ∘ mmap_lookup m) ` Z)))"
proof (cases "{x ∈ mmap_keys m. f x = z} = {}")
case True
have "z ∉ mmap_keys (mmap_fold m (λ(x, y). (f x, y)) sup [])"
using True[unfolded mmap_keys_def] mmap_fold_set[OF distinct]
by (auto simp: mmap_keys_def)
then have "mmap_lookup (fold_sup m f) z = None"
unfolding fold_sup_def
by (meson Mapping_keys_intro)
then show ?thesis
unfolding True
by auto
next
case False
have z_in_keys: "z ∈ mmap_keys (mmap_fold m (λ(x, y). (f x, y)) sup [])"
using False[unfolded mmap_keys_def] mmap_fold_set[OF distinct]
by (force simp: mmap_keys_def)
obtain v vs where vs_def: "mmap_lookup (fold_sup m f) z = Some (foldl sup v vs)"
"v # vs = map snd (filter (λ(k, v). f k = z) m)"
using mmap_fold_lookup[OF distinct, of "(λ(x, y). (f x, y))" sup z]
Mapping_keys_dest[OF z_in_keys]
by (force simp: fold_sup_def mmap_keys_def comp_def split: list.splits prod.splits)
have "set (v # vs) = (the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z}"
proof (rule set_eqI, rule iffI)
fix w
assume "w ∈ set (v # vs)"
then obtain x where x_def: "x ∈ mmap_keys m" "f x = z" "(x, w) ∈ set m"
using vs_def(2)
by (auto simp add: mmap_keys_def rev_image_eqI)
show "w ∈ (the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z}"
using x_def(1,2) mmap_lookup_distinct[OF distinct x_def(3)]
by force
next
fix w
assume "w ∈ (the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z}"
then obtain x where x_def: "x ∈ mmap_keys m" "f x = z" "(x, w) ∈ set m"
using mmap_lookup_distinct[OF distinct]
by (auto simp add: Mapping_keys_intro distinct mmap_lookup_def dest: Mapping_keys_dest)
show "w ∈ set (v # vs)"
using x_def
by (force simp: vs_def(2))
qed
then have "foldl sup v vs = Sup_fin ((the ∘ mmap_lookup m) ` {x ∈ mmap_keys m. f x = z})"
unfolding fold_sup
by (metis Sup_fin.set_eq_fold)
then show ?thesis
using False
by (auto simp: vs_def(1))
qed

definition mmap_map :: "('a ⇒ 'b ⇒ 'c) ⇒ ('a, 'b) mmap ⇒ ('a, 'c) mmap" where
"mmap_map f m = map (λ(k, v). (k, f k v)) m"

lemma mmap_map_keys: "mmap_keys (mmap_map f m) = mmap_keys m"
by (force simp: mmap_map_def mmap_keys_def)

lemma mmap_map_fst: "map fst (mmap_map f m) = map fst m"
by (auto simp: mmap_map_def)

definition cstep :: "('c ⇒ 'b ⇒ 'c) ⇒ ('c × 'b, 'c) mapping ⇒
'c ⇒ 'b ⇒ ('c × ('c × 'b, 'c) mapping)" where
"cstep step st q bs = (case Mapping.lookup st (q, bs) of None ⇒ (let res = step q bs in
(res, Mapping.update (q, bs) res st)) | Some v ⇒ (v, st))"

definition cac :: "('c ⇒ bool) ⇒ ('c, bool) mapping ⇒ 'c ⇒ (bool × ('c, bool) mapping)" where
"cac accept ac q = (case Mapping.lookup ac q of None ⇒ (let res = accept q in
(res, Mapping.update q res ac)) | Some v ⇒ (v, ac))"

fun mmap_fold_s :: "('c ⇒ 'b ⇒ 'c) ⇒ ('c × 'b, 'c) mapping ⇒
('c ⇒ bool) ⇒ ('c, bool) mapping ⇒
'b ⇒ 'd ⇒ nat ⇒ ('c, 'c × ('d × nat) option) mmap ⇒
(('c, 'c × ('d × nat) option) mmap × ('c × 'b, 'c) mapping × ('c, bool) mapping)" where
"mmap_fold_s step st accept ac bs t j [] = ([], st, ac)"
| "mmap_fold_s step st accept ac bs t j ((q, (q', tstp)) # qbss) =
(let (q'', st') = cstep step st q' bs;
(β, ac') = cac accept ac q'';
(qbss', st'', ac'') = mmap_fold_s step st' accept ac' bs t j qbss in
((q, (q'', if β then Some (t, j) else tstp)) # qbss', st'', ac''))"

lemma mmap_fold_s_sound: "mmap_fold_s step st accept ac bs t j qbss = (qbss', st', ac') ⟹
(⋀q bs. case Mapping.lookup st (q, bs) of None ⇒ True | Some v ⇒ step q bs = v) ⟹
(⋀q bs. case Mapping.lookup ac q of None ⇒ True | Some v ⇒ accept q = v) ⟹
qbss' = mmap_map (λq (q', tstp). (step q' bs, if accept (step q' bs) then Some (t, j) else tstp)) qbss ∧
(∀q bs. case Mapping.lookup st' (q, bs) of None ⇒ True | Some v ⇒ step q bs = v) ∧
(∀q bs. case Mapping.lookup ac' q of None ⇒ True | Some v ⇒ accept q = v)"
proof (induction qbss arbitrary: st ac qbss')
case (Cons a qbss)
obtain q q' tstp where a_def: "a = (q, (q', tstp))"
by (cases a) auto
obtain q'' st'' where q''_def: "cstep step st q' bs = (q'', st'')"
"q'' = step q' bs"
using Cons(3)
by (cases "cstep step st q' bs")
(auto simp: cstep_def Let_def option.case_eq_if split: option.splits if_splits)
obtain b ac'' where b_def: "cac accept ac q'' = (b, ac'')"
"b = accept q''"
using Cons(4)
by (cases "cac accept ac q''")
(auto simp: cac_def Let_def option.case_eq_if split: option.splits if_splits)
obtain qbss'' where qbss''_def: "mmap_fold_s step st'' accept ac'' bs t j qbss =
(qbss'', st', ac')" "qbss' = (q, q'', if b then Some (t, j) else tstp) # qbss''"
using Cons(2)[unfolded a_def mmap_fold_s.simps q''_def(1) b_def(1)]
unfolding Let_def
by (auto simp: b_def(1) split: prod.splits)
have ih: "⋀q bs. case Mapping.lookup st'' (q, bs) of None ⇒ True | Some a ⇒ step q bs = a"
"⋀q bs. case Mapping.lookup ac'' q of None ⇒ True | Some a ⇒ accept q = a"
using q''_def b_def Cons(3,4)
by (auto simp: cstep_def cac_def Let_def Mapping.lookup_update' option.case_eq_if
split: option.splits if_splits)
show ?case
using Cons(1)[OF qbss''_def(1) ih]
unfolding a_def q''_def(2) b_def(2) qbss''_def(2)
by (auto simp: mmap_map_def)
qed (auto simp: mmap_map_def)

definition adv_end :: "('b, 'c, 'd :: timestamp, 't, 'e) args ⇒
('b, 'c, 'd, 't, 'e) window ⇒ ('b, 'c, 'd, 't, 'e) window option" where
"adv_end args w = (let step = w_step args; accept = w_accept args;
run_t = w_run_t args; run_sub = w_run_sub args; st = w_st w; ac = w_ac w;
j = w_j w; tj = w_tj w; sj = w_sj w; s = w_s w; e = w_e w in
(case run_t tj of None ⇒ None | Some (tj', t) ⇒ (case run_sub sj of None ⇒ None | Some (sj', bs) ⇒
let (s', st', ac') = mmap_fold_s step st accept ac bs t j s;
(e', st'') = mmap_fold' e st' (λ((x, y), st). let (q', st') = cstep step st x bs in ((q', y), st')) sup [] in
Some (w⦇w_st := st'', w_ac := ac', w_j := Suc j, w_tj := tj', w_sj := sj', w_s := s', w_e := e'⦈))))"

lemma map_values_lookup: "mmap_lookup (mmap_map f m) z = Some v' ⟹
∃v. mmap_lookup m z = Some v ∧ v' = f z v"
by (induction m) (auto simp: mmap_lookup_def mmap_map_def)

lemma acc_app:
assumes "i ≤ j" "steps step rho q (i, Suc j) = q'" "accept q'"
shows "sup_acc step accept rho q i (Suc j) = Some (ts_at rho j, j)"
proof -
define L where "L = {l ∈ {i..<Suc j}. accept (steps step rho q (i, Suc l))}"
have nonempty: "finite L" "L ≠ {}"
using assms unfolding L_def by auto
moreover have "Max {l ∈ {i..<Suc j}. accept (steps step rho q (i, Suc l))} = j"
unfolding L_def[symmetric] Max_eq_iff[OF nonempty, of j]
unfolding L_def using assms by auto
ultimately show ?thesis
by (auto simp add: sup_acc_def acc_def L_def)
qed

lemma acc_app_idle:
assumes "i ≤ j" "steps step rho q (i, Suc j) = q'" "¬accept q'"
shows "sup_acc step accept rho q i (Suc j) = sup_acc step accept rho q i j"
using assms
by (auto simp add: sup_acc_def Let_def acc_def elim: less_SucE) (metis less_Suc_eq)+

lemma sup_fin_closed: "finite A ⟹ A ≠ {} ⟹
(⋀x y. x ∈ A ⟹ y ∈ A ⟹ sup x y ∈ {x, y}) ⟹ ⨆⇩f⇩i⇩n A ∈ A"
apply (induct A rule: finite.induct)
using Sup_fin.insert
by auto fastforce

assumes "valid_window args t0 sub rho w" "w_run_t args (w_tj w) = Some (tj', t)"
"w_run_sub args (w_sj w) = Some (sj', bs)"
"⋀t'. t' ∈ set (map fst rho) ⟹ t' ≤ t"
shows "case adv_end args w of None ⇒ False | Some w' ⇒ valid_window args t0 sub (rho @ [(t, bs)]) w'"
proof -
define init where "init = w_init args"
define step where "step = w_step args"
define accept where "accept = w_accept args"
define run_t where "run_t = w_run_t args"
define run_sub where "run_sub = w_run_sub args"
define st where "st = w_st w"
define ac where "ac = w_ac w"
define i where "i = w_i w"
define ti where "ti = w_ti w"
define si where "si = w_si w"
define j where "j = w_j w"
define tj where "tj = w_tj w"
define sj where "sj = w_sj w"
define s where "s = w_s w"
define e where "e = w_e w"
have valid_before: "reach_window args t0 sub rho (i, ti, si, j, tj, sj)"
"⋀i j. i ≤ j ⟹ j < length rho ⟹ ts_at rho i ≤ ts_at rho j"
"(⋀q bs. case Mapping.lookup st (q, bs) of None ⇒ True | Some v ⇒ step q bs = v)"
"(⋀q bs. case Mapping.lookup ac q of None ⇒ True | Some v ⇒ accept q = v)"
"∀q. mmap_lookup e q = sup_leadsto init step rho i j q" "distinct (map fst e)"
"valid_s init step st accept rho i i j s"
using assms(1)
unfolding valid_window_def valid_s_def Let_def init_def step_def accept_def run_t_def
run_sub_def st_def ac_def i_def ti_def si_def j_def tj_def sj_def s_def e_def
by auto
have i_j: "i ≤ j"
using valid_before(1)
by auto
have distinct_before: "distinct (map fst s)" "distinct (map fst e)"
using valid_before
by (auto simp: valid_s_def)
note run_tj = assms(2)[folded run_t_def tj_def]
note run_sj = assms(3)[folded run_sub_def sj_def]
define rho' where "rho' = rho @ [(t, bs)]"
have ts_at_mono: "⋀i j. i ≤ j ⟹ j < length rho' ⟹ ts_at rho' i ≤ ts_at rho' j"
using valid_before(2) assms(4)
by (auto simp: rho'_def ts_at_def nth_append split: option.splits list.splits if_splits)
obtain s' st' ac' where s'_def: "mmap_fold_s step st accept ac bs t j s = (s', st', ac')"
apply (cases "mmap_fold_s step st accept ac bs t j s")
apply (auto)
done
have s'_mmap_map: "s' = mmap_map (λq (q', tstp).
(step q' bs, if accept (step q' bs) then Some (t, j) else tstp)) s"
"(⋀q bs. case Mapping.lookup st' (q, bs) of None ⇒ True | Some v ⇒ step q bs = v)"
"(⋀q bs. case Mapping.lookup ac' q of None ⇒ True | Some v ⇒ accept q = v)"
using mmap_fold_s_sound[OF s'_def valid_before(3,4)]
by auto
obtain e' st'' where e'_def: "mmap_fold' e st' (λ((x, y), st).
let (q', st') = cstep step st x bs in ((q', y), st')) sup [] = (e', st'')"
by (metis old.prod.exhaust)
define inv where "inv ≡ λst'. ∀q bs. case Mapping.lookup st' (q, bs) of None ⇒ True
| Some v ⇒ step q bs = v"
have inv_st': "inv st'"
using s'_mmap_map(2)
by (auto simp: inv_def)
have "⋀p e p' e'. inv e ⟹ (case (p, e) of (x, xa) ⇒ (case x of (x, y) ⇒
λst. let (q', st') = cstep step st x bs in ((q', y), st')) xa) = (p', e') ⟹
p' = (case p of (x, y) ⇒ (step x bs, y)) ∧ inv e'"
by (auto simp: inv_def cstep_def Let_def Mapping.lookup_update' split: option.splits if_splits)
then have e'_fold_sup_st'': "e' = fold_sup e (λq. step q bs)"
"(⋀q bs. case Mapping.lookup st'' (q, bs) of None ⇒ True | Some v ⇒ step q bs = v)"
using mmap_fold'_eq[OF e'_def, of inv "λ(x, y). (step x bs, y)", OF inv_st']
by (fastforce simp: fold_sup_def inv_def)+
have adv_end: "adv_end args w = Some (w⦇w_st := st'', w_ac := ac',
w_j := Suc j, w_tj := tj', w_sj := sj', w_s := s', w_e := e'⦈)"
using run_tj run_sj e'_def[unfolded st_def]
unfolding adv_end_def init_def step_def accept_def run_t_def run_sub_def
i_def ti_def si_def j_def tj_def sj_def s_def e_def s'_def e'_def
by (auto simp: Let_def s'_def[unfolded step_def st_def accept_def ac_def j_def s_def])
have keys_s': "mmap_keys s' = mmap_keys s"
by (force simp: mmap_keys_def mmap_map_def s'_mmap_map(1))
have lookup_s: "⋀q q' tstp. mmap_lookup s q = Some (q', tstp) ⟹
steps step rho' q (i, j) = q' ∧ tstp = sup_acc step accept rho' q i j"
using valid_before Mapping_keys_intro
by (force simp add: Let_def rho'_def valid_s_def steps_app_cong sup_acc_app_cong
split: option.splits)
have bs_at_rho'_j: "bs_at rho' j = bs"
using valid_before
by (auto simp: rho'_def bs_at_def nth_append)
have ts_at_rho'_j: "ts_at rho' j = t"
using valid_before
by (auto simp: rho'_def ts_at_def nth_append)
have lookup_s': "⋀q q' tstp. mmap_lookup s' q = Some (q', tstp) ⟹
steps step rho' q (i, Suc j) = q' ∧ tstp = sup_acc step accept rho' q i (Suc j)"
proof -
fix q q'' tstp'
assume assm: "mmap_lookup s' q = Some (q'', tstp')"
obtain q' tstp where "mmap_lookup s q = Some (q', tstp)" "q'' = step q' bs"
"tstp' = (if accept (step q' bs) then Some (t, j) else tstp)"
using map_values_lookup[OF assm[unfolded s'_mmap_map]] by auto
then show "steps step rho' q (i, Suc j) = q'' ∧ tstp' = sup_acc step accept rho' q i (Suc j)"
using lookup_s
apply (auto simp: bs_at_rho'_j ts_at_rho'_j)
apply (metis Suc_eq_plus1 bs_at_rho'_j i_j steps_app)
apply (metis acc_app bs_at_rho'_j i_j steps_appE ts_at_rho'_j)
apply (metis Suc_eq_plus1 bs_at_rho'_j i_j steps_app)
apply (metis (no_types, lifting) acc_app_idle bs_at_rho'_j i_j steps_appE)
done
qed
have lookup_e: "⋀q. mmap_lookup e q = sup_leadsto init step rho' i j q"
using valid_before sup_leadsto_app_cong[of _ _ rho init step]
by (auto simp: rho'_def)
have keys_e_alt: "mmap_keys e = {q. ∃l < i. steps step rho' init (l, j) = q}"
using valid_before
apply (metis (no_types, lifting) Mapping_keys_dest lookup_e rho'_def sup_leadsto_SomeE)
apply (metis (no_types, lifting) Mapping_keys_intro option.simps(3) order_refl steps_app_cong)
done
have finite_keys_e: "finite (mmap_keys e)"
unfolding keys_e_alt
by (rule finite_surj[of "{l. l < i}"]) auto
have "reaches_on run_sub sub (map snd rho) sj"
using valid_before reaches_on_trans
unfolding run_sub_def sub_def
by fastforce
then have reaches_on': "reaches_on run_sub sub (map snd rho @ [bs]) sj'"
using reaches_on_app run_sj
by fast
have "reaches_on run_t t0 (map fst rho) tj"
using valid_before reaches_on_trans
unfolding run_t_def
by fastforce
then have reach_t': "reaches_on run_t t0 (map fst rho') tj'"
using reaches_on_app run_tj
unfolding rho'_def
by fastforce
have lookup_e': "⋀q. mmap_lookup e' q = sup_leadsto init step rho' i (Suc j) q"
proof -
fix q
define Z where "Z = {x ∈ mmap_keys e. step x bs = q}"
show "mmap_lookup e' q = sup_leadsto init step rho' i (Suc j) q"
proof (cases "Z = {}")
case True
then have "mmap_lookup e' q = None"
using Z_def lookup_fold_sup[OF distinct_before(2)]
unfolding e'_fold_sup_st''
by (auto simp: Let_def)
moreover have "sup_leadsto init step rho' i (Suc j) q = None"
proof (rule ccontr)
assume assm: "sup_leadsto init step rho' i (Suc j) q ≠ None"
obtain l where l_def: "l < i" "steps step rho' init (l, Suc j) = q"
using i_j sup_leadsto_SomeE[of i "Suc j"] assm
by force
have l_j: "l ≤ j"
using less_le_trans[OF l_def(1) i_j] by auto
obtain q'' where q''_def: "steps step rho' init (l, j) = q''" "step q'' bs = q"
using steps_appE[OF _ l_def(2)] l_j
by (auto simp: bs_at_rho'_j)
then have "q'' ∈ mmap_keys e"
using keys_e_alt l_def(1)
by auto
then show "False"
using Z_def q''_def(2) True
by auto
qed
ultimately show ?thesis
by auto
next
case False
then have lookup_e': "mmap_lookup e' q = Some (Sup_fin ((the ∘ mmap_lookup e) ` Z))"
using Z_def lookup_fold_sup[OF distinct_before(2)]
unfolding e'_fold_sup_st''
by (auto simp: Let_def)
define L where "L = {l. l < i ∧ steps step rho' init (l, Suc j) = q}"
have fin_L: "finite L"
unfolding L_def by auto
have Z_alt: "Z = {x. ∃l < i. steps step rho' init (l, j) = x ∧ step x bs = q}"
using Z_def[unfolded keys_e_alt] by auto
have fin_Z: "finite Z"
unfolding Z_alt by auto
have L_nonempty: "L ≠ {}"
using L_def Z_alt False i_j steps_app[of _ _ step rho q]
by (auto simp: bs_at_rho'_j)
(smt Suc_eq_plus1 bs_at_rho'_j less_irrefl_nat less_le_trans nat_le_linear steps_app)
have sup_leadsto: "sup_leadsto init step rho' i (Suc j) q = Some (ts_at rho' (Max L))"
using L_nonempty L_def