[STATEMENT]
lemma interp_ins_ref_nonex:
  assumes "insert_ops ops"
    and "ops = xs @ [(oid, Some ref)] @ ys"
    and "ref \<notin> set (interp_ins xs)"
  shows "oid \<notin> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<notin> set (interp_ins ops)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
ops = xs @ [(oid, Some ref)] @ ys
ref \<notin> set (interp_ins xs)

goal (1 subgoal):
 1. oid \<notin> set (interp_ins ops)
[PROOF STEP]
proof(induction ys arbitrary: ops rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ []; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
 2. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops ops
ops = xs @ [(oid, Some ref)] @ []
ref \<notin> set (interp_ins xs)

goal (2 subgoals):
 1. \<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ []; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
 2. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops ops
ops = xs @ [(oid, Some ref)] @ []
ref \<notin> set (interp_ins xs)
[PROOF STEP]
have "interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)"
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
ops = xs @ [(oid, Some ref)] @ []
ref \<notin> set (interp_ins xs)

goal (1 subgoal):
 1. interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)
[PROOF STEP]
by (simp add: interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)

goal (2 subgoals):
 1. \<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ []; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
 2. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)

goal (2 subgoals):
 1. \<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ []; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
 2. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
have "\<And>i. i \<in> set (map fst xs) \<Longrightarrow> i < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst xs) \<Longrightarrow> i < oid
[PROOF STEP]
using Nil.prems last_op_greatest
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
ops = xs @ [(oid, Some ref)] @ []
ref \<notin> set (interp_ins xs)
\<lbrakk>insert_ops (?op_list @ [(?oid, ?oper)]); ?x \<in> set (map fst ?op_list)\<rbrakk> \<Longrightarrow> ?x < ?oid

goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst xs) \<Longrightarrow> i < oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?i \<in> set (map fst xs) \<Longrightarrow> ?i < oid

goal (2 subgoals):
 1. \<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ []; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
 2. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
hence "\<And>i. i \<in> set (interp_ins xs) \<Longrightarrow> i < oid"
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst xs) \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. \<And>i. i \<in> set (interp_ins xs) \<Longrightarrow> i < oid
[PROOF STEP]
by (meson interp_ins_subset subsetCE)
[PROOF STATE]
proof (state)
this:
?i \<in> set (interp_ins xs) \<Longrightarrow> ?i < oid

goal (2 subgoals):
 1. \<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ []; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
 2. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)
?i \<in> set (interp_ins xs) \<Longrightarrow> ?i < oid
[PROOF STEP]
show "oid \<notin> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)
?i \<in> set (interp_ins xs) \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. oid \<notin> set (interp_ins ops)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = insert_spec (interp_ins xs) (oid, Some ref)
?i \<in> set (interp_ins xs) \<Longrightarrow> ?i < oid
ref \<notin> set (interp_ins xs)

goal (1 subgoal):
 1. oid \<notin> set (interp_ins ops)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
oid \<notin> set (interp_ins ops)

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
case (snoc x ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops ?ops; ?ops = xs @ [(oid, Some ref)] @ ys; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ?ops)
insert_ops ops
ops = xs @ [(oid, Some ref)] @ ys @ [x]
ref \<notin> set (interp_ins xs)

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>insert_ops ?ops; ?ops = xs @ [(oid, Some ref)] @ ys; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ?ops)
insert_ops ops
ops = xs @ [(oid, Some ref)] @ ys @ [x]
ref \<notin> set (interp_ins xs)
[PROOF STEP]
have "insert_ops (xs @ (oid, Some ref) # ys)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ?ops; ?ops = xs @ [(oid, Some ref)] @ ys; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ?ops)
insert_ops ops
ops = xs @ [(oid, Some ref)] @ ys @ [x]
ref \<notin> set (interp_ins xs)

goal (1 subgoal):
 1. insert_ops (xs @ (oid, Some ref) # ys)
[PROOF STEP]
by (metis append.assoc append.simps(1) append_Cons insert_ops_appendD)
[PROOF STATE]
proof (state)
this:
insert_ops (xs @ (oid, Some ref) # ys)

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
hence IH: "oid \<notin> set (interp_ins (xs @ (oid, Some ref) # ys))"
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ (oid, Some ref) # ys)

goal (1 subgoal):
 1. oid \<notin> set (interp_ins (xs @ (oid, Some ref) # ys))
[PROOF STEP]
by (simp add: snoc.IH snoc.prems(3))
[PROOF STATE]
proof (state)
this:
oid \<notin> set (interp_ins (xs @ (oid, Some ref) # ys))

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
oid \<notin> set (interp_ins (xs @ (oid, Some ref) # ys))

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
have "distinct (map fst (xs @ (oid, Some ref) # ys @ [x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (xs @ (oid, Some ref) # ys @ [x]))
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
ops = xs @ [(oid, Some ref)] @ ys @ [x]
ref \<notin> set (interp_ins xs)

goal (1 subgoal):
 1. distinct (map fst (xs @ (oid, Some ref) # ys @ [x]))
[PROOF STEP]
by (metis append_Cons append_self_conv2 insert_ops_def spec_ops_def)
[PROOF STATE]
proof (state)
this:
distinct (map fst (xs @ (oid, Some ref) # ys @ [x]))

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
hence "fst x \<noteq> oid"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (xs @ (oid, Some ref) # ys @ [x]))

goal (1 subgoal):
 1. fst x \<noteq> oid
[PROOF STEP]
using empty_iff
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (xs @ (oid, Some ref) # ys @ [x]))
(?c \<in> {}) = False

goal (1 subgoal):
 1. fst x \<noteq> oid
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x \<noteq> oid

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst x \<noteq> oid

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
have "insert_ops ((xs @ (oid, Some ref) # ys) @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops ((xs @ (oid, Some ref) # ys) @ [x])
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
ops = xs @ [(oid, Some ref)] @ ys @ [x]
ref \<notin> set (interp_ins xs)

goal (1 subgoal):
 1. insert_ops ((xs @ (oid, Some ref) # ys) @ [x])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_ops ((xs @ (oid, Some ref) # ys) @ [x])

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
hence "set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) =
         set (interp_ins (xs @ (oid, Some ref) # ys)) \<or>
         set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) =
         set (interp_ins (xs @ (oid, Some ref) # ys)) \<union> {fst x}"
[PROOF STATE]
proof (prove)
using this:
insert_ops ((xs @ (oid, Some ref) # ys) @ [x])

goal (1 subgoal):
 1. set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<or> set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<union> {fst x}
[PROOF STEP]
using interp_ins_maybe_grow2
[PROOF STATE]
proof (prove)
using this:
insert_ops ((xs @ (oid, Some ref) # ys) @ [x])
insert_ops (?xs @ [?x]) \<Longrightarrow> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<or> set (interp_ins (?xs @ [?x])) = set (interp_ins ?xs) \<union> {fst ?x}

goal (1 subgoal):
 1. set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<or> set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<union> {fst x}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<or> set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<union> {fst x}

goal (1 subgoal):
 1. \<And>x xsa ops. \<lbrakk>\<And>ops. \<lbrakk>insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops); insert_ops ops; ops = xs @ [(oid, Some ref)] @ xsa @ [x]; ref \<notin> set (interp_ins xs)\<rbrakk> \<Longrightarrow> oid \<notin> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
oid \<notin> set (interp_ins (xs @ (oid, Some ref) # ys))
fst x \<noteq> oid
set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<or> set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<union> {fst x}
[PROOF STEP]
show "oid \<notin> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
oid \<notin> set (interp_ins (xs @ (oid, Some ref) # ys))
fst x \<noteq> oid
set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<or> set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<union> {fst x}

goal (1 subgoal):
 1. oid \<notin> set (interp_ins ops)
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
oid \<notin> set (interp_ins (xs @ (oid, Some ref) # ys))
fst x \<noteq> oid
set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<or> set (interp_ins ((xs @ (oid, Some ref) # ys) @ [x])) = set (interp_ins (xs @ (oid, Some ref) # ys)) \<union> {fst x}
ops = xs @ [(oid, Some ref)] @ ys @ [x]

goal (1 subgoal):
 1. oid \<notin> set (interp_ins ops)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
oid \<notin> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_ins_last_None:
  shows "oid \<in> set (interp_ins (ops @ [(oid, None)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<in> set (interp_ins (ops @ [(oid, None)]))
[PROOF STEP]
by (simp add: interp_ins_tail_unfold)


[STATEMENT]
lemma interp_ins_monotonic:
  assumes "insert_ops (pre @ suf)"
    and "oid \<in> set (interp_ins pre)"
  shows "oid \<in> set (interp_ins (pre @ suf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<in> set (interp_ins (pre @ suf))
[PROOF STEP]
using assms interp_ins_maybe_grow3
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ suf)
oid \<in> set (interp_ins pre)
insert_ops (?xs @ ?ys) \<Longrightarrow> \<exists>A\<subseteq>set (map fst ?ys). set (interp_ins (?xs @ ?ys)) = set (interp_ins ?xs) \<union> A

goal (1 subgoal):
 1. oid \<in> set (interp_ins (pre @ suf))
[PROOF STEP]
by auto


[STATEMENT]
lemma interp_ins_append_non_memb:
  assumes "insert_ops (pre @ [(oid, Some ref)] @ suf)"
    and "ref \<notin> set (interp_ins pre)"
  shows "ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ suf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ suf))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ [(oid, Some ref)] @ suf)
ref \<notin> set (interp_ins pre)

goal (1 subgoal):
 1. ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ suf))
[PROOF STEP]
proof(induction suf rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ []); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ []))
 2. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops (pre @ [(oid, Some ref)] @ [])
ref \<notin> set (interp_ins pre)

goal (2 subgoals):
 1. \<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ []); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ []))
 2. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops (pre @ [(oid, Some ref)] @ [])
ref \<notin> set (interp_ins pre)
[PROOF STEP]
show "ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ []))"
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ [(oid, Some ref)] @ [])
ref \<notin> set (interp_ins pre)

goal (1 subgoal):
 1. ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ []))
[PROOF STEP]
by (metis append_Nil2 insert_spec_nonex interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ []))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))
insert_ops (pre @ [(oid, Some ref)] @ xs @ [x])
ref \<notin> set (interp_ins pre)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
hence IH: "ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))
insert_ops (pre @ [(oid, Some ref)] @ xs @ [x])
ref \<notin> set (interp_ins pre)

goal (1 subgoal):
 1. ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))
[PROOF STEP]
by (metis append_assoc insert_ops_rem_last)
[PROOF STATE]
proof (state)
this:
ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
have "ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
using insert_ops_ref_older snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
insert_ops (?pre @ [(?oid, Some ?ref)] @ ?suf) \<Longrightarrow> ?ref < ?oid
insert_ops (pre @ [(oid, Some ref)] @ xs @ [x])

goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ref < oid

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ref < oid

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
have "oid < fst x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid < fst x
[PROOF STEP]
using insert_ops_sorted_oids
[PROOF STATE]
proof (prove)
using this:
insert_ops (?xs @ [(?i1.0, ?r1.0)] @ ?ys @ [(?i2.0, ?r2.0)]) \<Longrightarrow> ?i1.0 < ?i2.0

goal (1 subgoal):
 1. oid < fst x
[PROOF STEP]
by (metis prod.collapse snoc.prems(1))
[PROOF STATE]
proof (state)
this:
oid < fst x

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
have "set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) =
        set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<or>
        set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) =
        set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<union> {fst x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<or> set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<union> {fst x}
[PROOF STEP]
by (metis (full_types) append.assoc interp_ins_maybe_grow2 snoc.prems(1))
[PROOF STATE]
proof (state)
this:
set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<or> set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<union> {fst x}

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops (pre @ [(oid, Some ref)] @ xs); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs)); insert_ops (pre @ [(oid, Some ref)] @ xs @ [x]); ref \<notin> set (interp_ins pre)\<rbrakk> \<Longrightarrow> ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))
ref < oid
set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<or> set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<union> {fst x}
[PROOF STEP]
show "ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))
ref < oid
set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<or> set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<union> {fst x}

goal (1 subgoal):
 1. ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
using \<open>oid < fst x\<close>
[PROOF STATE]
proof (prove)
using this:
ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs))
ref < oid
set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<or> set (interp_ins ((pre @ [(oid, Some ref)] @ xs) @ [x])) = set (interp_ins (pre @ [(oid, Some ref)] @ xs)) \<union> {fst x}
oid < fst x

goal (1 subgoal):
 1. ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ref \<notin> set (interp_ins (pre @ [(oid, Some ref)] @ xs @ [x]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_ins_append_memb:
  assumes "insert_ops (pre @ [(oid, Some ref)] @ suf)"
    and "ref \<in> set (interp_ins pre)"
  shows "oid \<in> set (interp_ins (pre @ [(oid, Some ref)] @ suf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<in> set (interp_ins (pre @ [(oid, Some ref)] @ suf))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ [(oid, Some ref)] @ suf)
ref \<in> set (interp_ins pre)

goal (1 subgoal):
 1. oid \<in> set (interp_ins (pre @ [(oid, Some ref)] @ suf))
[PROOF STEP]
by (metis UnCI append_assoc insert_spec_set interp_ins_monotonic
      interp_ins_tail_unfold singletonI)


[STATEMENT]
lemma interp_ins_append_forward:
  assumes "insert_ops (xs @ ys)"
    and "oid \<in> set (interp_ins (xs @ ys))"
    and "oid \<in> set (map fst xs)"
  shows "oid \<in> set (interp_ins xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<in> set (interp_ins xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ ys)
oid \<in> set (interp_ins (xs @ ys))
oid \<in> set (map fst xs)

goal (1 subgoal):
 1. oid \<in> set (interp_ins xs)
[PROOF STEP]
proof(induction ys rule: List.rev_induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>insert_ops (xs @ xsa); oid \<in> set (interp_ins (xs @ xsa)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs); insert_ops (xs @ xsa @ [x]); oid \<in> set (interp_ins (xs @ xsa @ [x])); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops (xs @ ys); oid \<in> set (interp_ins (xs @ ys)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
insert_ops (xs @ ys @ [y])
oid \<in> set (interp_ins (xs @ ys @ [y]))
oid \<in> set (map fst xs)

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>insert_ops (xs @ xsa); oid \<in> set (interp_ins (xs @ xsa)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs); insert_ops (xs @ xsa @ [x]); oid \<in> set (interp_ins (xs @ xsa @ [x])); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
[PROOF STEP]
obtain cs ds ref where "xs = cs @ (oid, ref) # ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs ref ds. xs = cs @ (oid, ref) # ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) imageE prod.collapse set_map snoc.prems(3) split_list_last)
[PROOF STATE]
proof (state)
this:
xs = cs @ (oid, ref) # ds

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>insert_ops (xs @ xsa); oid \<in> set (interp_ins (xs @ xsa)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs); insert_ops (xs @ xsa @ [x]); oid \<in> set (interp_ins (xs @ xsa @ [x])); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
[PROOF STEP]
hence "insert_ops (cs @ [(oid, ref)] @ (ds @ ys) @ [y])"
[PROOF STATE]
proof (prove)
using this:
xs = cs @ (oid, ref) # ds

goal (1 subgoal):
 1. insert_ops (cs @ [(oid, ref)] @ (ds @ ys) @ [y])
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
xs = cs @ (oid, ref) # ds
insert_ops (xs @ ys @ [y])

goal (1 subgoal):
 1. insert_ops (cs @ [(oid, ref)] @ (ds @ ys) @ [y])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_ops (cs @ [(oid, ref)] @ (ds @ ys) @ [y])

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>insert_ops (xs @ xsa); oid \<in> set (interp_ins (xs @ xsa)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs); insert_ops (xs @ xsa @ [x]); oid \<in> set (interp_ins (xs @ xsa @ [x])); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
[PROOF STEP]
hence "oid < fst y"
[PROOF STATE]
proof (prove)
using this:
insert_ops (cs @ [(oid, ref)] @ (ds @ ys) @ [y])

goal (1 subgoal):
 1. oid < fst y
[PROOF STEP]
using insert_ops_sorted_oids
[PROOF STATE]
proof (prove)
using this:
insert_ops (cs @ [(oid, ref)] @ (ds @ ys) @ [y])
insert_ops (?xs @ [(?i1.0, ?r1.0)] @ ?ys @ [(?i2.0, ?r2.0)]) \<Longrightarrow> ?i1.0 < ?i2.0

goal (1 subgoal):
 1. oid < fst y
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
oid < fst y

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>insert_ops (xs @ xsa); oid \<in> set (interp_ins (xs @ xsa)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs); insert_ops (xs @ xsa @ [x]); oid \<in> set (interp_ins (xs @ xsa @ [x])); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
[PROOF STEP]
hence "oid \<noteq> fst y"
[PROOF STATE]
proof (prove)
using this:
oid < fst y

goal (1 subgoal):
 1. oid \<noteq> fst y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
oid \<noteq> fst y

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>insert_ops (xs @ xsa); oid \<in> set (interp_ins (xs @ xsa)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs); insert_ops (xs @ xsa @ [x]); oid \<in> set (interp_ins (xs @ xsa @ [x])); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
oid \<noteq> fst y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
oid \<noteq> fst y

goal (1 subgoal):
 1. oid \<in> set (interp_ins xs)
[PROOF STEP]
using snoc.IH snoc.prems(1) snoc.prems(2) assms(3) inserted_item_ident
[PROOF STATE]
proof (prove)
using this:
oid \<noteq> fst y
\<lbrakk>insert_ops (xs @ ys); oid \<in> set (interp_ins (xs @ ys)); oid \<in> set (map fst xs)\<rbrakk> \<Longrightarrow> oid \<in> set (interp_ins xs)
insert_ops (xs @ ys @ [y])
oid \<in> set (interp_ins (xs @ ys @ [y]))
oid \<in> set (map fst xs)
\<lbrakk>?a \<in> set (insert_spec ?xs (?e, ?i)); ?a \<notin> set ?xs\<rbrakk> \<Longrightarrow> ?a = ?e

goal (1 subgoal):
 1. oid \<in> set (interp_ins xs)
[PROOF STEP]
by (metis append_assoc insert_ops_appendD interp_ins_tail_unfold prod.collapse)
[PROOF STATE]
proof (state)
this:
oid \<in> set (interp_ins xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_ins_find_ref:
  assumes "insert_ops (xs @ [(oid, Some ref)] @ ys)"
    and "ref \<in> set (interp_ins (xs @ [(oid, Some ref)] @ ys))"
  shows "\<exists>r. (ref, r) \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
have "ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
using assms(1) insert_ops_ref_older
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [(oid, Some ref)] @ ys)
insert_ops (?pre @ [(?oid, Some ?ref)] @ ?suf) \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ref < oid

goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
have "ref \<in> set (map fst (xs @ [(oid, Some ref)] @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref \<in> set (map fst (xs @ [(oid, Some ref)] @ ys))
[PROOF STEP]
by (meson assms(2) interp_ins_subset subsetCE)
[PROOF STATE]
proof (state)
this:
ref \<in> set (map fst (xs @ [(oid, Some ref)] @ ys))

goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ref \<in> set (map fst (xs @ [(oid, Some ref)] @ ys))
[PROOF STEP]
obtain x where x_prop: "x \<in> set (xs @ [(oid, Some ref)] @ ys) \<and> fst x = ref"
[PROOF STATE]
proof (prove)
using this:
ref \<in> set (map fst (xs @ [(oid, Some ref)] @ ys))

goal (1 subgoal):
 1. (\<And>x. x \<in> set (xs @ [(oid, Some ref)] @ ys) \<and> fst x = ref \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> set (xs @ [(oid, Some ref)] @ ys) \<and> fst x = ref

goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
obtain xr where x_pair: "x = (ref, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xr. x = (ref, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust_sel x_prop
[PROOF STATE]
proof (prove)
using this:
(?prod = (fst ?prod, snd ?prod) \<Longrightarrow> ?P) \<Longrightarrow> ?P
x \<in> set (xs @ [(oid, Some ref)] @ ys) \<and> fst x = ref

goal (1 subgoal):
 1. (\<And>xr. x = (ref, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = (ref, xr)

goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
show "\<exists>r. (ref, r) \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
proof(cases "x \<in> set xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
 2. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> set xs

goal (2 subgoals):
 1. x \<in> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
 2. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set xs
[PROOF STEP]
show "\<exists>r. (ref, r) \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs

goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
by (metis x_prop prod.collapse)
[PROOF STATE]
proof (state)
this:
\<exists>r. (ref, r) \<in> set xs

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> set xs

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
hence "(ref, xr) \<in> set ([(oid, Some ref)] @ ys)"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set xs

goal (1 subgoal):
 1. (ref, xr) \<in> set ([(oid, Some ref)] @ ys)
[PROOF STEP]
using x_prop x_pair
[PROOF STATE]
proof (prove)
using this:
x \<notin> set xs
x \<in> set (xs @ [(oid, Some ref)] @ ys) \<and> fst x = ref
x = (ref, xr)

goal (1 subgoal):
 1. (ref, xr) \<in> set ([(oid, Some ref)] @ ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(ref, xr) \<in> set ([(oid, Some ref)] @ ys)

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
hence "(ref, xr) \<in> set ys"
[PROOF STATE]
proof (prove)
using this:
(ref, xr) \<in> set ([(oid, Some ref)] @ ys)

goal (1 subgoal):
 1. (ref, xr) \<in> set ys
[PROOF STEP]
using \<open>ref < oid\<close> x_prop
[PROOF STATE]
proof (prove)
using this:
(ref, xr) \<in> set ([(oid, Some ref)] @ ys)
ref < oid
x \<in> set (xs @ [(oid, Some ref)] @ ys) \<and> fst x = ref

goal (1 subgoal):
 1. (ref, xr) \<in> set ys
[PROOF STEP]
by (metis append_Cons append_self_conv2 fst_conv min.strict_order_iff set_ConsD)
[PROOF STATE]
proof (state)
this:
(ref, xr) \<in> set ys

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(ref, xr) \<in> set ys
[PROOF STEP]
obtain as bs where "ys = as @ (ref, xr) # bs"
[PROOF STATE]
proof (prove)
using this:
(ref, xr) \<in> set ys

goal (1 subgoal):
 1. (\<And>as bs. ys = as @ (ref, xr) # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson split_list)
[PROOF STATE]
proof (state)
this:
ys = as @ (ref, xr) # bs

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
hence "insert_ops ((xs @ [(oid, Some ref)] @ as @ [(ref, xr)]) @ bs)"
[PROOF STATE]
proof (prove)
using this:
ys = as @ (ref, xr) # bs

goal (1 subgoal):
 1. insert_ops ((xs @ [(oid, Some ref)] @ as @ [(ref, xr)]) @ bs)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
ys = as @ (ref, xr) # bs
insert_ops (xs @ [(oid, Some ref)] @ ys)

goal (1 subgoal):
 1. insert_ops ((xs @ [(oid, Some ref)] @ as @ [(ref, xr)]) @ bs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_ops ((xs @ [(oid, Some ref)] @ as @ [(ref, xr)]) @ bs)

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
hence "insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])"
[PROOF STATE]
proof (prove)
using this:
insert_ops ((xs @ [(oid, Some ref)] @ as @ [(ref, xr)]) @ bs)

goal (1 subgoal):
 1. insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])
[PROOF STEP]
using insert_ops_appendD
[PROOF STATE]
proof (prove)
using this:
insert_ops ((xs @ [(oid, Some ref)] @ as @ [(ref, xr)]) @ bs)
insert_ops (?xs @ ?ys) \<Longrightarrow> insert_ops ?xs

goal (1 subgoal):
 1. insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
hence "oid < ref"
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])

goal (1 subgoal):
 1. oid < ref
[PROOF STEP]
(* contradiction *)
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])

goal (1 subgoal):
 1. oid < ref
[PROOF STEP]
using insert_ops_sorted_oids
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [(oid, Some ref)] @ as @ [(ref, xr)])
insert_ops (?xs @ [(?i1.0, ?r1.0)] @ ?ys @ [(?i2.0, ?r2.0)]) \<Longrightarrow> ?i1.0 < ?i2.0

goal (1 subgoal):
 1. oid < ref
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
oid < ref

goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
oid < ref
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
oid < ref

goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
using \<open>ref < oid\<close>
[PROOF STATE]
proof (prove)
using this:
oid < ref
ref < oid

goal (1 subgoal):
 1. \<exists>r. (ref, r) \<in> set xs
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>r. (ref, r) \<in> set xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>r. (ref, r) \<in> set xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_order_append:
  assumes "insert_ops (pre @ suf)"
    and "list_order pre x y"
  shows "list_order (pre @ suf) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order (pre @ suf) x y
[PROOF STEP]
by (metis Un_iff assms list_order_monotonic insert_ops_appendD set_append subset_code(1))


[STATEMENT]
lemma list_order_insert_ref:
  assumes "insert_ops (ops @ [(oid, Some ref)])"
    and "ref \<in> set (interp_ins ops)"
  shows "list_order (ops @ [(oid, Some ref)]) ref oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
have "interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
[PROOF STEP]
by (simp add: interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
obtain xs ys where "interp_ins ops = xs @ [ref] @ ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs ys. interp_ins ops = xs @ [ref] @ ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2) split_list_first
[PROOF STATE]
proof (prove)
using this:
ref \<in> set (interp_ins ops)
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>xs ys. interp_ins ops = xs @ [ref] @ ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
interp_ins ops = xs @ [ref] @ ys

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
hence "insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys"
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = xs @ [ref] @ ys

goal (1 subgoal):
 1. insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys
[PROOF STEP]
using assms(1) insert_after_ref interp_ins_distinct
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = xs @ [ref] @ ys
insert_ops (ops @ [(oid, Some ref)])
distinct (?xs @ ?ref # ?ys) \<Longrightarrow> insert_spec (?xs @ ?ref # ?ys) (?oid, Some ?ref) = ?xs @ ?ref # ?oid # ?ys
insert_ops ?op_list \<Longrightarrow> distinct (interp_ins ?op_list)

goal (1 subgoal):
 1. insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys
[PROOF STEP]
show "list_order (ops @ [(oid, Some ref)]) ref oid"
[PROOF STATE]
proof (prove)
using this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
using assms(1) list_orderI
[PROOF STATE]
proof (prove)
using this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
insert_spec (interp_ins ops) (oid, Some ref) = xs @ [ref] @ [] @ [oid] @ ys
insert_ops (ops @ [(oid, Some ref)])
interp_ins ?ops = ?xs @ [?x] @ ?ys @ [?y] @ ?zs \<Longrightarrow> list_order ?ops ?x ?y

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) ref oid
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
list_order (ops @ [(oid, Some ref)]) ref oid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_order_insert_none:
  assumes "insert_ops (ops @ [(oid, None)])"
    and "x \<in> set (interp_ins ops)"
  shows "list_order (ops @ [(oid, None)]) oid x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
have "interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)
[PROOF STEP]
by (simp add: interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)

goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)

goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
obtain xs ys where "interp_ins ops = xs @ [x] @ ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs ys. interp_ins ops = xs @ [x] @ ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2) split_list_first
[PROOF STATE]
proof (prove)
using this:
x \<in> set (interp_ins ops)
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>xs ys. interp_ins ops = xs @ [x] @ ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
interp_ins ops = xs @ [x] @ ys

goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
hence "insert_spec (interp_ins ops) (oid, None) = [] @ [oid] @ xs @ [x] @ ys"
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = xs @ [x] @ ys

goal (1 subgoal):
 1. insert_spec (interp_ins ops) (oid, None) = [] @ [oid] @ xs @ [x] @ ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_spec (interp_ins ops) (oid, None) = [] @ [oid] @ xs @ [x] @ ys

goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)
insert_spec (interp_ins ops) (oid, None) = [] @ [oid] @ xs @ [x] @ ys
[PROOF STEP]
show "list_order (ops @ [(oid, None)]) oid x"
[PROOF STATE]
proof (prove)
using this:
interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)
insert_spec (interp_ins ops) (oid, None) = [] @ [oid] @ xs @ [x] @ ys

goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
using assms(1) list_orderI
[PROOF STATE]
proof (prove)
using this:
interp_ins (ops @ [(oid, None)]) = insert_spec (interp_ins ops) (oid, None)
insert_spec (interp_ins ops) (oid, None) = [] @ [oid] @ xs @ [x] @ ys
insert_ops (ops @ [(oid, None)])
interp_ins ?ops = ?xs @ [?x] @ ?ys @ [?y] @ ?zs \<Longrightarrow> list_order ?ops ?x ?y

goal (1 subgoal):
 1. list_order (ops @ [(oid, None)]) oid x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
list_order (ops @ [(oid, None)]) oid x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_order_insert_between:
  assumes "insert_ops (ops @ [(oid, Some ref)])"
    and "list_order ops ref x"
  shows "list_order (ops @ [(oid, Some ref)]) oid x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
have "interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
[PROOF STEP]
by (simp add: interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
obtain xs ys zs where "interp_ins ops = xs @ [ref] @ ys @ [x] @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs ys zs. interp_ins ops = xs @ [ref] @ ys @ [x] @ zs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms list_orderE
[PROOF STATE]
proof (prove)
using this:
insert_ops (ops @ [(oid, Some ref)])
list_order ops ref x
list_order ?ops ?x ?y \<Longrightarrow> \<exists>xs ys zs. interp_ins ?ops = xs @ [?x] @ ys @ [?y] @ zs

goal (1 subgoal):
 1. (\<And>xs ys zs. interp_ins ops = xs @ [ref] @ ys @ [x] @ zs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
interp_ins ops = xs @ [ref] @ ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins ops = xs @ [ref] @ ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
have "... = xs @ ref # (ys @ [x] @ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
have "distinct (xs @ ref # (ys @ [x] @ zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (xs @ ref # ys @ [x] @ zs)
[PROOF STEP]
using assms(1) calculation
[PROOF STATE]
proof (prove)
using this:
insert_ops (ops @ [(oid, Some ref)])
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
interp_ins ops = xs @ [ref] @ ys @ [x] @ zs
xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs

goal (1 subgoal):
 1. distinct (xs @ ref # ys @ [x] @ zs)
[PROOF STEP]
by (metis interp_ins_distinct insert_ops_rem_last)
[PROOF STATE]
proof (state)
this:
distinct (xs @ ref # ys @ [x] @ zs)

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
hence "insert_spec (xs @ ref # (ys @ [x] @ zs)) (oid, Some ref) = xs @ ref # oid # (ys @ [x] @ zs)"
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ ref # ys @ [x] @ zs)

goal (1 subgoal):
 1. insert_spec (xs @ ref # ys @ [x] @ zs) (oid, Some ref) = xs @ ref # oid # ys @ [x] @ zs
[PROOF STEP]
using assms(1) calculation
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ ref # ys @ [x] @ zs)
insert_ops (ops @ [(oid, Some ref)])
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
interp_ins ops = xs @ [ref] @ ys @ [x] @ zs
xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs

goal (1 subgoal):
 1. insert_spec (xs @ ref # ys @ [x] @ zs) (oid, Some ref) = xs @ ref # oid # ys @ [x] @ zs
[PROOF STEP]
by (simp add: insert_after_ref)
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ref # ys @ [x] @ zs) (oid, Some ref) = xs @ ref # oid # ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ref # ys @ [x] @ zs) (oid, Some ref) = xs @ ref # oid # ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
have "... = (xs @ [ref]) @ [oid] @ ys @ [x] @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @ ref # oid # ys @ [x] @ zs = (xs @ [ref]) @ [oid] @ ys @ [x] @ zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs @ ref # oid # ys @ [x] @ zs = (xs @ [ref]) @ [oid] @ ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
interp_ins ops = xs @ [ref] @ ys @ [x] @ zs
xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs
insert_spec (xs @ ref # ys @ [x] @ zs) (oid, Some ref) = xs @ ref # oid # ys @ [x] @ zs
xs @ ref # oid # ys @ [x] @ zs = (xs @ [ref]) @ [oid] @ ys @ [x] @ zs
[PROOF STEP]
show "list_order (ops @ [(oid, Some ref)]) oid x"
[PROOF STATE]
proof (prove)
using this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
interp_ins ops = xs @ [ref] @ ys @ [x] @ zs
xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs
insert_spec (xs @ ref # ys @ [x] @ zs) (oid, Some ref) = xs @ ref # oid # ys @ [x] @ zs
xs @ ref # oid # ys @ [x] @ zs = (xs @ [ref]) @ [oid] @ ys @ [x] @ zs

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
using assms(1) list_orderI
[PROOF STATE]
proof (prove)
using this:
interp_ins (ops @ [(oid, Some ref)]) = insert_spec (interp_ins ops) (oid, Some ref)
interp_ins ops = xs @ [ref] @ ys @ [x] @ zs
xs @ [ref] @ ys @ [x] @ zs = xs @ ref # ys @ [x] @ zs
insert_spec (xs @ ref # ys @ [x] @ zs) (oid, Some ref) = xs @ ref # oid # ys @ [x] @ zs
xs @ ref # oid # ys @ [x] @ zs = (xs @ [ref]) @ [oid] @ ys @ [x] @ zs
insert_ops (ops @ [(oid, Some ref)])
interp_ins ?ops = ?xs @ [?x] @ ?ys @ [?y] @ ?zs \<Longrightarrow> list_order ?ops ?x ?y

goal (1 subgoal):
 1. list_order (ops @ [(oid, Some ref)]) oid x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
list_order (ops @ [(oid, Some ref)]) oid x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_seq_nonempty:
  assumes "insert_seq start xs"
  shows "xs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_seq start xs

goal (1 subgoal):
 1. xs \<noteq> []
[PROOF STEP]
by (induction rule: insert_seq.induct, auto)


[STATEMENT]
lemma insert_seq_hd:
  assumes "insert_seq start xs"
  shows "\<exists>oid. hd xs = (oid, start)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>oid. hd xs = (oid, start)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_seq start xs

goal (1 subgoal):
 1. \<exists>oid. hd xs = (oid, start)
[PROOF STEP]
by (induction rule: insert_seq.induct, simp,
      metis append_self_conv2 hd_append2 list.sel(1))


[STATEMENT]
lemma insert_seq_rem_last:
  assumes "insert_seq start (xs @ [x])"
    and "xs \<noteq> []"
  shows "insert_seq start xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_seq start xs
[PROOF STEP]
using assms insert_seq.cases
[PROOF STATE]
proof (prove)
using this:
insert_seq start (xs @ [x])
xs \<noteq> []
\<lbrakk>insert_seq ?a1.0 ?a2.0; \<And>start oid. \<lbrakk>?a1.0 = start; ?a2.0 = [(oid, start)]\<rbrakk> \<Longrightarrow> ?P; \<And>start list prev ref oid. \<lbrakk>?a1.0 = start; ?a2.0 = list @ [(prev, ref), (oid, Some prev)]; insert_seq start (list @ [(prev, ref)])\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. insert_seq start xs
[PROOF STEP]
by fastforce


[STATEMENT]
lemma insert_seq_butlast:
  assumes "insert_seq start xs"
    and "xs \<noteq> []" and "xs \<noteq> [last xs]"
  shows "insert_seq start (butlast xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
have "length xs > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length xs
[PROOF STEP]
by (metis One_nat_def Suc_lessI add_0_left append_butlast_last_id append_eq_append_conv
        append_self_conv2 assms(2) assms(3) length_greater_0_conv list.size(3) list.size(4))
[PROOF STATE]
proof (state)
this:
1 < length xs

goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
hence "butlast xs \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
1 < length xs

goal (1 subgoal):
 1. butlast xs \<noteq> []
[PROOF STEP]
by (metis length_butlast less_numeral_extra(3) list.size(3) zero_less_diff)
[PROOF STATE]
proof (state)
this:
butlast xs \<noteq> []

goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
butlast xs \<noteq> []
[PROOF STEP]
show "insert_seq start (butlast xs)"
[PROOF STATE]
proof (prove)
using this:
butlast xs \<noteq> []

goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
butlast xs \<noteq> []
insert_seq start xs
xs \<noteq> []
xs \<noteq> [last xs]

goal (1 subgoal):
 1. insert_seq start (butlast xs)
[PROOF STEP]
by (metis append_butlast_last_id insert_seq_rem_last)
[PROOF STATE]
proof (state)
this:
insert_seq start (butlast xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_seq_last_ref:
  assumes "insert_seq start (xs @ [(xi, xr), (yi, yr)])"
  shows "yr = Some xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yr = Some xi
[PROOF STEP]
using assms insert_seq.cases
[PROOF STATE]
proof (prove)
using this:
insert_seq start (xs @ [(xi, xr), (yi, yr)])
\<lbrakk>insert_seq ?a1.0 ?a2.0; \<And>start oid. \<lbrakk>?a1.0 = start; ?a2.0 = [(oid, start)]\<rbrakk> \<Longrightarrow> ?P; \<And>start list prev ref oid. \<lbrakk>?a1.0 = start; ?a2.0 = list @ [(prev, ref), (oid, Some prev)]; insert_seq start (list @ [(prev, ref)])\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. yr = Some xi
[PROOF STEP]
by fastforce


[STATEMENT]
lemma insert_seq_start_none:
  assumes "insert_ops ops"
    and "insert_seq None xs" and "insert_ops xs"
    and "set xs \<subseteq> set ops"
  shows "\<forall>i \<in> set (map fst xs). i \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
insert_seq None xs
insert_ops xs
set xs \<subseteq> set ops

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
[PROOF STEP]
proof(induction xs rule: List.rev_induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq None xs; insert_ops xs; set xs \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); insert_ops ops; insert_seq None (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops ops; insert_seq None xs; insert_ops xs; set xs \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
insert_ops ops
insert_seq None (xs @ [x])
insert_ops (xs @ [x])
set (xs @ [x]) \<subseteq> set ops

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq None xs; insert_ops xs; set xs \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); insert_ops ops; insert_seq None (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>insert_ops ops; insert_seq None xs; insert_ops xs; set xs \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
insert_ops ops
insert_seq None (xs @ [x])
insert_ops (xs @ [x])
set (xs @ [x]) \<subseteq> set ops
[PROOF STEP]
have IH: "\<forall>i \<in> set (map fst xs). i \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ops; insert_seq None xs; insert_ops xs; set xs \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
insert_ops ops
insert_seq None (xs @ [x])
insert_ops (xs @ [x])
set (xs @ [x]) \<subseteq> set ops

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
[PROOF STEP]
by (metis Nil_is_map_conv append_is_Nil_conv insert_ops_appendD insert_seq_rem_last
        le_supE list.simps(3) set_append split_list)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq None xs; insert_ops xs; set xs \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); insert_ops ops; insert_seq None (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
[PROOF STEP]
show "\<forall>i \<in> set (map fst (xs @ [x])). i \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
proof(cases "xs = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = []
[PROOF STEP]
obtain oid where "xs @ [x] = [(oid, None)]"
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. (\<And>oid. xs @ [x] = [(oid, None)] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert_seq_hd snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
xs = []
insert_seq ?start ?xs \<Longrightarrow> \<exists>oid. hd ?xs = (oid, ?start)
insert_seq None (xs @ [x])

goal (1 subgoal):
 1. (\<And>oid. xs @ [x] = [(oid, None)] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs @ [x] = [(oid, None)]

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
hence "(oid, None) \<in> set ops"
[PROOF STATE]
proof (prove)
using this:
xs @ [x] = [(oid, None)]

goal (1 subgoal):
 1. (oid, None) \<in> set ops
[PROOF STEP]
using snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
xs @ [x] = [(oid, None)]
set (xs @ [x]) \<subseteq> set ops

goal (1 subgoal):
 1. (oid, None) \<in> set ops
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(oid, None) \<in> set ops

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(oid, None) \<in> set ops
[PROOF STEP]
obtain as bs where "ops = as @ (oid, None) # bs"
[PROOF STATE]
proof (prove)
using this:
(oid, None) \<in> set ops

goal (1 subgoal):
 1. (\<And>as bs. ops = as @ (oid, None) # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson split_list)
[PROOF STATE]
proof (state)
this:
ops = as @ (oid, None) # bs

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
hence "ops = (as @ [(oid, None)]) @ bs"
[PROOF STATE]
proof (prove)
using this:
ops = as @ (oid, None) # bs

goal (1 subgoal):
 1. ops = (as @ [(oid, None)]) @ bs
[PROOF STEP]
by (simp add: \<open>ops = as @ (oid, None) # bs\<close>)
[PROOF STATE]
proof (state)
this:
ops = (as @ [(oid, None)]) @ bs

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ops = (as @ [(oid, None)]) @ bs

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
have "oid \<in> set (interp_ins (as @ [(oid, None)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<in> set (interp_ins (as @ [(oid, None)]))
[PROOF STEP]
by (simp add: interp_ins_last_None)
[PROOF STATE]
proof (state)
this:
oid \<in> set (interp_ins (as @ [(oid, None)]))

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ops = (as @ [(oid, None)]) @ bs
oid \<in> set (interp_ins (as @ [(oid, None)]))
[PROOF STEP]
have "oid \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
ops = (as @ [(oid, None)]) @ bs
oid \<in> set (interp_ins (as @ [(oid, None)]))

goal (1 subgoal):
 1. oid \<in> set (interp_ins ops)
[PROOF STEP]
using interp_ins_monotonic snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
ops = (as @ [(oid, None)]) @ bs
oid \<in> set (interp_ins (as @ [(oid, None)]))
\<lbrakk>insert_ops (?pre @ ?suf); ?oid \<in> set (interp_ins ?pre)\<rbrakk> \<Longrightarrow> ?oid \<in> set (interp_ins (?pre @ ?suf))
insert_ops ops

goal (1 subgoal):
 1. oid \<in> set (interp_ins ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
oid \<in> set (interp_ins ops)

goal (2 subgoals):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs = []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
 2. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
oid \<in> set (interp_ins ops)
[PROOF STEP]
show "\<forall>i \<in> set (map fst (xs @ [x])). i \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
oid \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
using \<open>xs @ [x] = [(oid, None)]\<close>
[PROOF STATE]
proof (prove)
using this:
oid \<in> set (interp_ins ops)
xs @ [x] = [(oid, None)]

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
[PROOF STEP]
obtain rest y where snoc_y: "xs = rest @ [y]"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. (\<And>rest y. xs = rest @ [y] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using append_butlast_last_id
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
?xs \<noteq> [] \<Longrightarrow> butlast ?xs @ [last ?xs] = ?xs

goal (1 subgoal):
 1. (\<And>rest y. xs = rest @ [y] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
xs = rest @ [y]

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
obtain yi yr xi xr where yx_pairs: "y = (yi, yr) \<and> x = (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>yi yr xi xr. y = (yi, yr) \<and> x = (xi, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y = (yi, yr) \<and> x = (xi, xr)

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = (yi, yr) \<and> x = (xi, xr)
[PROOF STEP]
have "xr = Some yi"
[PROOF STATE]
proof (prove)
using this:
y = (yi, yr) \<and> x = (xi, xr)

goal (1 subgoal):
 1. xr = Some yi
[PROOF STEP]
using insert_seq_last_ref snoc.prems(2) snoc_y
[PROOF STATE]
proof (prove)
using this:
y = (yi, yr) \<and> x = (xi, xr)
insert_seq ?start (?xs @ [(?xi, ?xr), (?yi, ?yr)]) \<Longrightarrow> ?yr = Some ?xi
insert_seq None (xs @ [x])
xs = rest @ [y]

goal (1 subgoal):
 1. xr = Some yi
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xr = Some yi

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
have "yi < xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yi < xi
[PROOF STEP]
using insert_ops_sorted_oids snoc_y yx_pairs snoc.prems(3)
[PROOF STATE]
proof (prove)
using this:
insert_ops (?xs @ [(?i1.0, ?r1.0)] @ ?ys @ [(?i2.0, ?r2.0)]) \<Longrightarrow> ?i1.0 < ?i2.0
xs = rest @ [y]
y = (yi, yr) \<and> x = (xi, xr)
insert_ops (xs @ [x])

goal (1 subgoal):
 1. yi < xi
[PROOF STEP]
by (metis (no_types, lifting) append_eq_append_conv2)
[PROOF STATE]
proof (state)
this:
yi < xi

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
have "(yi, yr) \<in> set ops" and "(xi, Some yi) \<in> set ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (yi, yr) \<in> set ops &&& (xi, Some yi) \<in> set ops
[PROOF STEP]
using snoc.prems(4) snoc_y yx_pairs \<open>xr = Some yi\<close>
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) \<subseteq> set ops
xs = rest @ [y]
y = (yi, yr) \<and> x = (xi, xr)
xr = Some yi

goal (1 subgoal):
 1. (yi, yr) \<in> set ops &&& (xi, Some yi) \<in> set ops
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(yi, yr) \<in> set ops
(xi, Some yi) \<in> set ops

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(yi, yr) \<in> set ops
(xi, Some yi) \<in> set ops
[PROOF STEP]
obtain as bs cs where ops_split: "ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs"
[PROOF STATE]
proof (prove)
using this:
(yi, yr) \<in> set ops
(xi, Some yi) \<in> set ops

goal (1 subgoal):
 1. (\<And>as bs cs. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert_ops_split_2 \<open>yi < xi\<close> snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
(yi, yr) \<in> set ops
(xi, Some yi) \<in> set ops
\<lbrakk>insert_ops ?ops; (?xid, ?xr) \<in> set ?ops; (?yid, ?yr) \<in> set ?ops; ?xid < ?yid\<rbrakk> \<Longrightarrow> \<exists>as bs cs. ?ops = as @ [(?xid, ?xr)] @ bs @ [(?yid, ?yr)] @ cs \<and> (\<forall>i\<in>set (map fst as). i < ?xid) \<and> (\<forall>i\<in>set (map fst bs). ?xid < i \<and> i < ?yid) \<and> (\<forall>i\<in>set (map fst cs). ?yid < i)
yi < xi
insert_ops ops

goal (1 subgoal):
 1. (\<And>as bs cs. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
hence "yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))"
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs

goal (1 subgoal):
 1. yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
have "yi \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yi \<in> set (interp_ins ops)
[PROOF STEP]
by (simp add: IH snoc_y yx_pairs)
[PROOF STATE]
proof (state)
this:
yi \<in> set (interp_ins ops)

goal (1 subgoal):
 1. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yi \<in> set (interp_ins ops)

goal (1 subgoal):
 1. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
have "ops = (as @ [(yi, yr)] @ bs) @ ([(xi, Some yi)] @ cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ops = (as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs
[PROOF STEP]
using ops_split
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs

goal (1 subgoal):
 1. ops = (as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ops = (as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs

goal (1 subgoal):
 1. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ops = (as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs

goal (1 subgoal):
 1. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
have "yi \<in> set (map fst (as @ [(yi, yr)] @ bs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yi \<in> set (map fst (as @ [(yi, yr)] @ bs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
yi \<in> set (map fst (as @ [(yi, yr)] @ bs))

goal (1 subgoal):
 1. ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs \<Longrightarrow> yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
yi \<in> set (interp_ins ops)
ops = (as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs
yi \<in> set (map fst (as @ [(yi, yr)] @ bs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
yi \<in> set (interp_ins ops)
ops = (as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs
yi \<in> set (map fst (as @ [(yi, yr)] @ bs))

goal (1 subgoal):
 1. yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
using snoc.prems(1) interp_ins_append_forward
[PROOF STATE]
proof (prove)
using this:
yi \<in> set (interp_ins ops)
ops = (as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs
yi \<in> set (map fst (as @ [(yi, yr)] @ bs))
insert_ops ops
\<lbrakk>insert_ops (?xs @ ?ys); ?oid \<in> set (interp_ins (?xs @ ?ys)); ?oid \<in> set (map fst ?xs)\<rbrakk> \<Longrightarrow> ?oid \<in> set (interp_ins ?xs)

goal (1 subgoal):
 1. yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
hence "xi \<in> set (interp_ins ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs))"
[PROOF STATE]
proof (prove)
using this:
yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))

goal (1 subgoal):
 1. xi \<in> set (interp_ins ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs))
[PROOF STEP]
using snoc.prems(1) interp_ins_append_memb ops_split
[PROOF STATE]
proof (prove)
using this:
yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
insert_ops ops
\<lbrakk>insert_ops (?pre @ [(?oid, Some ?ref)] @ ?suf); ?ref \<in> set (interp_ins ?pre)\<rbrakk> \<Longrightarrow> ?oid \<in> set (interp_ins (?pre @ [(?oid, Some ?ref)] @ ?suf))
ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs

goal (1 subgoal):
 1. xi \<in> set (interp_ins ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
xi \<in> set (interp_ins ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs))

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
hence "xi \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
xi \<in> set (interp_ins ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)] @ cs))

goal (1 subgoal):
 1. xi \<in> set (interp_ins ops)
[PROOF STEP]
by (simp add: ops_split)
[PROOF STATE]
proof (state)
this:
xi \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<lbrakk>\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops); xs \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xi \<in> set (interp_ins ops)
[PROOF STEP]
show "\<forall>i \<in> set (map fst (xs @ [x])). i \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
xi \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
using IH yx_pairs
[PROOF STATE]
proof (prove)
using this:
xi \<in> set (interp_ins ops)
\<forall>i\<in>set (map fst xs). i \<in> set (interp_ins ops)
y = (yi, yr) \<and> x = (xi, xr)

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst (xs @ [x])). i \<in> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed