theory Watched_Literals_VMTF imports IsaSAT_Literals begin subsection ‹Variable-Move-to-Front› subsubsection ‹Variants around head and last› definition option_hd :: ‹'a list ⇒ 'a option› where ‹option_hd xs = (if xs = [] then None else Some (hd xs))› lemma option_hd_None_iff[iff]: ‹option_hd zs = None ⟷ zs = []› ‹None = option_hd zs ⟷ zs = []› by (auto simp: option_hd_def) lemma option_hd_Some_iff[iff]: ‹option_hd zs = Some y ⟷ (zs ≠ [] ∧ y = hd zs)› ‹Some y = option_hd zs ⟷ (zs ≠ [] ∧ y = hd zs)› by (auto simp: option_hd_def) lemma option_hd_Some_hd[simp]: ‹zs ≠ [] ⟹ option_hd zs = Some (hd zs)› by (auto simp: option_hd_def) lemma option_hd_Nil[simp]: ‹option_hd [] = None› by (auto simp: option_hd_def) definition option_last where ‹option_last l = (if l = [] then None else Some (last l))› lemma option_last_None_iff[iff]: ‹option_last l = None ⟷ l = []› ‹None = option_last l ⟷ l = []› and option_last_Some_iff[iff]: ‹option_last l = Some a ⟷ l ≠ [] ∧ a = last l› ‹Some a = option_last l ⟷ l ≠ [] ∧ a = last l› by (auto simp: option_last_def) lemma option_last_Some[simp]: ‹l ≠ [] ⟹ option_last l = Some (last l)› by (auto simp: option_last_def) lemma option_last_Nil[simp]: ‹option_last [] = None› by (auto simp: option_last_def) lemma option_last_remove1_not_last: ‹x ≠ last xs ⟹ option_last xs = option_last (remove1 x xs)› by (cases xs rule: rev_cases) (auto simp: option_last_def remove1_Nil_iff remove1_append) lemma option_hd_rev: ‹option_hd (rev xs) = option_last xs› by (cases xs rule: rev_cases) auto lemma map_option_option_last: ‹map_option f (option_last xs) = option_last (map f xs)› by (cases xs rule: rev_cases) auto subsubsection ‹Specification› type_synonym 'v abs_vmtf_ns = ‹'v set × 'v set› type_synonym 'v abs_vmtf_ns_remove = ‹'v abs_vmtf_ns × '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. ▪ The atoms of \<^term>‹zs› are either in \<^term>‹xs› and \<^term>‹ys›. › definition vmtf_ℒ⇩a⇩l⇩l :: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ nat abs_vmtf_ns_remove ⇒ bool› where ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ≡ λ((xs, ys), zs). (∀L∈ys. L ∈ atm_of ` lits_of_l M) ∧ xs ∩ ys = {} ∧ zs ⊆ 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› type_synonym (in -) vmtf_remove_int = ‹vmtf × nat set› 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_remove_int set› where ‹vmtf 𝒜 M = {((ns, m, fst_As, lst_As, next_search), to_remove). (∃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'), to_remove) ∧ 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), remove) ∈ vmtf 𝒜 M› shows ‹((ns, m, fst_As, lst_As, next_search), remove) ∈ 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'), 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 𝒜 (L # M) ((set xs', set ys'), remove)› 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'), remove) ∧ 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 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), to_remove) ∈ 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'), to_remove) ∧ 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), to_remove)› 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)), to_remove)› 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), to_remove) ∈ vmtf 𝒜 M› and L: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and to_remove: ‹to_remove' ⊆ to_remove - {L}› and nempty: ‹isasat_input_nempty 𝒜› shows ‹(vmtf_en_dequeue M L (ns, m, fst_As, lst_As, next_search), to_remove') ∈ vmtf 𝒜 M› unfolding vmtf_def proof clarify fix xxs yys zzs ns' m' fst_As' lst_As' next_search' assume dequeue: ‹(ns', m', fst_As', lst_As', next_search') = vmtf_en_dequeue M L (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), to_remove)› 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'), to_remove)› 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'), to_remove') ∧ 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')), to_remove')› using abs_l to_remove 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 []), to_remove')› using abs_l to_remove 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, to_remove) ∈ vmtf 𝒜 M› and L: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and to_remove: ‹to_remove' ⊆ to_remove - {L}› and nempty: ‹isasat_input_nempty 𝒜› shows ‹(vmtf_en_dequeue M L vm, to_remove') ∈ vmtf 𝒜 M› using abs_vmtf_ns_bump_vmtf_en_dequeue assms by (cases vm) blast definition (in -) vmtf_unset :: ‹nat ⇒ vmtf_remove_int ⇒ vmtf_remove_int› where ‹vmtf_unset = (λL ((ns, m, fst_As, lst_As, next_search), to_remove). (if next_search = None ∨ stamp (ns ! (the next_search)) < stamp (ns ! L) then ((ns, m, fst_As, lst_As, Some L), to_remove) else ((ns, m, fst_As, lst_As, next_search), to_remove)))› 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'), to_remove)› 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 vmtf_ℒ⇩a⇩l⇩l_to_remove_mono: assumes ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((a, b), to_remove)› and ‹to_remove' ⊆ to_remove› shows ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((a, b), to_remove')› using assms unfolding vmtf_ℒ⇩a⇩l⇩l_def by (auto simp: mset_subset_eqD) lemma abs_vmtf_ns_unset_vmtf_unset: assumes vmtf:‹((ns, m, fst_As, lst_As, next_search), to_remove) ∈ vmtf 𝒜 M› and L_N: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and to_remove: ‹to_remove' ⊆ to_remove› shows ‹(vmtf_unset L ((ns, m, fst_As, lst_As, next_search), to_remove')) ∈ 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'), 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_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' to_remove'' lst_As' where S: ‹?S = ((ns', m', fst_As', lst_As', next_search'), to_remove'')› 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'), to_remove'') ∧ 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) have abs_vmtf: ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set xs', set ys'), to_remove'')› apply (rule vmtf_ℒ⇩a⇩l⇩l_to_remove_mono) apply (rule abs_vmtf) using to_remove S unfolding vmtf_unset_def by (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 to_remove 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› ‹to_remove'' = to_remove'› ‹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'), to_remove)› using abs_vmtf vmtf_ns_distinct[OF vmtf_ns] unfolding vmtf_ℒ⇩a⇩l⇩l_def ys'_y_x by auto then have ‹vmtf_ℒ⇩a⇩l⇩l 𝒜 M ((set ?xs', set ?ys'), to_remove')› by (rule vmtf_ℒ⇩a⇩l⇩l_to_remove_mono) (use to_remove in 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 ≤ uint64_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), to_remove) ∈ vmtf 𝒜 M› and i: ‹A ∈ to_remove› and m_le: ‹m + 1 ≤ uint64_max› and nempty: ‹isasat_input_nempty 𝒜› 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'), 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_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 i 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 i 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, to_remove) ∈ vmtf 𝒜 M› and i: ‹A ∈ to_remove› and ‹fst (snd vm) + 1 ≤ uint64_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), to_remove) ∈ 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'), to_remove)› 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), to_remove) ∈ 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)), to_remove) ∈ 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'), to_remove)› 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'), to_remove)› 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'), to_remove) ∧ 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_remove_int ⇒ (nat, nat) ann_lits ⇒ (nat option) nres› where ‹vmtf_find_next_undef 𝒜 = (λ((ns, m, fst_As, lst_As, next_search), to_remove) M. do { WHILE⇩T⇗λnext_search. ((ns, m, fst_As, lst_As, next_search), to_remove) ∈ 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), to_remove) ∈ vmtf 𝒜 M› shows ‹vmtf_find_next_undef 𝒜 ((ns, m, fst_As, lst_As, next_search), to_remove) M ≤ ⇓ Id (SPEC (λL. ((ns, m, fst_As, lst_As, L), to_remove) ∈ 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'), to_remove)› 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), remove) ∈ 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), remove) ∈ 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), remove) ∈ 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 definition vmtf_mark_to_rescore :: ‹nat ⇒ vmtf_remove_int ⇒ vmtf_remove_int› where ‹vmtf_mark_to_rescore L = (λ((ns, m, fst_As, next_search), to_remove). ((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), remove) ∈ 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), remove)) ∈ 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'), remove)› 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' remove'' lst_As' where S: ‹?S = ((ns', m', fst_As', lst_As', next_search'), remove'')› 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 [simp]: ‹remove'' = remove› using S unfolding vmtf_unset_def by (auto split: if_splits) 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'), remove'') ∧ 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'), remove)› 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'), remove)› 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'), remove)› 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 definition vmtf_mark_to_rescore_and_unset :: ‹nat ⇒ vmtf_remove_int ⇒ vmtf_remove_int› 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), to_remove) ∈ 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'), to_remove)› 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 ≤ uint32_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, to_remove) ∈ vmtf 𝒜 M› and nempty: ‹isasat_input_nempty 𝒜› and bounded: ‹isasat_input_bounded 𝒜› shows ‹vmtf_rescale vm ≤ SPEC (λvm. (vm, to_remove) ∈ vmtf 𝒜 M ∧ fst (snd vm) ≤ uint32_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'), to_remove)› 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 < uint32_max› using vmtf_ns_distinct[OF vmtf_ns] using simple_clss_size_upper_div2[OF bounded lits dist tauto] by (auto simp: uint32_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 ≤ uint32_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), to_remove) ∈ 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 ≤ uint32_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_remove_int ⇒ vmtf_remove_int nres› where ‹vmtf_flush 𝒜⇩i⇩n = (λM (vm, to_remove). RES (vmtf 𝒜⇩i⇩n M))› 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 :: ‹nat multiset ⇒ (('v list × 'v set) × 'v set) set› where ‹distinct_hash_atoms_rel 𝒜 = {((C, h), D). set C = D ∧ h = D ∧ distinct C}› 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 ≤ uint32_max); to_remove' ← reorder_list vm to_remove; ASSERT(length to_remove' ≤ uint32_max); vm ← (if length to_remove' + fst (snd vm) ≥ uint64_max then vmtf_rescale vm else RETURN vm); ASSERT(length to_remove' + fst (snd vm) ≤ uint64_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), to_remove) ∈ 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› 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), to_remove)› have vmtf_flush_alt_def: ‹vmtf_flush 𝒜⇩i⇩n M ?vm = do { _ ← RETURN (); _ ← RETURN (); vm ← RES(vmtf 𝒜⇩i⇩n M); RETURN (vm) }› unfolding vmtf_flush_def by (auto simp: RES_RES_RETURN_RES RES_RETURN_RES vmtf) have pre_sort: ‹∀x∈set x1a. x < length (fst x1)› 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 vmtf CD_rem that by (auto simp: vmtf_def vmtf_ℒ⇩a⇩l⇩l_def distinct_atoms_rel_alt_def) qed have length_le: ‹length x1a ≤ uint32_max› 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)› 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 unfolding vmtf_def vmtf_ℒ⇩a⇩l⇩l_def by (auto simp: literals_are_in_ℒ⇩i⇩n_alt_def distinct_atoms_rel_alt_def inj_on_def) 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: uint32_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 uint64_max ≤ length to_remove' + fst (snd x1) then vmtf_rescale x1 else RETURN x1) ≤ SPEC (λc. (c, ()) ∈ {(vm ,vm'). uint64_max ≥ length to_remove' + fst (snd vm) ∧ (vm, set to_remove') ∈ 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 ≤ uint32_max› and ‹(to_remove', uu) ∈ ?reorder_list› and ‹length to_remove' ≤ uint32_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 _ to_remove 𝒜⇩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: uint64_max_def uint32_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} (RES (vmtf 𝒜⇩i⇩n M))› if x2: ‹x2 = (x1a, x2a)› and CD: ‹((ns, m, fst_As, lst_As, next_search), C, D) = (x1', x2)› 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, set (drop i to_remove')) ∈ vmtf 𝒜⇩i⇩n M› have [simp]: ‹x2 = (C, D)› ‹x1' = (ns, m, fst_As, lst_As, next_search)› ‹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'] by (auto simp: vmtf_def vmtf_ℒ⇩a⇩l⇩l_def) have bound: ‹fst (snd x1) + 1 ≤ uint64_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 _ ‹set to_remove'›]) using rel vmtf to_rem that x1 bound nempty 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 vmtf by (auto simp: distinct_atoms_rel_def I'_def) 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, set (drop x2 to_remove')) ∈ 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, ?x2a'- {to_remove' ! x2}) ∈ vmtf 𝒜⇩i⇩n M› by (rule abs_vmtf_ns_bump_vmtf_en_dequeue'[OF vm in_lall[OF le]]) (use nempty in auto) have 2: ‹to_remove' ! Suc x2 ∈ ?x2a'- {to_remove' ! x2}› if ‹Suc x2 < length to_remove'› using I I' le dist that x1aa unfolding I_def I'_def by (auto simp: distinct_atoms_rel_alt_def in_set_drop_conv_nth I'_def nth_eq_iff_index_eq x2 intro: bex_geI[of _ ‹Suc x2›]) have 3: ‹fst (snd x2aa) = fst (snd x1) + x2› using I I' le dist that CD[unfolded x2] x2a' unfolding I_def I'_def x2 x2a' x1aa by (auto simp: distinct_atoms_rel_def in_set_drop_conv_nth I'_def nth_eq_iff_index_eq x2 intro: bex_geI[of _ ‹Suc x2›]) then have 4: ‹fst (snd (vmtf_en_dequeue M (to_remove' ! x2) x2aa)) + 1 ≤ uint64_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 2, rule that, rule 4[OF that], rule nempty) have 3: ‹(vmtf_en_dequeue M (to_remove' ! x2) x2aa, ?x2a' - {to_remove' ! x2}) ∈ 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, set (drop (Suc x2) to_remove')) ∈ 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 x2 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} (RES (vmtf 𝒜⇩i⇩n M))› 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 apply (assumption+)[5] subgoal by auto apply (rule loop_ref; assumption) subgoal by (auto simp: emptied_list_def) done qed lemma vmtf_change_to_remove_order': ‹(uncurry (vmtf_flush_int 𝒜⇩i⇩n), uncurry (vmtf_flush 𝒜⇩i⇩n)) ∈ [λ(M, vm). vm ∈ vmtf 𝒜⇩i⇩n M ∧ isasat_input_bounded 𝒜⇩i⇩n ∧ isasat_input_nempty 𝒜⇩i⇩n]⇩f Id ×⇩r (Id ×⇩r distinct_atoms_rel 𝒜⇩i⇩n) → ⟨(Id ×⇩r distinct_atoms_rel 𝒜⇩i⇩n)⟩ nres_rel› by (intro frefI nres_relI) (use vmtf_change_to_remove_order in auto) subsection ‹Phase saving› type_synonym phase_saver = ‹bool list› definition phase_saving :: ‹nat multiset ⇒ phase_saver ⇒ bool› where ‹phase_saving 𝒜 φ ⟷ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length φ)› text ‹Save phase as given (e.g. for literals in the trail):› definition save_phase :: ‹nat literal ⇒ phase_saver ⇒ phase_saver› where ‹save_phase L φ = φ[atm_of L := is_pos L]› lemma phase_saving_save_phase[simp]: ‹phase_saving 𝒜 (save_phase L φ) ⟷ phase_saving 𝒜 φ› by (auto simp: phase_saving_def save_phase_def) text ‹Save opposite of the phase (e.g. for literals in the conflict clause):› definition save_phase_inv :: ‹nat literal ⇒ phase_saver ⇒ phase_saver› where ‹save_phase_inv L φ = φ[atm_of L := ¬is_pos L]› end