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

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). list_order ops ref i
[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 (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst xs)) (list_order ops ref); insert_ops ops; insert_seq (Some ref) (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst (xs @ [x]))) (list_order ops ref)
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (map fst xs). list_order ops ref a
insert_ops ops
insert_seq (Some ref) (xs @ [x])
insert_ops (xs @ [x])
set (xs @ [x]) \<subseteq> set ops
ref \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst xs)) (list_order ops ref); insert_ops ops; insert_seq (Some ref) (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst (xs @ [x]))) (list_order ops ref)
[PROOF STEP]
have IH: "\<forall>i \<in> set (map fst xs). list_order ops ref i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). list_order ops ref i
[PROOF STEP]
using snoc.IH snoc.prems insert_seq_rem_last insert_ops_appendD
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (map fst xs). list_order ops ref a
insert_ops ops
insert_seq (Some ref) (xs @ [x])
insert_ops (xs @ [x])
set (xs @ [x]) \<subseteq> set ops
ref \<in> set (interp_ins ops)
\<lbrakk>insert_seq ?start (?xs @ [?x]); ?xs \<noteq> []\<rbrakk> \<Longrightarrow> insert_seq ?start ?xs
insert_ops (?xs @ ?ys) \<Longrightarrow> insert_ops ?xs

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). list_order ops ref i
[PROOF STEP]
by (metis Nil_is_map_conv Un_subset_iff empty_set equals0D set_append)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst xs). list_order ops ref i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst xs)) (list_order ops ref); insert_ops ops; insert_seq (Some ref) (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst (xs @ [x]))) (list_order ops ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst xs). list_order ops ref i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst xs)) (list_order ops ref); insert_ops ops; insert_seq (Some ref) (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops; ref \<in> set (interp_ins ops)\<rbrakk> \<Longrightarrow> Ball (set (map fst (xs @ [x]))) (list_order ops ref)
[PROOF STEP]
have "list_order ops ref (fst x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order ops ref (fst x)
[PROOF STEP]
proof(cases "xs = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
hence "snd x = Some ref"
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. snd x = Some ref
[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 (Some ref) (xs @ [x])

goal (1 subgoal):
 1. snd x = Some ref
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
snd x = Some ref

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
snd x = Some ref

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
have "x \<in> set ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set ops
[PROOF STEP]
using snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) \<subseteq> set ops

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

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set ops
[PROOF STEP]
obtain cs ds where x_split: "ops = cs @ x # ds"
[PROOF STATE]
proof (prove)
using this:
x \<in> set ops

goal (1 subgoal):
 1. (\<And>cs ds. ops = cs @ x # ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson split_list)
[PROOF STATE]
proof (state)
this:
ops = cs @ x # ds

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
have "list_order (cs @ [(fst x, Some ref)]) ref (fst x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
have "insert_ops (cs @ [(fst x, Some ref)] @ ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops (cs @ [(fst x, Some ref)] @ ds)
[PROOF STEP]
using x_split \<open>snd x = Some ref\<close>
[PROOF STATE]
proof (prove)
using this:
ops = cs @ x # ds
snd x = Some ref

goal (1 subgoal):
 1. insert_ops (cs @ [(fst x, Some ref)] @ ds)
[PROOF STEP]
by (metis append_Cons append_self_conv2 prod.collapse snoc.prems(1))
[PROOF STATE]
proof (state)
this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)

goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)

goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)
[PROOF STEP]
obtain rr where "(ref, rr) \<in> set cs"
[PROOF STATE]
proof (prove)
using this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)

goal (1 subgoal):
 1. (\<And>rr. (ref, rr) \<in> set cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using interp_ins_find_ref x_split \<open>snd x = Some ref\<close> assms(5)
[PROOF STATE]
proof (prove)
using this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)
\<lbrakk>insert_ops (?xs @ [(?oid, Some ?ref)] @ ?ys); ?ref \<in> set (interp_ins (?xs @ [(?oid, Some ?ref)] @ ?ys))\<rbrakk> \<Longrightarrow> \<exists>r. (?ref, r) \<in> set ?xs
ops = cs @ x # ds
snd x = Some ref
ref \<in> set (interp_ins ops)

goal (1 subgoal):
 1. (\<And>rr. (ref, rr) \<in> set cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) append_Cons append_self_conv2 prod.collapse)
[PROOF STATE]
proof (state)
this:
(ref, rr) \<in> set cs

goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
hence "ref \<in> set (interp_ins cs)"
[PROOF STATE]
proof (prove)
using this:
(ref, rr) \<in> set cs

goal (1 subgoal):
 1. ref \<in> set (interp_ins cs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ref, rr) \<in> set cs \<Longrightarrow> ref \<in> set (interp_ins cs)
[PROOF STEP]
have "ops = cs @ ([(fst x, Some ref)] @ ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ops = cs @ [(fst x, Some ref)] @ ds
[PROOF STEP]
by (metis x_split \<open>snd x = Some ref\<close> append_Cons append_self_conv2 prod.collapse)
[PROOF STATE]
proof (state)
this:
ops = cs @ [(fst x, Some ref)] @ ds

goal (1 subgoal):
 1. (ref, rr) \<in> set cs \<Longrightarrow> ref \<in> set (interp_ins cs)
[PROOF STEP]
thus "ref \<in> set (interp_ins cs)"
[PROOF STATE]
proof (prove)
using this:
ops = cs @ [(fst x, Some ref)] @ ds

goal (1 subgoal):
 1. ref \<in> set (interp_ins cs)
[PROOF STEP]
using assms(5) calculation interp_ins_append_forward interp_ins_append_non_memb
[PROOF STATE]
proof (prove)
using this:
ops = cs @ [(fst x, Some ref)] @ ds
ref \<in> set (interp_ins ops)
insert_ops (cs @ [(fst x, Some ref)] @ ds)
\<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)
\<lbrakk>insert_ops (?pre @ [(?oid, Some ?ref)] @ ?suf); ?ref \<notin> set (interp_ins ?pre)\<rbrakk> \<Longrightarrow> ?ref \<notin> set (interp_ins (?pre @ [(?oid, Some ?ref)] @ ?suf))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ref \<in> set (interp_ins cs)

goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)
ref \<in> set (interp_ins cs)
[PROOF STEP]
show "list_order (cs @ [(fst x, Some ref)]) ref (fst x)"
[PROOF STATE]
proof (prove)
using this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)
ref \<in> set (interp_ins cs)

goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
using list_order_insert_ref
[PROOF STATE]
proof (prove)
using this:
insert_ops (cs @ [(fst x, Some ref)] @ ds)
ref \<in> set (interp_ins cs)
\<lbrakk>insert_ops (?ops @ [(?oid, Some ?ref)]); ?ref \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> list_order (?ops @ [(?oid, Some ?ref)]) ?ref ?oid

goal (1 subgoal):
 1. list_order (cs @ [(fst x, Some ref)]) ref (fst x)
[PROOF STEP]
by (metis append.assoc insert_ops_appendD)
[PROOF STATE]
proof (state)
this:
list_order (cs @ [(fst x, Some ref)]) ref (fst x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_order (cs @ [(fst x, Some ref)]) ref (fst x)

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_order (cs @ [(fst x, Some ref)]) ref (fst x)

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
have "ops = (cs @ [(fst x, Some ref)]) @ ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ops = (cs @ [(fst x, Some ref)]) @ ds
[PROOF STEP]
using calculation x_split
[PROOF STATE]
proof (prove)
using this:
snd x = Some ref
list_order (cs @ [(fst x, Some ref)]) ref (fst x)
ops = cs @ x # ds

goal (1 subgoal):
 1. ops = (cs @ [(fst x, Some ref)]) @ ds
[PROOF STEP]
by (metis append_eq_Cons_conv append_eq_append_conv2 append_self_conv2 prod.collapse)
[PROOF STATE]
proof (state)
this:
ops = (cs @ [(fst x, Some ref)]) @ ds

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> list_order ops ref (fst x)
 2. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
snd x = Some ref
list_order (cs @ [(fst x, Some ref)]) ref (fst x)
ops = (cs @ [(fst x, Some ref)]) @ ds
[PROOF STEP]
show "list_order ops ref (fst x)"
[PROOF STATE]
proof (prove)
using this:
snd x = Some ref
list_order (cs @ [(fst x, Some ref)]) ref (fst x)
ops = (cs @ [(fst x, Some ref)]) @ ds

goal (1 subgoal):
 1. list_order ops ref (fst x)
[PROOF STEP]
using list_order_append snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
snd x = Some ref
list_order (cs @ [(fst x, Some ref)]) ref (fst x)
ops = (cs @ [(fst x, Some ref)]) @ ds
\<lbrakk>insert_ops (?pre @ ?suf); list_order ?pre ?x ?y\<rbrakk> \<Longrightarrow> list_order (?pre @ ?suf) ?x ?y
insert_ops ops

goal (1 subgoal):
 1. list_order ops ref (fst x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_order ops ref (fst x)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[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. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[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. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[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 (Some ref) (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. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[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. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[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. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[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. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
have "list_order ops ref yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order ops ref yi
[PROOF STEP]
by (simp add: IH snoc_y yx_pairs)
[PROOF STATE]
proof (state)
this:
list_order ops ref yi

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_order ops ref yi

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
have "list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi
[PROOF STEP]
have "insert_ops ((as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) @ cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops ((as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) @ cs)
[PROOF STEP]
using ops_split snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(yi, yr)] @ bs @ [(xi, Some yi)] @ cs
insert_ops ops

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

goal (1 subgoal):
 1. list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi
[PROOF STEP]
hence "insert_ops ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)])"
[PROOF STATE]
proof (prove)
using this:
insert_ops ((as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) @ cs)

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

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

goal (1 subgoal):
 1. list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_ops ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)])

goal (1 subgoal):
 1. list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi
[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]
using \<open>list_order ops ref yi\<close> list_order_memb2
[PROOF STATE]
proof (prove)
using this:
list_order ops ref yi
list_order ?ops ?x ?y \<Longrightarrow> ?y \<in> set (interp_ins ?ops)

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

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

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

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

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

goal (1 subgoal):
 1. list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi
[PROOF STEP]
using list_order_insert_ref
[PROOF STATE]
proof (prove)
using this:
insert_ops ((as @ [(yi, yr)] @ bs) @ [(xi, Some yi)])
yi \<in> set (interp_ins (as @ [(yi, yr)] @ bs))
\<lbrakk>insert_ops (?ops @ [(?oid, Some ?ref)]); ?ref \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> list_order (?ops @ [(?oid, Some ?ref)]) ?ref ?oid

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
hence "list_order ops yi xi"
[PROOF STATE]
proof (prove)
using this:
list_order (as @ [(yi, yr)] @ bs @ [(xi, Some yi)]) yi xi

goal (1 subgoal):
 1. list_order ops yi xi
[PROOF STEP]
by (metis append_assoc list_order_append ops_split snoc.prems(1))
[PROOF STATE]
proof (state)
this:
list_order ops yi xi

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> list_order ops ref (fst x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list_order ops ref yi
list_order ops yi xi
[PROOF STEP]
show "list_order ops ref (fst x)"
[PROOF STATE]
proof (prove)
using this:
list_order ops ref yi
list_order ops yi xi

goal (1 subgoal):
 1. list_order ops ref (fst x)
[PROOF STEP]
using list_order_trans snoc.prems(1) yx_pairs
[PROOF STATE]
proof (prove)
using this:
list_order ops ref yi
list_order ops yi xi
\<lbrakk>insert_ops ?op_list; list_order ?op_list ?x ?y; list_order ?op_list ?y ?z\<rbrakk> \<Longrightarrow> list_order ?op_list ?x ?z
insert_ops ops
y = (yi, yr) \<and> x = (xi, xr)

goal (1 subgoal):
 1. list_order ops ref (fst x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_order ops ref (fst x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_order ops ref (fst x)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i \<notin> 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 (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops); insert_ops ops; insert_seq (Some ref) (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<notin> set (interp_ins ops)
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops)
insert_ops ops
insert_seq (Some ref) (xs @ [x])
insert_ops (xs @ [x])
set (xs @ [x]) \<subseteq> set ops
ref \<notin> set (interp_ins ops)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops); insert_ops ops; insert_seq (Some ref) (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<notin> set (interp_ins ops)
[PROOF STEP]
have IH: "\<forall>i \<in> set (map fst xs). i \<notin> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops)
[PROOF STEP]
using snoc.IH snoc.prems insert_seq_rem_last insert_ops_appendD
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops)
insert_ops ops
insert_seq (Some ref) (xs @ [x])
insert_ops (xs @ [x])
set (xs @ [x]) \<subseteq> set ops
ref \<notin> set (interp_ins ops)
\<lbrakk>insert_seq ?start (?xs @ [?x]); ?xs \<noteq> []\<rbrakk> \<Longrightarrow> insert_seq ?start ?xs
insert_ops (?xs @ ?ys) \<Longrightarrow> insert_ops ?xs

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops)
[PROOF STEP]
by (metis append_is_Nil_conv le_sup_iff list.map_disc_iff set_append split_list_first)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops ops; insert_seq (Some ref) xs; insert_ops xs; set xs \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst xs). i \<notin> set (interp_ins ops); insert_ops ops; insert_seq (Some ref) (xs @ [x]); insert_ops (xs @ [x]); set (xs @ [x]) \<subseteq> set ops; ref \<notin> set (interp_ins ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (xs @ [x])). i \<notin> set (interp_ins ops)
[PROOF STEP]
obtain as bs where "ops = as @ x # bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as bs. ops = as @ x # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) \<subseteq> set ops

goal (1 subgoal):
 1. (\<And>as bs. ops = as @ x # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis split_list last_in_set snoc_eq_iff_butlast subset_code(1))
[PROOF STATE]
proof (state)
this:
ops = as @ x # bs

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

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
 2. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = []
[PROOF STEP]
obtain xi where "x = (xi, Some ref)"
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. (\<And>xi. x = (xi, Some ref) \<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 (Some ref) (xs @ [x])

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

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
 2. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (xi, Some ref)

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
 2. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
have "ref \<notin> set (interp_ins as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref \<notin> set (interp_ins as)
[PROOF STEP]
using interp_ins_monotonic snoc.prems(1) snoc.prems(5) \<open>ops = as @ x # bs\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops (?pre @ ?suf); ?oid \<in> set (interp_ins ?pre)\<rbrakk> \<Longrightarrow> ?oid \<in> set (interp_ins (?pre @ ?suf))
insert_ops ops
ref \<notin> set (interp_ins ops)
ops = as @ x # bs

goal (1 subgoal):
 1. ref \<notin> set (interp_ins as)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ref \<notin> set (interp_ins as)

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
 2. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = (xi, Some ref)
ref \<notin> set (interp_ins as)
[PROOF STEP]
have "xi \<notin> set (interp_ins (as @ [x] @ bs))"
[PROOF STATE]
proof (prove)
using this:
x = (xi, Some ref)
ref \<notin> set (interp_ins as)

goal (1 subgoal):
 1. xi \<notin> set (interp_ins (as @ [x] @ bs))
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
x = (xi, Some ref)
ref \<notin> set (interp_ins as)
insert_ops ops

goal (1 subgoal):
 1. xi \<notin> set (interp_ins (as @ [x] @ bs))
[PROOF STEP]
by (simp add: interp_ins_ref_nonex \<open>ops = as @ x # bs\<close>)
[PROOF STATE]
proof (state)
this:
xi \<notin> set (interp_ins (as @ [x] @ bs))

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
 2. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xi \<notin> set (interp_ins (as @ [x] @ bs))
[PROOF STEP]
show "fst x \<notin> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
xi \<notin> set (interp_ins (as @ [x] @ bs))

goal (1 subgoal):
 1. fst x \<notin> set (interp_ins ops)
[PROOF STEP]
by (simp add: \<open>ops = as @ x # bs\<close> \<open>x = (xi, Some ref)\<close>)
[PROOF STATE]
proof (state)
this:
fst x \<notin> set (interp_ins ops)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
case xs_nonempty: False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
[PROOF STEP]
obtain y where "xs = (butlast xs) @ [y]"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

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

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = butlast xs @ [y]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
xs = butlast xs @ [y]
[PROOF STEP]
obtain yi yr xi xr where "y = (yi, yr) \<and> x = (xi, xr)"
[PROOF STATE]
proof (prove)
using this:
xs = butlast xs @ [y]

goal (1 subgoal):
 1. (\<And>yi yr xi xr. y = (yi, yr) \<and> x = (xi, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y = (yi, yr) \<and> x = (xi, xr)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y = (yi, yr) \<and> x = (xi, xr)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
from this
[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.cases snoc.prems(2) calculation
[PROOF STATE]
proof (prove)
using this:
y = (yi, yr) \<and> x = (xi, xr)
\<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
insert_seq (Some ref) (xs @ [x])
xs = butlast xs @ [y]
y = (yi, yr) \<and> x = (xi, xr)

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

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xr = Some yi

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

goal (1 subgoal):
 1. yi \<notin> set (interp_ins ops)
[PROOF STEP]
by (metis Nil_is_map_conv fst_conv last_in_set last_map snoc_eq_iff_butlast)
[PROOF STATE]
proof (state)
this:
yi \<notin> set (interp_ins ops)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
hence "yi \<notin> set (interp_ins as)"
[PROOF STATE]
proof (prove)
using this:
yi \<notin> set (interp_ins ops)

goal (1 subgoal):
 1. yi \<notin> set (interp_ins as)
[PROOF STEP]
using \<open>ops = as @ x # bs\<close> interp_ins_monotonic snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
yi \<notin> set (interp_ins ops)
ops = as @ x # bs
\<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. yi \<notin> set (interp_ins as)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
yi \<notin> set (interp_ins as)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs = butlast xs @ [y]
y = (yi, yr) \<and> x = (xi, xr)
xr = Some yi
yi \<notin> set (interp_ins as)
[PROOF STEP]
have "xi \<notin> set (interp_ins (as @ [x] @ bs))"
[PROOF STATE]
proof (prove)
using this:
xs = butlast xs @ [y]
y = (yi, yr) \<and> x = (xi, xr)
xr = Some yi
yi \<notin> set (interp_ins as)

goal (1 subgoal):
 1. xi \<notin> set (interp_ins (as @ [x] @ bs))
[PROOF STEP]
using interp_ins_ref_nonex snoc.prems(1) \<open>ops = as @ x # bs\<close>
[PROOF STATE]
proof (prove)
using this:
xs = butlast xs @ [y]
y = (yi, yr) \<and> x = (xi, xr)
xr = Some yi
yi \<notin> set (interp_ins as)
\<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 = as @ x # bs

goal (1 subgoal):
 1. xi \<notin> set (interp_ins (as @ [x] @ bs))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xi \<notin> set (interp_ins (as @ [x] @ bs))

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> fst x \<notin> set (interp_ins ops)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xi \<notin> set (interp_ins (as @ [x] @ bs))
[PROOF STEP]
show "fst x \<notin> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
using this:
xi \<notin> set (interp_ins (as @ [x] @ bs))

goal (1 subgoal):
 1. fst x \<notin> set (interp_ins ops)
[PROOF STEP]
by (simp add: \<open>ops = as @ x # bs\<close> \<open>y = (yi, yr) \<and> x = (xi, xr)\<close>)
[PROOF STATE]
proof (state)
this:
fst x \<notin> set (interp_ins ops)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst x \<notin> set (interp_ins ops)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed