# Theory Interleaving

```(* Martin Kleppmann, University of Cambridge
Victor B. F. Gomes, University of Cambridge
Dominic P. Mulligan, Arm Research, Cambridge
Alastair Beresford, University of Cambridge
*)

section‹Interleaving of concurrent insertions›

text‹In this section we prove that our list specification rules out
interleaving of concurrent insertion sequences starting at the same position.›

theory Interleaving
imports Insert_Spec
begin

lemma map_fst_append1:
assumes "∀i ∈ set (map fst xs). P i"
and "P x"
shows "∀i ∈ set (map fst (xs @ [(x, y)])). P i"
using assms by (induction xs, auto)

lemma insert_ops_split:
assumes "insert_ops ops"
and "(oid, ref) ∈ set ops"
shows "∃pre suf. ops = pre @ [(oid, ref)] @ suf ∧
(∀i ∈ set (map fst pre). i < oid) ∧
(∀i ∈ set (map fst suf). oid < i)"
using assms proof(induction ops rule: List.rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
then show ?case
proof(cases "x = (oid, ref)")
case True
moreover from this have "∀i ∈ set (map fst xs). i < oid"
using last_op_greatest snoc.prems(1) by blast
ultimately have "xs @ [x] = xs @ [(oid, ref)] @ [] ∧
(∀i ∈ set (map fst xs). i < oid) ∧
(∀i ∈ set (map fst []). oid < i)"
by auto
then show ?thesis by force
next
case False
hence "(oid, ref) ∈ set xs"
using snoc.prems(2) by auto
from this obtain pre suf where IH: "xs = pre @ [(oid, ref)] @ suf ∧
(∀i ∈ set (map fst pre). i < oid) ∧
(∀i ∈ set (map fst suf). oid < i)"
using snoc.IH snoc.prems(1) by blast
obtain xi xr where x_pair: "x = (xi, xr)"
by force
hence "distinct (map fst (pre @ [(oid, ref)] @ suf @ [(xi, xr)]))"
by (metis IH append.assoc insert_ops_def spec_ops_def snoc.prems(1))
hence "xi ≠ oid"
by auto
have xi_max: "∀x ∈ set (map fst (pre @ [(oid, ref)] @ suf)). x < xi"
using IH last_op_greatest snoc.prems(1) x_pair by blast
then show ?thesis
proof(cases "xi < oid")
case True
moreover from this have "∀x ∈ set suf. fst x < oid"
using xi_max by auto
hence "suf = []"
using IH last_in_set by fastforce
ultimately have "xs @ [x] = (pre @ [(xi, xr)]) @ [] ∧
(∀i ∈ set (map fst ((pre @ [(xi, xr)]))). i < oid) ∧
(∀i ∈ set (map fst []). oid < i)"
using dual_order.asym xi_max by auto
then show ?thesis by (simp add: IH)
next
case False
hence "oid < xi"
using ‹xi ≠ oid› by auto
hence "∀i ∈ set (map fst (suf @ [(xi, xr)])). oid < i"
using IH map_fst_append1 by auto
hence "xs @ [x] = pre @ [(oid, ref)] @ (suf @ [(xi, xr)]) ∧
(∀i ∈ set (map fst pre). i < oid) ∧
(∀i ∈ set (map fst (suf @ [(xi, xr)])). oid < i)"
then show ?thesis by blast
qed
qed
qed

lemma insert_ops_split_2:
assumes "insert_ops ops"
and "(xid, xr) ∈ set ops"
and "(yid, yr) ∈ set ops"
and "xid < yid"
shows "∃as bs cs. ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs ∧
(∀i ∈ set (map fst as). i < xid) ∧
(∀i ∈ set (map fst bs). xid < i ∧ i < yid) ∧
(∀i ∈ set (map fst cs). yid < i)"
proof -
obtain as as1 where x_split: "ops = as @ [(xid, xr)] @ as1 ∧
(∀i ∈ set (map fst as). i < xid) ∧ (∀i ∈ set (map fst as1). xid < i)"
using assms insert_ops_split by blast
hence "insert_ops ((as @ [(xid, xr)]) @ as1)"
using assms(1) by auto
hence "insert_ops as1"
using assms(1) insert_ops_rem_prefix by blast
have "(yid, yr) ∈ set as1"
using x_split assms by auto
from this obtain bs cs where y_split: "as1 = bs @ [(yid, yr)] @ cs ∧
(∀i ∈ set (map fst bs). i < yid) ∧ (∀i ∈ set (map fst cs). yid < i)"
using assms insert_ops_split ‹insert_ops as1› by blast
hence "ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs"
using x_split by blast
moreover have "∀i ∈ set (map fst bs). xid < i ∧ i < yid"
ultimately show ?thesis
using x_split y_split by blast
qed

lemma insert_ops_sorted_oids:
assumes "insert_ops (xs @ [(i1, r1)] @ ys @ [(i2, r2)])"
shows "i1 < i2"
proof -
have "⋀i. i ∈ set (map fst (xs @ [(i1, r1)] @ ys)) ⟹ i < i2"
by (metis append.assoc assms last_op_greatest)
moreover have "i1 ∈ set (map fst (xs @ [(i1, r1)] @ ys))"
by auto
ultimately show "i1 < i2"
by blast
qed

lemma insert_ops_subset_last:
assumes "insert_ops (xs @ [x])"
and "insert_ops ys"
and "set ys ⊆ set (xs @ [x])"
and "x ∈ set ys"
shows "x = last ys"
using assms proof(induction ys, simp)
case (Cons y ys)
then show "x = last (y # ys)"
proof(cases "ys = []")
case True
then show "x = last (y # ys)"
using Cons.prems(4) by auto
next
case ys_nonempty: False
have "x ≠ y"
proof -
obtain mid l where "ys = mid @ [l]"
using append_butlast_last_id ys_nonempty by metis
moreover obtain li lr where "l = (li, lr)"
by force
moreover have "⋀i. i ∈ set (map fst (y # mid)) ⟹ i < li"
by (metis last_op_greatest Cons.prems(2) calculation append_Cons)
hence "fst y < li"
by simp
moreover have "⋀i. i ∈ set (map fst xs) ⟹ i < fst x"
using assms(1) last_op_greatest by (metis prod.collapse)
hence "⋀i. i ∈ set (map fst (y # ys)) ⟹ i ≤ fst x"
using Cons.prems(3) by fastforce
ultimately show "x ≠ y"
by fastforce
qed
then show "x = last (y # ys)"
using Cons.IH Cons.prems insert_ops_rem_cons ys_nonempty
by (metis dual_order.trans last_ConsR set_ConsD set_subset_Cons)
qed
qed

lemma subset_butlast:
assumes "set xs ⊆ set (ys @ [y])"
and "last xs = y"
and "distinct xs"
shows "set (butlast xs) ⊆ set ys"
using assms by (induction xs, auto)

lemma distinct_append_butlast1:
assumes "distinct (map fst xs @ map fst ys)"
shows "distinct (map fst (butlast xs) @ map fst ys)"
using assms proof(induction xs, simp)
case (Cons a xs)
have "fst a ∉ set (map fst xs @ map fst ys)"
using Cons.prems by auto
moreover have "set (map fst (butlast xs)) ⊆ set (map fst xs)"
by (metis in_set_butlastD map_butlast subsetI)
hence "set (map fst (butlast xs) @ map fst ys) ⊆ set (map fst xs @ map fst ys)"
by auto
ultimately have "fst a ∉ set (map fst (butlast xs) @ map fst ys)"
by blast
then show "distinct (map fst (butlast (a # xs)) @ map fst ys)"
using Cons.IH Cons.prems by auto
qed

lemma distinct_append_butlast2:
assumes "distinct (map fst xs @ map fst ys)"
shows "distinct (map fst xs @ map fst (butlast ys))"
using assms proof(induction xs)
case Nil
then show "distinct (map fst [] @ map fst (butlast ys))"
next
case (Cons a xs)
have "fst a ∉ set (map fst xs @ map fst ys)"
using Cons.prems by auto
moreover have "set (map fst (butlast ys)) ⊆ set (map fst ys)"
by (metis in_set_butlastD map_butlast subsetI)
hence "set (map fst xs @ map fst (butlast ys)) ⊆ set (map fst xs @ map fst ys)"
by auto
ultimately have "fst a ∉ set (map fst xs @ map fst (butlast ys))"
by blast
then show ?case
using Cons.IH Cons.prems by auto
qed

lemma interp_ins_maybe_grow:
assumes "insert_ops (xs @ [(oid, ref)])"
shows "set (interp_ins (xs @ [(oid, ref)])) = set (interp_ins xs) ∨
set (interp_ins (xs @ [(oid, ref)])) = (set (interp_ins xs) ∪ {oid})"
by (cases ref, simp add: interp_ins_tail_unfold,
metis insert_spec_nonex insert_spec_set interp_ins_tail_unfold)

lemma interp_ins_maybe_grow2:
assumes "insert_ops (xs @ [x])"
shows "set (interp_ins (xs @ [x])) = set (interp_ins xs) ∨
set (interp_ins (xs @ [x])) = (set (interp_ins xs) ∪ {fst x})"
using assms interp_ins_maybe_grow by (cases x, auto)

lemma interp_ins_maybe_grow3:
assumes "insert_ops (xs @ ys)"
shows "∃A. A ⊆ set (map fst ys) ∧ set (interp_ins (xs @ ys)) = set (interp_ins xs) ∪ A"
using assms proof(induction ys rule: List.rev_induct)
case Nil
then show ?case by simp
next
case (snoc x ys)
then have "insert_ops (xs @ ys)"
by (metis append_assoc insert_ops_rem_last)
then obtain A where IH: "A ⊆ set (map fst ys) ∧
set (interp_ins (xs @ ys)) = set (interp_ins xs) ∪ A"
using snoc.IH by blast
then show ?case
proof(cases "set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))")
case True
moreover have "A ⊆ set (map fst (ys @ [x]))"
using IH by auto
ultimately show ?thesis
using IH by auto
next
case False
then have "set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) ∪ {fst x}"
by (metis append_assoc interp_ins_maybe_grow2 snoc.prems)
moreover have "A ∪ {fst x} ⊆ set (map fst (ys @ [x]))"
using IH by auto
ultimately show ?thesis
using IH Un_assoc by metis
qed
qed

lemma interp_ins_ref_nonex:
assumes "insert_ops ops"
and "ops = xs @ [(oid, Some ref)] @ ys"
and "ref ∉ set (interp_ins xs)"
shows "oid ∉ set (interp_ins ops)"
using assms proof(induction ys arbitrary: ops rule: List.rev_induct)
case Nil
then have "interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)"
moreover have "⋀i. i ∈ set (map fst xs) ⟹ i < oid"
using Nil.prems last_op_greatest by fastforce
hence "⋀i. i ∈ set (interp_ins xs) ⟹ i < oid"
by (meson interp_ins_subset subsetCE)
ultimately show "oid ∉ set (interp_ins ops)"
using assms(3) by auto
next
case (snoc x ys)
then have "insert_ops (xs @ (oid, Some ref) # ys)"
by (metis append.assoc append.simps(1) append_Cons insert_ops_appendD)
hence IH: "oid ∉ set (interp_ins (xs @ (oid, Some ref) # ys))"
moreover have "distinct (map fst (xs @ (oid, Some ref) # ys @ [x]))"
using snoc.prems by (metis append_Cons append_self_conv2 insert_ops_def spec_ops_def)
hence "fst x ≠ oid"
using empty_iff by auto
moreover have "insert_ops ((xs @ (oid, Some ref) # ys) @ [x])"
using snoc.prems by auto
hence "set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) =
set (interp_ins (xs @ (oid, Some ref) # ys)) ∨
set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) =
set (interp_ins (xs @ (oid, Some ref) # ys)) ∪ {fst x}"
using interp_ins_maybe_grow2 by blast
ultimately show "oid ∉ set (interp_ins ops)"
using snoc.prems(2) by auto
qed

lemma interp_ins_last_None:
shows "oid ∈ set (interp_ins (ops @ [(oid, None)]))"

lemma interp_ins_monotonic:
assumes "insert_ops (pre @ suf)"
and "oid ∈ set (interp_ins pre)"
shows "oid ∈ set (interp_ins (pre @ suf))"
using assms interp_ins_maybe_grow3 by auto

lemma interp_ins_append_non_memb:
assumes "insert_ops (pre @ [(oid, Some ref)] @ suf)"
and "ref ∉ set (interp_ins pre)"
shows "ref ∉ set (interp_ins (pre @ [(oid, Some ref)] @ suf))"
using assms proof(induction suf rule: List.rev_induct)
case Nil
then show "ref ∉ set (interp_ins (pre @ [(oid, Some ref)] @ []))"
by (metis append_Nil2 insert_spec_nonex interp_ins_tail_unfold)
next
case (snoc x xs)
hence IH: "ref ∉ set (interp_ins (pre @ [(oid, Some ref)] @ xs))"
by (metis append_assoc insert_ops_rem_last)
moreover have "ref < oid"
using insert_ops_ref_older snoc.prems(1) by auto
moreover have "oid < fst x"
using insert_ops_sorted_oids by (metis prod.collapse snoc.prems(1))
have "set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) =
set (interp_ins (pre @ [(oid, Some ref)] @ xs)) ∨
set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) =
set (interp_ins (pre @ [(oid, Some ref)] @ xs)) ∪ {fst x}"
by (metis (full_types) append.assoc interp_ins_maybe_grow2 snoc.prems(1))
ultimately show "ref ∉ set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))"
using ‹oid < fst x› by auto
qed

lemma interp_ins_append_memb:
assumes "insert_ops (pre @ [(oid, Some ref)] @ suf)"
and "ref ∈ set (interp_ins pre)"
shows "oid ∈ set (interp_ins (pre @ [(oid, Some ref)] @ suf))"
using assms by (metis UnCI append_assoc insert_spec_set interp_ins_monotonic
interp_ins_tail_unfold singletonI)

lemma interp_ins_append_forward:
assumes "insert_ops (xs @ ys)"
and "oid ∈ set (interp_ins (xs @ ys))"
and "oid ∈ set (map fst xs)"
shows "oid ∈ set (interp_ins xs)"
using assms proof(induction ys rule: List.rev_induct, simp)
case (snoc y ys)
obtain cs ds ref where "xs = cs @ (oid, ref) # ds"
by (metis (no_types, lifting) imageE prod.collapse set_map snoc.prems(3) split_list_last)
hence "insert_ops (cs @ [(oid, ref)] @ (ds @ ys) @ [y])"
using snoc.prems(1) by auto
hence "oid < fst y"
using insert_ops_sorted_oids by (metis prod.collapse)
hence "oid ≠ fst y"
by blast
then show ?case
using snoc.IH snoc.prems(1) snoc.prems(2) assms(3) inserted_item_ident
by (metis append_assoc insert_ops_appendD interp_ins_tail_unfold prod.collapse)
qed

lemma interp_ins_find_ref:
assumes "insert_ops (xs @ [(oid, Some ref)] @ ys)"
and "ref ∈ set (interp_ins (xs @ [(oid, Some ref)] @ ys))"
shows "∃r. (ref, r) ∈ set xs"
proof -
have "ref < oid"
using assms(1) insert_ops_ref_older by blast
have "ref ∈ set (map fst (xs @ [(oid, Some ref)] @ ys))"
by (meson assms(2) interp_ins_subset subsetCE)
then obtain x where x_prop: "x ∈ set (xs @ [(oid, Some ref)] @ ys) ∧ fst x = ref"
by fastforce
obtain xr where x_pair: "x = (ref, xr)"
using prod.exhaust_sel x_prop by blast
show "∃r. (ref, r) ∈ set xs"
proof(cases "x ∈ set xs")
case True
then show "∃r. (ref, r) ∈ set xs"
by (metis x_prop prod.collapse)
next
case False
hence "(ref, xr) ∈ set ([(oid, Some ref)] @ ys)"
using x_prop x_pair by auto
hence "(ref, xr) ∈ set ys"
using ‹ref < oid› x_prop
by (metis append_Cons append_self_conv2 fst_conv min.strict_order_iff set_ConsD)
then obtain as bs where "ys = as @ (ref, xr) # bs"
by (meson split_list)
hence "insert_ops ((xs @ [(oid, Some ref)] @ as @ [(ref, xr)]) @ bs)"
using assms(1) by auto
hence "insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])"
using insert_ops_appendD by blast
hence "oid < ref" (* contradiction *)
using insert_ops_sorted_oids by auto
then show ?thesis
using ‹ref < oid› by force
qed
qed

lemma list_order_append:
assumes "insert_ops (pre @ suf)"
and "list_order pre x y"
shows "list_order (pre @ suf) x y"
by (metis Un_iff assms list_order_monotonic insert_ops_appendD set_append subset_code(1))

lemma list_order_insert_ref:
assumes "insert_ops (ops @ [(oid, Some ref)])"
and "ref ∈ set (interp_ins ops)"
shows "list_order (ops @ [(oid, Some ref)]) ref oid"
proof -
have "interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)"
moreover obtain xs ys where "interp_ins ops = xs @ [ref] @ ys"
using assms(2) split_list_first by fastforce
hence "insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys"
using assms(1) insert_after_ref interp_ins_distinct by fastforce
ultimately show "list_order (ops @ [(oid, Some ref)]) ref oid"
using assms(1) list_orderI by metis
qed

lemma list_order_insert_none:
assumes "insert_ops (ops @ [(oid, None)])"
and "x ∈ set (interp_ins ops)"
shows "list_order (ops @ [(oid, None)]) oid x"
proof -
have "interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)"
moreover obtain xs ys where "interp_ins ops = xs @ [x] @ ys"
using assms(2) split_list_first by fastforce
hence "insert_spec (interp_ins ops) (oid, None) = [] @ [oid] @ xs @ [x] @ ys"
by simp
ultimately show "list_order (ops @ [(oid, None)]) oid x"
using assms(1) list_orderI by metis
qed

lemma list_order_insert_between:
assumes "insert_ops (ops @ [(oid, Some ref)])"
and "list_order ops ref x"
shows "list_order (ops @ [(oid, Some ref)]) oid x"
proof -
have "interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)"
moreover obtain xs ys zs where "interp_ins ops = xs @ [ref] @ ys @ [x] @ zs"
using assms list_orderE by blast
moreover have "... = xs @ ref # (ys @ [x] @ zs)"
by simp
moreover have "distinct (xs @ ref # (ys @ [x] @ zs))"
using assms(1) calculation by (metis interp_ins_distinct insert_ops_rem_last)
hence "insert_spec (xs @ ref # (ys @ [x] @ zs)) (oid, Some ref) = xs @ ref # oid # (ys @ [x] @ zs)"
using assms(1) calculation by (simp add: insert_after_ref)
moreover have "... = (xs @ [ref]) @ [oid] @ ys @ [x] @ zs"
by simp
ultimately show "list_order (ops @ [(oid, Some ref)]) oid x"
using assms(1) list_orderI by metis
qed

subsection‹The \isa{insert-seq} predicate›

text‹The predicate \isa{insert-seq start ops} is true iff \isa{ops} is a list
of insertion operations that begins by inserting after \isa{start}, and then
continues by placing each subsequent insertion directly after its predecessor.
This definition models the sequential insertion of text at a particular place
in a text document.›

inductive insert_seq :: "'oid option ⇒ ('oid × 'oid option) list ⇒ bool" where
"insert_seq start [(oid, start)]" |
"⟦insert_seq start (list @ [(prev, ref)])⟧
⟹ insert_seq start (list @ [(prev, ref), (oid, Some prev)])"

lemma insert_seq_nonempty:
assumes "insert_seq start xs"
shows "xs ≠ []"
using assms by (induction rule: insert_seq.induct, auto)

lemma insert_seq_hd:
assumes "insert_seq start xs"
shows "∃oid. hd xs = (oid, start)"
using assms by (induction rule: insert_seq.induct, simp,
metis append_self_conv2 hd_append2 list.sel(1))

lemma insert_seq_rem_last:
assumes "insert_seq start (xs @ [x])"
and "xs ≠ []"
shows "insert_seq start xs"
using assms insert_seq.cases by fastforce

lemma insert_seq_butlast:
assumes "insert_seq start xs"
and "xs ≠ []" and "xs ≠ [last xs]"
shows "insert_seq start (butlast xs)"
proof -
have "length xs > 1"
by (metis One_nat_def Suc_lessI add_0_left append_butlast_last_id append_eq_append_conv
append_self_conv2 assms(2) assms(3) length_greater_0_conv list.size(3) list.size(4))
hence "butlast xs ≠ []"
by (metis length_butlast less_numeral_extra(3) list.size(3) zero_less_diff)
then show "insert_seq start (butlast xs)"
using assms by (metis append_butlast_last_id insert_seq_rem_last)
qed

lemma insert_seq_last_ref:
assumes "insert_seq start (xs @ [(xi, xr), (yi, yr)])"
shows "yr = Some xi"
using assms insert_seq.cases by fastforce

lemma insert_seq_start_none:
assumes "insert_ops ops"
and "insert_seq None xs" and "insert_ops xs"
and "set xs ⊆ set ops"
shows "∀i ∈ set (map fst xs). i ∈ set (interp_ins ops)"
using assms proof(induction xs rule: List.rev_induct, simp)
case (snoc x xs)
then have IH: "∀i ∈ set (map fst xs). i ∈ set (interp_ins ops)"
by (metis Nil_is_map_conv append_is_Nil_conv insert_ops_appendD insert_seq_rem_last
le_supE list.simps(3) set_append split_list)
then show "∀i ∈ set (map fst (xs @ [x])). i ∈ set (interp_ins ops)"
proof(cases "xs = []")
case True
then obtain oid where "xs @ [x] = [(oid, None)]"
using insert_seq_hd snoc.prems(2) by fastforce
hence "(oid, None) ∈ set ops"
using snoc.prems(4) by auto
then obtain as bs where "ops = as @ (oid, None) # bs"
by (meson split_list)
hence "ops = (as @ [(oid, None)]) @ bs"
by (simp add: ‹ops = as @ (oid, None) # bs›)
moreover have "oid ∈ set (interp_ins (as @ [(oid, None)]))"
ultimately have "oid ∈ set (interp_ins ops)"
using interp_ins_monotonic snoc.prems(1) by blast
then show "∀i ∈ set (map fst (xs @ [x])). i ∈ set (interp_ins ops)"
using ‹xs @ [x] = [(oid, None)]› by auto
next
case False
then obtain rest y where snoc_y: "xs = rest @ [y]"
using append_butlast_last_id by metis
obtain yi yr xi xr where yx_pairs: "y = (yi, yr) ∧ x = (xi, xr)"
by force
then have "xr = Some yi"
using insert_seq_last_ref snoc.prems(2) snoc_y by fastforce
have "yi < xi"
using insert_ops_sorted_oids snoc_y yx_pairs snoc.prems(3)
by (metis (no_types, lifting) append_eq_append_conv2)
have "(yi, yr) ∈ set ops" and "(xi, Some yi) ∈ set ops"
using snoc.prems(4) snoc_y yx_pairs ‹xr = Some yi› by auto
then obtain as bs cs where ops_split: "ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs"
using insert_ops_split_2 ‹yi < xi› snoc.prems(1) by blast
hence "yi ∈ set (interp_ins (as @ [(yi, yr)] @ bs))"
proof -
have "yi ∈ set (interp_ins ops)"
by (simp add: IH snoc_y yx_pairs)
moreover have "ops = (as @ [(yi, yr)] @ bs) @ ([(xi, Some yi)] @ cs)"
using ops_split by simp
moreover have "yi ∈ set (map fst (as @ [(yi, yr)] @ bs))"
by simp
ultimately show ?thesis
using snoc.prems(1) interp_ins_append_forward by blast
qed
hence "xi ∈ set (interp_ins ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs))"
using snoc.prems(1) interp_ins_append_memb ops_split by force
hence "xi ∈ set (interp_ins ops)"
then show "∀i ∈ set (map fst (xs @ [x])). i ∈ set (interp_ins ops)"
using IH yx_pairs by auto
qed
qed

lemma insert_seq_after_start:
assumes "insert_ops ops"
and "insert_seq (Some ref) xs" and "insert_ops xs"
and "set xs ⊆ set ops"
and "ref ∈ set (interp_ins ops)"
shows "∀i ∈ set (map fst xs). list_order ops ref i"
using assms proof(induction xs rule: List.rev_induct, simp)
case (snoc x xs)
have IH: "∀i ∈ set (map fst xs). list_order ops ref i"
using snoc.IH snoc.prems insert_seq_rem_last insert_ops_appendD
by (metis Nil_is_map_conv Un_subset_iff empty_set equals0D set_append)
moreover have "list_order ops ref (fst x)"
proof(cases "xs = []")
case True
hence "snd x = Some ref"
using insert_seq_hd snoc.prems(2) by fastforce
moreover have "x ∈ set ops"
using snoc.prems(4) by auto
then obtain cs ds where x_split: "ops = cs @ x # ds"
by (meson split_list)
have "list_order (cs @ [(fst x, Some ref)]) ref (fst x)"
proof -
have "insert_ops (cs @ [(fst x, Some ref)] @ ds)"
using x_split ‹snd x = Some ref›
by (metis append_Cons append_self_conv2 prod.collapse snoc.prems(1))
moreover from this obtain rr where "(ref, rr) ∈ set cs"
using interp_ins_find_ref x_split ‹snd x = Some ref› assms(5)
by (metis (no_types, lifting) append_Cons append_self_conv2 prod.collapse)
hence "ref ∈ set (interp_ins cs)"
proof -
have "ops = cs @ ([(fst x, Some ref)] @ ds)"
by (metis x_split ‹snd x = Some ref› append_Cons append_self_conv2 prod.collapse)
thus "ref ∈ set (interp_ins cs)"
using assms(5) calculation interp_ins_append_forward interp_ins_append_non_memb by blast
qed
ultimately show "list_order (cs @ [(fst x, Some ref)]) ref (fst x)"
using list_order_insert_ref by (metis append.assoc insert_ops_appendD)
qed
moreover have "ops = (cs @ [(fst x, Some ref)]) @ ds"
using calculation x_split
by (metis append_eq_Cons_conv append_eq_append_conv2 append_self_conv2 prod.collapse)
ultimately show "list_order ops ref (fst x)"
using list_order_append snoc.prems(1) by blast
next
case False
then obtain rest y where snoc_y: "xs = rest @ [y]"
using append_butlast_last_id by metis
obtain yi yr xi xr where yx_pairs: "y = (yi, yr) ∧ x = (xi, xr)"
by force
then have "xr = Some yi"
using insert_seq_last_ref snoc.prems(2) snoc_y by fastforce
have "yi < xi"
using insert_ops_sorted_oids snoc_y yx_pairs snoc.prems(3)
by (metis (no_types, lifting) append_eq_append_conv2)
have "(yi, yr) ∈ set ops" and "(xi, Some yi) ∈ set ops"
using snoc.prems(4) snoc_y yx_pairs ‹xr = Some yi› by auto
then obtain as bs cs where ops_split: "ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs"
using insert_ops_split_2 ‹yi < xi› snoc.prems(1) by blast
have "list_order ops ref yi"
by (simp add: IH snoc_y yx_pairs)
moreover have "list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi"
proof -
have "insert_ops ((as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) @ cs)"
using ops_split snoc.prems(1) by auto
hence "insert_ops ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)])"
using insert_ops_appendD by fastforce
moreover have "yi ∈ set (interp_ins ops)"
using ‹list_order ops ref yi› list_order_memb2 by auto
hence "yi ∈ set (interp_ins (as @ [(yi, yr)] @ bs))"
using interp_ins_append_non_memb ops_split snoc.prems(1) by force
ultimately show ?thesis
using list_order_insert_ref by force
qed
hence "list_order ops yi xi"
by (metis append_assoc list_order_append ops_split snoc.prems(1))
ultimately show "list_order ops ref (fst x)"
using list_order_trans snoc.prems(1) yx_pairs by auto
qed
ultimately show "∀i ∈ set (map fst (xs @ [x])). list_order ops ref i"
by auto
qed

lemma insert_seq_no_start:
assumes "insert_ops ops"
and "insert_seq (Some ref) xs" and "insert_ops xs"
and "set xs ⊆ set ops"
and "ref ∉ set (interp_ins ops)"
shows "∀i ∈ set (map fst xs). i ∉ set (interp_ins ops)"
using assms proof(induction xs rule: List.rev_induct, simp)
case (snoc x xs)
have IH: "∀i ∈ set (map fst xs). i ∉ set (interp_ins ops)"
using snoc.IH snoc.prems insert_seq_rem_last insert_ops_appendD
by (metis append_is_Nil_conv le_sup_iff list.map_disc_iff set_append split_list_first)
obtain as bs where "ops = as @ x # bs"
using snoc.prems(4) by (metis split_list last_in_set snoc_eq_iff_butlast subset_code(1))
have "fst x ∉ set (interp_ins ops)"
proof(cases "xs = []")
case True
then obtain xi where "x = (xi, Some ref)"
using insert_seq_hd snoc.prems(2) by force
moreover have "ref ∉ set (interp_ins as)"
using interp_ins_monotonic snoc.prems(1) snoc.prems(5) ‹ops = as @ x # bs› by blast
ultimately have "xi ∉ set (interp_ins (as @ [x] @ bs))"
using snoc.prems(1) by (simp add: interp_ins_ref_nonex ‹ops = as @ x # bs›)
then show "fst x ∉ set (interp_ins ops)"
by (simp add: ‹ops = as @ x # bs› ‹x = (xi, Some ref)›)
next
case xs_nonempty: False
then obtain y where "xs = (butlast xs) @ [y]"
by (metis append_butlast_last_id)
moreover from this obtain yi yr xi xr where "y = (yi, yr) ∧ x = (xi, xr)"
by fastforce
moreover from this have "xr = Some yi"
using insert_seq.cases snoc.prems(2) calculation by fastforce
moreover have "yi ∉ set (interp_ins ops)"
using IH calculation
by (metis Nil_is_map_conv fst_conv last_in_set last_map snoc_eq_iff_butlast)
hence "yi ∉ set (interp_ins as)"
using ‹ops = as @ x # bs› interp_ins_monotonic snoc.prems(1) by blast
ultimately have "xi ∉ set (interp_ins (as @ [x] @ bs))"
using interp_ins_ref_nonex snoc.prems(1) ‹ops = as @ x # bs› by fastforce
then show "fst x ∉ set (interp_ins ops)"
by (simp add: ‹ops = as @ x # bs› ‹y = (yi, yr) ∧ x = (xi, xr)›)
qed
then show "∀i ∈ set (map fst (xs @ [x])). i ∉ set (interp_ins ops)"
using IH by auto
qed

subsection‹The proof of no interleaving›

lemma no_interleaving_ordered:
assumes "insert_ops ops"
and "insert_seq start xs" and "insert_ops xs"
and "insert_seq start ys" and "insert_ops ys"
and "set xs ⊆ set ops" and "set ys ⊆ set ops"
and "distinct (map fst xs @ map fst ys)"
and "fst (hd xs) < fst (hd ys)"
and "⋀r. start = Some r ⟹ r ∈ set (interp_ins ops)"
shows "(∀x ∈ set (map fst xs). ∀y ∈ set (map fst ys). list_order ops y x) ∧
(∀r. start = Some r ⟶ (∀x ∈ set (map fst xs). list_order ops r x) ∧
(∀y ∈ set (map fst ys). list_order ops r y))"
using assms proof(induction ops arbitrary: xs ys rule: List.rev_induct, simp)
case (snoc a ops)
then have "insert_ops ops"
using insert_ops_rem_last by auto
consider (a_in_xs) "a ∈ set xs" | (a_in_ys) "a ∈ set ys" | (neither) "a ∉ set xs ∧ a ∉ set ys"
by blast
then show ?case
proof(cases)
case a_in_xs
then have "a ∉ set ys"
using snoc.prems(8) by auto
hence "set ys ⊆ set ops"
using snoc.prems(7) DiffE by auto
from a_in_xs have "a = last xs"
using insert_ops_subset_last snoc.prems by blast
have IH: "(∀x ∈ set (map fst (butlast xs)). ∀y ∈ set (map fst ys).  list_order ops y x) ∧
(∀r. start = Some r ⟶ (∀x ∈ set (map fst (butlast xs)). list_order ops r x) ∧
(∀y ∈ set (map fst          ys).  list_order ops r y))"
proof(cases "xs = [a]")
case True
moreover have "∀r. start = Some r ⟶ (∀y ∈ set (map fst ys). list_order ops r y)"
using insert_seq_after_start ‹insert_ops ops› ‹set ys ⊆ set ops› snoc.prems
by (metis append_Nil2 calculation insert_seq_hd interp_ins_append_non_memb list.sel(1))
ultimately show ?thesis by auto
next
case xs_longer: False
from ‹a = last xs› have "set (butlast xs) ⊆ set ops"
using snoc.prems by (simp add: distinct_fst subset_butlast)
moreover have "insert_seq start (butlast xs)"
using insert_seq_butlast insert_seq_nonempty xs_longer ‹a = last xs› snoc.prems(2) by blast
moreover have "insert_ops (butlast xs)"
using snoc.prems(2) snoc.prems(3) insert_ops_appendD
by (metis append_butlast_last_id insert_seq_nonempty)
moreover have "distinct (map fst (butlast xs) @ map fst ys)"
using distinct_append_butlast1 snoc.prems(8) by blast
moreover have "set ys ⊆ set ops"
using ‹a ∉ set ys› ‹set ys ⊆ set ops› by blast
moreover have "hd (butlast xs) = hd xs"
by (metis append_butlast_last_id calculation(2) hd_append2 insert_seq_nonempty snoc.prems(2))
hence "fst (hd (butlast xs)) < fst (hd ys)"
moreover have "⋀r. start = Some r ⟹ r ∈ set (interp_ins ops)"
proof -
fix r
assume "start = Some r"
then obtain xid where "hd xs = (xid, Some r)"
using insert_seq_hd snoc.prems(2) by auto
hence "r < xid"
by (metis hd_in_set insert_ops_memb_ref_older insert_seq_nonempty snoc.prems(2) snoc.prems(3))
moreover have "xid < fst a"
proof -
have "xs = (butlast xs) @ [a]"
using snoc.prems(2) insert_seq_nonempty ‹a = last xs› by fastforce
moreover have "(xid, Some r) ∈ set (butlast xs)"
using ‹hd xs = (xid, Some r)› insert_seq_nonempty list.set_sel(1) snoc.prems(2)
by (metis ‹hd (butlast xs) = hd xs› ‹insert_seq start (butlast xs)›)
hence "xid ∈ set (map fst (butlast xs))"
by (metis in_set_zipE zip_map_fst_snd)
ultimately show ?thesis
using snoc.prems(3) last_op_greatest by (metis prod.collapse)
qed
ultimately have "r ≠ fst a"
using dual_order.asym by blast
thus "r ∈ set (interp_ins ops)"
using snoc.prems(1) snoc.prems(10) interp_ins_maybe_grow2 ‹start = Some r› by blast
qed
ultimately show ?thesis
using ‹insert_ops ops› snoc.IH snoc.prems(4) snoc.prems(5) by blast
qed
moreover have x_exists: "∀x ∈ set (map fst (butlast xs)). x ∈ set (interp_ins ops)"
proof(cases start)
case None
moreover have "set (butlast xs) ⊆ set ops"
using ‹a = last xs› distinct_map snoc.prems(6) snoc.prems(8) subset_butlast by fastforce
ultimately show ?thesis
using insert_seq_start_none ‹insert_ops ops› snoc.prems
by (metis append_butlast_last_id butlast.simps(2) empty_iff empty_set
insert_ops_rem_last insert_seq_butlast insert_seq_nonempty list.simps(8))
next
case (Some a)
then show ?thesis
using IH list_order_memb2 by blast
qed
moreover have "∀y ∈ set (map fst ys). list_order (ops @ [a]) y (fst a)"
proof(cases "xs = [a]")
case xs_a: True
have "ys ≠ [] ⟹ False"
proof -
assume "ys ≠ []"
then obtain yi where yi_def: "ys = (yi, start) # (tl ys)"
by (metis hd_Cons_tl insert_seq_hd snoc.prems(4))
hence "(yi, start) ∈ set ops"
by (metis ‹set ys ⊆ set ops› list.set_intros(1) subsetCE)
hence "yi ∈ set (map fst ops)"
by force
hence "yi < fst a"
using snoc.prems(1) last_op_greatest by (metis prod.collapse)
moreover have "fst a < yi"
by (metis yi_def xs_a fst_conv list.sel(1) snoc.prems(9))
ultimately show False
using less_not_sym by blast
qed
then show "∀y ∈ set (map fst ys). list_order (ops @ [a]) y (fst a)"
using insert_seq_nonempty snoc.prems(4) by blast
next
case xs_longer: False
hence butlast_split: "butlast xs = (butlast (butlast xs)) @ [last (butlast xs)]"
using ‹a = last xs› insert_seq_butlast insert_seq_nonempty snoc.prems(2) by fastforce
hence ref_exists: "fst (last (butlast xs)) ∈ set (interp_ins ops)"
using x_exists by (metis last_in_set last_map map_is_Nil_conv snoc_eq_iff_butlast)
moreover from butlast_split have "xs = (butlast (butlast xs)) @ [last (butlast xs), a]"
by (metis ‹a = last xs› append.assoc append_butlast_last_id butlast.simps(2)
insert_seq_nonempty last_ConsL last_ConsR list.simps(3) snoc.prems(2))
hence "snd a = Some (fst (last (butlast xs)))"
using snoc.prems(2) insert_seq_last_ref by (metis prod.collapse)
hence "list_order (ops @ [a]) (fst (last (butlast xs))) (fst a)"
using list_order_insert_ref ref_exists snoc.prems(1) by (metis prod.collapse)
moreover have "∀y ∈ set (map fst ys). list_order ops y (fst (last (butlast xs)))"
by (metis IH butlast_split last_in_set last_map map_is_Nil_conv snoc_eq_iff_butlast)
hence "∀y ∈ set (map fst ys). list_order (ops @ [a]) y (fst (last (butlast xs)))"
using list_order_append snoc.prems(1) by blast
ultimately show "∀y ∈ set (map fst ys). list_order (ops @ [a]) y (fst a)"
using list_order_trans snoc.prems(1) by blast
qed
moreover have map_fst_xs: "map fst xs = map fst (butlast xs) @ map fst [last xs]"
by (metis append_butlast_last_id insert_seq_nonempty map_append snoc.prems(2))
hence "set (map fst xs) = set (map fst (butlast xs)) ∪ {fst a}"
by (simp add: ‹a = last xs›)
moreover have "∀r. start = Some r ⟶ list_order (ops @ [a]) r (fst a)"
using snoc.prems by (cases start, auto simp add: insert_seq_after_start ‹a = last xs› map_fst_xs)
ultimately show "(∀x ∈ set (map fst xs). ∀y ∈ set (map fst ys). list_order (ops @ [a]) y x) ∧
(∀r. start = Some r ⟶ (∀x ∈ set (map fst xs). list_order (ops @ [a]) r x) ∧
(∀y ∈ set (map fst ys). list_order (ops @ [a]) r y))"
using snoc.prems(1) by (simp add: list_order_append)
next
case a_in_ys
then have "a ∉ set xs"
using snoc.prems(8) by auto
hence "set xs ⊆ set ops"
using snoc.prems(6) DiffE by auto
from a_in_ys have "a = last ys"
using insert_ops_subset_last snoc.prems by blast
have IH: "(∀x ∈ set (map fst xs). ∀y ∈ set (map fst (butlast ys)).  list_order ops y x) ∧
(∀r. start = Some r ⟶ (∀x ∈ set (map fst          xs).  list_order ops r x) ∧
(∀y ∈ set (map fst (butlast ys)). list_order ops r y))"
proof(cases "ys = [a]")
case True
moreover have "∀r. start = Some r ⟶ (∀y ∈ set (map fst xs). list_order ops r y)"
using insert_seq_after_start ‹insert_ops ops› ‹set xs ⊆ set ops› snoc.prems
by (metis append_Nil2 calculation insert_seq_hd interp_ins_append_non_memb list.sel(1))
ultimately show ?thesis by auto
next
case ys_longer: False
from ‹a = last ys› have "set (butlast ys) ⊆ set ops"
using snoc.prems by (simp add: distinct_fst subset_butlast)
moreover have "insert_seq start (butlast ys)"
using insert_seq_butlast insert_seq_nonempty ys_longer ‹a = last ys› snoc.prems(4) by blast
moreover have "insert_ops (butlast ys)"
using snoc.prems(4) snoc.prems(5) insert_ops_appendD
by (metis append_butlast_last_id insert_seq_nonempty)
moreover have "distinct (map fst xs @ map fst (butlast ys))"
using distinct_append_butlast2 snoc.prems(8) by blast
moreover have "set xs ⊆ set ops"
using ‹a ∉ set xs› ‹set xs ⊆ set ops› by blast
moreover have "hd (butlast ys) = hd ys"
by (metis append_butlast_last_id calculation(2) hd_append2 insert_seq_nonempty snoc.prems(4))
hence "fst (hd xs) < fst (hd (butlast ys))"
moreover have "⋀r. start = Some r ⟹ r ∈ set (interp_ins ops)"
proof -
fix r
assume "start = Some r"
then obtain yid where "hd ys = (yid, Some r)"
using insert_seq_hd snoc.prems(4) by auto
hence "r < yid"
by (metis hd_in_set insert_ops_memb_ref_older insert_seq_nonempty snoc.prems(4) snoc.prems(5))
moreover have "yid < fst a"
proof -
have "ys = (butlast ys) @ [a]"
using snoc.prems(4) insert_seq_nonempty ‹a = last ys› by fastforce
moreover have "(yid, Some r) ∈ set (butlast ys)"
using ‹hd ys = (yid, Some r)› insert_seq_nonempty list.set_sel(1) snoc.prems(2)
by (metis ‹hd (butlast ys) = hd ys› ‹insert_seq start (butlast ys)›)
hence "yid ∈ set (map fst (butlast ys))"
by (metis in_set_zipE zip_map_fst_snd)
ultimately show ?thesis
using snoc.prems(5) last_op_greatest by (metis prod.collapse)
qed
ultimately have "r ≠ fst a"
using dual_order.asym by blast
thus "r ∈ set (interp_ins ops)"
using snoc.prems(1) snoc.prems(10) interp_ins_maybe_grow2 ‹start = Some r› by blast
qed
ultimately show ?thesis
using ‹insert_ops ops› snoc.IH snoc.prems(2) snoc.prems(3) by blast
qed
moreover have "∀x ∈ set (map fst xs). list_order (ops @ [a]) (fst a) x"
proof(cases "ys = [a]")
case ys_a: True
then show "∀x ∈ set (map fst xs). list_order (ops @ [a]) (fst a) x"
proof(cases start)
case None
then show ?thesis
using insert_seq_start_none list_order_insert_none snoc.prems
by (metis ‹insert_ops ops› ‹set xs ⊆ set ops› fst_conv insert_seq_hd list.sel(1) ys_a)
next
case (Some r)
moreover from this have "∀x ∈ set (map fst xs). list_order ops r x"
using IH by blast
ultimately show ?thesis
using snoc.prems(1) snoc.prems(4) list_order_insert_between
by (metis fst_conv insert_seq_hd list.sel(1) ys_a)
qed
next
case ys_longer: False
hence butlast_split: "butlast ys = (butlast (butlast ys)) @ [last (butlast ys)]"
using ‹a = last ys› insert_seq_butlast insert_seq_nonempty snoc.prems(4) by fastforce
moreover from this have "ys = (butlast (butlast ys)) @ [last (butlast ys), a]"
by (metis ‹a = last ys› append.assoc append_butlast_last_id butlast.simps(2)
insert_seq_nonempty last_ConsL last_ConsR list.simps(3) snoc.prems(4))
hence "snd a = Some (fst (last (butlast ys)))"
using snoc.prems(4) insert_seq_last_ref by (metis prod.collapse)
moreover have "∀x ∈ set (map fst xs). list_order ops (fst (last (butlast ys))) x"
by (metis IH butlast_split last_in_set last_map map_is_Nil_conv snoc_eq_iff_butlast)
ultimately show "∀x ∈ set (map fst xs). list_order (ops @ [a]) (fst a) x"
using list_order_insert_between snoc.prems(1) by (metis prod.collapse)
qed
moreover have map_fst_xs: "map fst ys = map fst (butlast ys) @ map fst [last ys]"
by (metis append_butlast_last_id insert_seq_nonempty map_append snoc.prems(4))
hence "set (map fst ys) = set (map fst (butlast ys)) ∪ {fst a}"
by (simp add: ‹a = last ys›)
moreover have "∀r. start = Some r ⟶ list_order (ops @ [a]) r (fst a)"
using snoc.prems by (cases start, auto simp add: insert_seq_after_start ‹a = last ys› map_fst_xs)
ultimately show "(∀x ∈ set (map fst xs). ∀y ∈ set (map fst ys). list_order (ops @ [a]) y x) ∧
(∀r. start = Some r ⟶ (∀x ∈ set (map fst xs). list_order (ops @ [a]) r x) ∧
(∀y ∈ set (map fst ys). list_order (ops @ [a]) r y))"
using snoc.prems(1) by (simp add: list_order_append)
next
case neither
hence "set xs ⊆ set ops" and "set ys ⊆ set ops"
using snoc.prems(6) snoc.prems(7) DiffE by auto
have "(∀r. start = Some r ⟶ r ∈ set (interp_ins ops)) ∨ (xs = [] ∧ ys = [])"
proof(cases xs)
case Nil
then show ?thesis using insert_seq_nonempty snoc.prems(2) by blast
next
case xs_nonempty: (Cons x xsa)
have "⋀r. start = Some r ⟹ r ∈ set (interp_ins ops)"
proof -
fix r
assume "start = Some r"
then obtain xi where "x = (xi, Some r)"
using insert_seq_hd xs_nonempty snoc.prems(2) by fastforce
hence "(xi, Some r) ∈ set ops"
using ‹set xs ⊆ set ops› xs_nonempty by auto
hence "r < xi"
using ‹insert_ops ops› insert_ops_memb_ref_older by blast
moreover have "xi ∈ set (map fst ops)"
using ‹(xi, Some r) ∈ set ops› by force
hence "xi < fst a"
using last_op_greatest snoc.prems(1) by (metis prod.collapse)
ultimately have "fst a ≠ r"
using order.asym by blast
then show "r ∈ set (interp_ins ops)"
using snoc.prems(1) snoc.prems(10) interp_ins_maybe_grow2 ‹start = Some r› by blast
qed
then show ?thesis by blast
qed
hence "(∀x ∈ set (map fst xs). ∀y ∈ set (map fst ys). list_order ops y x) ∧
(∀r. start = Some r ⟶ (∀x ∈ set (map fst xs). list_order ops r x) ∧
(∀y ∈ set (map fst ys). list_order ops r y))"
using snoc.prems snoc.IH ‹set xs ⊆ set ops› ‹set ys ⊆ set ops› by blast
then show "(∀x ∈ set (map fst xs). ∀y ∈ set (map fst ys). list_order (ops @ [a]) y x) ∧
(∀r. start = Some r ⟶ (∀x ∈ set (map fst xs). list_order (ops @ [a]) r x) ∧
(∀y ∈ set (map fst ys). list_order (ops @ [a]) r y))"
using snoc.prems(1) by (simp add: list_order_append)
qed
qed

text‹Consider an execution that contains two distinct insertion sequences,
\isa{xs} and \isa{ys}, that both begin at the same initial position \isa{start}.
We prove that, provided the starting element exists, the two insertion sequences
are not interleaved. That is, in the final list order, either all insertions by
\isa{xs} appear before all insertions by \isa{ys}, or vice versa.›

theorem no_interleaving:
assumes "insert_ops ops"
and "insert_seq start xs" and "insert_ops xs"
and "insert_seq start ys" and "insert_ops ys"
and "set xs ⊆ set ops" and "set ys ⊆ set ops"
and "distinct (map fst xs @ map fst ys)"
and "start = None ∨ (∃r. start = Some r ∧ r ∈ set (interp_ins ops))"
shows "(∀x ∈ set (map fst xs). ∀y ∈ set (map fst ys). list_order ops x y) ∨
(∀x ∈ set (map fst xs). ∀y ∈ set (map fst ys). list_order ops y x)"
proof(cases "fst (hd xs) < fst (hd ys)")
case True
moreover have "⋀r. start = Some r ⟹ r ∈ set (interp_ins ops)"
using assms(9) by blast
ultimately have "∀x∈set (map fst xs). ∀y∈set (map fst ys). list_order ops y x"
using assms no_interleaving_ordered by blast
then show ?thesis by blast
next
case False
hence "fst (hd ys) < fst (hd xs)"
using assms(2) assms(4) assms(8) insert_seq_nonempty distinct_fst_append
by (metis (no_types, lifting) hd_in_set hd_map list.map_disc_iff map_append neqE)
moreover have "distinct (map fst ys @ map fst xs)"
using assms(8) distinct_append_swap by blast
moreover have "⋀r. start = Some r ⟹ r ∈ set (interp_ins ops)"
using assms(9) by blast
ultimately have "∀x∈set (map fst ys). ∀y∈set (map fst xs). list_order ops y x"
using assms no_interleaving_ordered by blast
then show ?thesis by blast
qed

text‹For completeness, we also prove what happens if there are two insertion
sequences, \isa{xs} and \isa{ys}, but their initial position \isa{start} does
not exist. In that case, none of the insertions in \isa{xs} or \isa{ys} take
effect.›

theorem missing_start_no_insertion:
assumes "insert_ops ops"
and "insert_seq (Some start) xs" and "insert_ops xs"
and "insert_seq (Some start) ys" and "insert_ops ys"
and "set xs ⊆ set ops" and "set ys ⊆ set ops"
and "start ∉ set (interp_ins ops)"
shows "∀x ∈ set (map fst xs) ∪ set (map fst ys). x ∉ set (interp_ins ops)"
using assms insert_seq_no_start by (metis UnE)

end
```