Theory Watched_Literals_VMTF

theory Watched_Literals_VMTF
  imports IsaSAT_Literals
begin

subsection ‹Variable-Move-to-Front›

subsubsection ‹Specification›

type_synonym 'v abs_vmtf_ns = ‹'v set × 'v set›

datatype ('v, 'n) vmtf_node = VMTF_Node (stamp : 'n) (get_prev: ‹'v option›) (get_next: ‹'v option›)
type_synonym nat_vmtf_node = ‹(nat, nat) vmtf_node›

inductive vmtf_ns :: ‹nat list ⇒ nat ⇒ nat_vmtf_node list ⇒ bool› where
Nil: ‹vmtf_ns [] st xs› |
Cons1: ‹a < length xs ⟹ m ≥ n ⟹ xs ! a = VMTF_Node (n::nat) None None ⟹ vmtf_ns [a] m xs› |
Cons: ‹vmtf_ns (b # l) m xs ⟹ a < length xs ⟹ xs ! a = VMTF_Node n None (Some b) ⟹
  a ≠ b ⟹ a ∉ set l ⟹ n > m ⟹
  xs' = xs[b := VMTF_Node (stamp (xs!b)) (Some a) (get_next (xs!b))] ⟹ n' ≥ n ⟹
  vmtf_ns (a # b # l) n' xs'›

inductive_cases vmtf_nsE: ‹vmtf_ns xs st zs›

lemma vmtf_ns_le_length: ‹vmtf_ns l m xs ⟹ i ∈ set l ⟹ i < length xs›
  apply (induction rule: vmtf_ns.induct)
  subgoal by (auto intro: vmtf_ns.intros)
  subgoal by (auto intro: vmtf_ns.intros)
  subgoal by (auto intro: vmtf_ns.intros)
  done

lemma vmtf_ns_distinct: ‹vmtf_ns l m xs ⟹ distinct l›
  apply (induction rule: vmtf_ns.induct)
  subgoal by (auto intro: vmtf_ns.intros)
  subgoal by (auto intro: vmtf_ns.intros)
  subgoal by (auto intro: vmtf_ns.intros)
  done

lemma vmtf_ns_eq_iff:
  assumes
    ‹∀i ∈ set l. xs ! i = zs ! i› and
    ‹∀i ∈ set l. i < length xs ∧ i < length zs›
  shows ‹vmtf_ns l m zs ⟷ vmtf_ns l m xs› (is ‹?A ⟷ ?B›)
proof -
  have ‹vmtf_ns l m xs›
    if
      ‹vmtf_ns l m zs› and
      ‹(∀i ∈ set l. xs ! i = zs ! i)› and
      ‹(∀i ∈ set l. i < length xs ∧ i < length zs)›
    for xs zs
    using that
  proof (induction arbitrary: xs rule: vmtf_ns.induct)
    case (Nil st xs zs)
    then show ?case by (auto intro: vmtf_ns.intros)
  next
    case (Cons1 a xs n zs)
    show ?case by (rule vmtf_ns.Cons1) (use Cons1 in ‹auto intro: vmtf_ns.intros›)
  next
    case (Cons b l m xs c n zs n' zs') note vmtf_ns = this(1) and a_le_y = this(2) and zs_a = this(3)
      and ab = this(4) and a_l = this(5) and mn = this(6) and xs' = this(7) and nn' = this(8) and
       IH = this(9) and H = this(10-)
    have ‹vmtf_ns (c # b # l) n' zs›
      by (rule vmtf_ns.Cons[OF Cons.hyps])
    have [simp]: ‹b < length xs›  ‹b < length zs›
      using H xs' by auto
    have [simp]: ‹b ∉ set l›
      using vmtf_ns_distinct[OF vmtf_ns] by auto
    then have K: ‹∀i∈set l. zs ! i = (if b = i then x else xs ! i) =
       (∀i∈set l. zs ! i = xs ! i)› for x
       using H(2)
       by (simp add: H(1) xs')
    have next_xs_b: ‹get_next (xs ! b) = None› if ‹l = []›
      using vmtf_ns unfolding that by (auto simp: elim!: vmtf_nsE)
    have prev_xs_b: ‹get_prev (xs ! b) = None›
      using vmtf_ns by (auto elim: vmtf_nsE)
    have vmtf_ns_zs: ‹vmtf_ns (b # l) m (zs'[b := xs!b])›
      apply (rule IH)
      subgoal using H(1) ab next_xs_b prev_xs_b H unfolding xs' by (auto simp: K)
      subgoal using H(2) ab next_xs_b prev_xs_b unfolding xs' by (auto simp: K)
      done
    have ‹zs' ! b = VMTF_Node (stamp (xs ! b)) (Some c) (get_next (xs ! b))›
      using H(1) unfolding xs' by auto
    show ?case
      apply (rule vmtf_ns.Cons[OF vmtf_ns_zs, of _ n])
      subgoal using a_le_y xs' H(2) by auto
      subgoal using ab zs_a xs' H(1) by (auto simp: K)
      subgoal using ab .
      subgoal using a_l .
      subgoal using mn .
      subgoal using ab xs' H(1) by (metis H(2) insert_iff list.set(2) list_update_id
            list_update_overwrite nth_list_update_eq)
      subgoal using nn' .
      done
  qed
  then show ?thesis
    using assms by metis
qed

lemmas vmtf_ns_eq_iffI = vmtf_ns_eq_iff[THEN iffD1]

lemma vmtf_ns_stamp_increase: ‹vmtf_ns xs p zs ⟹ p ≤ p' ⟹ vmtf_ns xs p' zs›
  apply (induction rule: vmtf_ns.induct)
  subgoal by (auto intro: vmtf_ns.intros)
  subgoal by (rule vmtf_ns.Cons1) (auto intro!: vmtf_ns.intros)
  subgoal by (auto intro: vmtf_ns.intros)
  done

lemma vmtf_ns_single_iff: ‹vmtf_ns [a] m xs ⟷ (a < length xs ∧ m ≥ stamp (xs ! a) ∧
     xs ! a = VMTF_Node (stamp (xs ! a)) None None)›
  by (auto 5 5 elim!: vmtf_nsE intro: vmtf_ns.intros)

lemma vmtf_ns_append_decomp:
  assumes ‹vmtf_ns (axs @ [ax, ay] @ azs) an ns›
  shows ‹(vmtf_ns (axs @ [ax]) an (ns[ax:= VMTF_Node (stamp (ns!ax)) (get_prev (ns!ax)) None]) ∧
    vmtf_ns (ay # azs) (stamp (ns!ay)) (ns[ay:= VMTF_Node (stamp (ns!ay)) None (get_next (ns!ay))]) ∧
    stamp (ns!ax) > stamp (ns!ay))›
  using assms
proof (induction ‹axs @ [ax, ay] @ azs› an ns arbitrary: axs ax ay azs rule: vmtf_ns.induct)
  case (Nil st xs)
  then show ?case by simp
next
  case (Cons1 a xs m n)
  then show ?case by auto
next
  case (Cons b l m xs a n xs' n') note vmtf_ns = this(1) and IH = this(2) and a_le_y = this(3) and
    zs_a = this(4) and ab = this(5) and a_l = this(6) and mn = this(7) and xs' = this(8) and
    nn' = this(9) and decomp = this(10-)
  have b_le_xs: ‹b < length xs›
    using vmtf_ns by (auto intro: vmtf_ns_le_length simp: xs')
  show ?case
  proof (cases ‹axs›)
    case [simp]: Nil
    then have [simp]: ‹ax = a› ‹ay = b› ‹azs = l›
      using decomp by auto
    show ?thesis
    proof (cases l)
      case Nil
      then show ?thesis
        using vmtf_ns xs' a_le_y zs_a ab a_l mn nn' by (cases ‹xs ! b›)
          (auto simp: vmtf_ns_single_iff)
    next
      case (Cons al als) note l = this
      have vmtf_ns_b: ‹vmtf_ns [b] m (xs[b := VMTF_Node (stamp (xs ! b)) (get_prev (xs ! b)) None])› and
        vmtf_ns_l: ‹vmtf_ns (al # als) (stamp (xs ! al))
           (xs[al := VMTF_Node (stamp (xs ! al)) None (get_next (xs ! al))])› and
        stamp_al_b: ‹stamp (xs ! al) < stamp (xs ! b)›
        using IH[of Nil b al als] unfolding l by auto
      have ‹vmtf_ns [a] n' (xs'[a := VMTF_Node (stamp (xs' ! a)) (get_prev (xs' ! a)) None])›
          using a_le_y xs' ab mn nn' zs_a by (auto simp: vmtf_ns_single_iff)
      have al_b[simp]: ‹al ≠ b› and b_als: ‹b ∉ set als›
        using vmtf_ns unfolding l by (auto dest: vmtf_ns_distinct)
      have al_le_xs: ‹al < length xs›
        using vmtf_ns vmtf_ns_l by (auto intro: vmtf_ns_le_length simp: l xs')
      have xs_al: ‹xs ! al = VMTF_Node (stamp (xs ! al)) (Some b) (get_next (xs ! al))›
        using vmtf_ns unfolding l by (auto 5 5 elim: vmtf_nsE)
      have xs_b: ‹xs ! b = VMTF_Node (stamp (xs ! b)) None (get_next (xs ! b))›
        using vmtf_ns_b vmtf_ns xs' by (cases ‹xs ! b›) (auto elim: vmtf_nsE simp: l vmtf_ns_single_iff)

      have ‹vmtf_ns (b # al # als) (stamp (xs' ! b))
          (xs'[b := VMTF_Node (stamp (xs' ! b)) None (get_next (xs' ! b))])›
        apply (rule vmtf_ns.Cons[OF vmtf_ns_l, of _ ‹stamp (xs' ! b)›])
        subgoal using b_le_xs by auto
        subgoal using xs_b vmtf_ns_b vmtf_ns xs' by (cases ‹xs ! b›)
            (auto elim: vmtf_nsE simp: l vmtf_ns_single_iff)
        subgoal using al_b by blast
        subgoal using b_als .
        subgoal using xs' b_le_xs stamp_al_b by (simp add:)
        subgoal using ab unfolding xs' by (simp add: b_le_xs al_le_xs xs_al[symmetric]
              xs_b[symmetric])
        subgoal by simp
        done
      moreover have ‹vmtf_ns [a] n'
          (xs'[a := VMTF_Node (stamp (xs' ! a)) (get_prev (xs' ! a)) None])›
        using ab a_le_y mn nn' zs_a by (auto simp: vmtf_ns_single_iff xs')
      moreover have ‹stamp (xs' ! b) < stamp (xs' ! a)›
        using b_le_xs ab mn vmtf_ns_b zs_a by (auto simp add: xs' vmtf_ns_single_iff)
      ultimately show ?thesis
        unfolding l by (simp add: l)
    qed
  next
    case (Cons aaxs axs') note axs = this
    have [simp]: ‹aaxs = a› and bl: ‹b # l = axs' @ [ax, ay] @ azs›
      using decomp unfolding axs by simp_all
    have
      vmtf_ns_axs': ‹vmtf_ns (axs' @ [ax]) m
        (xs[ax := VMTF_Node (stamp (xs ! ax)) (get_prev (xs ! ax)) None])› and
      vmtf_ns_ay: ‹vmtf_ns (ay # azs) (stamp (xs ! ay))
        (xs[ay := VMTF_Node (stamp (xs ! ay)) None (get_next (xs ! ay))])› and
      stamp: ‹stamp (xs ! ay) < stamp (xs ! ax)›
      using IH[OF bl] by fast+
    have b_ay: ‹b ≠ ay›
      using bl vmtf_ns_distinct[OF vmtf_ns] by (cases axs') auto
    have vmtf_ns_ay': ‹vmtf_ns (ay # azs) (stamp (xs' ! ay))
        (xs[ay := VMTF_Node (stamp (xs ! ay)) None (get_next (xs ! ay))])›
      using vmtf_ns_ay xs' b_ay by (auto)
    have [simp]: ‹ay < length xs›
        using vmtf_ns by (auto intro: vmtf_ns_le_length simp: bl xs')
    have in_azs_noteq_b: ‹i ∈ set azs ⟹ i ≠ b› for i
      using vmtf_ns_distinct[OF vmtf_ns] bl by (cases axs') (auto simp: xs' b_ay)
    have a_ax[simp]: ‹a ≠ ax›
      using ab a_l bl by (cases axs') (auto simp: xs' b_ay)
    have ‹vmtf_ns (axs @ [ax]) n'
       (xs'[ax := VMTF_Node (stamp (xs' ! ax)) (get_prev (xs' ! ax)) None])›
    proof (cases axs')
      case Nil
      then have [simp]: ‹ax = b›
        using bl by auto
      have ‹vmtf_ns [ax] m (xs[ax := VMTF_Node (stamp (xs ! ax)) (get_prev (xs ! ax)) None])›
        using vmtf_ns_axs' unfolding axs Nil by simp
      then have ‹vmtf_ns (aaxs # ax # []) n'
          (xs'[ax := VMTF_Node (stamp (xs' ! ax)) (get_prev (xs' ! ax)) None])›
        apply (rule vmtf_ns.Cons[of _ _ _ _ _ n])
        subgoal using a_le_y by auto
        subgoal using zs_a a_le_y ab by auto
        subgoal using ab by auto
        subgoal by simp
        subgoal using mn .
        subgoal using zs_a a_le_y ab xs' b_le_xs by auto
        subgoal using nn' .
        done
      then show ?thesis
        using vmtf_ns_axs' unfolding axs Nil by simp
    next
      case (Cons aaaxs' axs'')
      have [simp]: ‹aaaxs' = b›
        using bl unfolding Cons by auto
      have ‹vmtf_ns (aaaxs' # axs'' @ [ax]) m
          (xs[ax := VMTF_Node (stamp (xs ! ax)) (get_prev (xs ! ax)) None])›
        using vmtf_ns_axs' unfolding axs Cons by simp
      then have ‹vmtf_ns (a # aaaxs' # axs'' @ [ax]) n'
          (xs'[ax := VMTF_Node (stamp (xs' ! ax)) (get_prev (xs' ! ax)) None])›
        apply (rule vmtf_ns.Cons[of _ _ _ _ _ n])
        subgoal using a_le_y by auto
        subgoal using zs_a a_le_y a_ax ab by (auto simp del: ‹a ≠ ax›)
        subgoal using ab by auto
        subgoal using a_l bl unfolding Cons by simp
        subgoal using mn .
        subgoal using zs_a a_le_y ab xs' b_le_xs by (auto simp: list_update_swap)
        subgoal using nn' .
        done
      then show ?thesis
        unfolding axs Cons by simp
    qed
    moreover have ‹vmtf_ns (ay # azs) (stamp (xs' ! ay))
        (xs'[ay := VMTF_Node (stamp (xs' ! ay)) None (get_next (xs' ! ay))])›
      apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf_ns_ay'])
      subgoal using vmtf_ns_distinct[OF vmtf_ns] bl b_le_xs in_azs_noteq_b by (auto simp: xs' b_ay)
      subgoal using vmtf_ns_le_length[OF vmtf_ns] bl unfolding xs' by auto
      done
    moreover have ‹stamp (xs' ! ay) < stamp (xs' ! ax)›
      using stamp unfolding axs xs' by (auto simp: b_le_xs b_ay)
    ultimately show ?thesis
      unfolding axs xs' by fast
  qed
qed

lemma vmtf_ns_append_rebuild:
  assumes
    ‹(vmtf_ns (axs @ [ax]) an ns) › and
    ‹vmtf_ns (ay # azs) (stamp (ns!ay)) ns› and
    ‹stamp (ns!ax) > stamp (ns!ay)› and
    ‹distinct (axs @ [ax, ay] @ azs)›
  shows ‹vmtf_ns (axs @ [ax, ay] @ azs) an
    (ns[ax := VMTF_Node (stamp (ns!ax)) (get_prev (ns!ax)) (Some ay) ,
       ay := VMTF_Node (stamp (ns!ay)) (Some ax) (get_next (ns!ay))])›
  using assms
proof (induction ‹axs @ [ax]› an ns arbitrary: axs ax ay azs rule: vmtf_ns.induct)
  case (Nil st xs)
  then show ?case by simp
next
  case (Cons1 a xs m n) note a_le_xs = this(1) and nm = this(2) and xs_a = this(3) and a = this(4)
    and vmtf_ns = this(5) and stamp = this(6) and dist = this(7)
  have a_ax: ‹ax = a›
    using a by simp

  have vmtf_ns_ay': ‹vmtf_ns (ay # azs) (stamp (xs ! ay)) (xs[ax := VMTF_Node n None (Some ay)])›
    apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf_ns])
    subgoal using dist a_ax a_le_xs by auto
    subgoal using vmtf_ns vmtf_ns_le_length by auto
    done

  then have ‹vmtf_ns (ax # ay # azs) m (xs[ax := VMTF_Node n None (Some ay),
      ay := VMTF_Node (stamp (xs ! ay)) (Some ax) (get_next (xs ! ay))])›
    apply (rule vmtf_ns.Cons[of _ _ _ _ _ ‹stamp (xs ! a)›])
    subgoal using a_le_xs unfolding a_ax by auto
    subgoal using xs_a a_ax a_le_xs by auto
    subgoal using dist by auto
    subgoal using dist by auto
    subgoal using stamp by (simp add: a_ax)
    subgoal using a_ax a_le_xs dist by auto
    subgoal by (simp add: nm xs_a)
    done
  then show ?case
    using a_ax a xs_a by auto
next
  case (Cons b l m xs a n xs' n') note vmtf_ns = this(1) and IH = this(2) and a_le_y = this(3) and
    zs_a = this(4) and ab = this(5) and a_l = this(6) and mn = this(7) and xs' = this(8) and
    nn' = this(9) and decomp = this(10) and vmtf_ns_ay = this(11) and stamp = this(12) and
    dist = this(13)

  have dist_b: ‹distinct ((a # b # l) @ ay # azs)›
    using dist unfolding decomp by auto
  then have b_ay: ‹b ≠ ay›
    by auto
  have b_le_xs: ‹b < length xs›
    using vmtf_ns vmtf_ns_le_length by auto
  have a_ax: ‹a ≠ ax› and a_ay: ‹a ≠ ay›
    using dist_b decomp dist by (cases axs; auto)+
  have vmtf_ns_ay': ‹vmtf_ns (ay # azs) (stamp (xs ! ay)) xs›
    apply (rule vmtf_ns_eq_iffI[of _ _ xs'])
    subgoal using xs' b_ay dist_b b_le_xs by auto
    subgoal using vmtf_ns_le_length[OF vmtf_ns_ay] xs' by auto
    subgoal using xs' b_ay dist_b b_le_xs vmtf_ns_ay xs' by auto
    done

  have ‹vmtf_ns (tl axs @ [ax, ay] @ azs) m
          (xs[ax := VMTF_Node (stamp (xs ! ax)) (get_prev (xs ! ax)) (Some ay),
              ay := VMTF_Node (stamp (xs ! ay)) (Some ax) (get_next (xs ! ay))])›
    apply (rule IH)
    subgoal using decomp by (cases axs) auto
    subgoal using vmtf_ns_ay' .
    subgoal using stamp xs' b_ay b_le_xs by (cases ‹ax = b›) auto
    subgoal using dist by (cases axs) auto
    done
  moreover have ‹tl axs @ [ax, ay] @ azs = b # l @ ay # azs›
    using decomp by (cases axs) auto
  ultimately have vmtf_ns_tl_axs: ‹vmtf_ns (b # l @ ay # azs) m
          (xs[ax := VMTF_Node (stamp (xs ! ax)) (get_prev (xs ! ax)) (Some ay),
              ay := VMTF_Node (stamp (xs ! ay)) (Some ax) (get_next (xs ! ay))])›
    by metis

  then have ‹vmtf_ns (a # b # l @ ay # azs) n'
     (xs'[ax := VMTF_Node (stamp (xs' ! ax)) (get_prev (xs' ! ax)) (Some ay),
          ay := VMTF_Node (stamp (xs' ! ay)) (Some ax) (get_next (xs' ! ay))])›
    apply (rule vmtf_ns.Cons[of _ _ _ _ _ ‹stamp (xs ! a)›])
    subgoal using a_le_y by simp
    subgoal using zs_a a_le_y a_ax a_ay by auto
    subgoal using ab .
    subgoal using dist_b by auto
    subgoal using mn by (simp add: zs_a)
    subgoal using zs_a a_le_y a_ax a_ay b_ay b_le_xs unfolding xs'
      by (auto simp: list_update_swap)
    subgoal using stamp xs' nn' b_ay b_le_xs zs_a by auto
    done
  then show ?case
    by (metis append.assoc append_Cons append_Nil decomp)
qed

text ‹
  It is tempting to remove the \<^term>‹update_x›. However, it leads to more complicated
  reasoning later: What happens if x is not in the list, but its successor is? Moreover, it is
  unlikely to really make a big difference (performance-wise).›
definition ns_vmtf_dequeue :: ‹nat ⇒ nat_vmtf_node list ⇒ nat_vmtf_node list› where
‹ns_vmtf_dequeue y xs =
  (let x = xs ! y;
   u_prev =
      (case get_prev x of None ⇒ xs
      | Some a ⇒ xs[a:= VMTF_Node (stamp (xs!a)) (get_prev (xs!a)) (get_next x)]);
   u_next =
      (case get_next x of None ⇒ u_prev
      | Some a ⇒ u_prev[a:= VMTF_Node (stamp (u_prev!a)) (get_prev x) (get_next (u_prev!a))]);
    u_x = u_next[y:= VMTF_Node (stamp (u_next!y)) None None]
    in
   u_x)
  ›

lemma vmtf_ns_different_same_neq: ‹vmtf_ns (b # c # l') m xs ⟹ vmtf_ns (c # l') m xs ⟹ False›
  apply (cases l')
  subgoal by (force elim: vmtf_nsE)
  subgoal for x xs
    apply (subst (asm) vmtf_ns.simps)
    apply (subst (asm)(2) vmtf_ns.simps)
    by (metis (no_types, lifting) vmtf_node.inject length_list_update list.discI list_tail_coinc
        nth_list_update_eq nth_list_update_neq option.discI)
  done

lemma vmtf_ns_last_next:
  ‹vmtf_ns (xs @ [x]) m ns ⟹ get_next (ns ! x) = None›
  apply (induction ‹xs @ [x]› m ns arbitrary: xs x rule: vmtf_ns.induct)
  subgoal by auto
  subgoal by auto
  subgoal for b l m xs a n xs' n' xsa x
    by (cases ‹xs ! b›; cases ‹x = b›; cases xsa)
       (force simp: vmtf_ns_le_length)+
  done

lemma vmtf_ns_hd_prev:
  ‹vmtf_ns (x # xs) m ns ⟹ get_prev (ns ! x) = None›
  apply (induction ‹x # xs› m ns arbitrary: xs x rule: vmtf_ns.induct)
  subgoal by auto
  subgoal by auto
  done

lemma vmtf_ns_last_mid_get_next:
  ‹vmtf_ns (xs @ [x, y] @ zs) m ns ⟹ get_next (ns ! x) = Some y›
  apply (induction ‹xs @ [x, y] @ zs› m ns arbitrary: xs x rule: vmtf_ns.induct)
  subgoal by auto
  subgoal by auto
  subgoal for b l m xs a n xs' n' xsa x
    by (cases ‹xs ! b›; cases ‹x = b›; cases xsa)
       (force simp: vmtf_ns_le_length)+
  done

lemma vmtf_ns_last_mid_get_next_option_hd:
  ‹vmtf_ns (xs @ x # zs) m ns ⟹ get_next (ns ! x) = option_hd zs›
  using vmtf_ns_last_mid_get_next[of xs x ‹hd zs› ‹tl zs› m ns]
  vmtf_ns_last_next[of xs x]
  by (cases zs) auto

lemma vmtf_ns_last_mid_get_prev:
  assumes ‹vmtf_ns (xs @ [x, y] @ zs) m ns›
  shows ‹get_prev (ns ! y) = Some x›
    using assms
proof (induction ‹xs @ [x, y] @ zs› m ns arbitrary: xs x rule: vmtf_ns.induct)
  case (Nil st xs)
  then show ?case by auto
next
  case (Cons1 a xs m n)
  then show ?case by auto
next
  case (Cons b l m xxs a n xxs' n') note vmtf_ns = this(1) and IH = this(2) and a_le_y = this(3) and
    zs_a = this(4) and ab = this(5) and a_l = this(6) and mn = this(7) and xs' = this(8) and
    nn' = this(9) and decomp = this(10)
  show ?case
  proof (cases xs)
    case Nil
    then show ?thesis using Cons vmtf_ns_le_length by auto
  next
    case (Cons aaxs axs')
    then have b_l: ‹b # l = tl xs @ [x, y] @ zs›
      using decomp by auto
    then have ‹get_prev (xxs ! y) = Some x›
      by (rule IH)
    moreover have ‹x ≠ y›
      using vmtf_ns_distinct[OF vmtf_ns] b_l by auto
    moreover have ‹b ≠ y›
      using vmtf_ns_distinct[OF vmtf_ns] decomp by (cases axs') (auto simp add: Cons)
    moreover have ‹y < length xxs› ‹b < length xxs›
      using vmtf_ns_le_length[OF vmtf_ns, unfolded b_l] vmtf_ns_le_length[OF vmtf_ns] by auto
    ultimately show ?thesis
      unfolding xs' by auto
  qed
qed

lemma vmtf_ns_last_mid_get_prev_option_last:
  ‹vmtf_ns (xs @ x # zs) m ns ⟹ get_prev (ns ! x) = option_last xs›
  using vmtf_ns_last_mid_get_prev[of ‹butlast xs› ‹last xs› ‹x› ‹zs› m ns]
  by (cases xs rule: rev_cases) (auto elim: vmtf_nsE)

lemma length_ns_vmtf_dequeue[simp]: ‹length (ns_vmtf_dequeue x ns) = length ns›
  unfolding ns_vmtf_dequeue_def by (auto simp: Let_def split: option.splits)

lemma vmtf_ns_skip_fst:
  assumes vmtf_ns: ‹vmtf_ns (x # y' # zs') m ns›
  shows ‹∃n. vmtf_ns (y' # zs') n (ns[y' := VMTF_Node (stamp (ns ! y')) None (get_next (ns ! y'))]) ∧
     m ≥ n›
  using assms
proof (rule vmtf_nsE, goal_cases)
  case 1
  then show ?case by simp
next
  case (2 a n)
  then show ?case by simp
next
  case (3 b l m xs a n)
  moreover have ‹get_prev (xs ! b) = None›
    using 3(3) by (fastforce elim: vmtf_nsE)
  moreover have ‹b < length xs›
    using 3(3) vmtf_ns_le_length by auto
  ultimately show ?case
    by (cases ‹xs ! b›) (auto simp: eq_commute[of ‹xs ! b›])
qed

definition vmtf_ns_notin where
  ‹vmtf_ns_notin l m xs ⟷ (∀i<length xs. i∉set l ⟶ (get_prev (xs ! i) = None ∧
      get_next (xs ! i) = None))›

lemma vmtf_ns_notinI:
  ‹(⋀i. i <length xs ⟹ i∉set l ⟹ get_prev (xs ! i) = None ∧
      get_next (xs ! i) = None) ⟹ vmtf_ns_notin l m xs›
  by (auto simp: vmtf_ns_notin_def)

lemma stamp_ns_vmtf_dequeue:
  ‹axs < length zs ⟹ stamp (ns_vmtf_dequeue x zs ! axs) = stamp (zs ! axs)›
  by (cases ‹zs ! (the (get_next (zs ! x)))›; cases ‹(the (get_next (zs ! x))) = axs›;
      cases ‹(the (get_prev (zs ! x))) = axs›; cases ‹zs ! x›)
    (auto simp: nth_list_update' ns_vmtf_dequeue_def Let_def split: option.splits)

lemma sorted_many_eq_append: ‹sorted (xs @ [x, y]) ⟷ sorted (xs @ [x]) ∧ x ≤ y›
  using sorted_append[of ‹xs @ [x]› ‹[y]›] sorted_append[of xs ‹[x]›]
  by force

lemma vmtf_ns_stamp_sorted:
  assumes ‹vmtf_ns l m ns›
  shows ‹sorted (map (λa. stamp (ns!a)) (rev l)) ∧ (∀a ∈ set l. stamp (ns!a) ≤ m)›
  using assms
proof (induction rule: vmtf_ns.induct)
  case (Cons b l m xs a n xs' n') note vmtf_ns = this(1) and IH = this(9) and a_le_y = this(2) and
    zs_a = this(3) and ab = this(4) and a_l = this(5) and mn = this(6) and xs' = this(7) and
    nn' = this(8)
  have H:
  ‹map (λaa. stamp (xs[b := VMTF_Node (stamp (xs ! b)) (Some a) (get_next (xs ! b))] ! aa)) (rev l) =
     map (λa. stamp (xs ! a)) (rev l)›
    apply (rule map_cong)
    subgoal by auto
    subgoal using vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns] by auto
    done
  have [simp]: ‹stamp (xs[b := VMTF_Node (stamp (xs ! b)) (Some a) (get_next (xs ! b))] ! b) =
     stamp (xs ! b)›
    using vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns] by (cases ‹xs ! b›) auto
  have ‹stamp (xs[b := VMTF_Node (stamp (xs ! b)) (Some a) (get_next (xs ! b))] ! aa) ≤ n'›
    if ‹aa ∈ set l› for aa
    apply (cases ‹aa = b›)
    subgoal using Cons by auto
    subgoal using vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns] IH nn' mn that by auto
    done
  then show ?case
    using Cons by (auto simp: H sorted_many_eq_append)
qed auto

lemma vmtf_ns_ns_vmtf_dequeue:
  assumes vmtf_ns: ‹vmtf_ns l m ns› and notin: ‹vmtf_ns_notin l m ns› and valid: ‹x < length ns›
  shows ‹vmtf_ns (remove1 x l) m (ns_vmtf_dequeue x ns)›
proof (cases ‹x ∈ set l›)
  case False
  then have H: ‹remove1 x l = l›
    by (simp add: remove1_idem)
  have simp_is_stupid[simp]: ‹a ∈ set l ⟹ x ∉ set l ⟹ a ≠ x› ‹a ∈ set l ⟹ x ∉ set l ⟹ x ≠ a›  for a x
    by auto
  have
      ‹get_prev (ns ! x) = None › and
      ‹get_next (ns ! x) = None›
    using notin False valid unfolding vmtf_ns_notin_def by auto
  then have vmtf_ns_eq: ‹(ns_vmtf_dequeue x ns) ! a = ns ! a› if ‹a ∈ set l› for a
    using that False valid unfolding vmtf_ns_notin_def ns_vmtf_dequeue_def
    by (cases ‹ns ! (the (get_prev (ns ! x)))›; cases ‹ns ! (the (get_next (ns ! x)))›)
      (auto simp: Let_def split: option.splits)
  show ?thesis
    unfolding H
    apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf_ns])
    subgoal using vmtf_ns_eq by blast
    subgoal using vmtf_ns_le_length[OF vmtf_ns] by auto
    done
next
  case True
  then obtain xs zs where
    l: ‹l = xs @ x # zs›
    by (meson split_list)
  have r_l: ‹remove1 x l = xs @ zs›
    using vmtf_ns_distinct[OF vmtf_ns] unfolding l by (simp add: remove1_append)
  have dist: ‹distinct l›
    using vmtf_ns_distinct[OF vmtf_ns] .
  have le_length: ‹i ∈ set l ⟹ i < length ns› for i
    using vmtf_ns_le_length[OF vmtf_ns] .
  consider
    (xs_zs_empty) ‹xs = []› and ‹zs = []› |
    (xs_nempty_zs_empty) x' xs' where ‹xs = xs' @ [x']› and ‹zs = []› |
    (xs_empty_zs_nempty) y' zs' where ‹xs = []› and ‹zs = y' # zs'› |
    (xs_zs_nempty) x' y' xs' zs' where  ‹xs = xs' @ [x']› and ‹zs = y' # zs'›
    by (cases xs rule: rev_cases; cases zs)
  then show ?thesis
  proof cases
    case xs_zs_empty
    then show ?thesis
      using vmtf_ns by (auto simp: r_l intro: vmtf_ns.intros)
  next
    case xs_empty_zs_nempty note xs = this(1) and zs = this(2)
    have [simp]: ‹x ≠ y'› ‹y' ≠ x› ‹x ∉ set zs'›
      using dist unfolding l xs zs by auto
    have prev_next: ‹get_prev (ns ! x) = None› ‹get_next (ns ! x) = option_hd zs›
      using vmtf_ns unfolding l xs zs
      by (cases zs; auto 5 5 simp: option_hd_def elim: vmtf_nsE; fail)+
    then have vmtf': ‹vmtf_ns (y' # zs') m (ns[y' := VMTF_Node (stamp (ns ! y')) None (get_next (ns ! y'))])›
      using vmtf_ns unfolding r_l unfolding l xs zs
      by (auto simp: ns_vmtf_dequeue_def Let_def nth_list_update' zs
          split: option.splits
          intro: vmtf_ns.intros vmtf_ns_stamp_increase dest: vmtf_ns_skip_fst)
    show ?thesis
      apply (rule vmtf_ns_eq_iffI[of _ _
            ‹(ns[y' := VMTF_Node (stamp (ns ! y')) None (get_next (ns ! y'))])› m])
      subgoal
        using prev_next unfolding r_l unfolding l xs zs
        by (cases ‹ns ! x›) (auto simp: ns_vmtf_dequeue_def Let_def nth_list_update')
      subgoal
        using prev_next le_length unfolding r_l unfolding l xs zs
        by (cases ‹ns ! x›) auto
      subgoal
        using vmtf' unfolding r_l unfolding l xs zs by auto
      done
  next
    case xs_nempty_zs_empty note xs = this(1) and zs = this(2)
    have [simp]: ‹x ≠ x'› ‹x' ≠ x› ‹x' ∉ set xs'› ‹x ∉ set xs'›
      using dist unfolding l xs zs by auto
    have prev_next: ‹get_prev (ns ! x) = Some x'› ‹get_next (ns ! x) = None›
      using vmtf_ns vmtf_ns_append_decomp[of xs' x' x zs m ns] unfolding l xs zs
      by (auto simp: vmtf_ns_single_iff intro: vmtf_ns_last_mid_get_prev)
    then have vmtf': ‹vmtf_ns (xs' @ [x']) m (ns[x' := VMTF_Node (stamp (ns ! x')) (get_prev (ns ! x')) None])›
      using vmtf_ns unfolding r_l unfolding l xs zs
      by (auto simp: ns_vmtf_dequeue_def Let_def vmtf_ns_append_decomp split: option.splits
          intro: vmtf_ns.intros)
    show ?thesis
      apply (rule vmtf_ns_eq_iffI[of _ _
            ‹(ns[x' := VMTF_Node (stamp (ns ! x')) (get_prev (ns ! x')) None])› m])
      subgoal
        using prev_next unfolding r_l unfolding l xs zs
        by (cases ‹ns ! x'›) (auto simp: ns_vmtf_dequeue_def Let_def nth_list_update')
      subgoal
        using prev_next le_length unfolding r_l unfolding l xs zs
        by (cases ‹ns ! x›) auto
      subgoal
        using vmtf' unfolding r_l unfolding l xs zs by auto
      done
  next
    case xs_zs_nempty note xs = this(1) and zs = this(2)
    have vmtf_ns_x'_x: ‹vmtf_ns (xs' @ [x', x] @ (y' #  zs')) m ns› and
      vmtf_ns_x_y: ‹vmtf_ns ((xs' @ [x']) @ [x, y'] @ zs') m ns›
      using vmtf_ns unfolding l xs zs by simp_all
    from vmtf_ns_append_decomp[OF vmtf_ns_x'_x] have
      vmtf_ns_xs: ‹vmtf_ns (xs' @ [x']) m (ns[x' := VMTF_Node (stamp (ns ! x')) (get_prev (ns ! x')) None])› and
      vmtf_ns_zs: ‹vmtf_ns (x # y' # zs') (stamp (ns ! x)) (ns[x := VMTF_Node (stamp (ns ! x)) None (get_next (ns ! x))])› and
      stamp: ‹stamp (ns ! x) < stamp (ns ! x')›
      by fast+
    have [simp]: ‹y' < length ns› ‹x < length ns› ‹x ≠ y'› ‹x' ≠ y'› ‹x' < length ns› ‹y' ≠ x'›
      ‹x' ≠ x› ‹x ≠ x'› ‹y' ≠ x›
      and x_zs': ‹x ∉ set zs'› ‹x ∉ set xs'› and x'_zs': ‹x' ∉ set zs'› and y'_xs': ‹y' ∉ set xs'›
      using vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns] unfolding l xs zs
      by auto
    obtain n where
      vmtf_ns_zs': ‹vmtf_ns (y' # zs') n (ns[x := VMTF_Node (stamp (ns ! x)) None (get_next (ns ! x)),
          y' := VMTF_Node (stamp (ns[x := VMTF_Node (stamp (ns ! x)) None (get_next (ns ! x))] ! y')) None
       (get_next (ns[x := VMTF_Node (stamp (ns ! x)) None (get_next (ns ! x))] ! y'))])› and
      ‹n ≤ stamp (ns ! x)›
      using vmtf_ns_skip_fst[OF vmtf_ns_zs] by blast
    then have vmtf_ns_y'_zs'_x_y': ‹vmtf_ns (y' # zs') n (ns[x := VMTF_Node (stamp (ns ! x)) None (get_next (ns ! x)),
          y' := VMTF_Node (stamp (ns ! y')) None (get_next (ns ! y'))])›
      by auto

    define ns' where ‹ns' = ns[x' := VMTF_Node (stamp (ns ! x')) (get_prev (ns ! x')) None,
         y' := VMTF_Node (stamp (ns ! y')) None (get_next (ns ! y'))]›
    have vmtf_ns_y'_zs'_y': ‹vmtf_ns (y' # zs') n (ns[y' := VMTF_Node (stamp (ns ! y')) None (get_next (ns ! y'))])›
      apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf_ns_y'_zs'_x_y'])
      subgoal using x_zs' by auto
      subgoal using vmtf_ns_le_length[OF vmtf_ns] unfolding l xs zs by auto
      done
    moreover have stamp_y'_n: ‹stamp (ns[x' := VMTF_Node (stamp (ns ! x')) (get_prev (ns ! x')) None] ! y') ≤ n›
      using vmtf_ns_stamp_sorted[OF vmtf_ns_y'_zs'_y'] stamp unfolding l xs zs
      by (auto simp: sorted_append)
    ultimately have vmtf_ns_y'_zs'_y': ‹vmtf_ns (y' # zs') (stamp (ns' ! y'))
       (ns[y' := VMTF_Node (stamp (ns ! y')) None (get_next (ns ! y'))])›
      using l vmtf_ns vmtf_ns_append_decomp xs_zs_nempty(2) ns'_def by auto
    have vmtf_ns_y'_zs'_x'_y': ‹vmtf_ns (y' # zs') (stamp (ns' ! y')) ns'›
      apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf_ns_y'_zs'_y'])
      subgoal using dist le_length x'_zs' ns'_def unfolding l xs zs by auto
      subgoal using dist le_length x'_zs' ns'_def unfolding l xs zs by auto
      done
    have vmtf_ns_xs': ‹vmtf_ns (xs' @ [x']) m ns'›
      apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf_ns_xs])
      subgoal using y'_xs' ns'_def by auto
      subgoal using vmtf_ns_le_length[OF vmtf_ns_xs] ns'_def by auto
      done
    have vmtf_x'_y': ‹vmtf_ns (xs' @ [x', y'] @ zs') m
       (ns'[x' := VMTF_Node (stamp (ns' ! x')) (get_prev (ns' ! x')) (Some y'),
         y' := VMTF_Node (stamp (ns' ! y')) (Some x') (get_next (ns' ! y'))])›
      apply (rule vmtf_ns_append_rebuild[OF vmtf_ns_xs' vmtf_ns_y'_zs'_x'_y'])
      subgoal using stamp_y'_n vmtf_ns_xs vmtf_ns_zs stamp ‹n ≤ stamp (ns ! x)›
        unfolding ns'_def by auto
      subgoal by (metis append.assoc append_Cons distinct_remove1 r_l self_append_conv2 vmtf_ns
            vmtf_ns_distinct xs zs)
      done
    have ‹vmtf_ns (xs' @ [x', y'] @ zs') m
       (ns'[x' := VMTF_Node (stamp (ns' ! x')) (get_prev (ns' ! x')) (Some y'),
         y' := VMTF_Node (stamp (ns' ! y')) (Some x') (get_next (ns' ! y')),
         x := VMTF_Node (stamp (ns' ! x)) None None])›
      apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf_x'_y'])
      subgoal
        using vmtf_ns_last_mid_get_next[OF vmtf_ns_x_y] vmtf_ns_last_mid_get_prev[OF vmtf_ns_x'_x] x_zs'
        by (cases ‹ns!x›; auto simp: nth_list_update' ns'_def)
      subgoal using le_length unfolding l xs zs ns'_def by auto
      done
    moreover have ‹xs' @ [x', y'] @ zs' = remove1 x l›
      unfolding r_l xs zs by auto
    moreover have ‹ns'[x' := VMTF_Node (stamp (ns' ! x')) (get_prev (ns' ! x')) (Some y'),
         y' := VMTF_Node (stamp (ns' ! y')) (Some x') (get_next (ns' ! y')),
         x := VMTF_Node (stamp (ns' ! x)) None None] = ns_vmtf_dequeue x ns›
      using vmtf_ns_last_mid_get_next[OF vmtf_ns_x_y] vmtf_ns_last_mid_get_prev[OF vmtf_ns_x'_x]
      list_update_swap[of x' y' _ ‹_ :: nat_vmtf_node›]
      unfolding ns'_def ns_vmtf_dequeue_def
      by (auto simp: Let_def)
    ultimately show ?thesis
      by force
  qed
qed

lemma vmtf_ns_hd_next:
   ‹vmtf_ns (x # a # list) m ns ⟹ get_next (ns ! x) = Some a›
  by (auto 5 5 elim: vmtf_nsE)

lemma vmtf_ns_notin_dequeue:
  assumes vmtf_ns: ‹vmtf_ns l m ns› and notin: ‹vmtf_ns_notin l m ns› and valid: ‹x < length ns›
  shows ‹vmtf_ns_notin (remove1 x l) m (ns_vmtf_dequeue x ns)›
proof (cases ‹x ∈ set l›)
  case False
  then have H: ‹remove1 x l = l›
    by (simp add: remove1_idem)
  have simp_is_stupid[simp]: ‹a ∈ set l ⟹ x ∉ set l ⟹ a ≠ x› ‹a ∈ set l ⟹ x ∉ set l ⟹ x ≠ a›  for a x
    by auto
  have
    ‹get_prev (ns ! x) = None› and
    ‹get_next (ns ! x) = None›
    using notin False valid unfolding vmtf_ns_notin_def by auto
  show ?thesis
    using notin valid False unfolding vmtf_ns_notin_def
    by (auto simp: vmtf_ns_notin_def ns_vmtf_dequeue_def Let_def H split: option.splits)
next
  case True
  then obtain xs zs where
    l: ‹l = xs @ x # zs›
    by (meson split_list)
  have r_l: ‹remove1 x l = xs @ zs›
    using vmtf_ns_distinct[OF vmtf_ns] unfolding l by (simp add: remove1_append)

  consider
    (xs_zs_empty) ‹xs = []› and ‹zs = []› |
    (xs_nempty_zs_empty) x' xs' where ‹xs = xs' @ [x']› and ‹zs = []› |
    (xs_empty_zs_nempty) y' zs' where ‹xs = []› and ‹zs = y' # zs'› |
    (xs_zs_nempty) x' y' xs' zs' where  ‹xs = xs' @ [x']› and ‹zs = y' # zs'›
    by (cases xs rule: rev_cases; cases zs)
  then show ?thesis
  proof cases
    case xs_zs_empty
    then show ?thesis
      using notin vmtf_ns unfolding l apply (cases ‹ns ! x›)
        by (auto simp: vmtf_ns_notin_def ns_vmtf_dequeue_def Let_def vmtf_ns_single_iff
           split: option.splits)
  next
    case xs_empty_zs_nempty note xs = this(1) and zs = this(1)
    have prev_next: ‹get_prev (ns ! x) = None› ‹get_next (ns ! x) = option_hd zs›
      using vmtf_ns unfolding l xs zs
      by (cases zs; auto simp: option_hd_def elim: vmtf_nsE dest: vmtf_ns_hd_next)+
    show ?thesis
      apply (rule vmtf_ns_notinI)
      apply (case_tac ‹i = x›)
      subgoal
        using vmtf_ns prev_next unfolding r_l unfolding l xs zs
        by (cases zs) (auto simp: ns_vmtf_dequeue_def Let_def
            vmtf_ns_notin_def vmtf_ns_single_iff
            split: option.splits)
      subgoal
        using vmtf_ns notin prev_next unfolding r_l unfolding l xs zs
        by (auto simp: ns_vmtf_dequeue_def Let_def
            vmtf_ns_notin_def vmtf_ns_single_iff
            split: option.splits
            intro: vmtf_ns.intros vmtf_ns_stamp_increase dest: vmtf_ns_skip_fst)
       done
  next
    case xs_nempty_zs_empty note xs = this(1) and zs = this(2)
    have prev_next: ‹get_prev (ns ! x) = Some x'› ‹get_next (ns ! x) = None›
      using vmtf_ns vmtf_ns_append_decomp[of xs' x' x zs m ns] unfolding l xs zs
      by (auto simp: vmtf_ns_single_iff intro: vmtf_ns_last_mid_get_prev)
    then show ?thesis
      using vmtf_ns notin unfolding r_l unfolding l xs zs
      by (auto simp: ns_vmtf_dequeue_def Let_def vmtf_ns_append_decomp vmtf_ns_notin_def
          split: option.splits
          intro: vmtf_ns.intros)
  next
    case xs_zs_nempty note xs = this(1) and zs = this(2)
    have vmtf_ns_x'_x: ‹vmtf_ns (xs' @ [x', x] @ (y' #  zs')) m ns› and
      vmtf_ns_x_y: ‹vmtf_ns ((xs' @ [x']) @ [x, y'] @ zs') m ns›
      using vmtf_ns unfolding l xs zs by simp_all
    have [simp]: ‹y' < length ns› ‹x < length ns› ‹x ≠ y'› ‹x' ≠ y'› ‹x' < length ns› ‹y' ≠ x'›
      ‹y' ≠ x› ‹y' ∉ set xs›  ‹y' ∉ set zs'›
      and x_zs': ‹x ∉ set zs'› and x'_zs': ‹x' ∉ set zs'› and y'_xs': ‹y' ∉ set xs'›
      using vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns] unfolding l xs zs
      by auto
    have ‹get_next (ns!x) = Some y'› ‹get_prev (ns!x) = Some x'›
      using vmtf_ns_last_mid_get_prev[OF vmtf_ns_x'_x] vmtf_ns_last_mid_get_next[OF vmtf_ns_x_y]
      by fast+
    then show ?thesis
      using notin x_zs' x'_zs' y'_xs' unfolding l xs zs
      by (auto simp: vmtf_ns_notin_def ns_vmtf_dequeue_def)
  qed
qed

lemma vmtf_ns_stamp_distinct:
  assumes ‹vmtf_ns l m ns›
  shows ‹distinct (map (λa. stamp (ns!a)) l)›
  using assms
proof (induction rule: vmtf_ns.induct)
  case (Cons b l m xs a n xs' n') note vmtf_ns = this(1) and IH = this(9) and a_le_y = this(2) and
    zs_a = this(3) and ab = this(4) and a_l = this(5) and mn = this(6) and xs' = this(7) and
    nn' = this(8)
  have [simp]: ‹map (λaa. stamp
                 (if b = aa
                  then VMTF_Node (stamp (xs ! aa)) (Some a) (get_next (xs ! aa))
                  else xs ! aa)) l =
        map (λaa. stamp (xs ! aa)) l
       › for a
    apply (rule map_cong)
    subgoal ..
    subgoal using vmtf_ns_distinct[OF vmtf_ns] by auto
    done
  show ?case
    using Cons vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns]
    by (auto simp: sorted_many_eq_append leD vmtf_ns_stamp_sorted cong: if_cong)
qed auto

lemma vmtf_ns_thighten_stamp:
  assumes vmtf_ns: ‹vmtf_ns l m xs› and n: ‹∀a∈set l. stamp (xs ! a) ≤ n›
  shows ‹vmtf_ns l n xs›
proof -
  consider
    (empty) ‹l = []› |
    (single) x where ‹l = [x]› |
    (more_than_two) x y ys where ‹l = x # y # ys›
    by (cases l; cases ‹tl l›) auto
  then show ?thesis
  proof cases
    case empty
    then show ?thesis by (auto intro: vmtf_ns.intros)
  next
    case (single x)
    then show ?thesis using n vmtf_ns by (auto simp: vmtf_ns_single_iff)
  next
    case (more_than_two x y ys) note l = this
    then have vmtf_ns': ‹vmtf_ns ([] @ [x, y] @ ys) m xs›
      using vmtf_ns by auto
    from vmtf_ns_append_decomp[OF this] have
      ‹vmtf_ns ([x]) m (xs[x := VMTF_Node (stamp (xs ! x)) (get_prev (xs ! x)) None])› and
      vmtf_ns_y_ys: ‹vmtf_ns (y # ys) (stamp (xs ! y))
        (xs[y := VMTF_Node (stamp (xs ! y)) None (get_next (xs ! y))])› and
      ‹stamp (xs ! y) < stamp (xs ! x)›
      by auto
    have [simp]: ‹x ≠ y› ‹x ∉ set ys› ‹x < length xs› ‹y < length xs›
      using vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns] unfolding l by auto
    show ?thesis
      unfolding l
      apply (rule vmtf_ns.Cons[OF vmtf_ns_y_ys, of _ ‹stamp (xs ! x)›])
      subgoal using vmtf_ns_le_length[OF vmtf_ns] unfolding l by auto
      subgoal using vmtf_ns unfolding l by (cases ‹xs ! x›) (auto elim: vmtf_nsE)
      subgoal by simp
      subgoal by simp
      subgoal using vmtf_ns_stamp_sorted[OF vmtf_ns] vmtf_ns_stamp_distinct[OF vmtf_ns]
       by (auto simp: l sorted_many_eq_append)
      subgoal
        using vmtf_ns vmtf_ns_last_mid_get_prev[OF vmtf_ns']
        apply (cases ‹xs ! y›)
        by simp (auto simp: l eq_commute[of ‹xs ! y›])
      subgoal using n unfolding l by auto
      done
  qed
qed

lemma vmtf_ns_rescale:
  assumes
    ‹vmtf_ns l m xs› and
    ‹sorted (map (λa. st ! a) (rev l))› and ‹distinct (map (λa. st ! a) l)›
    ‹∀a ∈ set l. get_prev (zs ! a) = get_prev (xs ! a)› and
    ‹∀a ∈ set l. get_next (zs ! a) = get_next (xs ! a)› and
    ‹∀a ∈ set l. stamp (zs ! a) = st ! a› and
    ‹length xs ≤ length zs› and
    ‹∀a∈set l. a < length st› and
    m': ‹∀a ∈ set l. st ! a < m'›
  shows ‹vmtf_ns l m' zs›
  using assms
proof (induction arbitrary: zs m' rule: vmtf_ns.induct)
  case (Nil st xs)
  then show ?case by (auto intro: vmtf_ns.intros)
next
  case (Cons1 a xs m n)
  then show ?case by (cases ‹zs ! a›) (auto simp: vmtf_ns_single_iff intro!: Max_ge nth_mem)
next
  case (Cons b l m xs a n xs' n' zs m') note vmtf_ns = this(1) and a_le_y = this(2) and
    zs_a = this(3) and ab = this(4) and a_l = this(5) and mn = this(6) and xs' = this(7) and
    nn' = this(8) and IH = this(9) and H = this(10-)
  have [simp]: ‹b < length xs› ‹b ≠ a› ‹a ≠ b› ‹b ∉ set l› ‹b < length zs› ‹a < length zs›
    using vmtf_ns_distinct[OF vmtf_ns] vmtf_ns_le_length[OF vmtf_ns] ab H(6) a_le_y unfolding xs'
    by force+

  have simp_is_stupid[simp]: ‹a ∈ set l ⟹ x ∉ set l ⟹ a ≠ x› ‹a ∈ set l ⟹ x ∉ set l ⟹ x ≠ a›  for a x
    by auto
  define zs' where ‹zs' ≡ (zs[b := VMTF_Node (st ! b) (get_prev (xs ! b)) (get_next (xs ! b)),
          a := VMTF_Node (st ! a) None (Some b)])›
  have zs_upd_zs: ‹zs = zs
    [b := VMTF_Node (st ! b) (get_prev (xs ! b)) (get_next (xs ! b)),
     a := VMTF_Node (st ! a) None (Some b),
     b := VMTF_Node (st ! b) (Some a) (get_next (xs ! b))]
    ›
    using H(2-5) xs' zs_a ‹b < length xs›
    by (metis list.set_intros(1) list.set_intros(2) list_update_id list_update_overwrite
      nth_list_update_eq nth_list_update_neq vmtf_node.collapse vmtf_node.sel(2,3))

  have vtmf_b_l: ‹vmtf_ns (b # l) m' zs'›
    unfolding zs'_def
    apply (rule IH)
    subgoal using H(1) by (simp add: sorted_many_eq_append)
    subgoal using H(2) by auto
    subgoal using H(3,4,5) xs' zs_a a_l ab by (auto split: if_splits)
    subgoal using H(4) xs' zs_a a_l ab by auto
    subgoal using H(5) xs' a_l ab by auto
    subgoal using H(6) xs' by auto
    subgoal using H(7) xs' by auto
    subgoal using H(8) by auto
    done
  then have ‹vmtf_ns (b # l) (stamp (zs' ! b)) zs'›
    by (rule vmtf_ns_thighten_stamp)
      (use vmtf_ns_stamp_sorted[OF vtmf_b_l] in ‹auto simp: sorted_append›)

  then show ?case
    apply (rule vmtf_ns.Cons[of _ _ _ _ _ ‹st ! a›])
    unfolding zs'_def
    subgoal using a_le_y H(6) xs' by auto
    subgoal using a_le_y by auto
    subgoal using ab.
    subgoal using a_l .
    subgoal using nn' mn H(1,2) by (auto simp: sorted_many_eq_append)
    subgoal using zs_upd_zs by auto
    subgoal using H by (auto intro!: Max_ge nth_mem)
    done
qed

lemma vmtf_ns_last_prev:
  assumes vmtf: ‹vmtf_ns (xs @ [x]) m ns›
  shows ‹get_prev (ns ! x) = option_last xs›
proof (cases xs rule: rev_cases)
  case Nil
  then show ?thesis using vmtf by (cases ‹ns!x›) (auto simp: vmtf_ns_single_iff)
next
  case (snoc xs' y')
  then show ?thesis
    using vmtf_ns_last_mid_get_prev[of xs' y' x ‹[]› m ns] vmtf by auto
qed


paragraph ‹Abstract Invariants›

text ‹
  Invariants
  ▪ The atoms of \<^term>‹xs› and \<^term>‹ys› are always disjoint.
  ▪ The atoms of \<^term>‹ys› are ∗‹always› set.
  ▪ The atoms of \<^term>‹xs› ∗‹can› be set but do not have to.
›

definition vmtf_ℒ⇩a⇩l⇩l :: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ nat abs_vmtf_ns ⇒ bool› where
‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ≡ λ(xs, ys).
  (∀L∈ys. L ∈ atm_of ` lits_of_l M) ∧
  xs ∩ ys = {} ∧
  xs ∪ ys = atms_of (ℒ⇩a⇩l⇩l 𝒜)
  ›

abbreviation abs_vmtf_ns_inv :: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ nat abs_vmtf_ns ⇒ bool› where
‹abs_vmtf_ns_inv 𝒜 M vm ≡ vmtf_ℒ⇩a⇩l⇩l 𝒜 M vm›


subsubsection ‹Implementation›

type_synonym (in -) vmtf = ‹nat_vmtf_node list × nat × nat × nat × nat option›

text ‹
  We use the opposite direction of the VMTF paper: The latest added element \<^term>‹fst_As› is at
  the beginning.
›

definition vmtf :: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ vmtf set› where
‹vmtf 𝒜 M = {(ns, m, fst_As, lst_As, next_search).
   (∃xs' ys'.
     vmtf_ns (ys' @ xs') m ns ∧ fst_As = hd (ys' @ xs') ∧ lst_As = last (ys' @ xs')
   ∧ next_search = option_hd xs'
   ∧ vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set xs', set ys')
   ∧ vmtf_ns_notin (ys' @ xs') m ns
   ∧ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns) ∧ (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))
  )}›

lemma vmtf_consD:
  assumes vmtf: ‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 M›
  shows ‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 (L # M)›
proof -
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'))› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  moreover have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 (L # M) ((set xs', set ys'))›
    using abs_vmtf unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
  ultimately have ‹vmtf_ns (ys' @ xs') m ns ∧
       fst_As = hd (ys' @ xs') ∧
       lst_As = last (ys' @ xs') ∧
       next_search = option_hd xs' ∧
       vmtf_ℒ⇩a⇩l⇩l 𝒜 (L # M) ((set xs', set ys')) ∧
       vmtf_ns_notin (ys' @ xs') m ns ∧ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns) ∧
       (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
      by fast
  then show ?thesis
    unfolding vmtf_def by fast
qed


lemma vmtf_consD':
  assumes vmtf: ‹x ∈ vmtf 𝒜 M›
  shows ‹x ∈ vmtf 𝒜 (L # M)›
  using vmtf_consD
  by (metis prod_cases5 vmtf) 

type_synonym (in -) vmtf_option_fst_As = ‹nat_vmtf_node list × nat × nat option × nat option × nat option›

definition (in -) vmtf_dequeue :: ‹nat ⇒ vmtf ⇒ vmtf_option_fst_As› where
‹vmtf_dequeue ≡ (λL (ns, m, fst_As, lst_As, next_search).
  (let fst_As' = (if fst_As = L then get_next (ns ! L) else Some fst_As);
       next_search' = if next_search = Some L then get_next (ns ! L) else next_search;
       lst_As' = if lst_As = L then get_prev (ns ! L) else Some lst_As in
   (ns_vmtf_dequeue L ns, m, fst_As', lst_As', next_search')))›

text ‹It would be better to distinguish whether L is set in M or not.›
definition vmtf_enqueue :: ‹(nat, nat) ann_lits ⇒ nat ⇒ vmtf_option_fst_As ⇒ vmtf› where
‹vmtf_enqueue = (λM L (ns, m, fst_As, lst_As, next_search).
  (case fst_As of
    None ⇒ (ns[L := VMTF_Node m fst_As None], m+1, L, L,
         (if defined_lit M (Pos L) then None else Some L))
  | Some fst_As ⇒
     let fst_As' = VMTF_Node (stamp (ns!fst_As)) (Some L) (get_next (ns!fst_As)) in
      (ns[L := VMTF_Node (m+1) None (Some fst_As), fst_As := fst_As'],
          m+1, L, the lst_As, (if defined_lit M (Pos L) then next_search else Some L))))›

definition (in -) vmtf_en_dequeue :: ‹(nat, nat) ann_lits ⇒ nat ⇒ vmtf ⇒  vmtf› where
‹vmtf_en_dequeue = (λM L vm. vmtf_enqueue M L (vmtf_dequeue L vm))›

lemma abs_vmtf_ns_bump_vmtf_dequeue:
  fixes M
  assumes vmtf:‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 M›  and
    L: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and
    dequeue: ‹(ns', m', fst_As', lst_As', next_search') =
       vmtf_dequeue L (ns, m, fst_As, lst_As, next_search)› and
    𝒜⇩i⇩n_nempty: ‹isasat_input_nempty 𝒜›
  shows ‹∃xs' ys'. vmtf_ns (ys' @ xs') m' ns' ∧ fst_As' = option_hd (ys' @ xs')
   ∧ lst_As' = option_last (ys' @ xs')
   ∧ next_search' = option_hd xs'
   ∧ next_search' = (if next_search = Some L then get_next (ns!L) else next_search)
   ∧ vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((insert L (set xs'), set ys'))
   ∧ vmtf_ns_notin (ys' @ xs') m' ns' ∧
   L ∉ set (ys' @ xs') ∧ (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
  unfolding vmtf_def
proof -
  have ns': ‹ns' = ns_vmtf_dequeue L ns› and
    fst_As': ‹fst_As' = (if fst_As = L then get_next (ns ! L) else Some fst_As)› and
    lst_As': ‹lst_As' = (if lst_As = L then get_prev (ns ! L) else Some lst_As)› and
    m'm: ‹m' = m› and
    next_search_L_next:
      ‹next_search' = (if next_search = Some L then get_next (ns!L) else next_search)›
    using dequeue unfolding vmtf_dequeue_def by auto
  obtain xs ys where
    vmtf: ‹vmtf_ns (ys @ xs) m ns› and
    notin: ‹vmtf_ns_notin (ys @ xs) m ns› and
    next_search: ‹next_search = option_hd xs› and
    abs_inv: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs, set ys))› and
    fst_As: ‹fst_As = hd (ys @ xs)› and
    lst_As: ‹lst_As = last (ys @ xs)› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    L_ys_xs: ‹∀L∈set (ys @ xs). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by auto
  have [dest]: ‹xs = [] ⟹ ys = [] ⟹ False›
    using abs_inv 𝒜⇩i⇩n_nempty unfolding atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n vmtf_ℒ⇩a⇩l⇩l_def
    by auto
  let ?ys = ‹ys›
  let ?xs = ‹xs›
  have dist: ‹distinct (xs @ ys)›
    using vmtf_ns_distinct[OF vmtf] by auto
  have xs_ys: ‹remove1 L ys @ remove1 L xs = remove1 L (ys @ xs)›
    using dist by (auto simp: remove1_append remove1_idem disjoint_iff_not_equal
        intro!: remove1_idem)
  have atm_L_A: ‹L < length ns›
    using atm_A L by blast

  have ‹vmtf_ns (remove1 L ys @ remove1 L xs) m' ns'›
    using vmtf_ns_ns_vmtf_dequeue[OF vmtf notin, of L] dequeue dist atm_L_A
    unfolding vmtf_dequeue_def by (auto split: if_splits simp: xs_ys)
  moreover have next_search': ‹next_search' = option_hd (remove1 L xs)›
  proof -
    have ‹[hd xs, hd (tl xs)] @ tl (tl xs) = xs›
      if ‹xs ≠ []› ‹tl xs ≠ []›
      apply (cases xs; cases ‹tl xs›)
       using that by (auto simp: tl_append split: list.splits)
    then have [simp]: ‹get_next (ns ! hd xs) = option_hd (remove1 (hd xs) xs)› if ‹xs ≠ []›
      using vmtf_ns_last_mid_get_next[of ‹?ys› ‹hd ?xs›
          ‹hd (tl ?xs)› ‹tl (tl ?xs)› m ns] vmtf vmtf_ns_distinct[OF vmtf] that
        distinct_remove1_last_butlast[of xs]
      by (cases xs; cases ‹tl xs›)
        (auto simp: tl_append vmtf_ns_last_next split: list.splits elim: vmtf_nsE)
    have ‹xs ≠ [] ⟹ xs ≠ [L] ⟹  L ≠ hd xs ⟹ hd xs = hd (remove1 L xs)›
      by (induction xs) (auto simp: remove1_Nil_iff)
    then have [simp]: ‹option_hd xs = option_hd (remove1 L xs)› if ‹L ≠ hd xs›
      using that vmtf_ns_distinct[OF vmtf]
      by (auto simp: option_hd_def remove1_Nil_iff)
    show ?thesis
      using dequeue dist atm_L_A next_search next_search unfolding vmtf_dequeue_def
      by (auto split: if_splits simp: xs_ys dest: last_in_set)
    qed
  moreover {
    have ‹[hd ys, hd (tl ys)] @ tl (tl ys) = ys›
      if ‹ys ≠ []› ‹tl ys ≠ []›
       using that by (auto simp: tl_append split: list.splits)
    then have ‹get_next (ns ! hd (ys @ xs)) = option_hd (remove1 (hd (ys @ xs)) (ys @ xs))›
      if ‹ys @ xs ≠ []›
      using vmtf_ns_last_next[of ‹?xs @ butlast ?ys› ‹last ?ys›] that
      using vmtf_ns_last_next[of ‹butlast ?xs› ‹last ?xs›]  vmtf dist
        distinct_remove1_last_butlast[of ‹?ys @ ?xs›]
      by (cases ys; cases ‹tl ys›)
       (auto simp: tl_append vmtf_ns_last_prev remove1_append hd_append remove1_Nil_iff
          split: list.splits if_splits elim: vmtf_nsE)
    moreover have ‹hd ys ∉ set xs› if ‹ys ≠ []›
      using vmtf_ns_distinct[OF vmtf] that by (cases ys) auto
    ultimately have ‹fst_As' = option_hd (remove1 L (ys @ xs))›
      using dequeue dist atm_L_A fst_As vmtf_ns_distinct[OF vmtf] vmtf
      unfolding vmtf_dequeue_def
      apply (cases ys)
      subgoal by (cases xs) (auto simp: remove1_append option_hd_def remove1_Nil_iff split: if_splits)
      subgoal by (auto simp: remove1_append option_hd_def remove1_Nil_iff)
      done
  }
  moreover have ‹lst_As' = option_last (remove1 L (ys @ xs))›
    apply (cases ‹ys @ xs› rule: rev_cases)
    using lst_As vmtf_ns_distinct[OF vmtf] vmtf_ns_last_prev vmtf
    by (auto simp: lst_As' remove1_append simp del: distinct_append) auto
  moreover have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (insert L (set (remove1 L xs)), set (remove1 L ys))›
    using abs_inv L dist
    unfolding vmtf_ℒ⇩a⇩l⇩l_def by (auto dest: in_set_remove1D)
  moreover have ‹vmtf_ns_notin (remove1 L ?ys @ remove1 L ?xs) m' ns'›
    unfolding xs_ys ns'
    apply (rule vmtf_ns_notin_dequeue)
    subgoal using vmtf unfolding m'm .
    subgoal using notin unfolding m'm .
    subgoal using atm_L_A .
    done
  moreover have ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns'›
    using atm_A unfolding ns' by auto
  moreover have ‹L ∉ set (remove1 L ys @ remove1 L xs)›
    using dist by auto
  moreover have ‹∀L∈set (remove1 L (ys @ xs)). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using L_ys_xs by (auto dest: in_set_remove1D)
  ultimately show ?thesis
    using next_search_L_next
    apply -
    apply (rule exI[of _ ‹remove1 L xs›])
    apply (rule exI[of _ ‹remove1 L ys›])
    unfolding xs_ys
    by blast
qed

lemma vmtf_ns_get_prev_not_itself:
  ‹vmtf_ns xs m ns ⟹ L ∈ set xs ⟹ L < length ns ⟹ get_prev (ns ! L) ≠ Some L›
  apply (induction rule: vmtf_ns.induct)
  subgoal by auto
  subgoal by (auto simp: vmtf_ns_single_iff)
  subgoal by auto
  done

lemma vmtf_ns_get_next_not_itself:
  ‹vmtf_ns xs m ns ⟹ L ∈ set xs ⟹ L < length ns ⟹ get_next (ns ! L) ≠ Some L›
  apply (induction rule: vmtf_ns.induct)
  subgoal by auto
  subgoal by (auto simp: vmtf_ns_single_iff)
  subgoal by auto
  done

lemma abs_vmtf_ns_bump_vmtf_en_dequeue:
  fixes M
  assumes
    vmtf: ‹(ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M› and
    L: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and
    nempty: ‹isasat_input_nempty 𝒜›
  shows ‹vmtf_en_dequeue M L (ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M›
  unfolding vmtf_def
proof clarify
  fix xxs yys zzs ns' m' fst_As' lst_As' next_search'
  assume dequeue: ‹vmtf_en_dequeue M L (ns, m, fst_As, lst_As, next_search) = (ns', m', fst_As', lst_As', next_search')›
  obtain xs ys where
    vmtf_ns: ‹vmtf_ns (ys @ xs) m ns› and
    notin: ‹vmtf_ns_notin (ys @ xs) m ns› and
    next_search: ‹next_search = option_hd xs› and
    abs_inv: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set xs, set ys)› and
    fst_As: ‹fst_As = hd (ys @ xs)› and
    lst_As: ‹lst_As = last (ys @ xs)› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    ys_xs_ℒ⇩a⇩l⇩l: ‹∀L∈set (ys @ xs). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using assms unfolding vmtf_def by auto
  have atm_L_A: ‹L < length ns›
    using atm_A L by blast
  text ‹d stands for dequeue›
  obtain nsd md fst_Asd lst_Asd next_searchd where
    de: ‹vmtf_dequeue L (ns, m, fst_As, lst_As, next_search) = (nsd, md, fst_Asd, lst_Asd, next_searchd) ›
    by (cases ‹vmtf_dequeue L (ns, m, fst_As, lst_As, next_search)›)
  obtain xs' ys' where
    vmtf_ns': ‹vmtf_ns (ys' @ xs') md nsd› and
    fst_Asd: ‹fst_Asd = option_hd (ys' @ xs')› and
    lst_Asd: ‹lst_Asd = option_last (ys' @ xs')› and
    next_searchd_hd: ‹next_searchd = option_hd xs'› and
    next_searchd_L_next:
      ‹next_searchd = (if next_search = Some L then get_next (ns!L) else next_search)› and
    abs_l: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (insert L (set xs'), set ys')›  and
    not_in: ‹vmtf_ns_notin (ys' @ xs') md nsd› and
    L_xs'_ys': ‹L ∉ set (ys' @ xs')› and
    L_xs'_ys'_ℒ⇩a⇩l⇩l: ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using abs_vmtf_ns_bump_vmtf_dequeue[OF vmtf L de[symmetric] nempty] by blast

  have [simp]: ‹length ns' = length ns›  ‹length nsd = length ns›
    using dequeue de unfolding vmtf_en_dequeue_def comp_def vmtf_dequeue_def
    by (auto simp add: vmtf_enqueue_def split: option.splits)
  have nsd: ‹nsd = ns_vmtf_dequeue L ns›
    using de unfolding vmtf_dequeue_def by auto
  have [simp]: ‹fst_As = L› if ‹ys' = []› and ‹xs' = []›
    proof -
      have 1: ‹set_mset 𝒜 = {L}›
        using abs_l unfolding that vmtf_ℒ⇩a⇩l⇩l_def by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
      show ?thesis
        using vmtf_ns_distinct[OF vmtf_ns] ys_xs_ℒ⇩a⇩l⇩l abs_inv
        unfolding atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n 1 fst_As vmtf_ℒ⇩a⇩l⇩l_def
        by (cases ‹ys @ xs›)  auto
    qed
    have fst_As': ‹fst_As' = L› and m': ‹m' = md + 1› and
      lst_As': ‹fst_Asd ≠ None ⟶ lst_As' = the (lst_Asd)›
      ‹fst_Asd = None ⟶ lst_As' = L›
      using dequeue unfolding vmtf_en_dequeue_def comp_def de
      by (auto simp add: vmtf_enqueue_def split: option.splits)
    have ‹lst_As = L› if ‹ys' = []› and ‹xs' = []›
    proof -
      have 1: ‹set_mset 𝒜 = {L}›
        using abs_l unfolding that vmtf_ℒ⇩a⇩l⇩l_def by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
      then have ‹set (ys @ xs) = {L} ›
        using vmtf_ns_distinct[OF vmtf_ns] ys_xs_ℒ⇩a⇩l⇩l abs_inv
        unfolding atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n 1 fst_As vmtf_ℒ⇩a⇩l⇩l_def
        by auto
      then have ‹ys @ xs = [L]›
        using vmtf_ns_distinct[OF vmtf_ns] ys_xs_ℒ⇩a⇩l⇩l abs_inv vmtf_ℒ⇩a⇩l⇩l_def
        unfolding atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n 1 fst_As
        by (cases ‹ys @ xs› rule: rev_cases) (auto simp del: set_append distinct_append
            simp: set_append[symmetric], auto)
      then show ?thesis
        using vmtf_ns_distinct[OF vmtf_ns] ys_xs_ℒ⇩a⇩l⇩l abs_inv vmtf_ℒ⇩a⇩l⇩l_def
        unfolding atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n 1 lst_As
        by (auto simp del: set_append distinct_append simp: set_append[symmetric])
    qed
    then have [simp]: ‹lst_As' = L›  if ‹ys' = []› and ‹xs' = []›
      using lst_As' fst_Asd unfolding that by auto
    have [simp]: ‹lst_As' = last (ys' @ xs')›  if ‹ys' ≠ [] ∨ xs' ≠ []›
      using lst_As' fst_Asd that lst_Asd by auto


    have ‹get_prev (nsd ! i) ≠ Some L›  (is ?prev) and
      ‹get_next (nsd ! i) ≠ Some L› (is ?next)
      if
        i_le_A: ‹i < length ns› and
        i_L: ‹i ≠ L› and
        i_ys': ‹i ∉ set ys'› and
        i_xs': ‹i ∉ set xs'›
      for i
    proof -
      have ‹i ∉ set xs› ‹i ∉ set ys› and L_xs_ys: ‹L ∈ set xs ∨ L ∈ set ys›
        using i_ys' i_xs' abs_l abs_inv i_L unfolding vmtf_ℒ⇩a⇩l⇩l_def
        by auto
      then have
        ‹get_next (ns ! i) = None›
        ‹get_prev (ns ! i) = None›
        using notin i_le_A unfolding nsd vmtf_ns_notin_def ns_vmtf_dequeue_def
        by (auto simp: Let_def split: option.splits)
      moreover have ‹get_prev (ns ! L) ≠ Some L› and ‹get_next (ns ! L) ≠ Some L›
        using vmtf_ns_get_prev_not_itself[OF vmtf_ns, of L] L_xs_ys atm_L_A
          vmtf_ns_get_next_not_itself[OF vmtf_ns, of L] by auto
      ultimately show ?next and ?prev
        using i_le_A L_xs_ys unfolding nsd ns_vmtf_dequeue_def vmtf_ns_notin_def
        by (auto simp: Let_def split: option.splits)
    qed
    then have vmtf_ns_notin': ‹vmtf_ns_notin (L # ys' @ xs') m' ns'›
      using not_in dequeue fst_Asd unfolding vmtf_en_dequeue_def comp_def de vmtf_ns_notin_def
        ns_vmtf_dequeue_def
      by (auto simp add: vmtf_enqueue_def hd_append split: option.splits if_splits)

  consider
     (defined) ‹defined_lit M (Pos L)› |
     (undef) ‹undefined_lit M (Pos L)›
    by blast
  then show ‹∃xs' ys'.
       vmtf_ns (ys' @ xs') m' ns' ∧
       fst_As' = hd (ys' @ xs') ∧
       lst_As' = last (ys' @ xs') ∧
       next_search' = option_hd xs' ∧
       vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys')) ∧
       vmtf_ns_notin (ys' @ xs') m' ns' ∧
       (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns') ∧
       (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
  proof cases
    case defined
    have L_in_M: ‹L ∈ atm_of ` lits_of_l M›
      using defined by (auto simp: defined_lit_map lits_of_def)
    have next_search': ‹fst_Asd ≠ None ⟶ next_search' = next_searchd›
      ‹fst_Asd = None ⟶ next_search' = None›
      using dequeue defined unfolding vmtf_en_dequeue_def comp_def de
      by (auto simp add: vmtf_enqueue_def split: option.splits)
    have next_searchd:
      ‹next_searchd = (if next_search = Some L then get_next (ns ! L) else next_search)›
      using de by (auto simp: vmtf_dequeue_def)
    have abs': ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M  ((set xs', insert L (set ys')))›
      using abs_l L_in_M L_xs'_ys' unfolding vmtf_ℒ⇩a⇩l⇩l_def
      by (auto 5 5 dest: in_diffD)

    have vmtf_ns: ‹vmtf_ns (L # (ys' @ xs')) m' ns'›
    proof (cases ‹ys' @ xs'›)
      case Nil
      then have ‹fst_Asd = None›
        using fst_Asd by auto
      then show ?thesis
        using atm_L_A dequeue Nil unfolding Nil vmtf_en_dequeue_def comp_def de nsd
        by (auto simp: vmtf_ns_single_iff vmtf_enqueue_def split: option.splits)
    next
      case (Cons z zs)
      let ?m = ‹(stamp (nsd!z))›
      let ?Ad = ‹nsd[L := VMTF_Node m' None (Some z)]›
      have L_z_zs: ‹L ∉ set (z # zs)›
        using L_xs'_ys' atm_L_A unfolding Cons
        by simp
      have vmtf_ns_z: ‹vmtf_ns (z # zs) md nsd›
        using vmtf_ns' unfolding Cons .

      have vmtf_ns_A: ‹vmtf_ns (z # zs) md ?Ad›
        apply (rule vmtf_ns_eq_iffI[of _ _ nsd])
        subgoal using L_z_zs atm_L_A by auto
        subgoal using vmtf_ns_le_length[OF vmtf_ns_z] by auto
        subgoal using vmtf_ns_z .
        done
      have [simp]: ‹fst_Asd = Some z›
        using fst_Asd unfolding Cons by simp
      show ?thesis
        unfolding Cons
        apply (rule vmtf_ns.Cons[of _ _ md ?Ad _ m'])
        subgoal using vmtf_ns_A .
        subgoal using atm_L_A by simp
        subgoal using atm_L_A by simp
        subgoal using L_z_zs by simp
        subgoal using L_z_zs by simp
        subgoal using m' by simp_all
        subgoal
          using atm_L_A dequeue L_z_zs unfolding Nil vmtf_en_dequeue_def comp_def de nsd
          apply (cases ‹ns_vmtf_dequeue z ns ! z›)
          by (auto simp: vmtf_ns_single_iff vmtf_enqueue_def split: option.splits)
        subgoal by linarith
        done
    qed
    have L_xs'_ys'_ℒ⇩a⇩l⇩l': ‹∀L'∈set ((L # ys') @ xs'). L' ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
      using L L_xs'_ys'_ℒ⇩a⇩l⇩l by auto
    have next_search'_xs': ‹next_search' = option_hd xs'›
      using next_searchd_L_next next_search' next_searchd_hd lst_As' fst_Asd
      by (auto split: if_splits)
    show ?thesis
      apply (rule exI[of _ ‹xs'›])
      apply (rule exI[of _ ‹L # ys'›])
      using fst_As' next_search' abs' atm_A vmtf_ns_notin' vmtf_ns ys_xs_ℒ⇩a⇩l⇩l L_xs'_ys'_ℒ⇩a⇩l⇩l'
        next_searchd next_search'_xs'
      by simp
  next
    case undef
    have next_search': ‹next_search' = Some L›
      using dequeue undef unfolding vmtf_en_dequeue_def comp_def de
      by (auto simp add: vmtf_enqueue_def split: option.splits)
    have next_searchd:
      ‹next_searchd = (if next_search = Some L then get_next (ns ! L) else next_search)›
      using de by (auto simp: vmtf_dequeue_def)
    have abs': ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M  ((insert L (set (ys' @ xs')), set []))›
      using abs_l L_xs'_ys' unfolding vmtf_ℒ⇩a⇩l⇩l_def
      by (auto 5 5 dest: in_diffD)

    have vmtf_ns: ‹vmtf_ns (L # (ys' @ xs')) m' ns'›
    proof (cases ‹ys' @ xs'›)
      case Nil
      then have ‹fst_Asd = None›
        using fst_Asd by auto
      then show ?thesis
        using atm_L_A dequeue Nil unfolding Nil vmtf_en_dequeue_def comp_def de nsd
        by (auto simp: vmtf_ns_single_iff vmtf_enqueue_def split: option.splits)
    next
      case (Cons z zs)
      let ?m = ‹(stamp (nsd!z))›
      let ?Ad = ‹nsd[L := VMTF_Node m' None (Some z)]›
      have L_z_zs: ‹L ∉ set (z # zs)›
        using L_xs'_ys' atm_L_A unfolding Cons
        by simp
      have vmtf_ns_z: ‹vmtf_ns (z # zs) md nsd›
        using vmtf_ns' unfolding Cons .

      have vmtf_ns_A: ‹vmtf_ns (z # zs) md ?Ad›
        apply (rule vmtf_ns_eq_iffI[of _ _ nsd])
        subgoal using L_z_zs atm_L_A by auto
        subgoal using vmtf_ns_le_length[OF vmtf_ns_z] by auto
        subgoal using vmtf_ns_z .
        done
      have [simp]: ‹fst_Asd = Some z›
        using fst_Asd unfolding Cons by simp
      show ?thesis
        unfolding Cons
        apply (rule vmtf_ns.Cons[of _ _ md ?Ad _ m'])
        subgoal using vmtf_ns_A .
        subgoal using atm_L_A by simp
        subgoal using atm_L_A by simp
        subgoal using L_z_zs by simp
        subgoal using L_z_zs by simp
        subgoal using m' by simp_all
        subgoal
          using atm_L_A dequeue L_z_zs unfolding Nil vmtf_en_dequeue_def comp_def de nsd
          apply (cases ‹ns_vmtf_dequeue z ns ! z›)
          by (auto simp: vmtf_ns_single_iff vmtf_enqueue_def split: option.splits)
        subgoal by linarith
        done
    qed
    have L_xs'_ys'_ℒ⇩a⇩l⇩l': ‹∀L'∈set ((L # ys') @ xs'). L' ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
      using L L_xs'_ys'_ℒ⇩a⇩l⇩l by auto
    show ?thesis
      apply (rule exI[of _ ‹(L # ys') @ xs'›])
      apply (rule exI[of _ ‹[]›])
      using fst_As' next_search' abs' atm_A vmtf_ns_notin' vmtf_ns ys_xs_ℒ⇩a⇩l⇩l L_xs'_ys'_ℒ⇩a⇩l⇩l'
        next_searchd
      by simp
  qed
qed


lemma abs_vmtf_ns_bump_vmtf_en_dequeue':
  fixes M
  assumes
    vmtf: ‹(vm) ∈ vmtf 𝒜 M› and
    L: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and
    nempty: ‹isasat_input_nempty 𝒜›
  shows ‹vmtf_en_dequeue M L vm ∈ vmtf 𝒜 M›
  using abs_vmtf_ns_bump_vmtf_en_dequeue assms by (cases vm) blast

definition (in -) vmtf_unset :: ‹nat ⇒ vmtf ⇒ vmtf› where
‹vmtf_unset = (λL (ns, m, fst_As, lst_As, next_search).
  (if next_search = None ∨ stamp (ns ! (the next_search)) < stamp (ns ! L)
  then ((ns, m, fst_As, lst_As, Some L))
  else ((ns, m, fst_As, lst_As, next_search))))›

lemma vmtf_atm_of_ys_iff:
  assumes
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'))› and
    L: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    shows ‹L ∈ set ys' ⟷ next_search = None ∨ stamp (ns ! (the next_search)) < stamp (ns ! L)›
proof -
  let ?xs' = ‹set xs'›
  let ?ys' = ‹set ys'›
  have L_xs_ys: ‹L ∈ ?xs' ∪ ?ys'›
    using abs_vmtf L unfolding vmtf_ℒ⇩a⇩l⇩l_def
    by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
  have dist: ‹distinct (xs' @ ys')›
    using vmtf_ns_distinct[OF vmtf_ns] by auto

  have sorted: ‹sorted (map (λa. stamp (ns ! a)) (rev xs' @ rev ys'))› and
    distinct: ‹distinct (map (λa. stamp (ns ! a)) (xs' @ ys'))›
    using vmtf_ns_stamp_sorted[OF vmtf_ns] vmtf_ns_stamp_distinct[OF vmtf_ns]
    by (auto simp: rev_map[symmetric])
  have next_search_xs: ‹?xs' = {} ⟷ next_search = None›
    using next_search by auto

  have ‹stamp (ns ! (the next_search)) < stamp (ns ! L) ⟹ L ∉ ?xs'›
    if ‹xs' ≠ []›
    using that sorted distinct L_xs_ys unfolding next_search
    by (cases xs') (auto simp: sorted_append)
  moreover have ‹stamp (ns ! (the next_search)) < stamp (ns ! L)› (is ‹?n < ?L›)
    if xs': ‹xs' ≠ []› and ‹L ∈ ?ys'›
  proof -
    have ‹?n ≤ ?L›
      using vmtf_ns_stamp_sorted[OF vmtf_ns] that last_in_set[OF xs']
      by (cases xs')
         (auto simp: rev_map[symmetric] next_search sorted_append sorted2)
    moreover have ‹?n ≠ ?L›
      using vmtf_ns_stamp_distinct[OF vmtf_ns] that last_in_set[OF xs']
      by (cases xs') (auto simp: rev_map[symmetric] next_search)
    ultimately show ?thesis
      by arith
  qed
  ultimately show ?thesis
    using L_xs_ys next_search_xs dist by auto
qed


lemma abs_vmtf_ns_unset_vmtf_unset:
  assumes vmtf:‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 M› and
  L_N: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
  shows ‹(vmtf_unset L ((ns, m, fst_As, lst_As, next_search))) ∈ vmtf 𝒜 M› (is ‹?S ∈ _›)
proof -
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'))› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    L_ys'_xs'_ℒ⇩a⇩l⇩l: ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  obtain ns' m' fst_As' next_search' lst_As' where
    S: ‹?S = ((ns', m', fst_As', lst_As', next_search'))›
    by (cases ?S) auto
  have L_ys'_iff: ‹L ∈ set ys' ⟷ (next_search = None ∨ stamp (ns ! the next_search) < stamp (ns ! L))›
    using vmtf_atm_of_ys_iff[OF vmtf_ns next_search abs_vmtf L_N] .
  have ‹L ∈ set (xs' @ ys')›
    using abs_vmtf L_N unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
  then have L_ys'_xs': ‹L ∈ set ys' ⟷ L ∉ set xs'›
    using vmtf_ns_distinct[OF vmtf_ns] by auto
  have ‹∃xs' ys'.
       vmtf_ns (ys' @ xs') m' ns' ∧
       fst_As' = hd (ys' @ xs') ∧
       lst_As' = last (ys' @ xs') ∧
       next_search' = option_hd xs' ∧
       vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys')) ∧
       vmtf_ns_notin (ys' @ xs') m' ns' ∧ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns') ∧
       (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
  proof (cases ‹L ∈ set xs'›)
    case True
    then have C: ‹¬(next_search = None ∨ stamp (ns ! the next_search) < stamp (ns ! L))›
      by (subst L_ys'_iff[symmetric]) (use L_ys'_xs' in auto)
    show ?thesis
      using S True unfolding vmtf_unset_def L_ys'_xs'[symmetric]
      apply -
      apply (simp add: C)
      using vmtf_ns fst_As next_search abs_vmtf notin atm_A L_ys'_xs'_ℒ⇩a⇩l⇩l lst_As
      by auto
  next
    case False
    then have C: ‹next_search = None ∨ stamp (ns ! the next_search) < stamp (ns ! L)›
      by (subst L_ys'_iff[symmetric]) (use L_ys'_xs' in auto)
    have L_ys: ‹L ∈ set ys'›
      by (use False L_ys'_xs' in auto)
    define y_ys where ‹y_ys ≡ takeWhile ((≠) L) ys'›
    define x_ys where ‹x_ys ≡ drop (length y_ys) ys'›
    let ?ys' = ‹y_ys›
    let ?xs' = ‹x_ys @ xs'›
    have x_ys_take_ys': ‹y_ys = take (length y_ys) ys'›
        unfolding y_ys_def
        by (subst take_length_takeWhile_eq_takeWhile[of ‹(≠) L› ‹ys'›, symmetric]) standard
    have ys'_y_x: ‹ys' = y_ys @ x_ys›
      by (subst x_ys_take_ys') (auto simp: x_ys_def)
    have y_ys_le_ys': ‹length y_ys < length ys'›
      using L_ys by (metis (full_types) append_eq_conv_conj append_self_conv le_antisym
        length_takeWhile_le not_less takeWhile_eq_all_conv x_ys_take_ys' y_ys_def)
    from nth_length_takeWhile[OF this[unfolded y_ys_def]] have [simp]: ‹x_ys ≠ []› ‹hd x_ys = L›
      using y_ys_le_ys' unfolding x_ys_def y_ys_def
      by (auto simp: x_ys_def y_ys_def hd_drop_conv_nth)
    have [simp]: ‹ns' = ns› ‹m' = m› ‹fst_As' = fst_As› ‹next_search' = Some L›
      ‹lst_As' = lst_As›
      using S unfolding vmtf_unset_def by (auto simp: C)

    have ‹vmtf_ns (?ys' @ ?xs') m ns›
      using vmtf_ns unfolding ys'_y_x by simp
    moreover have ‹fst_As' = hd (?ys' @ ?xs')›
      using fst_As unfolding ys'_y_x by simp
    moreover have ‹lst_As' = last (?ys' @ ?xs')›
      using lst_As unfolding ys'_y_x by simp
    moreover have ‹next_search' = option_hd ?xs'›
      by auto
    moreover
      have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set ?xs', set ?ys'))›
        using abs_vmtf vmtf_ns_distinct[OF vmtf_ns] unfolding vmtf_ℒ⇩a⇩l⇩l_def ys'_y_x
        by auto
    moreover have ‹vmtf_ns_notin (?ys' @ ?xs') m ns›
      using notin unfolding ys'_y_x by simp
    moreover have ‹∀L∈set (?ys' @ ?xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
      using L_ys'_xs'_ℒ⇩a⇩l⇩l unfolding ys'_y_x by auto
    ultimately show ?thesis
      using S False atm_A unfolding vmtf_unset_def L_ys'_xs'[symmetric]
      by (fastforce simp add: C)
  qed
  then show ?thesis
    unfolding vmtf_def S
    by fast
qed


definition (in -) vmtf_dequeue_pre where
  ‹vmtf_dequeue_pre = (λ(L,ns). L < length ns ∧
          (get_next (ns!L) ≠ None ⟶ the (get_next (ns!L)) < length ns) ∧
          (get_prev (ns!L) ≠ None ⟶ the (get_prev (ns!L)) < length ns))›

lemma (in -) vmtf_dequeue_pre_alt_def:
  ‹vmtf_dequeue_pre = (λ(L, ns). L < length ns ∧
          (∀a. Some a = get_next (ns!L) ⟶ a < length ns) ∧
          (∀a. Some a = get_prev (ns!L) ⟶ a < length ns))›
  apply (intro ext, rename_tac x)
  subgoal for x
    by (cases ‹get_next ((snd x)!(fst x))›; cases ‹get_prev ((snd x)!(fst x))›)
      (auto simp: vmtf_dequeue_pre_def intro!: ext)
  done

definition vmtf_en_dequeue_pre :: ‹nat multiset ⇒ ((nat, nat) ann_lits × nat) × vmtf ⇒ bool› where
  ‹vmtf_en_dequeue_pre 𝒜 = (λ((M, L),(ns,m,fst_As, lst_As, next_search)).
       L < length ns ∧ vmtf_dequeue_pre (L, ns) ∧
       fst_As < length ns ∧ (get_next (ns ! fst_As) ≠ None ⟶ get_prev (ns ! lst_As) ≠ None) ∧
       (get_next (ns ! fst_As) = None ⟶ fst_As = lst_As) ∧
       m+1 ≤ unat64_max ∧
       Pos L ∈# ℒ⇩a⇩l⇩l 𝒜)›

lemma (in -) id_reorder_list:
   ‹(RETURN o id, reorder_list vm) ∈ ⟨nat_rel⟩list_rel →⇩f ⟨⟨nat_rel⟩list_rel⟩nres_rel›
  unfolding reorder_list_def by (intro frefI nres_relI) auto

lemma vmtf_vmtf_en_dequeue_pre_to_remove:
  assumes vmtf: ‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 M› and
    m_le:  ‹m + 1 ≤ unat64_max› and
    nempty: ‹isasat_input_nempty 𝒜› and
    A:  ‹A ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
  shows ‹vmtf_en_dequeue_pre 𝒜 ((M, A), (ns, m, fst_As, lst_As, next_search))›
proof -
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'))› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    L_ys'_xs'_ℒ⇩a⇩l⇩l: ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  have [dest]: False if ‹ys' = []› and ‹xs' = []›
  proof -
    have 1: ‹set_mset 𝒜 = {}›
      using abs_vmtf unfolding that vmtf_ℒ⇩a⇩l⇩l_def by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
    then show ?thesis
      using nempty by auto
  qed

  have ‹A ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using abs_vmtf A unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
  then have remove_i_le_A: ‹A < length ns› and
    i_L: ‹Pos A ∈# ℒ⇩a⇩l⇩l 𝒜›
    using atm_A by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n atms_of_def)
  moreover have ‹fst_As < length ns›
    using fst_As atm_A L_ys'_xs'_ℒ⇩a⇩l⇩l by (cases ys'; cases xs') auto
  moreover have ‹get_prev (ns ! lst_As) ≠ None› if ‹get_next (ns ! fst_As) ≠ None›
    using that vmtf_ns_hd_next[of ‹hd (ys' @ xs')› ‹hd (tl (ys' @ xs'))› ‹tl (tl (ys' @ xs'))›]
      vmtf_ns vmtf_ns_last_prev[of ‹butlast (ys' @ xs')› ‹last (ys' @ xs')›]
      vmtf_ns_last_next[of ‹butlast (ys' @ xs')› ‹last (ys' @ xs')›]
    by (cases ‹ys' @ xs'›; cases ‹tl (ys' @ xs')›)
       (auto simp: fst_As lst_As)
  moreover have ‹vmtf_dequeue_pre (A, ns)›
  proof -
    have ‹A < length ns›
      using A abs_vmtf atm_A unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
    moreover have ‹y < length ns› if get_next: ‹get_next (ns ! (A)) = Some y› for y
    proof (cases ‹A ∈ set (ys' @ xs')›)
      case False
      then show ?thesis
        using notin get_next remove_i_le_A by (auto simp: vmtf_ns_notin_def)
    next
      case True
      then obtain zs zs' where zs: ‹ys' @ xs' = zs' @ [A] @ zs›
        using split_list by fastforce
      moreover have ‹set (ys' @ xs') = atms_of (ℒ⇩a⇩l⇩l 𝒜)›
        using abs_vmtf unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
      ultimately show ?thesis
        using vmtf_ns_last_mid_get_next_option_hd[of zs' A zs m ns] vmtf_ns atm_A get_next
          L_ys'_xs'_ℒ⇩a⇩l⇩l unfolding zs by force
    qed
    moreover have ‹y < length ns› if get_prev: ‹get_prev (ns ! (A)) = Some y› for y
    proof (cases ‹A ∈ set (ys' @ xs')›)
      case False
      then show ?thesis
        using notin get_prev remove_i_le_A by (auto simp: vmtf_ns_notin_def)
    next
      case True
      then obtain zs zs' where zs: ‹ys' @ xs' = zs' @ [A] @ zs›
        using split_list by fastforce
      moreover have ‹set (ys' @ xs') = atms_of (ℒ⇩a⇩l⇩l 𝒜)›
        using abs_vmtf unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
      ultimately show ?thesis
        using vmtf_ns_last_mid_get_prev_option_last[of zs' A zs m ns] vmtf_ns atm_A get_prev
          L_ys'_xs'_ℒ⇩a⇩l⇩l unfolding zs by force
    qed
    ultimately show ?thesis
      unfolding vmtf_dequeue_pre_def by auto
  qed
  moreover have ‹get_next (ns ! fst_As) = None ⟶ fst_As = lst_As›
    using vmtf_ns_hd_next[of ‹hd (ys' @ xs')› ‹hd (tl (ys' @ xs'))› ‹tl (tl (ys' @ xs'))›]
      vmtf_ns vmtf_ns_last_prev[of ‹butlast (ys' @ xs')› ‹last (ys' @ xs')›]
      vmtf_ns_last_next[of ‹butlast (ys' @ xs')› ‹last (ys' @ xs')›]
    by (cases ‹ys' @ xs'›; cases ‹tl (ys' @ xs')›)
       (auto simp: fst_As lst_As)
  ultimately show ?thesis
    using m_le unfolding vmtf_en_dequeue_pre_def by auto
qed

lemma vmtf_vmtf_en_dequeue_pre_to_remove':
  assumes vmtf: ‹(vm) ∈ vmtf 𝒜 M› and
    i:  ‹A ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and ‹fst (snd vm) + 1 ≤ unat64_max› and
    A: ‹isasat_input_nempty 𝒜›
  shows ‹vmtf_en_dequeue_pre 𝒜 ((M, A), vm)›
  using vmtf_vmtf_en_dequeue_pre_to_remove assms
  by (cases vm) auto

lemma wf_vmtf_get_next:
  assumes vmtf: ‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 M›
  shows ‹wf {(get_next (ns ! the a), a) |a. a ≠ None ∧ the a ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)}› (is ‹wf ?R›)
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain f where
    f: ‹(f (Suc i), f i) ∈ ?R› for i
    unfolding wf_iff_no_infinite_down_chain by blast

  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'))› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns›
    using vmtf unfolding vmtf_def by fast
  let ?f0 = ‹the (f 0)›
  have f_None: ‹f i ≠ None› for i
    using f[of i] by fast
  have f_Suc : ‹f (Suc n) = get_next (ns ! the (f n))› for n
    using f[of n] by auto
  have f0_length: ‹?f0 < length ns›
    using f[of 0] atm_A
    by auto
  have ‹?f0 ∈ set (ys' @ xs')›
    apply (rule ccontr)
    using notin f_Suc[of 0] f0_length unfolding vmtf_ns_notin_def
    by (auto simp: f_None)
  then obtain i0 where
    i0: ‹(ys' @ xs') ! i0 = ?f0› ‹i0 < length (ys' @ xs')›
    by (meson in_set_conv_nth)
  define zs where ‹zs = ys' @ xs'›
  have H: ‹ys' @ xs' = take m (ys' @ xs') @ [(ys' @ xs') ! m, (ys' @ xs') ! (m+1)] @
     drop (m+2) (ys' @ xs')›
    if ‹m+1 < length (ys' @ xs')›
    for m
    using that
    unfolding zs_def[symmetric]
    apply -
    apply (subst id_take_nth_drop[of m])
    by (auto simp: Cons_nth_drop_Suc simp del: append_take_drop_id)

  have ‹the (f n) = (ys' @ xs') ! (i0 + n) ∧ i0 + n < length (ys' @ xs')› for n
  proof (induction n)
    case 0
    then show ?case using i0 by simp
  next
    case (Suc n')
    have i0_le:  ‹i0 + n' + 1 < length (ys' @ xs')›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then have ‹i0 + n' + 1 = length (ys' @ xs')›
        using Suc by auto
      then have ‹ys' @ xs' = butlast (ys' @ xs') @ [the (f n')]›
        using Suc by (metis add_diff_cancel_right' append_butlast_last_id length_0_conv
            length_butlast less_one not_add_less2 nth_append_length)
      then show False
        using vmtf_ns_last_next[of ‹butlast (ys' @ xs')› ‹the (f n')› m ns] vmtf_ns
         f_Suc[of n'] by (auto simp: f_None)
    qed
    have get_next: ‹get_next (ns ! ((ys' @ xs') ! (i0 + n'))) = Some ((ys' @ xs') ! (i0 + n' + 1))›
      apply(rule vmtf_ns_last_mid_get_next[of ‹take (i0 + n') (ys' @ xs')›
        ‹(ys' @ xs') ! (i0 + n')›
        ‹(ys' @ xs') ! ((i0 + n') + 1)›
        ‹drop ((i0 + n') + 2) (ys' @ xs')›
        m ns])
      apply (subst H[symmetric])
      subgoal using i0_le .
      subgoal using vmtf_ns by simp
      done
    then show ?case
      using f_Suc[of n'] Suc i0_le by auto
  qed
  then show False
    by blast
qed

lemma vmtf_next_search_take_next:
  assumes
    vmtf: ‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 M› and
    n: ‹next_search ≠ None› and
    def_n: ‹defined_lit M (Pos (the next_search))›
  shows ‹(ns, m, fst_As, lst_As, get_next (ns!the next_search)) ∈ vmtf 𝒜 M›
  unfolding vmtf_def
proof clarify
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set xs', set ys')› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    ys'_xs'_ℒ⇩a⇩l⇩l: ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  let ?xs' = ‹tl xs'›
  let ?ys' = ‹ys' @ [hd xs']›
  have [simp]: ‹xs' ≠ []›
    using next_search n by auto
  have ‹vmtf_ns (?ys' @ ?xs') m ns›
    using vmtf_ns by (cases xs') auto
  moreover have ‹fst_As = hd (?ys' @ ?xs')›
    using fst_As by auto
  moreover have ‹lst_As = last (?ys' @ ?xs')›
    using lst_As by auto
  moreover have ‹get_next (ns ! the next_search) = option_hd ?xs'›
    using next_search n vmtf_ns
    by (cases xs') (auto dest: vmtf_ns_last_mid_get_next_option_hd)
  moreover {
    have [dest]: ‹defined_lit M (Pos a) ⟹ a ∈ atm_of ` lits_of_l M› for a
      by (auto simp: defined_lit_map lits_of_def)
    have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set ?xs', set ?ys')›
      using abs_vmtf def_n next_search n vmtf_ns_distinct[OF vmtf_ns]
      unfolding vmtf_ℒ⇩a⇩l⇩l_def
      by (cases xs') auto }
  moreover have ‹vmtf_ns_notin (?ys' @ ?xs') m ns›
    using notin by auto
  moreover have ‹∀L∈set (?ys' @ ?xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using ys'_xs'_ℒ⇩a⇩l⇩l by auto
  ultimately show ‹∃xs' ys'. vmtf_ns (ys' @ xs') m ns ∧
          fst_As = hd (ys' @ xs') ∧
          lst_As = last (ys' @ xs') ∧
          get_next (ns ! the next_search) = option_hd xs' ∧
          vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys')) ∧
          vmtf_ns_notin (ys' @ xs') m ns ∧
          (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns) ∧
          (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
    using atm_A by blast
qed


definition vmtf_find_next_undef :: ‹nat multiset ⇒ vmtf ⇒ (nat, nat) ann_lits ⇒ (nat option) nres› where
‹vmtf_find_next_undef 𝒜 = (λ(ns, m, fst_As, lst_As, next_search) M. do {
    WHILE⇩T⇗λnext_search. (ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M ∧
         (next_search ≠ None ⟶ Pos (the next_search) ∈# ℒ⇩a⇩l⇩l 𝒜)⇖
      (λnext_search. next_search ≠ None ∧ defined_lit M (Pos (the next_search)))
      (λnext_search. do {
         ASSERT(next_search ≠ None);
         let n = the next_search;
         ASSERT(Pos n ∈# ℒ⇩a⇩l⇩l  𝒜);
         ASSERT (n < length ns);
         RETURN (get_next (ns!n))
        }
      )
      next_search
  })›

lemma vmtf_find_next_undef_ref:
  assumes
    vmtf: ‹(ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M›
  shows ‹vmtf_find_next_undef 𝒜 (ns, m, fst_As, lst_As, next_search) M
     ≤ ⇓ Id (SPEC (λL. (ns, m, fst_As, lst_As, L) ∈ vmtf 𝒜 M ∧
        (L = None ⟶ (∀L∈#ℒ⇩a⇩l⇩l 𝒜. defined_lit M L)) ∧
        (L ≠ None ⟶ Pos (the L) ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ undefined_lit M (Pos (the L)))))›
proof -
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set xs', set ys')› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns›
    using vmtf unfolding vmtf_def by fast
  have no_next_search_all_defined:
    ‹(ns', m', fst_As', lst_As', None) ∈ vmtf 𝒜 M ⟹ x ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ defined_lit M x›
    for x ns' m' fst_As' lst_As' remove
    by (auto simp: vmtf_def vmtf_ℒ⇩a⇩l⇩l_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
        defined_lit_map lits_of_def)
  have next_search_ℒ⇩a⇩l⇩l:
    ‹(ns', m', fst_As', lst_As', Some y) ∈ vmtf 𝒜 M ⟹ y ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    for ns' m' fst_As' remove y lst_As'
    by (auto simp: vmtf_def vmtf_ℒ⇩a⇩l⇩l_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
        defined_lit_map lits_of_def)
  have next_search_le_A':
    ‹(ns', m', fst_As', lst_As', Some y) ∈ vmtf 𝒜 M ⟹ y < length ns'›
    for ns' m' fst_As' remove y lst_As'
    by (auto simp: vmtf_def vmtf_ℒ⇩a⇩l⇩l_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
        defined_lit_map lits_of_def)
  show ?thesis
    unfolding vmtf_find_next_undef_def
    apply (refine_vcg
       WHILEIT_rule[where R=‹{(get_next (ns ! the a), a) |a. a ≠ None ∧ the a ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)}›])
    subgoal using vmtf by (rule wf_vmtf_get_next)
    subgoal using next_search vmtf by auto
    subgoal using vmtf by (auto dest!: next_search_ℒ⇩a⇩l⇩l simp: image_image in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
    subgoal using vmtf by auto
    subgoal using vmtf by auto
    subgoal using vmtf by (auto dest: next_search_le_A')
    subgoal by (auto simp: image_image in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
        (metis next_search_ℒ⇩a⇩l⇩l option.distinct(1) option.sel vmtf_next_search_take_next)
    subgoal by (auto simp: image_image in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
        (metis next_search_ℒ⇩a⇩l⇩l option.distinct(1) option.sel vmtf_next_search_take_next)
    subgoal by (auto dest: no_next_search_all_defined next_search_ℒ⇩a⇩l⇩l)
    subgoal by (auto dest: next_search_le_A')
    subgoal for x1 ns' x2 m' x2a fst_As' next_search' x2c s
      by (auto dest: no_next_search_all_defined next_search_ℒ⇩a⇩l⇩l)
    subgoal by (auto dest: vmtf_next_search_take_next)
    subgoal by (auto simp: image_image in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
    done
qed

(*
TODO remove
definition vmtf_mark_to_rescore
  :: ‹nat ⇒ vmtf_remove_int ⇒ vmtf_remove_int›
where
  ‹vmtf_mark_to_rescore L = (λ((ns, m, fst_As, next_search)).
     ((ns, m, fst_As, next_search), insert L to_remove))›

lemma vmtf_mark_to_rescore:
  assumes
    L: ‹L ∈atms_of (ℒ⇩a⇩l⇩l 𝒜)› and
    vmtf: ‹((ns, m, fst_As, lst_As, next_search), to_remove) ∈ vmtf 𝒜 M›
  shows ‹vmtf_mark_to_rescore L ((ns, m, fst_As, lst_As, next_search), to_remove) ∈ vmtf 𝒜 M›
proof -
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), to_remove)› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  moreover have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), insert L to_remove)›
    using abs_vmtf L unfolding vmtf_ℒ⇩a⇩l⇩l_def
    by auto
  ultimately show ?thesis
    unfolding vmtf_def vmtf_mark_to_rescore_def by fast
qed
*)

lemma vmtf_unset_vmtf_tl:
  fixes M
  defines [simp]: ‹L ≡ atm_of (lit_of (hd M))›
  assumes vmtf:‹(ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M› and
    L_N: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and [simp]: ‹M ≠ []›
  shows ‹vmtf_unset L (ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 (tl M)›
     (is ‹?S ∈ _›)
proof -
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set xs', set ys')› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l  𝒜). L < length ns› and
    ys'_xs'_ℒ⇩a⇩l⇩l: ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  obtain ns' m' fst_As' next_search' lst_As' where
    S: ‹?S = (ns', m', fst_As', lst_As', next_search')›
    by (cases ?S) auto
  have L_ys'_iff: ‹L ∈ set ys' ⟷ (next_search = None ∨ stamp (ns ! the next_search) < stamp (ns ! L))›
    using vmtf_atm_of_ys_iff[OF vmtf_ns next_search abs_vmtf L_N] .
  have dist: ‹distinct (ys' @ xs')›
    using vmtf_ns_distinct[OF vmtf_ns] .
  have ‹L ∈ set (xs' @ ys')›
    using abs_vmtf L_N unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
  then have L_ys'_xs': ‹L ∈ set ys' ⟷ L ∉ set xs'›
    using dist by auto
  have ‹∃xs' ys'.
       vmtf_ns (ys' @ xs') m' ns' ∧
       fst_As' = hd (ys' @ xs') ∧
       lst_As' = last (ys' @ xs') ∧
       next_search' = option_hd xs' ∧
       vmtf_ℒ⇩a⇩l⇩l 𝒜 (tl M) (set xs', set ys') ∧
       vmtf_ns_notin (ys' @ xs') m' ns' ∧ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns') ∧
       (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
  proof (cases ‹L ∈ set xs'›)
    case True
    then have C[unfolded L_def]: ‹¬(next_search = None ∨ stamp (ns ! the next_search) < stamp (ns ! L))›
      by (subst L_ys'_iff[symmetric]) (use L_ys'_xs' in auto)
    have abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 (tl M) (set xs', set ys')›
      using S abs_vmtf dist L_ys'_xs' True unfolding vmtf_ℒ⇩a⇩l⇩l_def vmtf_unset_def
      by (cases M) (auto simp: C)
    show ?thesis
      using S True unfolding vmtf_unset_def L_ys'_xs'[symmetric]
      apply -
      apply (simp add: C)
      using vmtf_ns fst_As next_search abs_vmtf notin atm_A ys'_xs'_ℒ⇩a⇩l⇩l lst_As
      by auto
  next
    case False
    then have C[unfolded L_def]: ‹next_search = None ∨ stamp (ns ! the next_search) < stamp (ns ! L)›
      by (subst L_ys'_iff[symmetric]) (use L_ys'_xs' in auto)
    have L_ys: ‹L ∈ set ys'›
      by (use False L_ys'_xs' in auto)
    define y_ys where ‹y_ys ≡ takeWhile ((≠) L) ys'›
    define x_ys where ‹x_ys ≡ drop (length y_ys) ys'›
    let ?ys' = ‹y_ys›
    let ?xs' = ‹x_ys @ xs'›
    have x_ys_take_ys': ‹y_ys = take (length y_ys) ys'›
        unfolding y_ys_def
        by (subst take_length_takeWhile_eq_takeWhile[of ‹(≠) L› ‹ys'›, symmetric]) standard
    have ys'_y_x: ‹ys' = y_ys @ x_ys›
      by (subst x_ys_take_ys') (auto simp: x_ys_def)
    have y_ys_le_ys': ‹length y_ys < length ys'›
      using L_ys by (metis (full_types) append_eq_conv_conj append_self_conv le_antisym
        length_takeWhile_le not_less takeWhile_eq_all_conv x_ys_take_ys' y_ys_def)
    from nth_length_takeWhile[OF this[unfolded y_ys_def]] have [simp]: ‹x_ys ≠ []› ‹hd x_ys = L›
      using y_ys_le_ys' unfolding x_ys_def y_ys_def
      by (auto simp: x_ys_def y_ys_def hd_drop_conv_nth)
    have [simp]: ‹ns' = ns› ‹m' = m› ‹fst_As' = fst_As› ‹next_search' = Some (atm_of (lit_of (hd M)))›
      ‹lst_As' = lst_As›
      using S unfolding vmtf_unset_def by (auto simp: C)
    have L_y_ys: ‹L ∉ set y_ys›
       unfolding y_ys_def by (metis (full_types) takeWhile_eq_all_conv takeWhile_idem)
    have ‹vmtf_ns (?ys' @ ?xs') m ns›
      using vmtf_ns unfolding ys'_y_x by simp
    moreover have ‹fst_As' = hd (?ys' @ ?xs')›
      using fst_As unfolding ys'_y_x by simp
    moreover have ‹lst_As' = last (?ys' @ ?xs')›
      using lst_As unfolding ys'_y_x by simp
    moreover have ‹next_search' = option_hd ?xs'›
      by auto
    moreover {
      have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set ?xs', set ?ys')›
        using abs_vmtf dist unfolding vmtf_ℒ⇩a⇩l⇩l_def ys'_y_x
        by auto
      then have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 (tl M) (set ?xs', set ?ys')›
        using dist L_y_ys unfolding vmtf_ℒ⇩a⇩l⇩l_def ys'_y_x ys'_y_x
        by (cases M) auto
      }
    moreover have ‹vmtf_ns_notin (?ys' @ ?xs') m ns›
      using notin unfolding ys'_y_x by simp
    moreover have ‹∀L∈set (?ys' @ ?xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
      using ys'_xs'_ℒ⇩a⇩l⇩l unfolding ys'_y_x by simp
    ultimately show ?thesis
      using S False atm_A unfolding vmtf_unset_def L_ys'_xs'[symmetric]
      by (fastforce simp add: C)
  qed
  then show ?thesis
    unfolding vmtf_def S
    by fast
qed

(*
TODO remove
definition vmtf_mark_to_rescore_and_unset :: ‹nat ⇒ vmtf ⇒ vmtf› where
  ‹vmtf_mark_to_rescore_and_unset L M = vmtf_mark_to_rescore L (vmtf_unset L M)›


lemma vmtf_append_remove_iff:
  ‹((ns, m, fst_As, lst_As, next_search), insert L b) ∈ vmtf 𝒜 M ⟷
     L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜) ∧ ((ns, m, fst_As, lst_As, next_search), b) ∈ vmtf 𝒜 M›
  (is ‹?A ⟷ ?L ∧ ?B›)
proof
  assume vmtf: ?A
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), insert L b)› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  moreover have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), b)› and L: ?L
    using abs_vmtf unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
  ultimately have ‹vmtf_ns (ys' @ xs') m ns ∧
       fst_As = hd (ys' @ xs') ∧
       next_search = option_hd xs' ∧
       lst_As = last (ys' @ xs') ∧
       vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), b) ∧
       vmtf_ns_notin (ys' @ xs') m ns ∧ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns) ∧
       (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
      by fast
  then show ‹?L ∧ ?B›
    using L unfolding vmtf_def by fast
next
  assume vmtf: ‹?L ∧ ?B›
  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), b)› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def by fast
  moreover have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), insert L b)›
    using vmtf abs_vmtf unfolding vmtf_ℒ⇩a⇩l⇩l_def by auto
  ultimately have ‹vmtf_ns (ys' @ xs') m ns ∧
       fst_As = hd (ys' @ xs') ∧
       next_search = option_hd xs' ∧
       lst_As = last (ys' @ xs') ∧
       vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), insert L b) ∧
       vmtf_ns_notin (ys' @ xs') m ns ∧ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns) ∧
       (∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜))›
      by fast
  then show ?A
    unfolding vmtf_def by fast
qed

lemma vmtf_append_remove_iff':
  ‹(vm, insert L b) ∈ vmtf 𝒜 M ⟷
     L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜) ∧ (vm, b) ∈ vmtf 𝒜 M›
  by (cases vm) (auto simp: vmtf_append_remove_iff)
*)

(*
lemma vmtf_mark_to_rescore_unset:
  fixes M
  defines [simp]: ‹L ≡ atm_of (lit_of (hd M))›
  assumes vmtf:‹((ns, m, fst_As, lst_As, next_search), remove) ∈ vmtf 𝒜 M› and
    L_N: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and [simp]: ‹M ≠ []›
  shows ‹(vmtf_mark_to_rescore_and_unset L ((ns, m, fst_As, lst_As, next_search), remove)) ∈ vmtf 𝒜 (tl M)›
     (is ‹?S ∈ _›)
  using vmtf_unset_vmtf_tl[OF assms(2-)[unfolded assms(1)]] L_N
  unfolding vmtf_mark_to_rescore_and_unset_def vmtf_mark_to_rescore_def
  by (cases ‹vmtf_unset (atm_of (lit_of (hd M))) ((ns, m, fst_As, lst_As, next_search), remove)›)
     (auto simp: vmtf_append_remove_iff)

lemma vmtf_insert_sort_nth_code_preD:
  assumes vmtf: ‹vm ∈ vmtf 𝒜 M›
  shows ‹∀x∈snd vm. x < length (fst (fst vm))›
proof -
  obtain ns m fst_As lst_As next_search remove where
    vm: ‹vm = ((ns, m, fst_As, lst_As, next_search), remove)›
    by (cases vm) auto

  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), remove)› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def vm by fast
  show ?thesis
    using atm_A abs_vmtf unfolding vmtf_ℒ⇩a⇩l⇩l_def
    by (auto simp: vm)
qed
*)


lemma vmtf_ns_Cons:
  assumes
    vmtf: ‹vmtf_ns (b # l) m xs› and
    a_xs: ‹a < length xs› and
    ab: ‹a ≠ b› and
    a_l: ‹a ∉ set l› and
    nm: ‹n > m› and
    xs': ‹xs' = xs[a := VMTF_Node n None (Some b),
         b := VMTF_Node (stamp (xs!b)) (Some a) (get_next (xs!b))]› and
    nn': ‹n' ≥ n›
  shows ‹vmtf_ns (a # b # l) n' xs'›
proof -
  have ‹vmtf_ns (b # l) m (xs[a := VMTF_Node n None (Some b)])›
    apply (rule vmtf_ns_eq_iffI[OF _ _ vmtf])
    subgoal using ab a_l a_xs by auto
    subgoal using a_xs vmtf_ns_le_length[OF vmtf] by auto
    done
  then show ?thesis
    apply (rule vmtf_ns.Cons[of _ _ _ _ _ n])
    subgoal using a_xs by simp
    subgoal using a_xs by simp
    subgoal using ab .
    subgoal using a_l .
    subgoal using nm .
    subgoal using xs' ab a_xs by (cases ‹xs ! b›) auto
    subgoal using nn' .
    done
qed

definition (in -) vmtf_cons where
‹vmtf_cons ns L cnext st =
  (let
    ns = ns[L := VMTF_Node (Suc st) None cnext];
    ns = (case cnext of None ⇒ ns
        | Some cnext ⇒ ns[cnext := VMTF_Node (stamp (ns!cnext)) (Some L) (get_next (ns!cnext))]) in
  ns)
›

lemma vmtf_notin_vmtf_cons:
  assumes
    vmtf_ns: ‹vmtf_ns_notin xs m ns› and
    cnext: ‹cnext = option_hd xs› and
    L_xs: ‹L ∉ set xs›
  shows
    ‹vmtf_ns_notin (L # xs) (Suc m) (vmtf_cons ns L cnext m)›
proof (cases xs)
  case Nil
  then show ?thesis
    using assms by (auto simp: vmtf_ns_notin_def vmtf_cons_def elim: vmtf_nsE)
next
  case (Cons L' xs') note xs = this
  show ?thesis
    using assms unfolding xs vmtf_ns_notin_def xs vmtf_cons_def by auto
qed

lemma vmtf_cons:
  assumes
    vmtf_ns: ‹vmtf_ns xs m ns› and
    cnext: ‹cnext = option_hd xs› and
    L_A: ‹L < length ns› and
    L_xs: ‹L ∉ set xs›
  shows
    ‹vmtf_ns (L # xs) (Suc m) (vmtf_cons ns L cnext m)›
proof (cases xs)
  case Nil
  then show ?thesis
    using assms by (auto simp: vmtf_ns_single_iff vmtf_cons_def elim: vmtf_nsE)
next
  case (Cons L' xs') note xs = this
  show ?thesis
    unfolding xs
    apply (rule vmtf_ns_Cons[OF vmtf_ns[unfolded xs], of _ ‹Suc m›])
    subgoal using L_A .
    subgoal using L_xs unfolding xs by simp
    subgoal using L_xs unfolding xs by simp
    subgoal by simp
    subgoal using cnext L_xs
      by (auto simp: vmtf_cons_def Let_def xs)
    subgoal by linarith
    done
qed

lemma length_vmtf_cons[simp]: ‹length (vmtf_cons ns L n m) = length ns›
  by (auto simp: vmtf_cons_def Let_def split: option.splits)

lemma wf_vmtf_get_prev:
  assumes vmtf: ‹(ns, m, fst_As, lst_As, next_search) ∈ vmtf 𝒜 M›
  shows ‹wf {(get_prev (ns ! the a), a) |a. a ≠ None ∧ the a ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)}› (is ‹wf ?R›)
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain f where
    f: ‹(f (Suc i), f i) ∈ ?R› for i
    unfolding wf_iff_no_infinite_down_chain by blast

  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set xs', set ys')› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns›
    using vmtf unfolding vmtf_def by fast
  let ?f0 = ‹the (f 0)›
  have f_None: ‹f i ≠ None› for i
    using f[of i] by fast
  have f_Suc : ‹f (Suc n) = get_prev (ns ! the (f n))› for n
    using f[of n] by auto
  have f0_length: ‹?f0 < length ns›
    using f[of 0] atm_A
    by auto
  have f0_in:  ‹?f0 ∈ set (ys' @ xs')›
    apply (rule ccontr)
    using notin f_Suc[of 0] f0_length unfolding vmtf_ns_notin_def
    by (auto simp: f_None)
  then obtain i0 where
    i0: ‹(ys' @ xs') ! i0 = ?f0› ‹i0 < length (ys' @ xs')›
    by (meson in_set_conv_nth)
  define zs where ‹zs = ys' @ xs'›
  have H: ‹ys' @ xs' = take m (ys' @ xs') @ [(ys' @ xs') ! m, (ys' @ xs') ! (m+1)] @
     drop (m+2) (ys' @ xs')›
    if ‹m + 1 < length (ys' @ xs')›
    for m
    using that
    unfolding zs_def[symmetric]
    apply -
    apply (subst id_take_nth_drop[of m])
    by (auto simp: take_Suc_conv_app_nth Cons_nth_drop_Suc  simp del: append_take_drop_id)

  have ‹the (f n) = (ys' @ xs') ! (i0 - n) ∧ i0 - n ≥ 0 ∧ n ≤ i0› for n
  proof (induction n)
    case 0
    then show ?case using i0 by simp
  next
    case (Suc n')
    have i0_le: ‹n' < i0›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then have ‹i0 = n'›
        using Suc by auto
      then have ‹ys' @ xs' = [the (f n')] @ tl (ys' @ xs')›
        using Suc f0_in
        by (cases ‹ys' @ xs'›) auto
      then show False
        using vmtf_ns_hd_prev[of ‹the (f n')› ‹tl (ys' @ xs')› m ns] vmtf_ns
         f_Suc[of n'] by (auto simp: f_None)
    qed
    have get_prev: ‹get_prev (ns ! ((ys' @ xs') ! (i0 - (n' +1) + 1))) =
         Some ((ys' @ xs') ! ((i0 - (n' + 1))))›
      apply (rule vmtf_ns_last_mid_get_prev[of ‹take (i0 - (n' +1)) (ys' @ xs')› _ _
        ‹drop ((i0 - (n' + 1)) + 2) (ys' @ xs')› m])
      apply (subst H[symmetric])
      subgoal using i0_le i0 by auto
      subgoal using vmtf_ns by simp
      done
    then show ?case
      using f_Suc[of n'] Suc i0_le by auto
  qed
  from this[of ‹Suc i0›] show False
    by auto
qed

fun update_stamp where
  ‹update_stamp xs n a = xs[a := VMTF_Node n (get_prev (xs!a)) (get_next (xs!a))]›

definition vmtf_rescale :: ‹vmtf ⇒ vmtf nres› where
‹vmtf_rescale = (λ(ns, m, fst_As, lst_As :: nat, next_search). do {
  (ns, m, _) ← WHILE⇩T⇗λ_. True⇖
     (λ(ns, n, lst_As). lst_As ≠None)
     (λ(ns, n, a). do {
       ASSERT(a ≠ None);
       ASSERT(n+1 ≤ unat32_max);
       ASSERT(the a < length ns);
       RETURN (update_stamp ns n (the a), n+1, get_prev (ns ! the a))
     })
     (ns, 0, Some lst_As);
  RETURN ((ns, m, fst_As, lst_As, next_search))
  })
›


lemma vmtf_rescale_vmtf:
  assumes vmtf: ‹vm ∈ vmtf 𝒜 M› and
    nempty: ‹isasat_input_nempty 𝒜› and
    bounded: ‹isasat_input_bounded 𝒜›
  shows
    ‹vmtf_rescale vm ≤ SPEC (λvm. vm ∈ vmtf 𝒜 M ∧ fst (snd vm) ≤ unat32_max)›
    (is ‹?A ≤ ?R›)
proof -
  obtain ns m fst_As lst_As next_search where
    vm: ‹vm = ((ns, m, fst_As, lst_As, next_search))›
    by (cases vm) auto

  obtain xs' ys' where
    vmtf_ns: ‹vmtf_ns (ys' @ xs') m ns› and
    fst_As: ‹fst_As = hd (ys' @ xs')› and
    lst_As: ‹lst_As = last (ys' @ xs')› and
    next_search: ‹next_search = option_hd xs'› and
    abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M (set xs', set ys')› and
    notin: ‹vmtf_ns_notin (ys' @ xs') m ns› and
    atm_A: ‹∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length ns› and
    in_lall: ‹∀L∈set (ys' @ xs'). L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
    using vmtf unfolding vmtf_def vm by fast
  have [dest]: ‹ys' = [] ⟹ xs' = [] ⟹ False› and
    [simp]: ‹ys' = [] ⟶ xs' ≠ []›
    using abs_vmtf nempty unfolding vmtf_ℒ⇩a⇩l⇩l_def
    by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
  have 1: ‹RES (vmtf 𝒜 M) = do {
    a ← RETURN ();
    RES (vmtf 𝒜 M)
    }›
    by auto
  define zs where ‹zs ≡ ys' @ xs'›

  define I' where
    ‹I' ≡ λ(ns', n::nat, lst::nat option).
        map get_prev ns = map get_prev ns' ∧
        map get_next ns = map get_next ns' ∧
        (∀i<n. stamp (ns' ! (rev zs ! i)) = i) ∧
        (lst ≠ None ⟶ n < length (zs) ∧ the lst = zs ! (length zs - Suc n)) ∧
        (lst = None ⟶ n = length zs) ∧
          n ≤ length zs›
  have [simp]: ‹zs ≠ []›
    unfolding zs_def by auto
  have I'0: ‹I' (ns, 0, Some lst_As)›
    using vmtf lst_As unfolding I'_def vm zs_def[symmetric] by (auto simp: last_conv_nth)


  have lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (Pos `# mset zs)› and
    dist: ‹distinct zs›
    using abs_vmtf vmtf_ns_distinct[OF vmtf_ns] unfolding vmtf_def zs_def
      vmtf_ℒ⇩a⇩l⇩l_def
    by (auto simp: literals_are_in_ℒ⇩i⇩n_alt_def inj_on_def)
  have dist: ‹distinct_mset (Pos `# mset zs)›
    by (subst distinct_image_mset_inj)
      (use dist in ‹auto simp: inj_on_def›)
  have tauto: ‹¬ tautology (poss (mset zs))›
    by (auto simp: tautology_decomp)

  have length_zs_le:  ‹length zs < unat32_max› using vmtf_ns_distinct[OF vmtf_ns]
      using simple_clss_size_upper_div2[OF bounded lits dist tauto]
      by (auto simp: unat32_max_def)

  have ‹wf {(a, b). (a, b) ∈ {(get_prev (ns ! the a), a) |a. a ≠ None ∧ the a ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)}}›
    by (rule wf_subset[OF wf_vmtf_get_prev[OF vmtf[unfolded vm]]]) auto
  from wf_snd_wf_pair[OF wf_snd_wf_pair[OF this]]
  have wf: ‹wf {((_, _, a), (_, _, b)). (a, b) ∈ {(get_prev (ns ! the a), a) |a. a ≠ None ∧
      the a ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)}}›
    by (rule wf_subset) auto
  have zs_lall: ‹zs ! (length zs - Suc n) ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› for n
    using abs_vmtf nth_mem[of ‹length zs - Suc n› zs] unfolding zs_def vmtf_ℒ⇩a⇩l⇩l_def
    by auto
  then have zs_le_ns[simp]: ‹zs ! (length zs - Suc n) < length ns› for n
    using atm_A by auto
  have loop_body:  ‹(case s' of
        (ns, n, a) ⇒ do {
            ASSERT (a ≠ None);
            ASSERT (n + 1 ≤ unat32_max);
            ASSERT(the a < length ns);
            RETURN (update_stamp ns n (the a), n + 1, get_prev (ns ! the a))
          })
        ≤ SPEC
          (λs'a. True ∧
                  I' s'a ∧
                  (s'a, s')
                  ∈ {((_, _, a), _, _, b).
                    (a, b)
                    ∈ {(get_prev (ns ! the a), a) |a.
                        a ≠ None ∧ the a ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)}})›
    if
      I': ‹I' s'› and
      cond: ‹case s' of (ns, n, lst_As) ⇒ lst_As ≠ None›
    for s'
  proof -
    obtain ns' n' a' where s': ‹s' = (ns', n' , a')›
      by (cases s')
    have
      a[simp]: ‹a' = Some (zs ! (length zs - Suc n'))› and
      eq_prev: ‹map get_prev ns = map get_prev ns'› and
      eq_next: ‹map get_next ns = map get_next ns'› and
      eq_stamps: ‹⋀i. i<n' ⟹ stamp (ns' ! (rev zs ! i)) = i› and
      n'_le: ‹n' < length zs›
      using I' cond unfolding I'_def prod.simps s'
      by auto
    have [simp]: ‹length ns' = length ns›
      using arg_cong[OF eq_prev, of length] by auto
    have vmtf_as: ‹vmtf_ns
      (take (length zs - (n' + 1)) zs @
       zs ! (length zs - (n' + 1)) #
       drop (Suc (length zs - (n' + 1))) zs)
      m ns›
      apply (subst Cons_nth_drop_Suc)
      subgoal by auto
      apply (subst append_take_drop_id)
      using vmtf_ns unfolding zs_def[symmetric] .

    have ‹get_prev (ns' ! the a') ≠ None ⟶
        n' + 1 < length zs ∧
        the (get_prev (ns' ! the a')) = zs ! (length zs - Suc (n' + 1))›
      using n'_le vmtf_ns arg_cong[OF eq_prev, of ‹λxs. xs ! (zs ! (length zs - Suc n'))›]
        vmtf_ns_last_mid_get_prev_option_last[OF vmtf_as]
      by (auto simp: last_conv_nth)
    moreover have ‹map get_prev ns = map get_prev (update_stamp ns' n' (the a'))›
      unfolding update_stamp.simps
      apply (subst map_update)
      apply (subst list_update_id')
      subgoal by auto
      subgoal using eq_prev .
      done
    moreover have ‹map get_next ns = map get_next (update_stamp ns' n' (the a'))›
      unfolding update_stamp.simps
      apply (subst map_update)
      apply (subst list_update_id')
      subgoal by auto
      subgoal using eq_next .
      done
    moreover have ‹i<n' + 1 ⟹ stamp (update_stamp ns' n' (the a') ! (rev zs ! i)) = i› for i
      using eq_stamps[of i] vmtf_ns_distinct[OF vmtf_ns] n'_le
      unfolding zs_def[symmetric]
      by (cases ‹i < n'›)
        (auto simp: rev_nth nth_eq_iff_index_eq)
    moreover have ‹n' + 1 ≤ length zs›
     using n'_le by (auto simp: Suc_le_eq)
    moreover have ‹get_prev (ns' ! the a') = None ⟹ n' + 1 = length zs›
      using n'_le vmtf_ns arg_cong[OF eq_prev, of ‹λxs. xs ! (zs ! (length zs - Suc n'))›]
        vmtf_ns_last_mid_get_prev_option_last[OF vmtf_as]
      by auto
    ultimately have I'_f: ‹I' (update_stamp ns' n' (the a'), n' + 1, get_prev (ns' ! the a'))›
      using cond n'_le unfolding I'_def prod.simps s'
      by simp

    show ?thesis
      unfolding s' prod.case
      apply refine_vcg
      subgoal using cond by auto
      subgoal using length_zs_le n'_le by auto
      subgoal by auto
      subgoal by fast
      subgoal by (rule I'_f)
      subgoal
        using arg_cong[OF eq_prev, of ‹λxs. xs ! (zs ! (length zs - Suc n'))›] zs_lall
        by auto
      done
  qed
  have loop_final: ‹s ∈ {x. (case x of
                (ns, m, uua_) ⇒
                  RETURN ((ns, m, fst_As, lst_As, next_search)))
                ≤ ?R}›
    if
      ‹True› and
      ‹I' s› and
      ‹¬ (case s of (ns, n, lst_As) ⇒ lst_As ≠ None)›
    for s
  proof -
    obtain ns' n' a' where s: ‹s = (ns', n' , a')›
      by (cases s)
    have
      [simp]:‹a' = None› and
      eq_prev: ‹map get_prev ns = map get_prev ns'› and
      eq_next: ‹map get_next ns = map get_next ns'› and
      stamp: ‹∀i<n'. stamp (ns' ! (rev zs ! i)) = i› and
      [simp]: ‹n' = length zs›
      using that unfolding I'_def s prod.case by auto
    have [simp]: ‹length ns' = length ns›
      using arg_cong[OF eq_prev, of length] by auto
    have [simp]: ‹map ((!) (map stamp ns')) (rev zs) = [0..<length zs]›
      apply (subst list_eq_iff_nth_eq, intro conjI)
      subgoal by auto
      subgoal using stamp by (auto simp: rev_nth)
      done
    then have stamps_zs[simp]: ‹map ((!) (map stamp ns')) zs = rev [0..<length zs]›
        unfolding rev_map[symmetric]
        using rev_swap by blast

    have ‹sorted (map ((!) (map stamp ns')) (rev zs))›
      by simp
    moreover have ‹distinct (map ((!) (map stamp ns')) zs)›
      by simp
    moreover have ‹∀a∈set zs. get_prev (ns' ! a) = get_prev (ns ! a)›
      using eq_prev map_eq_nth_eq by fastforce
    moreover have ‹∀a∈set zs. get_next (ns' ! a) = get_next (ns ! a)›
      using eq_next map_eq_nth_eq by fastforce
    moreover have ‹∀a∈set zs. stamp (ns' ! a) = map stamp ns' ! a›
      using vmtf_ns vmtf_ns_le_length zs_def by auto
    moreover have ‹length ns ≤ length ns'›
     by simp
    moreover have ‹∀a∈set zs. a < length (map stamp ns')›
      using vmtf_ns vmtf_ns_le_length zs_def by auto
    moreover have ‹∀a∈set zs. map stamp ns' ! a < n'›
    proof
      fix a
      assume ‹a ∈ set zs›
      then have ‹map stamp ns' ! a ∈ set (map ((!) (map stamp ns')) zs)›
        by (metis in_set_conv_nth length_map nth_map)
      then show ‹map stamp ns' ! a < n'›
        unfolding stamps_zs by simp
    qed
    ultimately have ‹vmtf_ns zs n' ns'›
      using vmtf_ns_rescale[OF vmtf_ns, of ‹map stamp ns'› ns', unfolded zs_def[symmetric]]
      by fast
    moreover have ‹vmtf_ns_notin zs (length zs) ns'›
      using notin map_eq_nth_eq[OF eq_prev] map_eq_nth_eq[OF eq_next]
      unfolding zs_def[symmetric]
      by (auto simp: vmtf_ns_notin_def)
    ultimately have ‹(ns', n', fst_As, lst_As, next_search) ∈ vmtf 𝒜 M›
      using fst_As lst_As next_search abs_vmtf atm_A notin in_lall
      unfolding vmtf_def in_pair_collect_simp prod.case apply -
      apply (rule exI[of _ xs'])
      apply (rule exI[of _ ys'])
      unfolding zs_def[symmetric]
      by auto
    then show ?thesis
      using length_zs_le
      by (auto simp: s)
  qed

  have H: ‹WHILE⇩T⇗λ_. True⇖ (λ(ns, n, lst_As). lst_As ≠ None)
     (λ(ns, n, a). do {
           _ ← ASSERT (a ≠ None);
           _ ← ASSERT (n + 1 ≤ unat32_max);
           ASSERT(the a < length ns);
           RETURN (update_stamp ns n (the a), n + 1, get_prev (ns ! the a))
         })
     (ns, 0, Some lst_As)
    ≤ SPEC
       (λx. (case x of
             (ns, m, uua_) ⇒
               RETURN ((ns, m, fst_As, lst_As, next_search)))
            ≤ ?R)
  ›
  apply (rule WHILEIT_rule_stronger_inv_RES[where I' = I' and
      R = ‹{((_, _, a), (_, _, b)). (a, b) ∈
         {(get_prev (ns ! the a), a) |a. a ≠ None ∧ the a ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)}}›])
  subgoal
   by (rule wf)
  subgoal by fast
  subgoal by (rule I'0)
  subgoal for s'
    by (rule loop_body)
  subgoal for s
    by (rule loop_final)
  done

  show ?thesis
    unfolding vmtf_rescale_def vm prod.case
    apply (subst bind_rule_complete_RES)
    apply (rule H)
    done
qed


definition vmtf_flush
   :: ‹nat multiset ⇒ (nat,nat) ann_lits ⇒  vmtf ⇒ nat set ⇒ (vmtf × nat set) nres›
where
  ‹vmtf_flush 𝒜⇩i⇩n = (λM vm remove_int. SPEC (λx. (fst x) ∈ vmtf 𝒜⇩i⇩n M ∧ snd x = {}))›


definition atoms_hash_rel :: ‹nat multiset ⇒ (bool list × nat set) set› where
  ‹atoms_hash_rel 𝒜 = {(C, D). (∀L ∈ D. L < length C) ∧ (∀L < length C. C ! L ⟷ L ∈ D) ∧
    (∀L ∈# 𝒜. L < length C) ∧ D ⊆ set_mset 𝒜}›

definition distinct_hash_atoms_rel
  :: ‹'v multiset ⇒ (('v list × 'v set) × 'v set) set›
where
  ‹distinct_hash_atoms_rel 𝒜 = {((C, h), D). set C = D ∧ h = D ∧ distinct C ∧ D ⊆ set_mset 𝒜}›

definition distinct_atoms_rel
  :: ‹nat multiset ⇒ ((nat list × bool list) × nat set) set›
where
  ‹distinct_atoms_rel 𝒜 = (Id ×⇩r atoms_hash_rel 𝒜) O distinct_hash_atoms_rel 𝒜›

lemma distinct_atoms_rel_alt_def:
  ‹distinct_atoms_rel 𝒜 = {((D', C), D). (∀L ∈ D. L < length C) ∧ (∀L < length C. C ! L ⟷ L ∈ D) ∧
    (∀L ∈# 𝒜. L < length C) ∧ set D' = D ∧ distinct D' ∧ set D' ⊆ set_mset 𝒜}›
  unfolding distinct_atoms_rel_def atoms_hash_rel_def distinct_hash_atoms_rel_def prod_rel_def
  apply rule
  subgoal
    by (auto simp: mset_set_set)
  subgoal
    by (auto simp: mset_set_set)
  done

lemma distinct_atoms_rel_empty_hash_iff:
  ‹(([], h), {}) ∈ distinct_atoms_rel 𝒜 ⟷  (∀L ∈# 𝒜. L < length h) ∧ (∀i∈set h. i = False)›
  unfolding distinct_atoms_rel_alt_def all_set_conv_nth
  by auto

definition atoms_hash_del_pre where
  ‹atoms_hash_del_pre i xs = (i < length xs)›

definition atoms_hash_del where
‹atoms_hash_del i xs = xs[i := False]›


definition vmtf_flush_int :: ‹nat multiset ⇒ (nat,nat) ann_lits ⇒ _ ⇒ _ ⇒ _ nres› where
‹vmtf_flush_int 𝒜⇩i⇩n = (λM vm (to_remove, h). do {
    ASSERT(∀x∈set to_remove. x < length (fst vm));
    ASSERT(length to_remove ≤ unat32_max);
    to_remove' ← reorder_list vm to_remove;
    ASSERT(length to_remove' ≤ unat32_max);
    vm ← (if length to_remove' + fst (snd vm) ≥ unat64_max
      then vmtf_rescale vm else RETURN vm);
    ASSERT(length to_remove' + fst (snd vm) ≤ unat64_max);
    (_, vm, h) ← WHILE⇩T⇗λ(i, vm', h). i ≤ length to_remove' ∧ fst (snd vm') = i + fst (snd vm) ∧
          (i < length to_remove' ⟶ vmtf_en_dequeue_pre 𝒜⇩i⇩n ((M, to_remove'!i), vm'))⇖
      (λ(i, vm, h). i < length to_remove')
      (λ(i, vm, h). do {
         ASSERT(i < length to_remove');
         ASSERT(to_remove'!i ∈# 𝒜⇩i⇩n);
         ASSERT(atoms_hash_del_pre (to_remove'!i) h);
         RETURN (i+1, vmtf_en_dequeue M (to_remove'!i) vm, atoms_hash_del (to_remove'!i) h)})
      (0, vm, h);
    RETURN (vm, (emptied_list to_remove', h))
  })›


lemma vmtf_change_to_remove_order:
  assumes
    vmtf: ‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜⇩i⇩n M› and
    CD_rem: ‹((C, D), to_remove) ∈ distinct_atoms_rel 𝒜⇩i⇩n› and
    nempty: ‹isasat_input_nempty 𝒜⇩i⇩n› and
    bounded: ‹isasat_input_bounded 𝒜⇩i⇩n› and
    t: ‹to_remove ⊆ set_mset 𝒜⇩i⇩n›
  shows ‹vmtf_flush_int 𝒜⇩i⇩n M (ns, m, fst_As, lst_As, next_search) (C, D)
    ≤ ⇓(Id ×⇩r distinct_atoms_rel 𝒜⇩i⇩n)
       (vmtf_flush 𝒜⇩i⇩n M (ns, m, fst_As, lst_As, next_search) to_remove)›
proof -
  let ?vm = ‹(ns, m, fst_As, lst_As, next_search)›
  have vmtf_flush_alt_def: ‹vmtf_flush 𝒜⇩i⇩n M ?vm to_remove = do {
     _ ← RETURN ();
     _ ← RETURN ();
     vm ← SPEC (λx. (fst x) ∈ vmtf 𝒜⇩i⇩n M ∧ snd x = {});
     RETURN (vm)
  }›
    unfolding vmtf_flush_def by (auto simp: RES_RES_RETURN_RES RES_RETURN_RES vmtf)

  have pre_sort: ‹∀x∈set x1. x < length ((fst (ns, m, fst_As, lst_As, next_search)))›
    if
      ‹(C, D) = (x1, x2)›
    for x1 x2 x1a x2a
  proof -
    show ?thesis
      using vmtf CD_rem that t apply (auto simp: vmtf_def vmtf_ℒ⇩a⇩l⇩l_def
        distinct_atoms_rel_alt_def)
      by (metis atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n in_mono)
  qed

  have length_le: ‹length x1a ≤ unat32_max›
    if
      ‹(C, D) = (x1a, x2a)› and
      ‹∀x∈set x1a. x < length (fst x1)›
      for x1 x2 x1a x2a
  proof -
    have lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (Pos `# mset x1a)› and
      dist: ‹distinct x1a›
      using that vmtf CD_rem t unfolding vmtf_def
        vmtf_ℒ⇩a⇩l⇩l_def
      apply (auto simp: literals_are_in_ℒ⇩i⇩n_alt_def distinct_atoms_rel_alt_def inj_on_def)
      by (metis atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n in_mono)
    have dist: ‹distinct_mset (Pos `# mset x1a)›
      by (subst distinct_image_mset_inj)
        (use dist in ‹auto simp: inj_on_def›)
    have tauto: ‹¬ tautology (poss (mset x1a))›
      by (auto simp: tautology_decomp)

    show ?thesis
      using simple_clss_size_upper_div2[OF bounded lits dist tauto]
      by (auto simp: unat32_max_def)
  qed


  have [refine0]:
     ‹reorder_list x1 x1a ≤ SPEC (λc. (c, ()) ∈
        {(c, c'). ((c, D), to_remove) ∈ distinct_atoms_rel 𝒜⇩i⇩n ∧ to_remove = set c ∧
           length C = length c})›
     (is ‹_ ≤ SPEC(λ_. _ ∈ ?reorder_list)›)
    if
      ‹x2 = (x1a, x2a)› and
      ‹((ns, m, fst_As, lst_As, next_search), C, D) = (x1, x2)›
    for x1 x2 x1a x2a
  proof -
    show ?thesis
      using that assms by (force simp: reorder_list_def distinct_atoms_rel_alt_def
        dest: mset_eq_setD same_mset_distinct_iff mset_eq_length)
  qed


  have [refine0]: ‹(if unat64_max ≤ length to_remove' + fst (snd x1) then vmtf_rescale x1
      else RETURN x1)
      ≤ SPEC (λc. (c, ()) ∈
        {(vm ,vm'). unat64_max ≥ length to_remove' + fst (snd vm) ∧
          (vm) ∈ vmtf 𝒜⇩i⇩n M}) ›
    (is ‹_ ≤ SPEC(λc. (c, ()) ∈ ?rescale)› is ‹_ ≤ ?H›)
  if
    ‹x2 = (x1a, x2a)› and
    ‹((ns, m, fst_As, lst_As, next_search), C, D) = (x1, x2)› and
    ‹∀x∈set x1a. x < length (fst x1)› and
    ‹length x1a ≤ unat32_max› and
    ‹(to_remove', uu) ∈ ?reorder_list› and
    ‹length to_remove' ≤ unat32_max›
  for x1 x2 x1a x2a to_remove' uu
  proof -
    have ‹vmtf_rescale x1 ≤ ?H›
      apply (rule order_trans)
      apply (rule vmtf_rescale_vmtf[of _ 𝒜⇩i⇩n M])
      subgoal using vmtf that by auto
      subgoal using nempty by fast
      subgoal using bounded by fast
      subgoal using that by (auto intro!: RES_refine simp: unat64_max_def unat32_max_def)
      done
    then show ?thesis
      using that vmtf
      by (auto intro!: RETURN_RES_refine)
  qed


  have loop_ref: ‹WHILE⇩T⇗λ(i, vm', h).
                  i ≤ length to_remove' ∧ fst (snd vm') = i + fst (snd x1) ∧
                  (i < length to_remove' ⟶
                    vmtf_en_dequeue_pre 𝒜⇩i⇩n ((M, to_remove' ! i), vm'))⇖
        (λ(i, vm, h). i < length to_remove')
        (λ(i, vm, h). do {
              ASSERT (i < length to_remove');
              ASSERT(to_remove'!i ∈# 𝒜⇩i⇩n);
              ASSERT(atoms_hash_del_pre (to_remove'!i) h);
              RETURN
                (i + 1, vmtf_en_dequeue M (to_remove' ! i) vm,
                atoms_hash_del (to_remove'!i) h)
            })
        (0, x1, x2a)
        ≤ ⇓ {((i, vm::vmtf, h:: _), vm'). (vm, {}) = vm' ∧ (∀i∈set h. i = False) ∧ i = length to_remove' ∧
               ((drop i to_remove', h), set(drop i to_remove')) ∈ distinct_atoms_rel 𝒜⇩i⇩n}
	    (SPEC (λx. (fst x) ∈ vmtf 𝒜⇩i⇩n M ∧ snd x = {}))›
    if
      CD: ‹(C, D) = (x1a, x2a)› and
      x1: ‹(x1, u') ∈ ?rescale to_remove'›
      ‹(to_remove', u) ∈ ?reorder_list›
    for x1 x2 x1a x2a to_remove' u u' x1'
  proof -
    define I where ‹I ≡ λ(i, vm'::vmtf, h::bool list).
                  i ≤ length to_remove' ∧ fst (snd vm') = i + fst (snd x1) ∧
                  (i < length to_remove' ⟶
                    vmtf_en_dequeue_pre 𝒜⇩i⇩n ((M, to_remove' ! i), vm'))›
    define I' where ‹I' ≡ λ(i, vm::vmtf, h:: bool list).
       ((drop i to_remove', h), set(drop i to_remove')) ∈ distinct_atoms_rel 𝒜⇩i⇩n ∧
              vm ∈ vmtf 𝒜⇩i⇩n M›
    have [simp]:
        ‹x1a = C›
        ‹x2a = D› and
      rel: ‹((to_remove', D), to_remove) ∈ distinct_atoms_rel 𝒜⇩i⇩n› and
      to_rem: ‹to_remove = set to_remove'›
      using that by (auto simp: )
    have D: ‹set to_remove' = to_remove› and dist: ‹distinct to_remove'›
      using rel unfolding distinct_atoms_rel_alt_def by auto
    have in_lall: ‹to_remove' ! x1 ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n)› if le': ‹x1 < length to_remove'› for x1
      using vmtf to_rem nth_mem[OF le'] t by (auto simp: vmtf_def vmtf_ℒ⇩a⇩l⇩l_def
         atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n subsetD)
    have bound: ‹fst (snd x1) + 1 ≤ unat64_max› if ‹0 < length to_remove'›
        using rel vmtf to_rem that x1 by (cases to_remove') auto
    have I_init: ‹I (0, x1, x2a)› (is ?A)
      for x1a x2 x1aa x2aa
    proof -
      have ‹vmtf_en_dequeue_pre 𝒜⇩i⇩n ((M, to_remove' ! 0), x1)› if ‹0 < length to_remove'›
        apply (rule vmtf_vmtf_en_dequeue_pre_to_remove'[of _])
        using rel vmtf to_rem that x1 bound nempty in_lall[of 0] by (auto simp: )
      then show ?A
        unfolding I_def by auto
    qed
    have I'_init: ‹I' (0, x1, x2a)› (is ?B)
      for x1a x2 x1aa x2aa
    proof -
      show ?B
        using rel to_rem CD_rem that[symmetric] vmtf t unfolding I'_def by auto
    qed
    have post_loop: ‹do {
            ASSERT (x2 < length to_remove');
            ASSERT(to_remove' ! x2 ∈# 𝒜⇩i⇩n);
            ASSERT(atoms_hash_del_pre (to_remove' ! x2) x2a');
            RETURN
              (x2 + 1, vmtf_en_dequeue M (to_remove' ! x2) x2aa,
                  atoms_hash_del (to_remove'!x2) x2a')
          } ≤ SPEC
              (λs'. I s' ∧ I' s' ∧ (s', x1a) ∈ measure (λ(i, vm, h). Suc (length to_remove') - i))›
      if
        I: ‹I x1a› and
        I': ‹I' x1a› and
        ‹case x1a of (i, vm, h) ⇒ i < length to_remove'› and
        x1aa: ‹x1aa = (x2aa, x2a')› ‹x1a = (x2, x1aa)›
      for s x2 x1a x2a x1a' x2a' x1aa x2aa
    proof -
      let ?x2a' = ‹set (drop x2 to_remove')›
      have le: ‹x2 < length to_remove'› and vm: ‹(x2aa) ∈ vmtf 𝒜⇩i⇩n M› and
        x2a': ‹fst (snd x2aa) = x2 + fst (snd x1)›
        using that unfolding I_def I'_def by (auto simp: distinct_atoms_rel_alt_def)
      have 1: ‹(vmtf_en_dequeue M (to_remove' ! x2) x2aa) ∈ vmtf 𝒜⇩i⇩n M›
        by (rule abs_vmtf_ns_bump_vmtf_en_dequeue'[OF vm in_lall[OF le]])
          (use nempty in auto)
      have 3: ‹fst (snd x2aa) = fst (snd x1) + x2›
        using I I' le dist that CD x2a' unfolding I_def I'_def x2a' x1aa
         by (auto simp: distinct_atoms_rel_def in_set_drop_conv_nth I'_def
             nth_eq_iff_index_eq intro: bex_geI[of _ ‹Suc x2›])
      then have 4: ‹fst (snd (vmtf_en_dequeue M (to_remove' ! x2) x2aa)) + 1 ≤ unat64_max›
        if ‹Suc x2 < length to_remove'›
        using x1 le that
        by (cases x2aa)
          (auto simp: vmtf_en_dequeue_def vmtf_enqueue_def vmtf_dequeue_def
          split: option.splits)
      have 1: ‹vmtf_en_dequeue_pre 𝒜⇩i⇩n
          ((M, to_remove' ! Suc x2), vmtf_en_dequeue M (to_remove' ! x2) x2aa)›
        if ‹Suc x2 < length to_remove'›
        by (rule vmtf_vmtf_en_dequeue_pre_to_remove')
         (rule 1, rule in_lall, rule that, rule 4[OF that], rule nempty)
      have 3: ‹(vmtf_en_dequeue M (to_remove' ! x2) x2aa) ∈ vmtf 𝒜⇩i⇩n M›
        by (rule abs_vmtf_ns_bump_vmtf_en_dequeue'[OF vm in_lall[OF le]]) (use nempty in auto)
      have 4: ‹((drop (Suc x2) to_remove', atoms_hash_del (to_remove' ! x2) x2a'),
            set (drop (Suc x2) to_remove'))
        ∈ distinct_atoms_rel 𝒜⇩i⇩n› and
        3: ‹(vmtf_en_dequeue M (to_remove' ! x2) x2aa)
         ∈ vmtf 𝒜⇩i⇩n M›
        using 3 I' le to_rem that unfolding I'_def distinct_atoms_rel_alt_def atoms_hash_del_def
        by (auto simp: Cons_nth_drop_Suc[symmetric] intro: mset_le_add_mset_decr_left1)

      have A: ‹to_remove' ! x2 ∈ ?x2a'›
        using I I' le dist that x1aa unfolding I_def I'_def
        by (auto simp: distinct_atoms_rel_def in_set_drop_conv_nth I'_def
             nth_eq_iff_index_eq x2a' intro: bex_geI[of _ ‹x2›])
      moreover have ‹I (Suc x2, vmtf_en_dequeue M (to_remove' ! x2) x2aa,
          atoms_hash_del (to_remove' ! x2) x2a')›
        using that 1 unfolding I_def
        by (cases x2aa)
          (auto simp: vmtf_en_dequeue_def vmtf_enqueue_def vmtf_dequeue_def
          split: option.splits)
      moreover have ‹length to_remove' - x2 < Suc (length to_remove') - x2›
        using le by auto
      moreover have ‹I' (Suc x2, vmtf_en_dequeue M (to_remove' ! x2) x2aa,
          atoms_hash_del (to_remove' ! x2) x2a')›
        using that 3 4 I' unfolding I'_def
        by auto
      moreover have ‹atoms_hash_del_pre (to_remove' ! x2) x2a'›
        unfolding atoms_hash_del_pre_def
        using that le A unfolding I_def I'_def by (auto simp: distinct_atoms_rel_alt_def)
      ultimately show ?thesis
        using that in_lall[OF le]
        by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
    qed
    have [simp]: ‹∀L<length ba. ¬ ba ! L ⟹  True ∉ set ba› for ba
      by (simp add: in_set_conv_nth)
    have post_rel: ‹RETURN s
        ≤ ⇓ {((i, vm, h), vm').
             (vm, {}) = vm' ∧
             (∀i∈set h. i = False) ∧
             i = length to_remove' ∧
             ((drop i to_remove', h), set (drop i to_remove'))
      ∈ distinct_atoms_rel 𝒜⇩i⇩n}
      (SPEC (λx. (fst x) ∈ vmtf 𝒜⇩i⇩n M ∧ snd x = {}))›
        if
         ‹¬ (case s of (i, vm, h) ⇒ i < length to_remove')› and
         ‹I s› and
         ‹I' s›
       for s
    proof -
      obtain i vm h where s: ‹s = (i, vm, h)› by (cases s)
      have [simp]: ‹i = length (to_remove')› and [iff]: ‹True ∉ set h› and
        [simp]: ‹(([], h), {}) ∈ distinct_atoms_rel 𝒜⇩i⇩n›
          ‹(vm) ∈ vmtf 𝒜⇩i⇩n M›
        using that unfolding s I_def I'_def by (auto simp: distinct_atoms_rel_empty_hash_iff)
      show ?thesis
        unfolding s
        by (rule RETURN_RES_refine) auto
    qed

    show ?thesis
      unfolding I_def[symmetric]
      apply (refine_rcg
        WHILEIT_rule_stronger_inv_RES'[where R=‹measure (λ(i, vm::vmtf, h). Suc (length to_remove') -i)› and
            I'=‹I'›])
      subgoal by auto
      subgoal by (rule I_init)
      subgoal by (rule I'_init)
      subgoal for x1'' x2'' x1a'' x2a'' by (rule post_loop)
      subgoal by (rule post_rel)
      done
  qed


  show ?thesis
    unfolding vmtf_flush_int_def vmtf_flush_alt_def
    apply (refine_rcg)
    subgoal by (rule pre_sort)
    subgoal by (rule length_le)
    apply (assumption+)[2]
    subgoal by auto
    subgoal by auto
    apply (assumption+)[5]
    subgoal by auto
    apply (assumption+)[3]
    subgoal by auto
    apply (rule loop_ref; assumption)
    subgoal by (auto simp: emptied_list_def)
    done
qed

lemma vmtf_change_to_remove_order':
  ‹(uncurry2 (vmtf_flush_int 𝒜⇩i⇩n), uncurry2 (vmtf_flush 𝒜⇩i⇩n)) ∈
   [λ((M, vm), to_r). vm ∈ vmtf 𝒜⇩i⇩n M ∧ isasat_input_bounded 𝒜⇩i⇩n ∧ isasat_input_nempty 𝒜⇩i⇩n ∧ to_r ⊆ set_mset 𝒜⇩i⇩n]⇩f
     Id ×⇩f Id ×⇩f distinct_atoms_rel 𝒜⇩i⇩n → ⟨(Id ×⇩r distinct_atoms_rel 𝒜⇩i⇩n)⟩ nres_rel›
  by (intro frefI nres_relI)
    (use in ‹auto intro!: vmtf_change_to_remove_order›)

definition (in -) isa_vmtf_unset :: ‹nat ⇒ vmtf ⇒ vmtf› where
‹isa_vmtf_unset = (λL (ns, m, fst_As, lst_As, next_search).
  (if next_search = None ∨ stamp (ns ! (the next_search)) < stamp (ns ! L)
  then ((ns, m, fst_As, lst_As, Some L))
  else ((ns, m, fst_As, lst_As, next_search))))›

definition vmtf_unset_pre where
‹vmtf_unset_pre = (λL (ns, m, fst_As, lst_As, next_search).
  L < length ns ∧ (next_search ≠ None ⟶ the next_search < length ns))›

lemma vmtf_unset_pre_vmtf:
  assumes
    ‹((ns, m, fst_As, lst_As, next_search)) ∈ vmtf 𝒜 M› and
    ‹L ∈# 𝒜›
  shows ‹vmtf_unset_pre L ((ns, m, fst_As, lst_As, next_search))›
  using assms
  by (auto simp: vmtf_def vmtf_unset_pre_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)


definition vmtf_heur_fst where
  ‹vmtf_heur_fst = (λ(_, _, a, _). a)›


subsection ‹Hash for lists›

definition atms_hash_insert_pre :: ‹nat ⇒ nat list × bool list ⇒ bool› where
‹atms_hash_insert_pre i = (λ(n, xs). i < length xs ∧ (¬xs!i ⟶ length n < 2 + unat32_max div 2))›

definition atoms_hash_insert :: ‹nat ⇒ nat list × bool list ⇒ (nat list × bool list)› where
‹atoms_hash_insert i  = (λ(n, xs). if xs ! i then (n, xs) else (n @ [i], xs[i := True]))›

end