Quelle  OpSet.thy

(* 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
  to any one particular datatype. We develop a library of useful lemmas
  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
  IDs (represented here with the \isa{linorder} typeclass), and satisfying the
  properties:
 begin{enumerate}
 item The ID is unique (that is, if any two pairs in the set have the same ID,
  their operation is also the same).
 item If the operation references the IDs of any other operations, those
  IDs are less than that of the operation itself, according to the
  order on IDs. To avoid assuming anything about the structure of operations
 , we use a function \isa{deps} that returns the set of dependent IDs for a
  operation. This requirement is a weak expression of causality: an operation
  only depend on causally prior operations, and by making the total order on
  a linear extension of the causal order, we can easily ensure that any
  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
  because, although an operation can depend on causally prior operations,
  OpSet does not require those prior operations to actually exist. This weak
  makes the OpSet model more general and simplifies reasoning about
 .›

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
  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
  to the linearisation of an OpSet, and which we use for sequentially
  the OpSet. A list satisfies \isa{spec-ops} iff it is sorted in ascending
  of IDs, if the IDs are unique, and if every operation's dependencies have
  IDs than the operation itself. A list is implicitly finite in Isabelle/HOL.
  requirements correspond to the OpSet definition above, and indeed we prove
  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
  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
  OpSet into a list. Like \isa{spec-ops}, it requires IDs to be unique. However,
  other properties are different: \isa{crdt-ops} does not require operations to
  in sorted order, but instead, whenever any operation references the
  of a prior operation, that prior operation must appear previously in the
 isa{crdt-ops} list. Thus, the order of operations is partially constrained:
  must appear in causal order, but concurrent operations can be
  arbitrarily.

  list describes the operation sequence in the order it is typically applied to
  operation-based CRDT. Applying operations in the order they appear in
 isa{crdt-ops} requires that concurrent operations commute. For any \isa{crdt-ops}
  sequence, there is a permutation that satisfies the \isa{spec-ops}
 . Thus, to check whether a CRDT satisfies its sequential specification,
  can prove that interpreting any \isa{crdt-ops} operation sequence with the
  operation interpretation results in the same end result as
  the \isa{spec-ops} permutation of that operation sequence with the
  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