# 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"
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 [] = []"

lemma interp_ins_tail_unfold:
shows "interp_ins (xs @ [x]) = insert_spec (interp_ins xs) x"

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 [])"
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)"
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 [])"
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]))"
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 [] = {}" |

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
(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
then show ?case by simp
next
then show ?case
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

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

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

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}"
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"
using assms proof(induction ops rule: List.rev_induct)
case Nil
next
case (snoc x 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
by (simp add: interp_alt_def None x_pair)
moreover have "... = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)"
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)
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)"
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
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)"
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)"
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"
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)"
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"
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)"
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"
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
```