Theory Insert_Spec

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

section‹Specifying list insertion›

theory Insert_Spec
  imports OpSet
begin

text‹In this section we consider only list insertion. We model an insertion
operation as a pair (\isa{ID, ref}), where \isa{ref} is either \isa{None}
(signifying an insertion at the head of the list) or \isa{Some r}
(an insertion immediately after a reference element with ID \isa{r}).
If the reference element does not exist, the operation does nothing.

We provide two different definitions of the interpretation function for list
insertion: \isa{insert-spec} and \isa{insert-alt}. The \isa{insert-alt} definition
matches the paper, while \isa{insert-spec} uses the Isabelle/HOL list datatype,
making it more suitable for formal reasoning. In a later subsection we prove
that the two definitions are in fact equivalent.›

fun insert_spec :: "'oid list ⇒ ('oid × 'oid option) ⇒ 'oid list" where
  "insert_spec xs     (oid, None)     = oid#xs" |
  "insert_spec []     (oid, _)        = []" |
  "insert_spec (x#xs) (oid, Some ref) =
     (if x = ref then x # oid # xs
                 else x # (insert_spec xs (oid, Some ref)))"

fun insert_alt :: "('oid × 'oid option) set ⇒ ('oid × 'oid) ⇒ ('oid × 'oid option) set" where
  "insert_alt list_rel (oid, ref) = (
      if ∃n. (ref, n) ∈ list_rel
      then {(p, n) ∈ list_rel. p ≠ ref} ∪ {(ref, Some oid)} ∪
           {(i, n). i = oid ∧ (ref, n) ∈ list_rel}
      else list_rel)"

text‹\isa{interp-ins} is the sequential interpretation of a set of insertion
operations. It starts with an empty list as initial state, and then applies
the operations from left to right.›

definition interp_ins :: "('oid × 'oid option) list ⇒ 'oid list" where
  "interp_ins ops ≡ foldl insert_spec [] ops"


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

text‹We now specialise the definitions from the abstract OpSet section for list
insertion. \isa{insert-opset} is an opset consisting only of insertion operations,
and \isa{insert-ops} is the specialisation of the \isa{spec-ops} predicate for
insertion operations. We prove several useful lemmas about \isa{insert-ops}.›

locale insert_opset = opset opset set_option
  for opset :: "('oid::{linorder} × 'oid option) set"

definition insert_ops :: "('oid::{linorder} × 'oid option) list ⇒ bool" where
  "insert_ops list ≡ spec_ops list set_option"

lemma insert_ops_NilI [intro!]:
  shows "insert_ops []"
  by (auto simp add: insert_ops_def spec_ops_def)

lemma insert_ops_rem_last [dest]:
  assumes "insert_ops (xs @ [x])"
  shows "insert_ops xs"
  using assms insert_ops_def spec_ops_rem_last by blast

lemma insert_ops_rem_cons:
  assumes "insert_ops (x # xs)"
  shows "insert_ops xs"
  using assms insert_ops_def spec_ops_rem_cons by blast

lemma insert_ops_appendD:
  assumes "insert_ops (xs @ ys)"
  shows "insert_ops xs"
  using assms by (induction ys rule: List.rev_induct,
      auto, metis insert_ops_rem_last append_assoc)

lemma insert_ops_rem_prefix:
  assumes "insert_ops (pre @ suf)"
  shows "insert_ops suf"
  using assms proof(induction pre)
  case Nil
  then show "insert_ops ([] @ suf) ⟹ insert_ops suf"
    by auto
next
  case (Cons a pre)
  have "sorted (map fst suf)"
    using assms by (simp add: insert_ops_def sorted_append spec_ops_def)
  moreover have "distinct (map fst suf)"
    using assms by (simp add: insert_ops_def spec_ops_def)
  ultimately show "insert_ops ((a # pre) @ suf) ⟹ insert_ops suf"
    by (simp add: insert_ops_def spec_ops_def)
qed

lemma insert_ops_remove1:
  assumes "insert_ops xs"
  shows "insert_ops (remove1 x xs)"
  using assms insert_ops_def spec_ops_remove1 by blast

lemma last_op_greatest:
  assumes "insert_ops (op_list @ [(oid, oper)])"
    and "x ∈ set (map fst op_list)"
  shows "x < oid"
  using assms spec_ops_id_inc insert_ops_def by metis

lemma insert_ops_ref_older:
  assumes "insert_ops (pre @ [(oid, Some ref)] @ suf)"
  shows "ref < oid"
  using assms by (auto simp add: insert_ops_def spec_ops_def)

lemma insert_ops_memb_ref_older:
  assumes "insert_ops op_list"
    and "(oid, Some ref) ∈ set op_list"
  shows "ref < oid"
  using assms insert_ops_ref_older split_list_first by fastforce


subsection ‹Properties of the \isa{insert-spec} function›

lemma insert_spec_none [simp]:
  shows "set (insert_spec xs (oid, None)) = set xs ∪ {oid}"
  by (induction xs, auto simp add: insert_commute sup_commute)

lemma insert_spec_set [simp]:
  assumes "ref ∈ set xs"
  shows "set (insert_spec xs (oid, Some ref)) = set xs ∪ {oid}"
  using assms proof(induction xs)
  assume "ref ∈ set []"
  thus "set (insert_spec [] (oid, Some ref)) = set [] ∪ {oid}"
    by auto
next
  fix a xs
  assume "ref ∈ set xs ⟹ set (insert_spec xs (oid, Some ref)) = set xs ∪ {oid}"
    and "ref ∈ set (a#xs)"
  thus "set (insert_spec (a#xs) (oid, Some ref)) = set (a#xs) ∪ {oid}"
    by(cases "a = ref", auto simp add: insert_commute sup_commute)
qed

lemma insert_spec_nonex [simp]:
  assumes "ref ∉ set xs"
  shows "insert_spec xs (oid, Some ref) = xs"
  using assms proof(induction xs)
  show "insert_spec [] (oid, Some ref) = []"
    by simp
next
  fix a xs
  assume "ref ∉ set xs ⟹ insert_spec xs (oid, Some ref) = xs"
    and "ref ∉ set (a#xs)"
  thus "insert_spec (a#xs) (oid, Some ref) = a#xs"
    by(cases "a = ref", auto simp add: insert_commute sup_commute)
qed

lemma list_greater_non_memb:
  fixes oid :: "'oid::{linorder}"
  assumes "⋀x. x ∈ set xs ⟹ x < oid"
    and "oid ∈ set xs"
  shows "False"
  using assms by blast  

lemma inserted_item_ident:
  assumes "a ∈ set (insert_spec xs (e, i))"
    and "a ∉ set xs"
  shows "a = e"
  using assms proof(induction xs)
  case Nil
  then show "a = e" by (cases i, auto)
next
  case (Cons x xs)
  then show "a = e"
  proof(cases i)
    case None
    then show "a = e" using assms by auto
  next
    case (Some ref)
    then show "a = e" using Cons by (case_tac "x = ref", auto)
  qed
qed

lemma insert_spec_distinct [intro]:
  fixes oid :: "'oid::{linorder}"
  assumes "distinct xs"
    and "⋀x. x ∈ set xs ⟹ x < oid"
    and "ref = Some r ⟶ r < oid"
  shows "distinct (insert_spec xs (oid, ref))"
  using assms(1) assms(2) proof(induction xs)
  show "distinct (insert_spec [] (oid, ref))"
    by(cases ref, auto)
next
  fix a xs
  assume IH: "distinct xs ⟹ (⋀x. x ∈ set xs ⟹ x < oid) ⟹ distinct (insert_spec xs (oid, ref))"
    and D: "distinct (a#xs)"
    and L: "⋀x. x ∈ set (a#xs) ⟹ x < oid"
  show "distinct (insert_spec (a#xs) (oid, ref))"
  proof(cases "ref")
    assume "ref = None"
    thus "distinct (insert_spec (a#xs) (oid, ref))"
      using D L by auto
  next
    fix id
    assume S: "ref = Some id"
    {
      assume EQ: "a = id"
      hence "id ≠ oid"
        using D L by auto
      moreover have "id ∉ set xs"
        using D EQ by auto
      moreover have "oid ∉ set xs"
        using L by auto
      ultimately have "id ≠ oid ∧ id ∉ set xs ∧ oid ∉ set xs ∧ distinct xs"
        using D by auto
    }
    note T = this
    {
      assume NEQ: "a ≠ id"
      have 0: "a ∉ set (insert_spec xs (oid, Some id))"
        using D L by(metis distinct.simps(2) insert_spec.simps(1) insert_spec_none insert_spec_nonex
            insert_spec_set insert_iff list.set(2) not_less_iff_gr_or_eq)
      have 1: "distinct xs"
        using D by auto
      have "⋀x. x ∈ set xs ⟹ x < oid"
        using L by auto
      hence "distinct (insert_spec xs (oid, Some id))"
        using S IH[OF 1] by blast
      hence "a ∉ set (insert_spec xs (oid, Some id)) ∧ distinct (insert_spec xs (oid, Some id))"
        using 0 by auto
    }
    from this S T show "distinct (insert_spec (a # xs) (oid, ref))"
      by clarsimp
  qed
qed

lemma insert_after_ref:
  assumes "distinct (xs @ ref # ys)"
  shows "insert_spec (xs @ ref # ys) (oid, Some ref) = xs @ ref # oid # ys"
  using assms by (induction xs, auto)

lemma insert_somewhere:
  assumes "ref = None ∨ (ref = Some r ∧ r ∈ set list)"
  shows "∃xs ys. list = xs @ ys ∧ insert_spec list (oid, ref) = xs @ oid # ys"
  using assms proof(induction list)
  assume "ref = None ∨ ref = Some r ∧ r ∈ set []"
  thus "∃xs ys. [] = xs @ ys ∧ insert_spec [] (oid, ref) = xs @ oid # ys"
  proof
    assume "ref = None"
    thus "∃xs ys. [] = xs @ ys ∧ insert_spec [] (oid, ref) = xs @ oid # ys"
      by auto
  next
    assume "ref = Some r ∧ r ∈ set []"
    thus "∃xs ys. [] = xs @ ys ∧ insert_spec [] (oid, ref) = xs @ oid # ys"
      by auto
  qed
next
  fix a list
  assume 1: "ref = None ∨ ref = Some r ∧ r ∈ set (a#list)"
    and IH: "ref = None ∨ ref = Some r ∧ r ∈ set list ⟹
         ∃xs ys. list = xs @ ys ∧ insert_spec list (oid, ref) = xs @ oid # ys"
  show "∃xs ys. a # list = xs @ ys ∧ insert_spec (a # list) (oid, ref) = xs @ oid # ys"
  proof(rule disjE[OF 1])
    assume "ref = None"
    thus "∃xs ys. a # list = xs @ ys ∧ insert_spec (a # list) (oid, ref) = xs @ oid # ys"
      by force
  next
    assume "ref = Some r ∧ r ∈ set (a # list)"
    hence 2: "r = a ∨ r ∈ set list" and 3: "ref = Some r"
      by auto
    show "∃xs ys. a # list = xs @ ys ∧ insert_spec (a # list) (oid, ref) = xs @ oid # ys"
    proof(rule disjE[OF 2])
      assume "r = a"
      thus "∃xs ys. a # list = xs @ ys ∧ insert_spec (a # list) (oid, ref) = xs @ oid # ys"
        using 3 by(metis append_Cons append_Nil insert_spec.simps(3))
    next
      assume "r ∈ set list"
      from this obtain xs ys
        where "list = xs @ ys ∧ insert_spec list (oid, ref) = xs @ oid # ys"
        using IH 3 by auto
      thus "∃xs ys. a # list = xs @ ys ∧ insert_spec (a # list) (oid, ref) = xs @ oid # ys"
        using 3 by clarsimp (metis append_Cons append_Nil)
    qed
  qed
qed

lemma insert_first_part:
  assumes "ref = None ∨ (ref = Some r ∧ r ∈ set xs)"
  shows "insert_spec (xs @ ys) (oid, ref) = (insert_spec xs (oid, ref)) @ ys"
  using assms proof(induction ys rule: rev_induct)
  assume "ref = None ∨ ref = Some r ∧ r ∈ set xs"
  thus "insert_spec (xs @ []) (oid, ref) = insert_spec xs (oid, ref) @ []"
    by auto
next
  fix x xsa
  assume IH: "ref = None ∨ ref = Some r ∧ r ∈ set xs ⟹ insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa"
    and "ref = None ∨ ref = Some r ∧ r ∈ set xs"
  thus "insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]"
  proof(induction xs)
    assume "ref = None ∨ ref = Some r ∧ r ∈ set []"
    thus "insert_spec ([] @ xsa @ [x]) (oid, ref) = insert_spec [] (oid, ref) @ xsa @ [x]"
      by auto
  next
    fix a xs
    assume 1: "ref = None ∨ ref = Some r ∧ r ∈ set (a # xs)"
      and 2: "((ref = None ∨ ref = Some r ∧ r ∈ set xs ⟹ insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa) ⟹
             ref = None ∨ ref = Some r ∧ r ∈ set xs ⟹ insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x])"
      and 3: "(ref = None ∨ ref = Some r ∧ r ∈ set (a # xs) ⟹ insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa)"
    show "insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]"
    proof(rule disjE[OF 1])
      assume "ref = None"
      thus "insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]"
        by auto
    next
      assume "ref = Some r ∧ r ∈ set (a # xs)"
      thus "insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]"
        using 2 3 by auto
    qed
  qed
qed

lemma insert_second_part:
  assumes "ref = Some r"
    and "r ∉ set xs"
    and "r ∈ set ys"
  shows "insert_spec (xs @ ys) (oid, ref) = xs @ (insert_spec ys (oid, ref))"
  using assms proof(induction xs)
  assume "ref = Some r"
  thus "insert_spec ([] @ ys) (oid, ref) = [] @ insert_spec ys (oid, ref)"
    by auto
next
  fix a xs
  assume "ref = Some r" and "r ∉ set (a # xs)" and "r ∈ set ys"
    and "ref = Some r ⟹ r ∉ set xs ⟹ r ∈ set ys ⟹ insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref)"
  thus "insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)"
    by auto
qed


subsection ‹Properties of the \isa{interp-ins} function›

lemma interp_ins_empty [simp]:
  shows "interp_ins [] = []"
  by (simp add: interp_ins_def)

lemma interp_ins_tail_unfold:
  shows "interp_ins (xs @ [x]) = insert_spec (interp_ins xs) x"
  by (clarsimp simp add: interp_ins_def)

lemma interp_ins_subset [simp]:
  shows "set (interp_ins op_list) ⊆ set (map fst op_list)"
proof(induction op_list rule: List.rev_induct)
  case Nil
  then show "set (interp_ins []) ⊆ set (map fst [])"
    by (simp add: interp_ins_def)
next
  case (snoc x xs)
  hence IH: "set (interp_ins xs) ⊆ set (map fst xs)"
    using interp_ins_def by blast
  obtain oid ref where x_pair: "x = (oid, ref)"
    by fastforce
  hence spec: "interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref)"
    by (simp add: interp_ins_def)
  then show "set (interp_ins (xs @ [x])) ⊆ set (map fst (xs @ [x]))"
  proof(cases ref)
    case None
    then show "set (interp_ins (xs @ [x])) ⊆ set (map fst (xs @ [x]))"
      using IH spec x_pair by auto
  next
    case (Some a)
    then show "set (interp_ins (xs @ [x])) ⊆ set (map fst (xs @ [x]))"
      using IH spec x_pair by (cases "a ∈ set (interp_ins xs)", auto)
  qed
qed

lemma interp_ins_distinct:
  assumes "insert_ops op_list"
  shows "distinct (interp_ins op_list)"
  using assms proof(induction op_list rule: rev_induct)
  case Nil
  then show "distinct (interp_ins [])"
    by (simp add: interp_ins_def)
next
  case (snoc x xs)
  hence IH: "distinct (interp_ins xs)" by blast
  obtain oid ref where x_pair: "x = (oid, ref)" by force
  hence "∀x ∈ set (map fst xs). x < oid"
    using last_op_greatest snoc.prems by blast
  hence "∀x ∈ set (interp_ins xs). x < oid"
    using interp_ins_subset by fastforce
  hence "distinct (insert_spec (interp_ins xs) (oid, ref))"
    using IH insert_spec_distinct insert_spec_nonex by metis
  then show "distinct (interp_ins (xs @ [x]))"
    by (simp add: x_pair interp_ins_tail_unfold)
qed


subsection ‹Equivalence of the two definitions of insertion›

text‹At the beginning of this section we gave two different definitions of
interpretation functions for list insertion: \isa{insert-spec} and
\isa{insert-alt}. In this section we prove that the two are equivalent.

We first define how to derive the successor relation from an Isabelle list.
This relation contains (\isa{id}, \isa{None}) if \isa{id} is the last element
of the list, and (\isa{id1}, \isa{id2}) if \isa{id1} is immediately
followed by \isa{id2} in the list.›

fun succ_rel :: "'oid list ⇒ ('oid × 'oid option) set" where
  "succ_rel [] = {}" |
  "succ_rel [head] = {(head, None)}" |
  "succ_rel (head#x#xs) = {(head, Some x)} ∪ succ_rel (x#xs)"

text‹\isa{interp-alt} is the equivalent of \isa{interp-ins}, but using
\isa{insert-alt} instead of \isa{insert-spec}. To match the paper, it uses a
distinct head element to refer to the beginning of the list.›

definition interp_alt :: "'oid ⇒ ('oid × 'oid option) list ⇒ ('oid × 'oid option) set" where
  "interp_alt head ops ≡ foldl insert_alt {(head, None)}
     (map (λx. case x of
            (oid, None)     ⇒ (oid, head) |
            (oid, Some ref) ⇒ (oid, ref)) 
      ops)"

lemma succ_rel_set_fst:
  shows "fst ` (succ_rel xs) = set xs"
  by (induction xs rule: succ_rel.induct, auto)

lemma succ_rel_functional:
  assumes "(a, b1) ∈ succ_rel xs"
    and "(a, b2) ∈ succ_rel xs"
    and "distinct xs"
  shows "b1 = b2"
  using assms proof(induction xs rule: succ_rel.induct)
  case 1
  then show ?case by simp
next
  case (2 head)
  then show ?case by simp
next
  case (3 head x xs)
  then show ?case
  proof(cases "a = head")
    case True
    hence "a ∉ set (x#xs)"
      using 3 by auto
    hence "a ∉ fst ` (succ_rel (x#xs))"
      using succ_rel_set_fst by metis
    then show "b1 = b2"
      using 3 image_iff by fastforce
  next
    case False
    hence "{(a, b1), (a, b2)} ⊆ succ_rel (x#xs)"
      using 3 by auto
    moreover have "distinct (x#xs)"
      using 3 by auto
    ultimately show "b1 = b2"
      using "3.IH" by auto
  qed
qed

lemma succ_rel_rem_head:
  assumes "distinct (x # xs)"
  shows "{(p, n) ∈ succ_rel (x # xs). p ≠ x} = succ_rel xs"
proof -
  have head_notin: "x ∉ fst ` succ_rel xs"
    using assms by (simp add: succ_rel_set_fst)
  moreover obtain y where "(x, y) ∈ succ_rel (x # xs)"
    by (cases xs, auto)
  moreover have "succ_rel (x # xs) = {(x, y)} ∪ succ_rel xs"
    using calculation head_notin image_iff by (cases xs, fastforce+)
  moreover from this have "⋀n. (x, n) ∈ succ_rel (x # xs) ⟹ n = y"
    by (metis Pair_inject fst_conv head_notin image_eqI insertE insert_is_Un)
  hence "{(p, n) ∈ succ_rel (x # xs). p ≠ x} = succ_rel (x # xs) - {(x, y)}"
    by blast
  moreover have "succ_rel (x # xs) - {(x, y)} = succ_rel xs"
    using image_iff calculation by fastforce
  ultimately show "{(p, n) ∈ succ_rel (x # xs). p ≠ x} = succ_rel xs"
    by simp
qed

lemma succ_rel_swap_head:
  assumes "distinct (ref # list)"
    and "(ref, n) ∈ succ_rel (ref # list)"
  shows "succ_rel (oid # list) = {(oid, n)} ∪ succ_rel list"
proof(cases list)
  case Nil
  then show ?thesis using assms by auto
next
  case (Cons a list)
  moreover from this have "n = Some a"
    by (metis Un_iff assms singletonI succ_rel.simps(3) succ_rel_functional)
  ultimately show ?thesis by simp
qed

lemma succ_rel_insert_alt:
  assumes "a ≠ ref"
    and "distinct (oid # a # b # list)"
  shows "insert_alt (succ_rel (a # b # list)) (oid, ref) =
         {(a, Some b)} ∪ insert_alt (succ_rel (b # list)) (oid, ref)"
proof(cases "∃n. (ref, n) ∈ succ_rel (a # b # list)")
  case True
  hence "insert_alt (succ_rel (a # b # list)) (oid, ref) =
           {(p, n) ∈ succ_rel (a # b # list). p ≠ ref} ∪ {(ref, Some oid)} ∪
           {(i, n). i = oid ∧ (ref, n) ∈ succ_rel (a # b # list)}"
    by simp
  moreover have "{(p, n) ∈ succ_rel (a # b # list). p ≠ ref} =
                 {(a, Some b)} ∪ {(p, n) ∈ succ_rel (b # list). p ≠ ref}"
    using assms(1) by auto
  moreover have "insert_alt (succ_rel (b # list)) (oid, ref) =
           {(p, n) ∈ succ_rel (b # list). p ≠ ref} ∪ {(ref, Some oid)} ∪
           {(i, n). i = oid ∧ (ref, n) ∈ succ_rel (b # list)}"
  proof -
    have "∃n. (ref, n) ∈ succ_rel (b # list)"
      using assms(1) True by auto
    thus ?thesis by simp
  qed
  moreover have "{(i, n). i = oid ∧ (ref, n) ∈ succ_rel (a # b # list)} =
                 {(i, n). i = oid ∧ (ref, n) ∈ succ_rel (b # list)}"
    using assms(1) by auto
  ultimately show ?thesis by simp
next
  case False
  then show ?thesis by auto
qed

lemma succ_rel_insert_head:
  assumes "distinct (ref # list)"
  shows "succ_rel (insert_spec (ref # list) (oid, Some ref)) =
         insert_alt (succ_rel (ref # list)) (oid, ref)"
proof -
  obtain n where ref_in_rel: "(ref, n) ∈ succ_rel (ref # list)"
    by (cases list, auto)
  moreover from this have "{(p, n) ∈ succ_rel (ref # list). p ≠ ref} = succ_rel list"
    using assms succ_rel_rem_head by (metis (mono_tags, lifting))
  moreover have "{(i, n). i = oid ∧ (ref, n) ∈ succ_rel (ref # list)} = {(oid, n)}"
  proof -
    have "⋀nx. (ref, nx) ∈ succ_rel (ref # list) ⟹ nx = n"
      using assms by (simp add: succ_rel_functional ref_in_rel)
    hence "{(i, n) ∈ succ_rel (ref # list). i = ref} ⊆ {(ref, n)}"
      by blast
    moreover have "{(ref, n)} ⊆ {(i, n) ∈ succ_rel (ref # list). i = ref}"
      by (simp add: ref_in_rel)
    ultimately show ?thesis by blast
  qed
  moreover have "insert_alt (succ_rel (ref # list)) (oid, ref) =
                   {(p, n) ∈ succ_rel (ref # list). p ≠ ref} ∪ {(ref, Some oid)} ∪
                   {(i, n). i = oid ∧ (ref, n) ∈ succ_rel (ref # list)}"
  proof -
    have "∃n. (ref, n) ∈ succ_rel (ref # list)"
      using ref_in_rel by blast
    thus ?thesis by simp
  qed
  ultimately have "insert_alt (succ_rel (ref # list)) (oid, ref) =
                   succ_rel list ∪ {(ref, Some oid)} ∪ {(oid, n)}"
    by simp
  moreover have "succ_rel (oid # list) = {(oid, n)} ∪ succ_rel list"
    using assms ref_in_rel succ_rel_swap_head by metis
  hence "succ_rel (ref # oid # list) = {(ref, Some oid), (oid, n)} ∪ succ_rel list"
    by auto
  ultimately show "succ_rel (insert_spec (ref # list) (oid, Some ref)) =
                   insert_alt (succ_rel (ref # list)) (oid, ref)"
    by auto
qed

lemma succ_rel_insert_later:
  assumes "succ_rel (insert_spec (b # list) (oid, Some ref)) =
           insert_alt (succ_rel (b # list)) (oid, ref)"
    and "a ≠ ref"
    and "distinct (a # b # list)"
  shows "succ_rel (insert_spec (a # b # list) (oid, Some ref)) =
         insert_alt (succ_rel (a # b # list)) (oid, ref)"
proof -
  have "succ_rel (a # b # list) = {(a, Some b)} ∪ succ_rel (b # list)"
    by simp
  moreover have "insert_spec (a # b # list) (oid, Some ref) =
                 a # (insert_spec (b # list) (oid, Some ref))"
    using assms(2) by simp
  hence "succ_rel (insert_spec (a # b # list) (oid, Some ref)) =
         {(a, Some b)} ∪ succ_rel (insert_spec (b # list) (oid, Some ref))"
    by auto
  hence "succ_rel (insert_spec (a # b # list) (oid, Some ref)) =
         {(a, Some b)} ∪ insert_alt (succ_rel (b # list)) (oid, ref)"
    using assms(1) by auto
  moreover have "insert_alt (succ_rel (a # b # list)) (oid, ref) =
                 {(a, Some b)} ∪ insert_alt (succ_rel (b # list)) (oid, ref)"
    using succ_rel_insert_alt assms(2) by auto
  ultimately show ?thesis by blast
qed

lemma succ_rel_insert_Some:
  assumes "distinct list"
  shows "succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)"
  using assms proof(induction list)
  case Nil
  then show "succ_rel (insert_spec [] (oid, Some ref)) = insert_alt (succ_rel []) (oid, ref)"
    by simp
next
  case (Cons a list)
  hence "distinct (a # list)"
    by simp
  then show "succ_rel (insert_spec (a # list) (oid, Some ref)) =
             insert_alt (succ_rel (a # list)) (oid, ref)"
  proof(cases "a = ref")
    case True
    then show ?thesis
      using succ_rel_insert_head ‹distinct (a # list)› by metis
  next
    case False
    hence "a ≠ ref" by simp
    moreover have "succ_rel (insert_spec list (oid, Some ref)) =
                   insert_alt (succ_rel list) (oid, ref)"
      using Cons.IH Cons.prems by auto
    ultimately show "succ_rel (insert_spec (a # list) (oid, Some ref)) =
                     insert_alt (succ_rel (a # list)) (oid, ref)"
      by (cases list, force, metis Cons.prems succ_rel_insert_later)
  qed
qed

text‹The main result of this section, that \isa{insert-spec} and \isa{insert-alt}
are equivalent.›

theorem insert_alt_equivalent:
  assumes "insert_ops ops"
    and "head ∉ fst ` set ops"
    and "⋀r. Some r ∈ snd ` set ops ⟹ r ≠ head"
  shows "succ_rel (head # interp_ins ops) = interp_alt head ops"
  using assms proof(induction ops rule: List.rev_induct)
  case Nil
  then show "succ_rel (head # interp_ins []) = interp_alt head []"
    by (simp add: interp_ins_def interp_alt_def)
next
  case (snoc x xs)
  have IH: "succ_rel (head # interp_ins xs) = interp_alt head xs"
    using snoc by auto
  have distinct_list: "distinct (head # interp_ins xs)"
  proof -
    have "distinct (interp_ins xs)"
      using interp_ins_distinct snoc.prems(1) by blast
    moreover have "set (interp_ins xs) ⊆ fst ` set xs"
      using interp_ins_subset snoc.prems(1) by fastforce
    ultimately show "distinct (head # interp_ins xs)"
      using snoc.prems(2) by auto
  qed
  obtain oid r where x_pair: "x = (oid, r)" by force
  then show "succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])"
  proof(cases r)
    case None
    have "interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, head)"
      by (simp add: interp_alt_def None x_pair)
    moreover have "... = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)"
      by (simp add: IH)
    moreover have "... = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))"
      using distinct_list succ_rel_insert_Some by metis
    moreover have "... = succ_rel (head # (insert_spec (interp_ins xs) (oid, None)))"
      by auto
    moreover have "... = succ_rel (head # (interp_ins (xs @ [x])))"
      by (simp add: interp_ins_tail_unfold None x_pair)
    ultimately show ?thesis by simp
  next
    case (Some ref)
    have "ref ≠ head"
      by (simp add: Some snoc.prems(3) x_pair)
    have "interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, ref)"
      by (simp add: interp_alt_def Some x_pair)
    moreover have "... = insert_alt (succ_rel (head # interp_ins xs)) (oid, ref)"
      by (simp add: IH)
    moreover have "... = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))"
      using distinct_list succ_rel_insert_Some by metis
    moreover have "... = succ_rel (head # (insert_spec (interp_ins xs) (oid, Some ref)))"
      using ‹ref ≠ head› by auto
    moreover have "... = succ_rel (head # (interp_ins (xs @ [x])))"
      by (simp add: interp_ins_tail_unfold Some x_pair)
    ultimately show ?thesis by simp
  qed
qed


subsection ‹The \isa{list-order} predicate›

text‹\isa{list-order ops x y} holds iff, after interpreting the list of
insertion operations \isa{ops}, the list element with ID \isa{x} appears
before the list element with ID \isa{y} in the resulting list. We prove several
lemmas about this predicate; in particular, that executing additional insertion
operations does not change the relative ordering of existing list elements.›

definition list_order :: "('oid::{linorder} × 'oid option) list ⇒ 'oid ⇒ 'oid ⇒ bool" where
  "list_order ops x y ≡ ∃xs ys zs. interp_ins ops = xs @ [x] @ ys @ [y] @ zs"

lemma list_orderI:
  assumes "interp_ins ops = xs @ [x] @ ys @ [y] @ zs"
  shows "list_order ops x y"
  using assms by (auto simp add: list_order_def)

lemma list_orderE:
  assumes "list_order ops x y"
  shows "∃xs ys zs. interp_ins ops = xs @ [x] @ ys @ [y] @ zs"
  using assms by (auto simp add: list_order_def)

lemma list_order_memb1:
  assumes "list_order ops x y"
  shows "x ∈ set (interp_ins ops)"
  using assms by (auto simp add: list_order_def)

lemma list_order_memb2:
  assumes "list_order ops x y"
  shows "y ∈ set (interp_ins ops)"
  using assms by (auto simp add: list_order_def)

lemma list_order_trans:
  assumes "insert_ops op_list"
    and "list_order op_list x y"
    and "list_order op_list y z"
  shows "list_order op_list x z"
proof -
  obtain xxs xys xzs where 1: "interp_ins op_list = (xxs@[x]@xys)@(y#xzs)"
    using assms by (auto simp add: list_order_def interp_ins_def)
  obtain yxs yys yzs where 2: "interp_ins op_list = yxs@y#(yys@[z]@yzs)"
    using assms by (auto simp add: list_order_def interp_ins_def)
  have 3: "distinct (interp_ins op_list)"
    using assms interp_ins_distinct by blast
  hence "xzs = yys@[z]@yzs"
    using distinct_list_split[OF 3, OF 2, OF 1] by auto
  hence "interp_ins op_list = xxs@[x]@xys@[y]@yys@[z]@yzs"
    using 1 2 3 by clarsimp
  thus "list_order op_list x z"
    using assms by (metis append.assoc list_orderI)
qed

lemma insert_preserves_order:
  assumes "insert_ops ops" and "insert_ops rest"
    and "rest = before @ after"
    and "ops  = before @ (oid, ref) # after"
  shows "∃xs ys zs. interp_ins rest = xs @ zs ∧ interp_ins ops = xs @ ys @ zs"
  using assms proof(induction after arbitrary: rest ops rule: List.rev_induct)
  case Nil
  then have 1: "interp_ins ops = insert_spec (interp_ins before) (oid, ref)"
    by (simp add: interp_ins_tail_unfold)
  then show "∃xs ys zs. interp_ins rest = xs @ zs ∧ interp_ins ops = xs @ ys @ zs"
  proof(cases ref)
    case None
    hence "interp_ins rest = [] @ (interp_ins before) ∧
           interp_ins ops = [] @ [oid] @ (interp_ins before)"
      using 1 Nil.prems(3) by simp
    then show ?thesis by blast
  next
    case (Some a)
    then show ?thesis
    proof(cases "a ∈ set (interp_ins before)")
      case True
      then obtain xs ys where "interp_ins before = xs @ ys ∧
          insert_spec (interp_ins before) (oid, ref) = xs @ oid # ys"
        using insert_somewhere Some by metis
      hence "interp_ins rest = xs @ ys ∧ interp_ins ops = xs @ [oid] @ ys"
        using 1 Nil.prems(3) by auto
      then show ?thesis by blast
    next
      case False
      hence "interp_ins ops = (interp_ins rest) @ [] @ []"
        using insert_spec_nonex 1 Nil.prems(3) Some by simp
      then show ?thesis by blast
    qed
  qed
next
  case (snoc oper op_list)
  then have "insert_ops ((before @ (oid, ref) # op_list) @ [oper])"
    and "insert_ops ((before @ op_list) @ [oper])"
    by auto
  then have ops1: "insert_ops (before @ op_list)"
    and ops2: "insert_ops (before @ (oid, ref) # op_list)"
    using insert_ops_appendD by blast+
  then obtain xs ys zs where IH1: "interp_ins (before @ op_list) = xs @ zs"
    and IH2: "interp_ins (before @ (oid, ref) # op_list) = xs @ ys @ zs"
    using snoc.IH by blast
  obtain i2 r2 where "oper = (i2, r2)" by force
  then show "∃xs ys zs. interp_ins rest = xs @ zs ∧ interp_ins ops = xs @ ys @ zs"
  proof(cases r2)
    case None
    hence "interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs"
      by (metis IH1 ‹oper = (i2, r2)› append.assoc append_Cons insert_spec.simps(1)
          interp_ins_tail_unfold)
    moreover have "interp_ins (before @ (oid, ref) # op_list @ [oper]) = (i2 # xs) @ ys @ zs"
      by (metis IH2 None ‹oper = (i2, r2)› append.assoc append_Cons insert_spec.simps(1)
          interp_ins_tail_unfold)
    ultimately show ?thesis
      using snoc.prems(3) snoc.prems(4) by blast
  next
    case (Some r)
    then have 1: "interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) =
                  insert_spec (xs @ ys @ zs) (i2, Some r)"
      by (metis IH2 append.assoc append_Cons interp_ins_tail_unfold)
    have 2: "interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)"
      by (metis IH1 append.assoc interp_ins_tail_unfold Some)
    consider (r_xs) "r ∈ set xs" | (r_ys) "r ∈ set ys" | (r_zs) "r ∈ set zs" |
      (r_nonex) "r ∉ set (xs @ ys @ zs)"
      by auto
    then show "∃xs ys zs. interp_ins rest = xs @ zs ∧ interp_ins ops = xs @ ys @ zs"
    proof(cases)
      case r_xs
      from this have "insert_spec (xs @ ys @ zs) (i2, Some r) =
                      (insert_spec xs (i2, Some r)) @ ys @ zs"
        by (meson insert_first_part)
      moreover have "insert_spec (xs @ zs) (i2, Some r) = (insert_spec xs (i2, Some r)) @ zs"
        by (meson r_xs insert_first_part)
      ultimately show ?thesis
        using 1 2 ‹oper = (i2, r2)› snoc.prems by auto
    next
      case r_ys
      hence "r ∉ set xs" and "r ∉ set zs"
        using IH2 ops2 interp_ins_distinct by force+
      moreover from this have "insert_spec (xs @ ys @ zs) (i2, Some r) =
                               xs @ (insert_spec ys (i2, Some r)) @ zs"
        using insert_first_part insert_second_part insert_spec_nonex
        by (metis Some UnE r_ys set_append)
      moreover have "insert_spec (xs @ zs) (i2, Some r) = xs @ zs"
        by (simp add: Some calculation(1) calculation(2))
      ultimately show ?thesis
        using 1 2 ‹oper = (i2, r2)› snoc.prems by auto
    next
      case r_zs
      hence "r ∉ set xs" and "r ∉ set ys"
        using IH2 ops2 interp_ins_distinct by force+
      moreover from this have "insert_spec (xs @ ys @ zs) (i2, Some r) =
                               xs @ ys @ (insert_spec zs (i2, Some r))"
        by (metis Some UnE insert_second_part insert_spec_nonex set_append)
      moreover have "insert_spec (xs @ zs) (i2, Some r) = xs @ (insert_spec zs (i2, Some r))"
        by (simp add: r_zs calculation(1) insert_second_part)
      ultimately show ?thesis
        using 1 2 ‹oper = (i2, r2)› snoc.prems by auto
    next
      case r_nonex
      then have "insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs"
        by simp
      moreover have "insert_spec (xs @ zs) (i2, Some r) = xs @ zs"
        using r_nonex by simp
      ultimately show ?thesis
        using 1 2 ‹oper = (i2, r2)› snoc.prems by auto
    qed
  qed
qed

lemma distinct_fst:
  assumes "distinct (map fst A)"
  shows "distinct A"
  using assms by (induction A) auto

lemma subset_distinct_le:
  assumes "set A ⊆ set B" and "distinct A" and "distinct B"
  shows "length A ≤ length B"
  using assms proof(induction B arbitrary: A)
  case Nil
  then show "length A ≤ length []" by simp
next
  case (Cons a B)
  then show "length A ≤ length (a # B)"
  proof(cases "a ∈ set A")
    case True
    have "set (remove1 a A) ⊆ set B"
      using Cons.prems by auto
    hence "length (remove1 a A) ≤ length B"
      using Cons.IH Cons.prems by auto
    then show "length A ≤ length (a # B)"
      by (simp add: True length_remove1)
  next
    case False
    hence "set A ⊆ set B"
      using Cons.prems by auto
    hence "length A ≤ length B"
      using Cons.IH Cons.prems by auto
    then show "length A ≤ length (a # B)"
      by simp
  qed
qed

lemma set_subset_length_eq:
  assumes "set A ⊆ set B" and "length B ≤ length A"
    and "distinct A" and "distinct B"
  shows "set A = set B"
proof -
  have "length A ≤ length B"
    using assms by (simp add: subset_distinct_le)
  moreover from this have "card (set A) = card (set B)"
    using assms by (simp add: distinct_card le_antisym)
  ultimately show "set A = set B"
    using assms(1) by (simp add: card_subset_eq)
qed

lemma length_diff_Suc_exists:
  assumes "length xs - length ys = Suc m"
    and "set ys ⊆ set xs"
    and "distinct ys" and "distinct xs"
  shows "∃e. e ∈ set xs ∧ e ∉ set ys"
  using assms proof(induction xs arbitrary: ys)
  case Nil
  then show "∃e. e ∈ set [] ∧ e ∉ set ys"
    by simp
next
  case (Cons a xs)
  then show "∃e. e ∈ set (a # xs) ∧ e ∉ set ys"
  proof(cases "a ∈ set ys")
    case True
    have IH: "∃e. e ∈ set xs ∧ e ∉ set (remove1 a ys)"
    proof -
      have "length xs - length (remove1 a ys) = Suc m"
        by (metis Cons.prems(1) One_nat_def Suc_pred True diff_Suc_Suc length_Cons
            length_pos_if_in_set length_remove1)
      moreover have "set (remove1 a ys) ⊆ set xs"
        using Cons.prems by auto
      ultimately show ?thesis
        by (meson Cons.IH Cons.prems distinct.simps(2) distinct_remove1)
    qed
    moreover have "set ys - {a} ⊆ set xs"
      using Cons.prems(2) by auto
    ultimately show "∃e. e ∈ set (a # xs) ∧ e ∉ set ys"
      by (metis Cons.prems(4) distinct.simps(2) in_set_remove1 set_subset_Cons subsetCE)
  next
    case False
    then show "∃e. e ∈ set (a # xs) ∧ e ∉ set ys"
      by auto
  qed
qed

lemma app_length_lt_exists:
  assumes "xsa @ zsa = xs @ ys"
    and "length xsa ≤ length xs"
  shows "xsa @ (drop (length xsa) xs) = xs"
  using assms by (induction xsa arbitrary: xs zsa ys, simp,
      metis append_eq_append_conv_if append_take_drop_id)

lemma list_order_monotonic:
  assumes "insert_ops A" and "insert_ops B"
    and "set A ⊆ set B"
    and "list_order A x y"
  shows "list_order B x y"
  using assms proof(induction rule: measure_induct_rule[where f="λx. (length x - length A)"])
  case (less xa)
  have "distinct (map fst A)" and "distinct (map fst xa)" and
    "sorted (map fst A)" and "sorted (map fst xa)"
    using less.prems by (auto simp add: insert_ops_def spec_ops_def)
  hence "distinct A" and "distinct xa"
    by (auto simp add: distinct_fst)
  then show "list_order xa x y"
  proof(cases "length xa - length A")
    case 0
    hence "set A = set xa"
      using set_subset_length_eq less.prems(3) ‹distinct A› ‹distinct xa› diff_is_0_eq by blast
    hence "A = xa"
      using ‹distinct (map fst A)› ‹distinct (map fst xa)›
        ‹sorted (map fst A)› ‹sorted (map fst xa)› map_sorted_distinct_set_unique
      by (metis distinct_map less.prems(3) subset_Un_eq)
    then show "list_order xa x y" 
      using less.prems(4) by blast
  next
    case (Suc nat)
    then obtain e where "e ∈ set xa" and "e ∉ set A"
      using length_diff_Suc_exists ‹distinct A› ‹distinct xa› less.prems(3) by blast
    hence IH: "list_order (remove1 e xa) x y"
    proof -
      have "length (remove1 e xa) - length A < Suc nat"
        using diff_Suc_1 diff_commute length_remove1 less_Suc_eq Suc ‹e ∈ set xa› by metis
      moreover have "insert_ops (remove1 e xa)"
        by (simp add: insert_ops_remove1 less.prems(2))
      moreover have "set A ⊆ set (remove1 e xa)"
        by (metis (no_types, lifting) ‹e ∉ set A› in_set_remove1 less.prems(3) rev_subsetD subsetI)
      ultimately show ?thesis
        by (simp add: Suc less.IH less.prems(1) less.prems(4))
    qed
    then obtain xs ys zs where "interp_ins (remove1 e xa) = xs @ x # ys @ y # zs"
      using list_order_def by fastforce
    moreover obtain oid ref where e_pair: "e = (oid, ref)"
      by fastforce
    moreover obtain ps ss where xa_split: "xa = ps @ [e] @ ss" and "e ∉ set ps"
      using split_list_first ‹e ∈ set xa› by fastforce
    hence "remove1 e (ps @ e # ss) = ps @ ss"
      by (simp add: remove1_append)
    moreover from this have "insert_ops (ps @ ss)" and "insert_ops (ps @ e # ss)"
      using xa_split less.prems(2) by (metis append_Cons append_Nil insert_ops_remove1, auto)
    then obtain xsa ysa zsa where "interp_ins (ps @ ss) = xsa @ zsa"
      and interp_xa: "interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa"
      using insert_preserves_order e_pair by metis
    moreover have xsa_zsa: "xsa @ zsa = xs @ x # ys @ y # zs"
      using interp_ins_def remove1_append calculation xa_split by auto
    then show "list_order xa x y"
    proof(cases "length xsa ≤ length xs")
      case True
      then obtain ts where "xsa@ts = xs"
        using app_length_lt_exists xsa_zsa by blast
      hence "interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs"
        using calculation xa_split by auto
      then show "list_order xa x y"
        using list_order_def by blast
    next
      case False
      then show "list_order xa x y"
      proof(cases "length xsa ≤ length (xs @ x # ys)")
        case True
        have xsa_zsa1: "xsa @ zsa = (xs @ x # ys) @ (y # zs)"
          by (simp add: xsa_zsa)
        then obtain us where "xsa @ us = xs @ x # ys"
          using app_length_lt_exists True by blast
        moreover from this have "xs @ x # (drop (Suc (length xs)) xsa) = xsa"
          using append_eq_append_conv_if id_take_nth_drop linorder_not_less
            nth_append nth_append_length False by metis
        moreover have "us @ y # zs = zsa"
          by (metis True xsa_zsa1 append_eq_append_conv_if append_eq_conv_conj calculation(1))
        ultimately have "interp_ins xa = xs @ [x] @
              ((drop (Suc (length xs)) xsa) @ ysa @ us) @ [y] @ zs"
          by (simp add: e_pair interp_xa xa_split)
        then show "list_order xa x y"
          using list_order_def by blast
      next
        case False
        hence "length (xs @ x # ys) < length xsa"
          using not_less by blast
        hence "length (xs @ x # ys @ [y]) ≤ length xsa"
          by simp
        moreover have "(xs @ x # ys @ [y]) @ zs = xsa @ zsa"
          by (simp add: xsa_zsa)
        ultimately obtain vs where "(xs @ x # ys @ [y]) @ vs = xsa"
          using app_length_lt_exists by blast
        hence "xsa @ ysa @ zsa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa"
          by simp
        hence "interp_ins xa = xs @ [x] @ ys @ [y] @ (vs @ ysa @ zsa)"
          using e_pair interp_xa xa_split by auto
        then show "list_order xa x y"
          using list_order_def by blast
      qed
    qed
  qed
qed


end