[STATEMENT]
lemma insert_ops_split:
  assumes "insert_ops ops"
    and "(oid, ref) \<in> set ops"
  shows "\<exists>pre suf. ops = pre @ [(oid, ref)] @ suf \<and>
            (\<forall>i \<in> set (map fst pre). i < oid) \<and>
            (\<forall>i \<in> set (map fst suf). oid < i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre suf. ops = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
(oid, ref) \<in> set ops

goal (1 subgoal):
 1. \<exists>pre suf. ops = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
[PROOF STEP]
proof(induction ops rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>insert_ops []; (oid, ref) \<in> set []\<rbrakk> \<Longrightarrow> \<exists>pre suf. [] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
 2. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops []
(oid, ref) \<in> set []

goal (2 subgoals):
 1. \<lbrakk>insert_ops []; (oid, ref) \<in> set []\<rbrakk> \<Longrightarrow> \<exists>pre suf. [] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
 2. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops []
(oid, ref) \<in> set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
insert_ops []
(oid, ref) \<in> set []

goal (1 subgoal):
 1. \<exists>pre suf. [] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. [] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
insert_ops (xs @ [x])
(oid, ref) \<in> set (xs @ [x])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
insert_ops (xs @ [x])
(oid, ref) \<in> set (xs @ [x])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
insert_ops (xs @ [x])
(oid, ref) \<in> set (xs @ [x])

goal (1 subgoal):
 1. \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
proof(cases "x = (oid, ref)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x = (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = (oid, ref)

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x = (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (oid, ref)

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x = (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x = (oid, ref)
[PROOF STEP]
have "\<forall>i \<in> set (map fst xs). i < oid"
[PROOF STATE]
proof (prove)
using this:
x = (oid, ref)

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i < oid
[PROOF STEP]
using last_op_greatest snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
x = (oid, ref)
\<lbrakk>insert_ops (?op_list @ [(?oid, ?oper)]); ?x \<in> set (map fst ?op_list)\<rbrakk> \<Longrightarrow> ?x < ?oid
insert_ops (xs @ [x])

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

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x = (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = (oid, ref)
\<forall>i\<in>set (map fst xs). i < oid
[PROOF STEP]
have "xs @ [x] = xs @ [(oid, ref)] @ [] \<and>
            (\<forall>i \<in> set (map fst xs). i < oid) \<and>
            (\<forall>i \<in> set (map fst []). oid < i)"
[PROOF STATE]
proof (prove)
using this:
x = (oid, ref)
\<forall>i\<in>set (map fst xs). i < oid

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

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x = (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs @ [x] = xs @ [(oid, ref)] @ [] \<and> (\<forall>i\<in>set (map fst xs). i < oid) \<and> (\<forall>i\<in>set (map fst []). oid < i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs @ [x] = xs @ [(oid, ref)] @ [] \<and> (\<forall>i\<in>set (map fst xs). i < oid) \<and> (\<forall>i\<in>set (map fst []). oid < i)

goal (1 subgoal):
 1. \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> (oid, ref)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
hence "(oid, ref) \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (oid, ref)

goal (1 subgoal):
 1. (oid, ref) \<in> set xs
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (oid, ref)
(oid, ref) \<in> set (xs @ [x])

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(oid, ref) \<in> set xs
[PROOF STEP]
obtain pre suf where IH: "xs = pre @ [(oid, ref)] @ suf \<and>
         (\<forall>i \<in> set (map fst pre). i < oid) \<and>
         (\<forall>i \<in> set (map fst suf). oid < i)"
[PROOF STATE]
proof (prove)
using this:
(oid, ref) \<in> set xs

goal (1 subgoal):
 1. (\<And>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using snoc.IH snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
(oid, ref) \<in> set xs
\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
insert_ops (xs @ [x])

goal (1 subgoal):
 1. (\<And>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
obtain xi xr where x_pair: "x = (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi xr. x = (xi, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (xi, xr)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
hence "distinct (map fst (pre @ [(oid, ref)] @ suf @ [(xi, xr)]))"
[PROOF STATE]
proof (prove)
using this:
x = (xi, xr)

goal (1 subgoal):
 1. distinct (map fst (pre @ [(oid, ref)] @ suf @ [(xi, xr)]))
[PROOF STEP]
by (metis IH append.assoc insert_ops_def spec_ops_def snoc.prems(1))
[PROOF STATE]
proof (state)
this:
distinct (map fst (pre @ [(oid, ref)] @ suf @ [(xi, xr)]))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
hence "xi \<noteq> oid"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (pre @ [(oid, ref)] @ suf @ [(xi, xr)]))

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
have xi_max: "\<forall>x \<in> set (map fst (pre @ [(oid, ref)] @ suf)). x < xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi
[PROOF STEP]
using IH last_op_greatest snoc.prems(1) x_pair
[PROOF STATE]
proof (prove)
using this:
xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
\<lbrakk>insert_ops (?op_list @ [(?oid, ?oper)]); ?x \<in> set (map fst ?op_list)\<rbrakk> \<Longrightarrow> ?x < ?oid
insert_ops (xs @ [x])
x = (xi, xr)

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops xs; (oid, ref) \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); insert_ops (xs @ [x]); (oid, ref) \<in> set (xs @ [x]); x \<noteq> (oid, ref)\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi

goal (1 subgoal):
 1. \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
proof(cases "xi < oid")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xi < oid

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xi < oid

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
xi < oid
[PROOF STEP]
have "\<forall>x \<in> set suf. fst x < oid"
[PROOF STATE]
proof (prove)
using this:
xi < oid

goal (1 subgoal):
 1. \<forall>x\<in>set suf. fst x < oid
[PROOF STEP]
using xi_max
[PROOF STATE]
proof (prove)
using this:
xi < oid
\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi

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

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
hence "suf = []"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set suf. fst x < oid

goal (1 subgoal):
 1. suf = []
[PROOF STEP]
using IH last_in_set
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set suf. fst x < oid
xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as

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

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xi < oid
suf = []
[PROOF STEP]
have "xs @ [x] = (pre @ [(xi, xr)]) @ [] \<and>
              (\<forall>i \<in> set (map fst ((pre @ [(xi, xr)]))). i < oid) \<and>
              (\<forall>i \<in> set (map fst []). oid < i)"
[PROOF STATE]
proof (prove)
using this:
xi < oid
suf = []

goal (1 subgoal):
 1. xs @ [x] = (pre @ [(xi, xr)]) @ [] \<and> (\<forall>i\<in>set (map fst (pre @ [(xi, xr)])). i < oid) \<and> (\<forall>i\<in>set (map fst []). oid < i)
[PROOF STEP]
using dual_order.asym xi_max
[PROOF STATE]
proof (prove)
using this:
xi < oid
suf = []
\<lbrakk>?b < ?a; ?a < ?b\<rbrakk> \<Longrightarrow> False
\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi

goal (1 subgoal):
 1. xs @ [x] = (pre @ [(xi, xr)]) @ [] \<and> (\<forall>i\<in>set (map fst (pre @ [(xi, xr)])). i < oid) \<and> (\<forall>i\<in>set (map fst []). oid < i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs @ [x] = (pre @ [(xi, xr)]) @ [] \<and> (\<forall>i\<in>set (map fst (pre @ [(xi, xr)])). i < oid) \<and> (\<forall>i\<in>set (map fst []). oid < i)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs @ [x] = (pre @ [(xi, xr)]) @ [] \<and> (\<forall>i\<in>set (map fst (pre @ [(xi, xr)])). i < oid) \<and> (\<forall>i\<in>set (map fst []). oid < i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs @ [x] = (pre @ [(xi, xr)]) @ [] \<and> (\<forall>i\<in>set (map fst (pre @ [(xi, xr)])). i < oid) \<and> (\<forall>i\<in>set (map fst []). oid < i)

goal (1 subgoal):
 1. \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
by (simp add: IH)
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> xi < oid

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
hence "oid < xi"
[PROOF STATE]
proof (prove)
using this:
\<not> xi < oid

goal (1 subgoal):
 1. oid < xi
[PROOF STEP]
using \<open>xi \<noteq> oid\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> xi < oid
xi \<noteq> oid

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
hence "\<forall>i \<in> set (map fst (suf @ [(xi, xr)])). oid < i"
[PROOF STATE]
proof (prove)
using this:
oid < xi

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i
[PROOF STEP]
using IH map_fst_append1
[PROOF STATE]
proof (prove)
using this:
oid < xi
xs = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst suf). oid < i)
\<lbrakk>\<forall>i\<in>set (map fst ?xs). ?P i; ?P ?x\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst (?xs @ [(?x, ?y)])). ?P i

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
hence "xs @ [x] = pre @ [(oid, ref)] @ (suf @ [(xi, xr)]) \<and>
              (\<forall>i \<in> set (map fst pre). i < oid) \<and>
              (\<forall>i \<in> set (map fst (suf @ [(xi, xr)])). oid < i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i

goal (1 subgoal):
 1. xs @ [x] = pre @ [(oid, ref)] @ suf @ [(xi, xr)] \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i)
[PROOF STEP]
by (simp add: IH x_pair)
[PROOF STATE]
proof (state)
this:
xs @ [x] = pre @ [(oid, ref)] @ suf @ [(xi, xr)] \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set (map fst (pre @ [(oid, ref)] @ suf)). x < xi; \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs @ [x] = pre @ [(oid, ref)] @ suf @ [(xi, xr)] \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs @ [x] = pre @ [(oid, ref)] @ suf @ [(xi, xr)] \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>i\<in>set (map fst (suf @ [(xi, xr)])). oid < i)

goal (1 subgoal):
 1. \<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pre suf. xs @ [x] = pre @ [(oid, ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_ops_split_2:
  assumes "insert_ops ops"
    and "(xid, xr) \<in> set ops"
    and "(yid, yr) \<in> set ops"
    and "xid < yid"
  shows "\<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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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)
[PROOF STEP]
obtain as as1 where x_split: "ops = as @ [(xid, xr)] @ as1 \<and>
      (\<forall>i \<in> set (map fst as). i < xid) \<and> (\<forall>i \<in> set (map fst as1). xid < i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as as1. ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms insert_ops_split
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
(xid, xr) \<in> set ops
(yid, yr) \<in> set ops
xid < yid
\<lbrakk>insert_ops ?ops; (?oid, ?ref) \<in> set ?ops\<rbrakk> \<Longrightarrow> \<exists>pre suf. ?ops = pre @ [(?oid, ?ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < ?oid) \<and> (\<forall>i\<in>set (map fst suf). ?oid < i)

goal (1 subgoal):
 1. (\<And>as as1. ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i)

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
hence "insert_ops ((as @ [(xid, xr)]) @ as1)"
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i)

goal (1 subgoal):
 1. insert_ops ((as @ [(xid, xr)]) @ as1)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i)
insert_ops ops

goal (1 subgoal):
 1. insert_ops ((as @ [(xid, xr)]) @ as1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_ops ((as @ [(xid, xr)]) @ as1)

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
hence "insert_ops as1"
[PROOF STATE]
proof (prove)
using this:
insert_ops ((as @ [(xid, xr)]) @ as1)

goal (1 subgoal):
 1. insert_ops as1
[PROOF STEP]
using assms(1) insert_ops_rem_prefix
[PROOF STATE]
proof (prove)
using this:
insert_ops ((as @ [(xid, xr)]) @ as1)
insert_ops ops
insert_ops (?pre @ ?suf) \<Longrightarrow> insert_ops ?suf

goal (1 subgoal):
 1. insert_ops as1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
insert_ops as1

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
have "(yid, yr) \<in> set as1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (yid, yr) \<in> set as1
[PROOF STEP]
using x_split assms
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i)
insert_ops ops
(xid, xr) \<in> set ops
(yid, yr) \<in> set ops
xid < yid

goal (1 subgoal):
 1. (yid, yr) \<in> set as1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(yid, yr) \<in> set as1

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(yid, yr) \<in> set as1
[PROOF STEP]
obtain bs cs where y_split: "as1 = bs @ [(yid, yr)] @ cs \<and>
      (\<forall>i \<in> set (map fst bs). i < yid) \<and> (\<forall>i \<in> set (map fst cs). yid < i)"
[PROOF STATE]
proof (prove)
using this:
(yid, yr) \<in> set as1

goal (1 subgoal):
 1. (\<And>bs cs. as1 = bs @ [(yid, yr)] @ cs \<and> (\<forall>i\<in>set (map fst bs). i < yid) \<and> (\<forall>i\<in>set (map fst cs). yid < i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms insert_ops_split \<open>insert_ops as1\<close>
[PROOF STATE]
proof (prove)
using this:
(yid, yr) \<in> set as1
insert_ops ops
(xid, xr) \<in> set ops
(yid, yr) \<in> set ops
xid < yid
\<lbrakk>insert_ops ?ops; (?oid, ?ref) \<in> set ?ops\<rbrakk> \<Longrightarrow> \<exists>pre suf. ?ops = pre @ [(?oid, ?ref)] @ suf \<and> (\<forall>i\<in>set (map fst pre). i < ?oid) \<and> (\<forall>i\<in>set (map fst suf). ?oid < i)
insert_ops as1

goal (1 subgoal):
 1. (\<And>bs cs. as1 = bs @ [(yid, yr)] @ cs \<and> (\<forall>i\<in>set (map fst bs). i < yid) \<and> (\<forall>i\<in>set (map fst cs). yid < i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
as1 = bs @ [(yid, yr)] @ cs \<and> (\<forall>i\<in>set (map fst bs). i < yid) \<and> (\<forall>i\<in>set (map fst cs). yid < i)

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
hence "ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs"
[PROOF STATE]
proof (prove)
using this:
as1 = bs @ [(yid, yr)] @ cs \<and> (\<forall>i\<in>set (map fst bs). i < yid) \<and> (\<forall>i\<in>set (map fst cs). yid < i)

goal (1 subgoal):
 1. ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs
[PROOF STEP]
using x_split
[PROOF STATE]
proof (prove)
using this:
as1 = bs @ [(yid, yr)] @ cs \<and> (\<forall>i\<in>set (map fst bs). i < yid) \<and> (\<forall>i\<in>set (map fst cs). yid < i)
ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i)

goal (1 subgoal):
 1. ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
have "\<forall>i \<in> set (map fst bs). xid < i \<and> i < yid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst bs). xid < i \<and> i < yid
[PROOF STEP]
by (simp add: x_split y_split)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst bs). xid < i \<and> i < yid

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs
\<forall>i\<in>set (map fst bs). xid < i \<and> i < yid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs
\<forall>i\<in>set (map fst bs). xid < i \<and> i < yid

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
using x_split y_split
[PROOF STATE]
proof (prove)
using this:
ops = as @ [(xid, xr)] @ bs @ [(yid, yr)] @ cs
\<forall>i\<in>set (map fst bs). xid < i \<and> i < yid
ops = as @ [(xid, xr)] @ as1 \<and> (\<forall>i\<in>set (map fst as). i < xid) \<and> (\<forall>i\<in>set (map fst as1). xid < i)
as1 = bs @ [(yid, yr)] @ cs \<and> (\<forall>i\<in>set (map fst bs). i < yid) \<and> (\<forall>i\<in>set (map fst cs). yid < i)

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<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)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_ops_sorted_oids:
  assumes "insert_ops (xs @ [(i1, r1)] @ ys @ [(i2, r2)])"
  shows "i1 < i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i1 < i2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i1 < i2
[PROOF STEP]
have "\<And>i. i \<in> set (map fst (xs @ [(i1, r1)] @ ys)) \<Longrightarrow> i < i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst (xs @ [(i1, r1)] @ ys)) \<Longrightarrow> i < i2
[PROOF STEP]
by (metis append.assoc assms last_op_greatest)
[PROOF STATE]
proof (state)
this:
?i \<in> set (map fst (xs @ [(i1, r1)] @ ys)) \<Longrightarrow> ?i < i2

goal (1 subgoal):
 1. i1 < i2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i \<in> set (map fst (xs @ [(i1, r1)] @ ys)) \<Longrightarrow> ?i < i2

goal (1 subgoal):
 1. i1 < i2
[PROOF STEP]
have "i1 \<in> set (map fst (xs @ [(i1, r1)] @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i1 \<in> set (map fst (xs @ [(i1, r1)] @ ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i1 \<in> set (map fst (xs @ [(i1, r1)] @ ys))

goal (1 subgoal):
 1. i1 < i2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i \<in> set (map fst (xs @ [(i1, r1)] @ ys)) \<Longrightarrow> ?i < i2
i1 \<in> set (map fst (xs @ [(i1, r1)] @ ys))
[PROOF STEP]
show "i1 < i2"
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst (xs @ [(i1, r1)] @ ys)) \<Longrightarrow> ?i < i2
i1 \<in> set (map fst (xs @ [(i1, r1)] @ ys))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_ops_subset_last:
  assumes "insert_ops (xs @ [x])"
    and "insert_ops ys"
    and "set ys \<subseteq> set (xs @ [x])"
    and "x \<in> set ys"
  shows "x = last ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = last ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [x])
insert_ops ys
set ys \<subseteq> set (xs @ [x])
x \<in> set ys

goal (1 subgoal):
 1. x = last ys
[PROOF STEP]
proof(induction ys, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (a # ys); set (a # ys) \<subseteq> set (xs @ [x]); x \<in> set (a # ys)\<rbrakk> \<Longrightarrow> x = last (a # ys)
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys
insert_ops (xs @ [x])
insert_ops (y # ys)
set (y # ys) \<subseteq> set (xs @ [x])
x \<in> set (y # ys)

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (a # ys); set (a # ys) \<subseteq> set (xs @ [x]); x \<in> set (a # ys)\<rbrakk> \<Longrightarrow> x = last (a # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys
insert_ops (xs @ [x])
insert_ops (y # ys)
set (y # ys) \<subseteq> set (xs @ [x])
x \<in> set (y # ys)
[PROOF STEP]
show "x = last (y # ys)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys
insert_ops (xs @ [x])
insert_ops (y # ys)
set (y # ys) \<subseteq> set (xs @ [x])
x \<in> set (y # ys)

goal (1 subgoal):
 1. x = last (y # ys)
[PROOF STEP]
proof(cases "ys = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys = []\<rbrakk> \<Longrightarrow> x = last (y # ys)
 2. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> x = last (y # ys)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ys = []

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys = []\<rbrakk> \<Longrightarrow> x = last (y # ys)
 2. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> x = last (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = []
[PROOF STEP]
show "x = last (y # ys)"
[PROOF STATE]
proof (prove)
using this:
ys = []

goal (1 subgoal):
 1. x = last (y # ys)
[PROOF STEP]
using Cons.prems(4)
[PROOF STATE]
proof (prove)
using this:
ys = []
x \<in> set (y # ys)

goal (1 subgoal):
 1. x = last (y # ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = last (y # ys)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> x = last (y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> x = last (y # ys)
[PROOF STEP]
case ys_nonempty: False
[PROOF STATE]
proof (state)
this:
ys \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> x = last (y # ys)
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
obtain mid l where "ys = mid @ [l]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>mid l. ys = mid @ [l] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using append_butlast_last_id ys_nonempty
[PROOF STATE]
proof (prove)
using this:
?xs \<noteq> [] \<Longrightarrow> butlast ?xs @ [last ?xs] = ?xs
ys \<noteq> []

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

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys = mid @ [l]

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
obtain li lr where "l = (li, lr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>li lr. l = (li, lr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
l = (li, lr)

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l = (li, lr)

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
have "\<And>i. i \<in> set (map fst (y # mid)) \<Longrightarrow> i < li"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst (y # mid)) \<Longrightarrow> i < li
[PROOF STEP]
by (metis last_op_greatest Cons.prems(2) calculation append_Cons)
[PROOF STATE]
proof (state)
this:
?i \<in> set (map fst (y # mid)) \<Longrightarrow> ?i < li

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
hence "fst y < li"
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst (y # mid)) \<Longrightarrow> ?i < li

goal (1 subgoal):
 1. fst y < li
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst y < li

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst y < li

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
have "\<And>i. i \<in> set (map fst xs) \<Longrightarrow> i < fst x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst xs) \<Longrightarrow> i < fst x
[PROOF STEP]
using assms(1) last_op_greatest
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [x])
\<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 < fst x
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
?i \<in> set (map fst xs) \<Longrightarrow> ?i < fst x

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
hence "\<And>i. i \<in> set (map fst (y # ys)) \<Longrightarrow> i \<le> fst x"
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst xs) \<Longrightarrow> ?i < fst x

goal (1 subgoal):
 1. \<And>i. i \<in> set (map fst (y # ys)) \<Longrightarrow> i \<le> fst x
[PROOF STEP]
using Cons.prems(3)
[PROOF STATE]
proof (prove)
using this:
?i \<in> set (map fst xs) \<Longrightarrow> ?i < fst x
set (y # ys) \<subseteq> set (xs @ [x])

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

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ys = mid @ [l]
l = (li, lr)
fst y < li
?i \<in> set (map fst (y # ys)) \<Longrightarrow> ?i \<le> fst x
[PROOF STEP]
show "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
ys = mid @ [l]
l = (li, lr)
fst y < li
?i \<in> set (map fst (y # ys)) \<Longrightarrow> ?i \<le> fst x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys; insert_ops (xs @ [x]); insert_ops (y # ys); set (y # ys) \<subseteq> set (xs @ [x]); x \<in> set (y # ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> x = last (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
[PROOF STEP]
show "x = last (y # ys)"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. x = last (y # ys)
[PROOF STEP]
using Cons.IH Cons.prems insert_ops_rem_cons ys_nonempty
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
\<lbrakk>insert_ops (xs @ [x]); insert_ops ys; set ys \<subseteq> set (xs @ [x]); x \<in> set ys\<rbrakk> \<Longrightarrow> x = last ys
insert_ops (xs @ [x])
insert_ops (y # ys)
set (y # ys) \<subseteq> set (xs @ [x])
x \<in> set (y # ys)
insert_ops (?x # ?xs) \<Longrightarrow> insert_ops ?xs
ys \<noteq> []

goal (1 subgoal):
 1. x = last (y # ys)
[PROOF STEP]
by (metis dual_order.trans last_ConsR set_ConsD set_subset_Cons)
[PROOF STATE]
proof (state)
this:
x = last (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = last (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_butlast:
  assumes "set xs \<subseteq> set (ys @ [y])"
    and "last xs = y"
    and "distinct xs"
  shows "set (butlast xs) \<subseteq> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (butlast xs) \<subseteq> set ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> set (ys @ [y])
last xs = y
distinct xs

goal (1 subgoal):
 1. set (butlast xs) \<subseteq> set ys
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma distinct_append_butlast1:
  assumes "distinct (map fst xs @ map fst ys)"
  shows "distinct (map fst (butlast xs) @ map fst ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (butlast xs) @ map fst ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (map fst xs @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst (butlast xs) @ map fst ys)
[PROOF STEP]
proof(induction xs, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys)
distinct (map fst (a # xs) @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
have "fst a \<notin> set (map fst xs @ map fst ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst a \<notin> set (map fst xs @ map fst ys)
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (a # xs) @ map fst ys)

goal (1 subgoal):
 1. fst a \<notin> set (map fst xs @ map fst ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst a \<notin> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst a \<notin> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
have "set (map fst (butlast xs)) \<subseteq> set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map fst (butlast xs)) \<subseteq> set (map fst xs)
[PROOF STEP]
by (metis in_set_butlastD map_butlast subsetI)
[PROOF STATE]
proof (state)
this:
set (map fst (butlast xs)) \<subseteq> set (map fst xs)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
hence "set (map fst (butlast xs) @ map fst ys) \<subseteq> set (map fst xs @ map fst ys)"
[PROOF STATE]
proof (prove)
using this:
set (map fst (butlast xs)) \<subseteq> set (map fst xs)

goal (1 subgoal):
 1. set (map fst (butlast xs) @ map fst ys) \<subseteq> set (map fst xs @ map fst ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map fst (butlast xs) @ map fst ys) \<subseteq> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst a \<notin> set (map fst xs @ map fst ys)
set (map fst (butlast xs) @ map fst ys) \<subseteq> set (map fst xs @ map fst ys)
[PROOF STEP]
have "fst a \<notin> set (map fst (butlast xs) @ map fst ys)"
[PROOF STATE]
proof (prove)
using this:
fst a \<notin> set (map fst xs @ map fst ys)
set (map fst (butlast xs) @ map fst ys) \<subseteq> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. fst a \<notin> set (map fst (butlast xs) @ map fst ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst a \<notin> set (map fst (butlast xs) @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst a \<notin> set (map fst (butlast xs) @ map fst ys)
[PROOF STEP]
show "distinct (map fst (butlast (a # xs)) @ map fst ys)"
[PROOF STATE]
proof (prove)
using this:
fst a \<notin> set (map fst (butlast xs) @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
using Cons.IH Cons.prems
[PROOF STATE]
proof (prove)
using this:
fst a \<notin> set (map fst (butlast xs) @ map fst ys)
distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst (butlast xs) @ map fst ys)
distinct (map fst (a # xs) @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst (butlast (a # xs)) @ map fst ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map fst (butlast (a # xs)) @ map fst ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_append_butlast2:
  assumes "distinct (map fst xs @ map fst ys)"
  shows "distinct (map fst xs @ map fst (butlast ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs @ map fst (butlast ys))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (map fst xs @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst xs @ map fst (butlast ys))
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct (map fst [] @ map fst ys) \<Longrightarrow> distinct (map fst [] @ map fst (butlast ys))
 2. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
distinct (map fst [] @ map fst ys)

goal (2 subgoals):
 1. distinct (map fst [] @ map fst ys) \<Longrightarrow> distinct (map fst [] @ map fst (butlast ys))
 2. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst [] @ map fst ys)
[PROOF STEP]
show "distinct (map fst [] @ map fst (butlast ys))"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst [] @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst [] @ map fst (butlast ys))
[PROOF STEP]
by (simp add: distinct_butlast map_butlast)
[PROOF STATE]
proof (state)
this:
distinct (map fst [] @ map fst (butlast ys))

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys))
distinct (map fst (a # xs) @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
have "fst a \<notin> set (map fst xs @ map fst ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst a \<notin> set (map fst xs @ map fst ys)
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (a # xs) @ map fst ys)

goal (1 subgoal):
 1. fst a \<notin> set (map fst xs @ map fst ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst a \<notin> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst a \<notin> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
have "set (map fst (butlast ys)) \<subseteq> set (map fst ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map fst (butlast ys)) \<subseteq> set (map fst ys)
[PROOF STEP]
by (metis in_set_butlastD map_butlast subsetI)
[PROOF STATE]
proof (state)
this:
set (map fst (butlast ys)) \<subseteq> set (map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
hence "set (map fst xs @ map fst (butlast ys)) \<subseteq> set (map fst xs @ map fst ys)"
[PROOF STATE]
proof (prove)
using this:
set (map fst (butlast ys)) \<subseteq> set (map fst ys)

goal (1 subgoal):
 1. set (map fst xs @ map fst (butlast ys)) \<subseteq> set (map fst xs @ map fst ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map fst xs @ map fst (butlast ys)) \<subseteq> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst a \<notin> set (map fst xs @ map fst ys)
set (map fst xs @ map fst (butlast ys)) \<subseteq> set (map fst xs @ map fst ys)
[PROOF STEP]
have "fst a \<notin> set (map fst xs @ map fst (butlast ys))"
[PROOF STATE]
proof (prove)
using this:
fst a \<notin> set (map fst xs @ map fst ys)
set (map fst xs @ map fst (butlast ys)) \<subseteq> set (map fst xs @ map fst ys)

goal (1 subgoal):
 1. fst a \<notin> set (map fst xs @ map fst (butlast ys))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst a \<notin> set (map fst xs @ map fst (butlast ys))

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys)); distinct (map fst (a # xs) @ map fst ys)\<rbrakk> \<Longrightarrow> distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst a \<notin> set (map fst xs @ map fst (butlast ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fst a \<notin> set (map fst xs @ map fst (butlast ys))

goal (1 subgoal):
 1. distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
using Cons.IH Cons.prems
[PROOF STATE]
proof (prove)
using this:
fst a \<notin> set (map fst xs @ map fst (butlast ys))
distinct (map fst xs @ map fst ys) \<Longrightarrow> distinct (map fst xs @ map fst (butlast ys))
distinct (map fst (a # xs) @ map fst ys)

goal (1 subgoal):
 1. distinct (map fst (a # xs) @ map fst (butlast ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map fst (a # xs) @ map fst (butlast ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_ins_maybe_grow:
  assumes "insert_ops (xs @ [(oid, ref)])"
  shows "set (interp_ins (xs @ [(oid, ref)])) = set (interp_ins xs) \<or>
         set (interp_ins (xs @ [(oid, ref)])) = (set (interp_ins xs) \<union> {oid})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (interp_ins (xs @ [(oid, ref)])) = set (interp_ins xs) \<or> set (interp_ins (xs @ [(oid, ref)])) = set (interp_ins xs) \<union> {oid}
[PROOF STEP]
by (cases ref, simp add: interp_ins_tail_unfold,
      metis insert_spec_nonex insert_spec_set interp_ins_tail_unfold)


[STATEMENT]
lemma interp_ins_maybe_grow2:
  assumes "insert_ops (xs @ [x])"
  shows "set (interp_ins (xs @ [x])) = set (interp_ins xs) \<or>
         set (interp_ins (xs @ [x])) = (set (interp_ins xs) \<union> {fst x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (interp_ins (xs @ [x])) = set (interp_ins xs) \<or> set (interp_ins (xs @ [x])) = set (interp_ins xs) \<union> {fst x}
[PROOF STEP]
using assms interp_ins_maybe_grow
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [x])
insert_ops (?xs @ [(?oid, ?ref)]) \<Longrightarrow> set (interp_ins (?xs @ [(?oid, ?ref)])) = set (interp_ins ?xs) \<or> set (interp_ins (?xs @ [(?oid, ?ref)])) = set (interp_ins ?xs) \<union> {?oid}

goal (1 subgoal):
 1. set (interp_ins (xs @ [x])) = set (interp_ins xs) \<or> set (interp_ins (xs @ [x])) = set (interp_ins xs) \<union> {fst x}
[PROOF STEP]
by (cases x, auto)


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

goal (1 subgoal):
 1. \<exists>A\<subseteq>set (map fst ys). set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A
[PROOF STEP]
proof(induction ys rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. insert_ops (xs @ []) \<Longrightarrow> \<exists>A\<subseteq>set (map fst []). set (interp_ins (xs @ [])) = set (interp_ins xs) \<union> A
 2. \<And>x xsa. \<lbrakk>insert_ops (xs @ xsa) \<Longrightarrow> \<exists>A\<subseteq>set (map fst xsa). set (interp_ins (xs @ xsa)) = set (interp_ins xs) \<union> A; insert_ops (xs @ xsa @ [x])\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (xsa @ [x])). set (interp_ins (xs @ xsa @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops (xs @ [])

goal (2 subgoals):
 1. insert_ops (xs @ []) \<Longrightarrow> \<exists>A\<subseteq>set (map fst []). set (interp_ins (xs @ [])) = set (interp_ins xs) \<union> A
 2. \<And>x xsa. \<lbrakk>insert_ops (xs @ xsa) \<Longrightarrow> \<exists>A\<subseteq>set (map fst xsa). set (interp_ins (xs @ xsa)) = set (interp_ins xs) \<union> A; insert_ops (xs @ xsa @ [x])\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (xsa @ [x])). set (interp_ins (xs @ xsa @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops (xs @ [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [])

goal (1 subgoal):
 1. \<exists>A\<subseteq>set (map fst []). set (interp_ins (xs @ [])) = set (interp_ins xs) \<union> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>A\<subseteq>set (map fst []). set (interp_ins (xs @ [])) = set (interp_ins xs) \<union> A

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>insert_ops (xs @ xsa) \<Longrightarrow> \<exists>A\<subseteq>set (map fst xsa). set (interp_ins (xs @ xsa)) = set (interp_ins xs) \<union> A; insert_ops (xs @ xsa @ [x])\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (xsa @ [x])). set (interp_ins (xs @ xsa @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>insert_ops (xs @ xsa) \<Longrightarrow> \<exists>A\<subseteq>set (map fst xsa). set (interp_ins (xs @ xsa)) = set (interp_ins xs) \<union> A; insert_ops (xs @ xsa @ [x])\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (xsa @ [x])). set (interp_ins (xs @ xsa @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
case (snoc x ys)
[PROOF STATE]
proof (state)
this:
insert_ops (xs @ ys) \<Longrightarrow> \<exists>A\<subseteq>set (map fst ys). set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A
insert_ops (xs @ ys @ [x])

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>insert_ops (xs @ xsa) \<Longrightarrow> \<exists>A\<subseteq>set (map fst xsa). set (interp_ins (xs @ xsa)) = set (interp_ins xs) \<union> A; insert_ops (xs @ xsa @ [x])\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (xsa @ [x])). set (interp_ins (xs @ xsa @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops (xs @ ys) \<Longrightarrow> \<exists>A\<subseteq>set (map fst ys). set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A
insert_ops (xs @ ys @ [x])
[PROOF STEP]
have "insert_ops (xs @ ys)"
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ ys) \<Longrightarrow> \<exists>A\<subseteq>set (map fst ys). set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A
insert_ops (xs @ ys @ [x])

goal (1 subgoal):
 1. insert_ops (xs @ ys)
[PROOF STEP]
by (metis append_assoc insert_ops_rem_last)
[PROOF STATE]
proof (state)
this:
insert_ops (xs @ ys)

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>insert_ops (xs @ xsa) \<Longrightarrow> \<exists>A\<subseteq>set (map fst xsa). set (interp_ins (xs @ xsa)) = set (interp_ins xs) \<union> A; insert_ops (xs @ xsa @ [x])\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (xsa @ [x])). set (interp_ins (xs @ xsa @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops (xs @ ys)
[PROOF STEP]
obtain A where IH: "A \<subseteq> set (map fst ys) \<and>
            set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A"
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ ys)

goal (1 subgoal):
 1. (\<And>A. A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ ys)
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. (\<And>A. A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>insert_ops (xs @ xsa) \<Longrightarrow> \<exists>A\<subseteq>set (map fst xsa). set (interp_ins (xs @ xsa)) = set (interp_ins xs) \<union> A; insert_ops (xs @ xsa @ [x])\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (xsa @ [x])). set (interp_ins (xs @ xsa @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A

goal (1 subgoal):
 1. \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
proof(cases "set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
 2. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))

goal (2 subgoals):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
 2. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))

goal (2 subgoals):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
 2. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
have "A \<subseteq> set (map fst (ys @ [x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> set (map fst (ys @ [x]))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A

goal (1 subgoal):
 1. A \<subseteq> set (map fst (ys @ [x]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<subseteq> set (map fst (ys @ [x]))

goal (2 subgoals):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
 2. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))
A \<subseteq> set (map fst (ys @ [x]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))
A \<subseteq> set (map fst (ys @ [x]))

goal (1 subgoal):
 1. \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys))
A \<subseteq> set (map fst (ys @ [x]))
A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A

goal (1 subgoal):
 1. \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A

goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))

goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))
[PROOF STEP]
have "set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) \<union> {fst x}"
[PROOF STATE]
proof (prove)
using this:
set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))

goal (1 subgoal):
 1. set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) \<union> {fst x}
[PROOF STEP]
by (metis append_assoc interp_ins_maybe_grow2 snoc.prems)
[PROOF STATE]
proof (state)
this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) \<union> {fst x}

goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) \<union> {fst x}

goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
have "A \<union> {fst x} \<subseteq> set (map fst (ys @ [x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<union> {fst x} \<subseteq> set (map fst (ys @ [x]))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A

goal (1 subgoal):
 1. A \<union> {fst x} \<subseteq> set (map fst (ys @ [x]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<union> {fst x} \<subseteq> set (map fst (ys @ [x]))

goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A; set (interp_ins (xs @ ys @ [x])) \<noteq> set (interp_ins (xs @ ys))\<rbrakk> \<Longrightarrow> \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) \<union> {fst x}
A \<union> {fst x} \<subseteq> set (map fst (ys @ [x]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) \<union> {fst x}
A \<union> {fst x} \<subseteq> set (map fst (ys @ [x]))

goal (1 subgoal):
 1. \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
using IH Un_assoc
[PROOF STATE]
proof (prove)
using this:
set (interp_ins (xs @ ys @ [x])) = set (interp_ins (xs @ ys)) \<union> {fst x}
A \<union> {fst x} \<subseteq> set (map fst (ys @ [x]))
A \<subseteq> set (map fst ys) \<and> set (interp_ins (xs @ ys)) = set (interp_ins xs) \<union> A
?A \<union> ?B \<union> ?C = ?A \<union> (?B \<union> ?C)

goal (1 subgoal):
 1. \<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>A\<subseteq>set (map fst (ys @ [x])). set (interp_ins (xs @ ys @ [x])) = set (interp_ins xs) \<union> A

goal:
No subgoals!
[PROOF STEP]
qed