(* Martin Kleppmann, University of Cambridge Victor B. F. Gomes, University of Cambridge Dominic P. Mulligan, Arm Research, Cambridge Alastair Beresford, University of Cambridge *) section‹Abstract OpSet› text‹In this section, we define a general-purpose OpSet abstraction that is not specific to any one particular datatype. We develop a library of useful lemmas that we can build upon later when reasoning about a specific datatype.› theory OpSet imports Main begin subsection‹OpSet definition› text‹An OpSet is a set of (ID, operation) pairs with an associated total order on IDs (represented here with the \isa{linorder} typeclass), and satisfying the following properties: \begin{enumerate} \item The ID is unique (that is, if any two pairs in the set have the same ID, then their operation is also the same). \item If the operation references the IDs of any other operations, those referenced IDs are less than that of the operation itself, according to the total order on IDs. To avoid assuming anything about the structure of operations here, we use a function \isa{deps} that returns the set of dependent IDs for a given operation. This requirement is a weak expression of causality: an operation can only depend on causally prior operations, and by making the total order on IDs a linear extension of the causal order, we can easily ensure that any referenced IDs are less than that of the operation itself. \item The OpSet is finite (but we do not assume any particular maximum size). \end{enumerate}› locale opset = fixes opset :: "('oid::{linorder} × 'oper) set" and deps :: "'oper ⇒ 'oid set" assumes unique_oid: "(oid, op1) ∈ opset ⟹ (oid, op2) ∈ opset ⟹ op1 = op2" and ref_older: "(oid, oper) ∈ opset ⟹ ref ∈ deps oper ⟹ ref < oid" and finite_opset: "finite opset" text‹We prove that any subset of an OpSet is also a valid OpSet. This is the case because, although an operation can depend on causally prior operations, the OpSet does not require those prior operations to actually exist. This weak assumption makes the OpSet model more general and simplifies reasoning about OpSets.› lemma opset_subset: assumes "opset Y deps" and "X ⊆ Y" shows "opset X deps" proof fix oid op1 op2 assume "(oid, op1) ∈ X" and "(oid, op2) ∈ X" thus "op1 = op2" using assms by (meson opset.unique_oid subsetD) next fix oid oper ref assume "(oid, oper) ∈ X" and "ref ∈ deps oper" thus "ref < oid" using assms by (meson opset.ref_older rev_subsetD) next show "finite X" using assms opset.finite_opset finite_subset by blast qed lemma opset_insert: assumes "opset (insert x ops) deps" shows "opset ops deps" using assms opset_subset by blast lemma opset_sublist: assumes "opset (set (xs @ ys @ zs)) deps" shows "opset (set (xs @ zs)) deps" proof - have "set (xs @ zs) ⊆ set (xs @ ys @ zs)" by auto thus "opset (set (xs @ zs)) deps" using assms opset_subset by blast qed subsection‹Helper lemmas about lists› text‹Some general-purpose lemas about lists and sets that are helpful for subsequent proofs.› lemma distinct_rem_mid: assumes "distinct (xs @ [x] @ ys)" shows "distinct (xs @ ys)" using assms by (induction ys rule: rev_induct, simp_all) lemma distinct_fst_append: assumes "x ∈ set (map fst xs)" and "distinct (map fst (xs @ ys))" shows "x ∉ set (map fst ys)" using assms by (induction ys, force+) lemma distinct_set_remove_last: assumes "distinct (xs @ [x])" shows "set xs = set (xs @ [x]) - {x}" using assms by force lemma distinct_set_remove_mid: assumes "distinct (xs @ [x] @ ys)" shows "set (xs @ ys) = set (xs @ [x] @ ys) - {x}" using assms by force lemma distinct_list_split: assumes "distinct xs" and "xs = xa @ x # ya" and "xs = xb @ x # yb" shows "xa = xb ∧ ya = yb" using assms proof(induction xs arbitrary: xa xb x) fix xa xb x assume "[] = xa @ x # ya" thus "xa = xb ∧ ya = yb" by auto next fix a xs xa xb x assume IH: "⋀xa xb x. distinct xs ⟹ xs = xa @ x # ya ⟹ xs = xb @ x # yb ⟹ xa = xb ∧ ya = yb" and "distinct (a # xs)" and "a # xs = xa @ x # ya" and "a # xs = xb @ x # yb" thus "xa = xb ∧ ya = yb" by(case_tac xa; case_tac xb) auto qed lemma distinct_append_swap: assumes "distinct (xs @ ys)" shows "distinct (ys @ xs)" using assms by (induction ys, auto) lemma append_subset: assumes "set xs = set (ys @ zs)" shows "set ys ⊆ set xs" and "set zs ⊆ set xs" by (metis Un_iff assms set_append subsetI)+ lemma append_set_rem_last: assumes "set (xs @ [x]) = set (ys @ [x] @ zs)" and "distinct (xs @ [x])" and "distinct (ys @ [x] @ zs)" shows "set xs = set (ys @ zs)" proof - have "distinct xs" using assms distinct_append by blast moreover from this have "set xs = set (xs @ [x]) - {x}" by (meson assms distinct_set_remove_last) moreover have "distinct (ys @ zs)" using assms distinct_rem_mid by simp ultimately show "set xs = set (ys @ zs)" using assms distinct_set_remove_mid by metis qed lemma distinct_map_fst_remove1: assumes "distinct (map fst xs)" shows "distinct (map fst (remove1 x xs))" using assms proof(induction xs) case Nil then show "distinct (map fst (remove1 x []))" by simp next case (Cons a xs) hence IH: "distinct (map fst (remove1 x xs))" by simp then show "distinct (map fst (remove1 x (a # xs)))" proof(cases "a = x") case True then show ?thesis using Cons.prems by auto next case False moreover have "fst a ∉ fst ` set (remove1 x xs)" by (metis (no_types, lifting) Cons.prems distinct.simps(2) image_iff list.simps(9) notin_set_remove1 set_map) ultimately show ?thesis using IH by auto qed qed subsection‹The \isa{spec-ops} predicate› text‹The \isa{spec-ops} predicate describes a list of (ID, operation) pairs that corresponds to the linearisation of an OpSet, and which we use for sequentially interpreting the OpSet. A list satisfies \isa{spec-ops} iff it is sorted in ascending order of IDs, if the IDs are unique, and if every operation's dependencies have lower IDs than the operation itself. A list is implicitly finite in Isabelle/HOL. These requirements correspond to the OpSet definition above, and indeed we prove later that every OpSet has a linearisation that satisfies \isa{spec-ops}.› definition spec_ops :: "('oid::{linorder} × 'oper) list ⇒ ('oper ⇒ 'oid set) ⇒ bool" where "spec_ops ops deps ≡ (sorted (map fst ops) ∧ distinct (map fst ops) ∧ (∀oid oper ref. (oid, oper) ∈ set ops ∧ ref ∈ deps oper ⟶ ref < oid))" lemma spec_ops_empty: shows "spec_ops [] deps" by (simp add: spec_ops_def) lemma spec_ops_distinct: assumes "spec_ops ops deps" shows "distinct ops" using assms distinct_map spec_ops_def by blast lemma spec_ops_distinct_fst: assumes "spec_ops ops deps" shows "distinct (map fst ops)" using assms by (simp add: spec_ops_def) lemma spec_ops_sorted: assumes "spec_ops ops deps" shows "sorted (map fst ops)" using assms by (simp add: spec_ops_def) lemma spec_ops_rem_cons: assumes "spec_ops (x # xs) deps" shows "spec_ops xs deps" proof - have "sorted (map fst (x # xs))" and "distinct (map fst (x # xs))" using assms spec_ops_def by blast+ moreover from this have "sorted (map fst xs)" by simp moreover have "∀oid oper ref. (oid, oper) ∈ set xs ∧ ref ∈ deps oper ⟶ ref < oid" by (meson assms set_subset_Cons spec_ops_def subsetCE) ultimately show "spec_ops xs deps" by (simp add: spec_ops_def) qed lemma spec_ops_rem_last: assumes "spec_ops (xs @ [x]) deps" shows "spec_ops xs deps" proof - have "sorted (map fst (xs @ [x]))" and "distinct (map fst (xs @ [x]))" using assms spec_ops_def by blast+ moreover from this have "sorted (map fst xs)" and "distinct xs" by (auto simp add: sorted_append distinct_butlast distinct_map) moreover have "∀oid oper ref. (oid, oper) ∈ set xs ∧ ref ∈ deps oper ⟶ ref < oid" by (metis assms butlast_snoc in_set_butlastD spec_ops_def) ultimately show "spec_ops xs deps" by (simp add: spec_ops_def) qed lemma spec_ops_remove1: assumes "spec_ops xs deps" shows "spec_ops (remove1 x xs) deps" using assms distinct_map_fst_remove1 spec_ops_def by (metis notin_set_remove1 sorted_map_remove1 spec_ops_def) lemma spec_ops_ref_less: assumes "spec_ops xs deps" and "(oid, oper) ∈ set xs" and "r ∈ deps oper" shows "r < oid" using assms spec_ops_def by force lemma spec_ops_ref_less_last: assumes "spec_ops (xs @ [(oid, oper)]) deps" and "r ∈ deps oper" shows "r < oid" using assms spec_ops_ref_less by fastforce lemma spec_ops_id_inc: assumes "spec_ops (xs @ [(oid, oper)]) deps" and "x ∈ set (map fst xs)" shows "x < oid" proof - have "sorted ((map fst xs) @ (map fst [(oid, oper)]))" using assms(1) by (simp add: spec_ops_def) hence "∀i ∈ set (map fst xs). i ≤ oid" by (simp add: sorted_append) moreover have "distinct ((map fst xs) @ (map fst [(oid, oper)]))" using assms(1) by (simp add: spec_ops_def) hence "∀i ∈ set (map fst xs). i ≠ oid" by auto ultimately show "x < oid" using assms(2) le_neq_trans by auto qed lemma spec_ops_add_last: assumes "spec_ops xs deps" and "∀i ∈ set (map fst xs). i < oid" and "∀ref ∈ deps oper. ref < oid" shows "spec_ops (xs @ [(oid, oper)]) deps" proof - have "sorted ((map fst xs) @ [oid])" using assms sorted_append spec_ops_sorted by fastforce moreover have "distinct ((map fst xs) @ [oid])" using assms spec_ops_distinct_fst by fastforce moreover have "∀oid oper ref. (oid, oper) ∈ set xs ∧ ref ∈ deps oper ⟶ ref < oid" using assms(1) spec_ops_def by fastforce hence "∀i opr r. (i, opr) ∈ set (xs @ [(oid, oper)]) ∧ r ∈ deps opr ⟶ r < i" using assms(3) by auto ultimately show "spec_ops (xs @ [(oid, oper)]) deps" by (simp add: spec_ops_def) qed lemma spec_ops_add_any: assumes "spec_ops (xs @ ys) deps" and "∀i ∈ set (map fst xs). i < oid" and "∀i ∈ set (map fst ys). oid < i" and "∀ref ∈ deps oper. ref < oid" shows "spec_ops (xs @ [(oid, oper)] @ ys) deps" using assms proof(induction ys rule: rev_induct) case Nil then show "spec_ops (xs @ [(oid, oper)] @ []) deps" by (simp add: spec_ops_add_last) next case (snoc y ys) have IH: "spec_ops (xs @ [(oid, oper)] @ ys) deps" proof - from snoc have "spec_ops (xs @ ys) deps" by (metis append_assoc spec_ops_rem_last) thus "spec_ops (xs @ [(oid, oper)] @ ys) deps" using assms(2) snoc by auto qed obtain yi yo where y_pair: "y = (yi, yo)" by force have oid_yi: "oid < yi" by (simp add: snoc.prems(3) y_pair) have yi_biggest: "∀i ∈ set (map fst (xs @ [(oid, oper)] @ ys)). i < yi" proof - have "∀i ∈ set (map fst xs). i < yi" using oid_yi assms(2) less_trans by blast moreover have "∀i ∈ set (map fst ys). i < yi" by (metis UnCI append_assoc map_append set_append snoc.prems(1) spec_ops_id_inc y_pair) ultimately show ?thesis using oid_yi by auto qed have "sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))" proof - from IH have "sorted (map fst (xs @ [(oid, oper)] @ ys))" using spec_ops_def by blast hence "sorted (map fst (xs @ [(oid, oper)] @ ys) @ [yi])" using yi_biggest by (simp add: sorted_append dual_order.strict_implies_order) thus "sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))" by (simp add: y_pair) qed moreover have "distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))" proof - have "distinct (map fst (xs @ [(oid, oper)] @ ys) @ [yi])" using IH yi_biggest spec_ops_def by (metis distinct.simps(2) distinct1_rotate order_less_irrefl rotate1.simps(2)) thus "distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))" by (simp add: y_pair) qed moreover have "∀i opr r. (i, opr) ∈ set (xs @ [(oid, oper)] @ ys @ [y]) ∧ r ∈ deps opr ⟶ r < i" proof - have "∀i opr r. (i, opr) ∈ set (xs @ [(oid, oper)] @ ys) ∧ r ∈ deps opr ⟶ r < i" by (meson IH spec_ops_def) moreover have "∀ref. ref ∈ deps yo ⟶ ref < yi" by (metis spec_ops_ref_less append_is_Nil_conv last_appendR last_in_set last_snoc list.simps(3) snoc.prems(1) y_pair) ultimately show ?thesis using y_pair by auto qed ultimately show "spec_ops (xs @ [(oid, oper)] @ ys @ [y]) deps" using spec_ops_def by blast qed lemma spec_ops_split: assumes "spec_ops xs deps" and "oid ∉ set (map fst xs)" shows "∃pre suf. xs = pre @ suf ∧ (∀i ∈ set (map fst pre). i < oid) ∧ (∀i ∈ set (map fst suf). oid < i)" using assms proof(induction xs rule: rev_induct) case Nil then show ?case by force next case (snoc x xs) obtain xi xr where y_pair: "x = (xi, xr)" by force obtain pre suf where IH: "xs = pre @ suf ∧ (∀a∈set (map fst pre). a < oid) ∧ (∀a∈set (map fst suf). oid < a)" by (metis UnCI map_append set_append snoc spec_ops_rem_last) then show ?case proof(cases "xi < oid") case xi_less: True have "∀x ∈ set (map fst (pre @ suf)). x < xi" using IH spec_ops_id_inc snoc.prems(1) y_pair by metis hence "∀x ∈ set suf. fst x < xi" by simp hence "∀x ∈ set suf. fst x < oid" using xi_less by auto hence "suf = []" using IH last_in_set by fastforce hence "xs @ [x] = (pre @ [(xi, xr)]) @ [] ∧ (∀a∈set (map fst ((pre @ [(xi, xr)]))). a < oid) ∧ (∀a∈set (map fst []). oid < a)" by (simp add: IH xi_less y_pair) then show ?thesis by force next case False hence "oid < xi" using snoc.prems(2) y_pair by auto hence "xs @ [x] = pre @ (suf @ [(xi, xr)]) ∧ (∀i ∈ set (map fst pre). i < oid) ∧ (∀i ∈ set (map fst (suf @ [(xi, xr)])). oid < i)" by (simp add: IH y_pair) then show ?thesis by blast qed qed lemma spec_ops_exists_base: assumes "finite ops" and "⋀oid op1 op2. (oid, op1) ∈ ops ⟹ (oid, op2) ∈ ops ⟹ op1 = op2" and "⋀oid oper ref. (oid, oper) ∈ ops ⟹ ref ∈ deps oper ⟹ ref < oid" shows "∃op_list. set op_list = ops ∧ spec_ops op_list deps" using assms proof(induct ops rule: Finite_Set.finite_induct_select) case empty then show "∃op_list. set op_list = {} ∧ spec_ops op_list deps" by (simp add: spec_ops_empty) next case (select subset) from this obtain op_list where "set op_list = subset" and "spec_ops op_list deps" using assms by blast moreover obtain oid oper where select: "(oid, oper) ∈ ops - subset" using select.hyps(1) by auto moreover from this have "⋀op2. (oid, op2) ∈ ops ⟹ op2 = oper" using assms(2) by auto hence "oid ∉ fst ` subset" by (metis (no_types, lifting) DiffD2 select image_iff prod.collapse psubsetD select.hyps(1)) from this obtain pre suf where "op_list = pre @ suf" and "∀i ∈ set (map fst pre). i < oid" and "∀i ∈ set (map fst suf). oid < i" using spec_ops_split calculation by (metis (no_types, lifting) set_map) moreover have "set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset" using calculation by auto moreover have "spec_ops (pre @ [(oid, oper)] @ suf) deps" using calculation spec_ops_add_any assms(3) by (metis DiffD1) ultimately show ?case by blast qed text‹We prove that for any given OpSet, a \isa{spec-ops} linearisation exists:› lemma spec_ops_exists: assumes "opset ops deps" shows "∃op_list. set op_list = ops ∧ spec_ops op_list deps" proof - have "finite ops" using assms opset.finite_opset by force moreover have "⋀oid op1 op2. (oid, op1) ∈ ops ⟹ (oid, op2) ∈ ops ⟹ op1 = op2" using assms opset.unique_oid by force moreover have "⋀oid oper ref. (oid, oper) ∈ ops ⟹ ref ∈ deps oper ⟹ ref < oid" using assms opset.ref_older by force ultimately show "∃op_list. set op_list = ops ∧ spec_ops op_list deps" by (simp add: spec_ops_exists_base) qed lemma spec_ops_oid_unique: assumes "spec_ops op_list deps" and "(oid, op1) ∈ set op_list" and "(oid, op2) ∈ set op_list" shows "op1 = op2" using assms proof(induction op_list, simp) case (Cons x op_list) have "distinct (map fst (x # op_list))" using Cons.prems(1) spec_ops_def by blast hence notin: "fst x ∉ set (map fst op_list)" by simp then show "op1 = op2" proof(cases "fst x = oid") case True then show "op1 = op2" using Cons.prems notin by (metis Pair_inject in_set_zipE set_ConsD zip_map_fst_snd) next case False then have "(oid, op1) ∈ set op_list" and "(oid, op2) ∈ set op_list" using Cons.prems by auto then show "op1 = op2" using Cons.IH Cons.prems(1) spec_ops_rem_cons by blast qed qed text‹Conversely, for any given \isa{spec-ops} list, the set of pairs in the list is an OpSet:› lemma spec_ops_is_opset: assumes "spec_ops op_list deps" shows "opset (set op_list) deps" proof - have "⋀oid op1 op2. (oid, op1) ∈ set op_list ⟹ (oid, op2) ∈ set op_list ⟹ op1 = op2" using assms spec_ops_oid_unique by fastforce moreover have "⋀oid oper ref. (oid, oper) ∈ set op_list ⟹ ref ∈ deps oper ⟹ ref < oid" by (meson assms spec_ops_ref_less) moreover have "finite (set op_list)" by simp ultimately show "opset (set op_list) deps" by (simp add: opset_def) qed subsection‹The \isa{crdt-ops} predicate› text‹Like \isa{spec-ops}, the \isa{crdt-ops} predicate describes the linearisation of an OpSet into a list. Like \isa{spec-ops}, it requires IDs to be unique. However, its other properties are different: \isa{crdt-ops} does not require operations to appear in sorted order, but instead, whenever any operation references the ID of a prior operation, that prior operation must appear previously in the \isa{crdt-ops} list. Thus, the order of operations is partially constrained: operations must appear in causal order, but concurrent operations can be ordered arbitrarily. This list describes the operation sequence in the order it is typically applied to an operation-based CRDT. Applying operations in the order they appear in \isa{crdt-ops} requires that concurrent operations commute. For any \isa{crdt-ops} operation sequence, there is a permutation that satisfies the \isa{spec-ops} predicate. Thus, to check whether a CRDT satisfies its sequential specification, we can prove that interpreting any \isa{crdt-ops} operation sequence with the commutative operation interpretation results in the same end result as interpreting the \isa{spec-ops} permutation of that operation sequence with the sequential operation interpretation.› inductive crdt_ops :: "('oid::{linorder} × 'oper) list ⇒ ('oper ⇒ 'oid set) ⇒ bool" where "crdt_ops [] deps" | "⟦crdt_ops xs deps; oid ∉ set (map fst xs); ∀ref ∈ deps oper. ref ∈ set (map fst xs) ∧ ref < oid ⟧ ⟹ crdt_ops (xs @ [(oid, oper)]) deps" inductive_cases crdt_ops_last: "crdt_ops (xs @ [x]) deps" lemma crdt_ops_intro: assumes "⋀r. r ∈ deps oper ⟹ r ∈ fst ` set xs ∧ r < oid" and "oid ∉ fst ` set xs" and "crdt_ops xs deps" shows "crdt_ops (xs @ [(oid, oper)]) deps" using assms crdt_ops.simps by force lemma crdt_ops_rem_last: assumes "crdt_ops (xs @ [x]) deps" shows "crdt_ops xs deps" using assms crdt_ops.cases snoc_eq_iff_butlast by blast lemma crdt_ops_ref_less: assumes "crdt_ops xs deps" and "(oid, oper) ∈ set xs" and "r ∈ deps oper" shows "r < oid" using assms by (induction rule: crdt_ops.induct, auto) lemma crdt_ops_ref_less_last: assumes "crdt_ops (xs @ [(oid, oper)]) deps" and "r ∈ deps oper" shows "r < oid" using assms crdt_ops_ref_less by fastforce lemma crdt_ops_distinct_fst: assumes "crdt_ops xs deps" shows "distinct (map fst xs)" using assms proof (induction xs rule: List.rev_induct, simp) case (snoc x xs) hence "distinct (map fst xs)" using crdt_ops_last by blast moreover have "fst x ∉ set (map fst xs)" using snoc by (metis crdt_ops_last fstI image_set) ultimately show "distinct (map fst (xs @ [x]))" by simp qed lemma crdt_ops_distinct: assumes "crdt_ops xs deps" shows "distinct xs" using assms crdt_ops_distinct_fst distinct_map by blast lemma crdt_ops_unique_last: assumes "crdt_ops (xs @ [(oid, oper)]) deps" shows "oid ∉ set (map fst xs)" using assms crdt_ops.cases by blast lemma crdt_ops_unique_mid: assumes "crdt_ops (xs @ [(oid, oper)] @ ys) deps" shows "oid ∉ set (map fst xs) ∧ oid ∉ set (map fst ys)" using assms proof(induction ys rule: rev_induct) case Nil then show "oid ∉ set (map fst xs) ∧ oid ∉ set (map fst [])" by (metis crdt_ops_unique_last Nil_is_map_conv append_Nil2 empty_iff empty_set) next case (snoc y ys) obtain yi yr where y_pair: "y = (yi, yr)" by fastforce have IH: "oid ∉ set (map fst xs) ∧ oid ∉ set (map fst ys)" using crdt_ops_rem_last snoc by (metis append_assoc) have "(xs @ (oid, oper) # ys) @ [(yi, yr)] = xs @ (oid, oper) # ys @ [(yi, yr)]" by simp hence "yi ∉ set (map fst (xs @ (oid, oper) # ys))" using crdt_ops_unique_last by (metis append_Cons append_self_conv2 snoc.prems y_pair) thus "oid ∉ set (map fst xs) ∧ oid ∉ set (map fst (ys @ [y]))" using IH y_pair by auto qed lemma crdt_ops_ref_exists: assumes "crdt_ops (pre @ (oid, oper) # suf) deps" and "ref ∈ deps oper" shows "ref ∈ fst ` set pre" using assms proof(induction suf rule: List.rev_induct) case Nil thus ?case by (metis crdt_ops_last prod.sel(2)) next case (snoc x xs) thus ?case using crdt_ops.cases by force qed lemma crdt_ops_no_future_ref: assumes "crdt_ops (xs @ [(oid, oper)] @ ys) deps" shows "⋀ref. ref ∈ deps oper ⟹ ref ∉ fst ` set ys" proof - from assms(1) have "⋀ref. ref ∈ deps oper ⟹ ref ∈ set (map fst xs)" by (simp add: crdt_ops_ref_exists) moreover have "distinct (map fst (xs @ [(oid, oper)] @ ys))" using assms crdt_ops_distinct_fst by blast ultimately have "⋀ref. ref ∈ deps oper ⟹ ref ∉ set (map fst ([(oid, oper)] @ ys))" using distinct_fst_append by metis thus "⋀ref. ref ∈ deps oper ⟹ ref ∉ fst ` set ys" by simp qed lemma crdt_ops_reorder: assumes "crdt_ops (xs @ [(oid, oper)] @ ys) deps" and "⋀op2 r. op2 ∈ snd ` set ys ⟹ r ∈ deps op2 ⟹ r ≠ oid" shows "crdt_ops (xs @ ys @ [(oid, oper)]) deps" using assms proof(induction ys rule: rev_induct) case Nil then show "crdt_ops (xs @ [] @ [(oid, oper)]) deps" using crdt_ops_rem_last by auto next case (snoc y ys) then obtain yi yo where y_pair: "y = (yi, yo)" by fastforce have IH: "crdt_ops (xs @ ys @ [(oid, oper)]) deps" proof - have "crdt_ops (xs @ [(oid, oper)] @ ys) deps" by (metis snoc(2) append.assoc crdt_ops_rem_last) thus "crdt_ops (xs @ ys @ [(oid, oper)]) deps" using snoc.IH snoc.prems(2) by auto qed have "crdt_ops (xs @ ys @ [y]) deps" proof - have "yi ∉ fst ` set (xs @ [(oid, oper)] @ ys)" by (metis y_pair append_assoc crdt_ops_unique_last set_map snoc.prems(1)) hence "yi ∉ fst ` set (xs @ ys)" by auto moreover have "⋀r. r ∈ deps yo ⟹ r ∈ fst ` set (xs @ ys) ∧ r < yi" proof - have "⋀r. r ∈ deps yo ⟹ r ≠ oid" using snoc.prems(2) y_pair by fastforce moreover have "⋀r. r ∈ deps yo ⟹ r ∈ fst ` set (xs @ [(oid, oper)] @ ys)" by (metis y_pair append_assoc snoc.prems(1) crdt_ops_ref_exists) moreover have "⋀r. r ∈ deps yo ⟹ r < yi" using crdt_ops_ref_less snoc.prems(1) y_pair by fastforce ultimately show "⋀r. r ∈ deps yo ⟹ r ∈ fst ` set (xs @ ys) ∧ r < yi" by simp qed moreover from IH have "crdt_ops (xs @ ys) deps" using crdt_ops_rem_last by force ultimately show "crdt_ops (xs @ ys @ [y]) deps" using y_pair crdt_ops_intro by (metis append.assoc) qed moreover have "oid ∉ fst ` set (xs @ ys @ [y])" using crdt_ops_unique_mid by (metis (no_types, lifting) UnE image_Un image_set set_append snoc.prems(1)) moreover have "⋀r. r ∈ deps oper ⟹ r ∈ fst ` set (xs @ ys @ [y])" using crdt_ops_ref_exists by (metis UnCI append_Cons image_Un set_append snoc.prems(1)) moreover have "⋀r. r ∈ deps oper ⟹ r < oid" using IH crdt_ops_ref_less by fastforce ultimately show "crdt_ops (xs @ (ys @ [y]) @ [(oid, oper)]) deps" using crdt_ops_intro by (metis append_assoc) qed lemma crdt_ops_rem_middle: assumes "crdt_ops (xs @ [(oid, ref)] @ ys) deps" and "⋀op2 r. op2 ∈ snd ` set ys ⟹ r ∈ deps op2 ⟹ r ≠ oid" shows "crdt_ops (xs @ ys) deps" using assms crdt_ops_rem_last crdt_ops_reorder append_assoc by metis lemma crdt_ops_independent_suf: assumes "spec_ops (xs @ [(oid, oper)]) deps" and "crdt_ops (ys @ [(oid, oper)] @ zs) deps" and "set (xs @ [(oid, oper)]) = set (ys @ [(oid, oper)] @ zs)" shows "⋀op2 r. op2 ∈ snd ` set zs ⟹ r ∈ deps op2 ⟹ r ≠ oid" proof - have "⋀op2 r. op2 ∈ snd ` set xs ⟹ r ∈ deps op2 ⟹ r < oid" proof - from assms(1) have "⋀i. i ∈ fst ` set xs ⟹ i < oid" using spec_ops_id_inc by fastforce moreover have "⋀i2 op2 r. (i2, op2) ∈ set xs ⟹ r ∈ deps op2 ⟹ r < i2" using assms(1) spec_ops_ref_less spec_ops_rem_last by fastforce ultimately show "⋀op2 r. op2 ∈ snd ` set xs ⟹ r ∈ deps op2 ⟹ r < oid" by fastforce qed moreover have "set zs ⊆ set xs" proof - have "distinct (xs @ [(oid, oper)])" and "distinct (ys @ [(oid, oper)] @ zs)" using assms spec_ops_distinct crdt_ops_distinct by blast+ hence "set xs = set (ys @ zs)" by (meson append_set_rem_last assms(3)) then show "set zs ⊆ set xs" using append_subset(2) by simp qed ultimately show "⋀op2 r. op2 ∈ snd ` set zs ⟹ r ∈ deps op2 ⟹ r ≠ oid" by fastforce qed lemma crdt_ops_reorder_spec: assumes "spec_ops (xs @ [x]) deps" and "crdt_ops (ys @ [x] @ zs) deps" and "set (xs @ [x]) = set (ys @ [x] @ zs)" shows "crdt_ops (ys @ zs @ [x]) deps" using assms proof - obtain oid oper where x_pair: "x = (oid, oper)" by force hence "⋀op2 r. op2 ∈ snd ` set zs ⟹ r ∈ deps op2 ⟹ r ≠ oid" using assms crdt_ops_independent_suf by fastforce thus "crdt_ops (ys @ zs @ [x]) deps" using assms(2) crdt_ops_reorder x_pair by metis qed lemma crdt_ops_rem_spec: assumes "spec_ops (xs @ [x]) deps" and "crdt_ops (ys @ [x] @ zs) deps" and "set (xs @ [x]) = set (ys @ [x] @ zs)" shows "crdt_ops (ys @ zs) deps" using assms crdt_ops_rem_last crdt_ops_reorder_spec append_assoc by metis lemma crdt_ops_rem_penultimate: assumes "crdt_ops (xs @ [(i1, r1)] @ [(i2, r2)]) deps" and "⋀r. r ∈ deps r2 ⟹ r ≠ i1" shows "crdt_ops (xs @ [(i2, r2)]) deps" proof - have "crdt_ops (xs @ [(i1, r1)]) deps" using assms(1) crdt_ops_rem_last by force hence "crdt_ops xs deps" using crdt_ops_rem_last by force moreover have "distinct (map fst (xs @ [(i1, r1)] @ [(i2, r2)]))" using assms(1) crdt_ops_distinct_fst by blast hence "i2 ∉ set (map fst xs)" by auto moreover have "crdt_ops ((xs @ [(i1, r1)]) @ [(i2, r2)]) deps" using assms(1) by auto hence "⋀r. r ∈ deps r2 ⟹ r ∈ fst ` set (xs @ [(i1, r1)])" using crdt_ops_ref_exists by metis hence "⋀r. r ∈ deps r2 ⟹ r ∈ set (map fst xs)" using assms(2) by auto moreover have "⋀r. r ∈ deps r2 ⟹ r < i2" using assms(1) crdt_ops_ref_less by fastforce ultimately show "crdt_ops (xs @ [(i2, r2)]) deps" by (simp add: crdt_ops_intro) qed lemma crdt_ops_spec_ops_exist: assumes "crdt_ops xs deps" shows "∃ys. set xs = set ys ∧ spec_ops ys deps" using assms proof(induction xs rule: List.rev_induct) case Nil then show "∃ys. set [] = set ys ∧ spec_ops ys deps" by (simp add: spec_ops_empty) next case (snoc x xs) hence IH: "∃ys. set xs = set ys ∧ spec_ops ys deps" using crdt_ops_rem_last by blast then obtain ys oid ref where "set xs = set ys" and "spec_ops ys deps" and "x = (oid, ref)" by force moreover have "∃pre suf. ys = pre@suf ∧ (∀i ∈ set (map fst pre). i < oid) ∧ (∀i ∈ set (map fst suf). oid < i)" proof - have "oid ∉ set (map fst xs)" using calculation(3) crdt_ops_unique_last snoc.prems by force hence "oid ∉ set (map fst ys)" by (simp add: calculation(1)) thus ?thesis using spec_ops_split ‹spec_ops ys deps› by blast qed from this obtain pre suf where "ys = pre @ suf" and "∀i ∈ set (map fst pre). i < oid" and "∀i ∈ set (map fst suf). oid < i" by force moreover have "set (xs @ [(oid, ref)]) = set (pre @ [(oid, ref)] @ suf)" using crdt_ops_distinct calculation snoc.prems by simp moreover have "spec_ops (pre @ [(oid, ref)] @ suf) deps" proof - have "∀r ∈ deps ref. r < oid" using calculation(3) crdt_ops_ref_less_last snoc.prems by fastforce hence "spec_ops (pre @ [(oid, ref)] @ suf) deps" using spec_ops_add_any calculation by metis thus ?thesis by simp qed ultimately show "∃ys. set (xs @ [x]) = set ys ∧ spec_ops ys deps" by blast qed end