(* 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 subsection‹Lemmas about \isa{insert-ops}› 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)" by (simp add: IH x_pair) 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" by (simp add: x_split y_split) 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))" by (simp add: distinct_butlast map_butlast) 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 subsection‹Lemmas about \isa{interp-ins}› 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)" by (simp add: interp_ins_tail_unfold) 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))" by (simp add: snoc.IH snoc.prems(3)) 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)]))" by (simp add: interp_ins_tail_unfold) 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 subsection‹Lemmas about \isa{list-order}› 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)" by (simp add: interp_ins_tail_unfold) 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)" by (simp add: interp_ins_tail_unfold) 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)" by (simp add: interp_ins_tail_unfold) 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)]))" by (simp add: interp_ins_last_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)" by (simp add: ops_split) 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)" by (simp add: snoc.prems(9)) 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))" by (simp add: snoc.prems(9)) 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