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"

copy_bnf (dead 'b, dead 'c, dead 'd, dead 't, 'e, dead 'ext) window_ext

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')"
  by (fastforce simp add: reaches_on_app)

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
      apply (metis (no_types, lifting) le_add1 le_add_same_cancel1 le_less less_le_trans nth_Cons_0)
      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)
    by (metis le_Suc_ex upt_add_eq_append)
  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
    by (auto simp add: sup_acc_def)
       (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"
  by (auto simp add: sup_acc_def)

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]
    apply (auto simp add: acc_def)
    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)
    by (auto simp add: sup_acc_def)
  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
qed (auto simp add: sup_acc_same)

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)
    by (auto simp add: L'_def)
  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)
    by (auto simp add: sup_acc_def)
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'
    by (auto simp add: sup_leadsto_def)
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
    by (auto simp add: sup_leadsto_def split: if_splits)
  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
    by (fastforce simp add: sup_leadsto_def split: if_splits)
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
    by (auto simp add: sup_leadsto_def split: if_splits)
  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
    apply (auto simp add: sup_leadsto_def split: if_splits)
    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
  by (simp add: map_of_eq_None_iff)

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

lemma valid_adv_end:
  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 (auto simp add: sup_leadsto_def rho'_def)
     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
        by (auto simp add: sup_leadsto_def)
      have j_lt_rho': "j < length rho'"
        using valid_before
        by (auto simp: rho'_def)
      have "Sup_fin ((the ∘ mmap_lookup e) ` Z) = ts_at rho' (Max L)"
      proof (rule antisym)
        obtain z ts where zts_def: "z ∈ Z" "(the ∘ mmap_lookup e) z = ts"
          "Sup_fin ((the ∘ mmap_lookup e) ` Z) = ts"
        proof -
          assume lassm: "⋀z ts. z ∈ Z ⟹ (the ∘ mmap_lookup e) z = ts ⟹
          ⨆⇩f⇩i⇩n ((the ∘ mmap_lookup e) ` Z) = ts ⟹ thesis"
          define T where "T = (the ∘ mmap_lookup e) ` Z"