[STATEMENT]
lemma spec_ops_exists_base:
  assumes "finite ops"
    and "\<And>oid op1 op2. (oid, op1) \<in> ops \<Longrightarrow> (oid, op2) \<in> ops \<Longrightarrow> op1 = op2"
    and "\<And>oid oper ref. (oid, oper) \<in> ops \<Longrightarrow> ref \<in> deps oper \<Longrightarrow> ref < oid"
  shows "\<exists>op_list. set op_list = ops \<and> spec_ops op_list deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite ops
\<lbrakk>(?oid, ?op1.0) \<in> ops; (?oid, ?op2.0) \<in> ops\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> ops; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
proof(induct ops rule: Finite_Set.finite_induct_select)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> {}; (oid, op2) \<in> {}\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> {}; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = {} \<and> spec_ops op_list deps
 2. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?op1.0) \<in> {}; (?oid, ?op2.0) \<in> {}\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> {}; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (2 subgoals):
 1. \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> {}; (oid, op2) \<in> {}\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> {}; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = {} \<and> spec_ops op_list deps
 2. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?oid, ?op1.0) \<in> {}; (?oid, ?op2.0) \<in> {}\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> {}; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid
[PROOF STEP]
show "\<exists>op_list. set op_list = {} \<and> spec_ops op_list deps"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?oid, ?op1.0) \<in> {}; (?oid, ?op2.0) \<in> {}\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> {}; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. \<exists>op_list. set op_list = {} \<and> spec_ops op_list deps
[PROOF STEP]
by (simp add: spec_ops_empty)
[PROOF STATE]
proof (state)
this:
\<exists>op_list. set op_list = {} \<and> spec_ops op_list deps

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
case (select subset)
[PROOF STATE]
proof (state)
this:
subset \<subset> ops
\<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> subset; (oid, op2) \<in> subset\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> subset; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = subset \<and> spec_ops op_list deps

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subset \<subset> ops
\<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> subset; (oid, op2) \<in> subset\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> subset; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = subset \<and> spec_ops op_list deps
[PROOF STEP]
obtain op_list where "set op_list = subset" and "spec_ops op_list deps"
[PROOF STATE]
proof (prove)
using this:
subset \<subset> ops
\<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> subset; (oid, op2) \<in> subset\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> subset; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = subset \<and> spec_ops op_list deps

goal (1 subgoal):
 1. (\<And>op_list. \<lbrakk>set op_list = subset; spec_ops op_list deps\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subset \<subset> ops
\<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> subset; (oid, op2) \<in> subset\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> subset; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = subset \<and> spec_ops op_list deps
finite ops
\<lbrakk>(?oid, ?op1.0) \<in> ops; (?oid, ?op2.0) \<in> ops\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> ops; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. (\<And>op_list. \<lbrakk>set op_list = subset; spec_ops op_list deps\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set op_list = subset
spec_ops op_list deps

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set op_list = subset
spec_ops op_list deps

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
obtain oid oper where select: "(oid, oper) \<in> ops - subset"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid oper. (oid, oper) \<in> ops - subset \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using select.hyps(1)
[PROOF STATE]
proof (prove)
using this:
subset \<subset> ops

goal (1 subgoal):
 1. (\<And>oid oper. (oid, oper) \<in> ops - subset \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(oid, oper) \<in> ops - subset

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(oid, oper) \<in> ops - subset

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(oid, oper) \<in> ops - subset
[PROOF STEP]
have "\<And>op2. (oid, op2) \<in> ops \<Longrightarrow> op2 = oper"
[PROOF STATE]
proof (prove)
using this:
(oid, oper) \<in> ops - subset

goal (1 subgoal):
 1. \<And>op2. (oid, op2) \<in> ops \<Longrightarrow> op2 = oper
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(oid, oper) \<in> ops - subset
\<lbrakk>(?oid, ?op1.0) \<in> ops; (?oid, ?op2.0) \<in> ops\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0

goal (1 subgoal):
 1. \<And>op2. (oid, op2) \<in> ops \<Longrightarrow> op2 = oper
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(oid, ?op2.0) \<in> ops \<Longrightarrow> ?op2.0 = oper

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
hence "oid \<notin> fst ` subset"
[PROOF STATE]
proof (prove)
using this:
(oid, ?op2.0) \<in> ops \<Longrightarrow> ?op2.0 = oper

goal (1 subgoal):
 1. oid \<notin> fst ` subset
[PROOF STEP]
by (metis (no_types, lifting) DiffD2 select image_iff prod.collapse psubsetD select.hyps(1))
[PROOF STATE]
proof (state)
this:
oid \<notin> fst ` subset

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
oid \<notin> fst ` subset
[PROOF STEP]
obtain pre suf
    where "op_list = pre @ 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 \<notin> fst ` subset

goal (1 subgoal):
 1. (\<And>pre suf. \<lbrakk>op_list = pre @ suf; \<forall>i\<in>set (map fst pre). i < oid; \<forall>i\<in>set (map fst suf). oid < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using spec_ops_split calculation
[PROOF STATE]
proof (prove)
using this:
oid \<notin> fst ` subset
\<lbrakk>spec_ops ?xs ?deps; ?oid \<notin> set (map fst ?xs)\<rbrakk> \<Longrightarrow> \<exists>pre suf. ?xs = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < ?oid) \<and> (\<forall>i\<in>set (map fst suf). ?oid < i)
set op_list = subset
spec_ops op_list deps
(oid, oper) \<in> ops - subset

goal (1 subgoal):
 1. (\<And>pre suf. \<lbrakk>op_list = pre @ suf; \<forall>i\<in>set (map fst pre). i < oid; \<forall>i\<in>set (map fst suf). oid < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) set_map)
[PROOF STATE]
proof (state)
this:
op_list = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op_list = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
have "set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
set op_list = subset
spec_ops op_list deps
(oid, oper) \<in> ops - subset
op_list = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i

goal (1 subgoal):
 1. set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
have "spec_ops (pre @ [(oid, oper)] @ suf) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops (pre @ [(oid, oper)] @ suf) deps
[PROOF STEP]
using calculation spec_ops_add_any assms(3)
[PROOF STATE]
proof (prove)
using this:
set op_list = subset
spec_ops op_list deps
(oid, oper) \<in> ops - subset
op_list = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i
set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset
\<lbrakk>spec_ops (?xs @ ?ys) ?deps; \<forall>i\<in>set (map fst ?xs). i < ?oid; \<forall>i\<in>set (map fst ?ys). ?oid < i; \<forall>ref\<in>?deps ?oper. ref < ?oid\<rbrakk> \<Longrightarrow> spec_ops (?xs @ [(?oid, ?oper)] @ ?ys) ?deps
\<lbrakk>(?oid, ?oper) \<in> ops; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. spec_ops (pre @ [(oid, oper)] @ suf) deps
[PROOF STEP]
by (metis DiffD1)
[PROOF STATE]
proof (state)
this:
spec_ops (pre @ [(oid, oper)] @ suf) deps

goal (1 subgoal):
 1. \<And>T. \<lbrakk>T \<subset> ops; \<lbrakk>\<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> T; (oid, op2) \<in> T\<rbrakk> \<Longrightarrow> op1 = op2; \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> T; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid\<rbrakk> \<Longrightarrow> \<exists>op_list. set op_list = T \<and> spec_ops op_list deps\<rbrakk> \<Longrightarrow> \<exists>s\<in>ops - T. (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> (x, xb) \<in> insert s T \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s T \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s T \<and> spec_ops op_list deps)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set op_list = subset
spec_ops op_list deps
(oid, oper) \<in> ops - subset
op_list = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i
set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset
spec_ops (pre @ [(oid, oper)] @ suf) deps
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set op_list = subset
spec_ops op_list deps
(oid, oper) \<in> ops - subset
op_list = pre @ suf
\<forall>i\<in>set (map fst pre). i < oid
\<forall>i\<in>set (map fst suf). oid < i
set (pre @ [(oid, oper)] @ suf) = insert (oid, oper) subset
spec_ops (pre @ [(oid, oper)] @ suf) deps

goal (1 subgoal):
 1. \<exists>s\<in>ops - subset. (\<forall>x xa xb. (x, xa) \<in> insert s subset \<longrightarrow> (x, xb) \<in> insert s subset \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s subset \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s subset \<and> spec_ops op_list deps)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s\<in>ops - subset. (\<forall>x xa xb. (x, xa) \<in> insert s subset \<longrightarrow> (x, xb) \<in> insert s subset \<longrightarrow> xa = xb) \<longrightarrow> (\<forall>x xa xb. (x, xa) \<in> insert s subset \<longrightarrow> xb \<in> deps xa \<longrightarrow> xb < x) \<longrightarrow> (\<exists>op_list. set op_list = insert s subset \<and> spec_ops op_list deps)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_exists:
  assumes "opset ops deps"
  shows "\<exists>op_list. set op_list = ops \<and> spec_ops op_list deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
have "finite ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ops
[PROOF STEP]
using assms opset.finite_opset
[PROOF STATE]
proof (prove)
using this:
opset ops deps
opset ?opset ?deps \<Longrightarrow> finite ?opset

goal (1 subgoal):
 1. finite ops
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite ops

goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite ops

goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
have "\<And>oid op1 op2. (oid, op1) \<in> ops \<Longrightarrow> (oid, op2) \<in> ops \<Longrightarrow> op1 = op2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> ops; (oid, op2) \<in> ops\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
using assms opset.unique_oid
[PROOF STATE]
proof (prove)
using this:
opset ops deps
\<lbrakk>opset ?opset ?deps; (?oid, ?op1.0) \<in> ?opset; (?oid, ?op2.0) \<in> ?opset\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0

goal (1 subgoal):
 1. \<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> ops; (oid, op2) \<in> ops\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?op1.0) \<in> ops; (?oid, ?op2.0) \<in> ops\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0

goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?op1.0) \<in> ops; (?oid, ?op2.0) \<in> ops\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0

goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
have "\<And>oid oper ref. (oid, oper) \<in> ops \<Longrightarrow> ref \<in> deps oper \<Longrightarrow> ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> ops; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
[PROOF STEP]
using assms opset.ref_older
[PROOF STATE]
proof (prove)
using this:
opset ops deps
\<lbrakk>opset ?opset ?deps; (?oid, ?oper) \<in> ?opset; ?ref \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> ops; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?oper) \<in> ops; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite ops
\<lbrakk>(?oid, ?op1.0) \<in> ops; (?oid, ?op2.0) \<in> ops\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> ops; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid
[PROOF STEP]
show "\<exists>op_list. set op_list = ops \<and> spec_ops op_list deps"
[PROOF STATE]
proof (prove)
using this:
finite ops
\<lbrakk>(?oid, ?op1.0) \<in> ops; (?oid, ?op2.0) \<in> ops\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> ops; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. \<exists>op_list. set op_list = ops \<and> spec_ops op_list deps
[PROOF STEP]
by (simp add: spec_ops_exists_base)
[PROOF STATE]
proof (state)
this:
\<exists>op_list. set op_list = ops \<and> spec_ops op_list deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_oid_unique:
  assumes "spec_ops op_list deps"
    and "(oid, op1) \<in> set op_list"
    and "(oid, op2) \<in> set op_list"
  shows "op1 = op2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
spec_ops op_list deps
(oid, op1) \<in> set op_list
(oid, op2) \<in> set op_list

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
proof(induction op_list, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a op_list. \<lbrakk>\<lbrakk>spec_ops op_list deps; (oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2; spec_ops (a # op_list) deps; (oid, op1) \<in> set (a # op_list); (oid, op2) \<in> set (a # op_list)\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
case (Cons x op_list)
[PROOF STATE]
proof (state)
this:
\<lbrakk>spec_ops op_list deps; (oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2
spec_ops (x # op_list) deps
(oid, op1) \<in> set (x # op_list)
(oid, op2) \<in> set (x # op_list)

goal (1 subgoal):
 1. \<And>a op_list. \<lbrakk>\<lbrakk>spec_ops op_list deps; (oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2; spec_ops (a # op_list) deps; (oid, op1) \<in> set (a # op_list); (oid, op2) \<in> set (a # op_list)\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
have "distinct (map fst (x # op_list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (x # op_list))
[PROOF STEP]
using Cons.prems(1) spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops (x # op_list) deps
spec_ops ?ops ?deps \<equiv> sorted (map fst ?ops) \<and> distinct (map fst ?ops) \<and> (\<forall>oid oper ref. (oid, oper) \<in> set ?ops \<and> ref \<in> ?deps oper \<longrightarrow> ref < oid)

goal (1 subgoal):
 1. distinct (map fst (x # op_list))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map fst (x # op_list))

goal (1 subgoal):
 1. \<And>a op_list. \<lbrakk>\<lbrakk>spec_ops op_list deps; (oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2; spec_ops (a # op_list) deps; (oid, op1) \<in> set (a # op_list); (oid, op2) \<in> set (a # op_list)\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
hence notin: "fst x \<notin> set (map fst op_list)"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (x # op_list))

goal (1 subgoal):
 1. fst x \<notin> set (map fst op_list)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst x \<notin> set (map fst op_list)

goal (1 subgoal):
 1. \<And>a op_list. \<lbrakk>\<lbrakk>spec_ops op_list deps; (oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2; spec_ops (a # op_list) deps; (oid, op1) \<in> set (a # op_list); (oid, op2) \<in> set (a # op_list)\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst x \<notin> set (map fst op_list)
[PROOF STEP]
show "op1 = op2"
[PROOF STATE]
proof (prove)
using this:
fst x \<notin> set (map fst op_list)

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
proof(cases "fst x = oid")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>fst x \<notin> set (map fst op_list); fst x = oid\<rbrakk> \<Longrightarrow> op1 = op2
 2. \<lbrakk>fst x \<notin> set (map fst op_list); fst x \<noteq> oid\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fst x = oid

goal (2 subgoals):
 1. \<lbrakk>fst x \<notin> set (map fst op_list); fst x = oid\<rbrakk> \<Longrightarrow> op1 = op2
 2. \<lbrakk>fst x \<notin> set (map fst op_list); fst x \<noteq> oid\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst x = oid
[PROOF STEP]
show "op1 = op2"
[PROOF STATE]
proof (prove)
using this:
fst x = oid

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
using Cons.prems notin
[PROOF STATE]
proof (prove)
using this:
fst x = oid
spec_ops (x # op_list) deps
(oid, op1) \<in> set (x # op_list)
(oid, op2) \<in> set (x # op_list)
fst x \<notin> set (map fst op_list)

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
by (metis Pair_inject in_set_zipE set_ConsD zip_map_fst_snd)
[PROOF STATE]
proof (state)
this:
op1 = op2

goal (1 subgoal):
 1. \<lbrakk>fst x \<notin> set (map fst op_list); fst x \<noteq> oid\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>fst x \<notin> set (map fst op_list); fst x \<noteq> oid\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst x \<noteq> oid

goal (1 subgoal):
 1. \<lbrakk>fst x \<notin> set (map fst op_list); fst x \<noteq> oid\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst x \<noteq> oid
[PROOF STEP]
have "(oid, op1) \<in> set op_list" and "(oid, op2) \<in> set op_list"
[PROOF STATE]
proof (prove)
using this:
fst x \<noteq> oid

goal (1 subgoal):
 1. (oid, op1) \<in> set op_list &&& (oid, op2) \<in> set op_list
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
fst x \<noteq> oid
spec_ops (x # op_list) deps
(oid, op1) \<in> set (x # op_list)
(oid, op2) \<in> set (x # op_list)

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

goal (1 subgoal):
 1. \<lbrakk>fst x \<notin> set (map fst op_list); fst x \<noteq> oid\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(oid, op1) \<in> set op_list
(oid, op2) \<in> set op_list
[PROOF STEP]
show "op1 = op2"
[PROOF STATE]
proof (prove)
using this:
(oid, op1) \<in> set op_list
(oid, op2) \<in> set op_list

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
using Cons.IH Cons.prems(1) spec_ops_rem_cons
[PROOF STATE]
proof (prove)
using this:
(oid, op1) \<in> set op_list
(oid, op2) \<in> set op_list
\<lbrakk>spec_ops op_list deps; (oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2
spec_ops (x # op_list) deps
spec_ops (?x # ?xs) ?deps \<Longrightarrow> spec_ops ?xs ?deps

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
op1 = op2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
op1 = op2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_is_opset:
  assumes "spec_ops op_list deps"
  shows "opset (set op_list) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
have "\<And>oid op1 op2. (oid, op1) \<in> set op_list \<Longrightarrow> (oid, op2) \<in> set op_list \<Longrightarrow> op1 = op2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
using assms spec_ops_oid_unique
[PROOF STATE]
proof (prove)
using this:
spec_ops op_list deps
\<lbrakk>spec_ops ?op_list ?deps; (?oid, ?op1.0) \<in> set ?op_list; (?oid, ?op2.0) \<in> set ?op_list\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0

goal (1 subgoal):
 1. \<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> set op_list; (oid, op2) \<in> set op_list\<rbrakk> \<Longrightarrow> op1 = op2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?op1.0) \<in> set op_list; (?oid, ?op2.0) \<in> set op_list\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0

goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?op1.0) \<in> set op_list; (?oid, ?op2.0) \<in> set op_list\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0

goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
have "\<And>oid oper ref. (oid, oper) \<in> set op_list \<Longrightarrow> ref \<in> deps oper \<Longrightarrow> ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> set op_list; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
[PROOF STEP]
by (meson assms spec_ops_ref_less)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?oper) \<in> set op_list; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?oid, ?oper) \<in> set op_list; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid

goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
have "finite (set op_list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set op_list)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (set op_list)

goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?oid, ?op1.0) \<in> set op_list; (?oid, ?op2.0) \<in> set op_list\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> set op_list; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid
finite (set op_list)
[PROOF STEP]
show "opset (set op_list) deps"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?oid, ?op1.0) \<in> set op_list; (?oid, ?op2.0) \<in> set op_list\<rbrakk> \<Longrightarrow> ?op1.0 = ?op2.0
\<lbrakk>(?oid, ?oper) \<in> set op_list; ?ref \<in> deps ?oper\<rbrakk> \<Longrightarrow> ?ref < ?oid
finite (set op_list)

goal (1 subgoal):
 1. opset (set op_list) deps
[PROOF STEP]
by (simp add: opset_def)
[PROOF STATE]
proof (state)
this:
opset (set op_list) deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_intro:
  assumes "\<And>r. r \<in> deps oper \<Longrightarrow> r \<in> fst ` set xs \<and> r < oid"
    and "oid \<notin> fst ` set xs"
    and "crdt_ops xs deps"
  shows "crdt_ops (xs @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
using assms crdt_ops.simps
[PROOF STATE]
proof (prove)
using this:
?r \<in> deps oper \<Longrightarrow> ?r \<in> fst ` set xs \<and> ?r < oid
oid \<notin> fst ` set xs
crdt_ops xs deps
crdt_ops ?a1.0 ?a2.0 = ((\<exists>deps. ?a1.0 = [] \<and> ?a2.0 = deps) \<or> (\<exists>xs deps oid oper. ?a1.0 = xs @ [(oid, oper)] \<and> ?a2.0 = deps \<and> crdt_ops xs deps \<and> oid \<notin> set (map fst xs) \<and> (\<forall>ref\<in>deps oper. ref \<in> set (map fst xs) \<and> ref < oid)))

goal (1 subgoal):
 1. crdt_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
by force


[STATEMENT]
lemma crdt_ops_rem_last:
  assumes "crdt_ops (xs @ [x]) deps"
  shows "crdt_ops xs deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops xs deps
[PROOF STEP]
using assms crdt_ops.cases snoc_eq_iff_butlast
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [x]) deps
\<lbrakk>crdt_ops ?a1.0 ?a2.0; \<And>deps. \<lbrakk>?a1.0 = []; ?a2.0 = deps\<rbrakk> \<Longrightarrow> ?P; \<And>xs deps oid oper. \<lbrakk>?a1.0 = xs @ [(oid, oper)]; ?a2.0 = deps; crdt_ops xs deps; oid \<notin> set (map fst xs); \<forall>ref\<in>deps oper. ref \<in> set (map fst xs) \<and> ref < oid\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(?xs @ [?x] = ?ys) = (?ys \<noteq> [] \<and> butlast ?ys = ?xs \<and> last ?ys = ?x)

goal (1 subgoal):
 1. crdt_ops xs deps
[PROOF STEP]
by blast


[STATEMENT]
lemma crdt_ops_ref_less:
  assumes "crdt_ops xs deps"
    and "(oid, oper) \<in> set xs"
    and "r \<in> deps oper"
  shows "r < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r < oid
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps
(oid, oper) \<in> set xs
r \<in> deps oper

goal (1 subgoal):
 1. r < oid
[PROOF STEP]
by (induction rule: crdt_ops.induct, auto)


[STATEMENT]
lemma crdt_ops_ref_less_last:
  assumes "crdt_ops (xs @ [(oid, oper)]) deps"
    and "r \<in> deps oper"
  shows "r < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r < oid
[PROOF STEP]
using assms crdt_ops_ref_less
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)]) deps
r \<in> deps oper
\<lbrakk>crdt_ops ?xs ?deps; (?oid, ?oper) \<in> set ?xs; ?r \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?r < ?oid

goal (1 subgoal):
 1. r < oid
[PROOF STEP]
by fastforce


[STATEMENT]
lemma crdt_ops_distinct_fst:
  assumes "crdt_ops xs deps"
  shows "distinct (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps

goal (1 subgoal):
 1. distinct (map fst xs)
[PROOF STEP]
proof (induction xs rule: List.rev_induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> distinct (map fst xs); crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> distinct (map fst (xs @ [x]))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
crdt_ops xs deps \<Longrightarrow> distinct (map fst xs)
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> distinct (map fst xs); crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> distinct (map fst (xs @ [x]))
[PROOF STEP]
hence "distinct (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps \<Longrightarrow> distinct (map fst xs)
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. distinct (map fst xs)
[PROOF STEP]
using crdt_ops_last
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps \<Longrightarrow> distinct (map fst xs)
crdt_ops (xs @ [x]) deps
\<lbrakk>crdt_ops (?xs @ [?x]) ?deps; \<And>oid oper. \<lbrakk>?x = (oid, oper); crdt_ops ?xs ?deps; oid \<notin> fst ` set ?xs; \<forall>ref\<in>?deps oper. ref \<in> fst ` set ?xs \<and> ref < oid\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. distinct (map fst xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map fst xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> distinct (map fst xs); crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> distinct (map fst (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map fst xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> distinct (map fst xs); crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> distinct (map fst (xs @ [x]))
[PROOF STEP]
have "fst x \<notin> set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst x \<notin> set (map fst xs)
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps \<Longrightarrow> distinct (map fst xs)
crdt_ops (xs @ [x]) deps

goal (1 subgoal):
 1. fst x \<notin> set (map fst xs)
[PROOF STEP]
by (metis crdt_ops_last fstI image_set)
[PROOF STATE]
proof (state)
this:
fst x \<notin> set (map fst xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>crdt_ops xs deps \<Longrightarrow> distinct (map fst xs); crdt_ops (xs @ [x]) deps\<rbrakk> \<Longrightarrow> distinct (map fst (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst xs)
fst x \<notin> set (map fst xs)
[PROOF STEP]
show "distinct (map fst (xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst xs)
fst x \<notin> set (map fst xs)

goal (1 subgoal):
 1. distinct (map fst (xs @ [x]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map fst (xs @ [x]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_distinct:
  assumes "crdt_ops xs deps"
  shows "distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
using assms crdt_ops_distinct_fst distinct_map
[PROOF STATE]
proof (prove)
using this:
crdt_ops xs deps
crdt_ops ?xs ?deps \<Longrightarrow> distinct (map fst ?xs)
distinct (map ?f ?xs) = (distinct ?xs \<and> inj_on ?f (set ?xs))

goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
by blast


[STATEMENT]
lemma crdt_ops_unique_last:
  assumes "crdt_ops (xs @ [(oid, oper)]) deps"
  shows "oid \<notin> set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<notin> set (map fst xs)
[PROOF STEP]
using assms crdt_ops.cases
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)]) deps
\<lbrakk>crdt_ops ?a1.0 ?a2.0; \<And>deps. \<lbrakk>?a1.0 = []; ?a2.0 = deps\<rbrakk> \<Longrightarrow> ?P; \<And>xs deps oid oper. \<lbrakk>?a1.0 = xs @ [(oid, oper)]; ?a2.0 = deps; crdt_ops xs deps; oid \<notin> set (map fst xs); \<forall>ref\<in>deps oper. ref \<in> set (map fst xs) \<and> ref < oid\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. oid \<notin> set (map fst xs)
[PROOF STEP]
by blast


[STATEMENT]
lemma crdt_ops_unique_mid:
  assumes "crdt_ops (xs @ [(oid, oper)] @ ys) deps"
  shows "oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps

goal (1 subgoal):
 1. oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)
[PROOF STEP]
proof(induction ys rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. crdt_ops (xs @ [(oid, oper)] @ []) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst [])
 2. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ [(oid, oper)] @ []) deps

goal (2 subgoals):
 1. crdt_ops (xs @ [(oid, oper)] @ []) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst [])
 2. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
crdt_ops (xs @ [(oid, oper)] @ []) deps
[PROOF STEP]
show "oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst [])"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ []) deps

goal (1 subgoal):
 1. oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst [])
[PROOF STEP]
by (metis crdt_ops_unique_last Nil_is_map_conv append_Nil2 empty_iff empty_set)
[PROOF STATE]
proof (state)
this:
oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst [])

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)
crdt_ops (xs @ [(oid, oper)] @ ys @ [y]) deps

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
obtain yi yr where y_pair: "y = (yi, yr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>yi yr. y = (yi, yr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y = (yi, yr)

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
have IH: "oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)
[PROOF STEP]
using crdt_ops_rem_last snoc
[PROOF STATE]
proof (prove)
using this:
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps
crdt_ops (xs @ [(oid, oper)] @ ys) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)
crdt_ops (xs @ [(oid, oper)] @ ys @ [y]) deps

goal (1 subgoal):
 1. oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)
[PROOF STEP]
by (metis append_assoc)
[PROOF STATE]
proof (state)
this:
oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
have "(xs @ (oid, oper) # ys) @ [(yi, yr)] = xs @ (oid, oper) # ys @ [(yi, yr)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs @ (oid, oper) # ys) @ [(yi, yr)] = xs @ (oid, oper) # ys @ [(yi, yr)]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(xs @ (oid, oper) # ys) @ [(yi, yr)] = xs @ (oid, oper) # ys @ [(yi, yr)]

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
hence "yi \<notin> set (map fst (xs @ (oid, oper) # ys))"
[PROOF STATE]
proof (prove)
using this:
(xs @ (oid, oper) # ys) @ [(yi, yr)] = xs @ (oid, oper) # ys @ [(yi, yr)]

goal (1 subgoal):
 1. yi \<notin> set (map fst (xs @ (oid, oper) # ys))
[PROOF STEP]
using crdt_ops_unique_last
[PROOF STATE]
proof (prove)
using this:
(xs @ (oid, oper) # ys) @ [(yi, yr)] = xs @ (oid, oper) # ys @ [(yi, yr)]
crdt_ops (?xs @ [(?oid, ?oper)]) ?deps \<Longrightarrow> ?oid \<notin> set (map fst ?xs)

goal (1 subgoal):
 1. yi \<notin> set (map fst (xs @ (oid, oper) # ys))
[PROOF STEP]
by (metis append_Cons append_self_conv2 snoc.prems y_pair)
[PROOF STATE]
proof (state)
this:
yi \<notin> set (map fst (xs @ (oid, oper) # ys))

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst xsa); crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps\<rbrakk> \<Longrightarrow> oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (xsa @ [x]))
[PROOF STEP]
thus "oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (ys @ [y]))"
[PROOF STATE]
proof (prove)
using this:
yi \<notin> set (map fst (xs @ (oid, oper) # ys))

goal (1 subgoal):
 1. oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst (ys @ [y]))
[PROOF STEP]
using IH y_pair
[PROOF STATE]
proof (prove)
using this:
yi \<notin> set (map fst (xs @ (oid, oper) # ys))
oid \<notin> set (map fst xs) \<and> oid \<notin> set (map fst ys)
y = (yi, yr)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_ref_exists:
  assumes "crdt_ops (pre @ (oid, oper) # suf) deps"
    and "ref \<in> deps oper"
  shows "ref \<in> fst ` set pre"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ (oid, oper) # suf) deps
ref \<in> deps oper

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
proof(induction suf rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>crdt_ops (pre @ [(oid, oper)]) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
 2. \<And>x xs. \<lbrakk>\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre; crdt_ops (pre @ (oid, oper) # xs @ [x]) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
crdt_ops (pre @ [(oid, oper)]) deps
ref \<in> deps oper

goal (2 subgoals):
 1. \<lbrakk>crdt_ops (pre @ [(oid, oper)]) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
 2. \<And>x xs. \<lbrakk>\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre; crdt_ops (pre @ (oid, oper) # xs @ [x]) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
crdt_ops (pre @ [(oid, oper)]) deps
ref \<in> deps oper

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
by (metis crdt_ops_last prod.sel(2))
[PROOF STATE]
proof (state)
this:
ref \<in> fst ` set pre

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre; crdt_ops (pre @ (oid, oper) # xs @ [x]) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre; crdt_ops (pre @ (oid, oper) # xs @ [x]) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
crdt_ops (pre @ (oid, oper) # xs @ [x]) deps
ref \<in> deps oper

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre; crdt_ops (pre @ (oid, oper) # xs @ [x]) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
crdt_ops (pre @ (oid, oper) # xs @ [x]) deps
ref \<in> deps oper

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
using crdt_ops.cases
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>crdt_ops (pre @ (oid, oper) # xs) deps; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref \<in> fst ` set pre
crdt_ops (pre @ (oid, oper) # xs @ [x]) deps
ref \<in> deps oper
\<lbrakk>crdt_ops ?a1.0 ?a2.0; \<And>deps. \<lbrakk>?a1.0 = []; ?a2.0 = deps\<rbrakk> \<Longrightarrow> ?P; \<And>xs deps oid oper. \<lbrakk>?a1.0 = xs @ [(oid, oper)]; ?a2.0 = deps; crdt_ops xs deps; oid \<notin> set (map fst xs); \<forall>ref\<in>deps oper. ref \<in> set (map fst xs) \<and> ref < oid\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. ref \<in> fst ` set pre
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ref \<in> fst ` set pre

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_no_future_ref:
  assumes "crdt_ops (xs @ [(oid, oper)] @ ys) deps"
  shows "\<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps
[PROOF STEP]
have "\<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<in> set (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<in> set (map fst xs)
[PROOF STEP]
by (simp add: crdt_ops_ref_exists)
[PROOF STATE]
proof (state)
this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<in> set (map fst xs)

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<in> set (map fst xs)

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys
[PROOF STEP]
have "distinct (map fst (xs @ [(oid, oper)] @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (xs @ [(oid, oper)] @ ys))
[PROOF STEP]
using assms crdt_ops_distinct_fst
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps
crdt_ops ?xs ?deps \<Longrightarrow> distinct (map fst ?xs)

goal (1 subgoal):
 1. distinct (map fst (xs @ [(oid, oper)] @ ys))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map fst (xs @ [(oid, oper)] @ ys))

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<in> set (map fst xs)
distinct (map fst (xs @ [(oid, oper)] @ ys))
[PROOF STEP]
have "\<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> set (map fst ([(oid, oper)] @ ys))"
[PROOF STATE]
proof (prove)
using this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<in> set (map fst xs)
distinct (map fst (xs @ [(oid, oper)] @ ys))

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> set (map fst ([(oid, oper)] @ ys))
[PROOF STEP]
using distinct_fst_append
[PROOF STATE]
proof (prove)
using this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<in> set (map fst xs)
distinct (map fst (xs @ [(oid, oper)] @ ys))
\<lbrakk>?x \<in> set (map fst ?xs); distinct (map fst (?xs @ ?ys))\<rbrakk> \<Longrightarrow> ?x \<notin> set (map fst ?ys)

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> set (map fst ([(oid, oper)] @ ys))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<notin> set (map fst ([(oid, oper)] @ ys))

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys
[PROOF STEP]
thus "\<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys"
[PROOF STATE]
proof (prove)
using this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<notin> set (map fst ([(oid, oper)] @ ys))

goal (1 subgoal):
 1. \<And>ref. ref \<in> deps oper \<Longrightarrow> ref \<notin> fst ` set ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?ref \<in> deps oper \<Longrightarrow> ?ref \<notin> fst ` set ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_reorder:
  assumes "crdt_ops (xs @ [(oid, oper)] @ ys) deps"
    and "\<And>op2 r. op2 \<in> snd ` set ys \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r \<noteq> oid"
  shows "crdt_ops (xs @ ys @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps
\<lbrakk>?op2.0 \<in> snd ` set ys; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
proof(induction ys rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ []) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set []; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ [] @ [(oid, oper)]) deps
 2. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ [(oid, oper)] @ []) deps
\<lbrakk>?op2.0 \<in> snd ` set []; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (2 subgoals):
 1. \<lbrakk>crdt_ops (xs @ [(oid, oper)] @ []) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set []; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ [] @ [(oid, oper)]) deps
 2. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
crdt_ops (xs @ [(oid, oper)] @ []) deps
\<lbrakk>?op2.0 \<in> snd ` set []; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid
[PROOF STEP]
show "crdt_ops (xs @ [] @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ []) deps
\<lbrakk>?op2.0 \<in> snd ` set []; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. crdt_ops (xs @ [] @ [(oid, oper)]) deps
[PROOF STEP]
using crdt_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ []) deps
\<lbrakk>?op2.0 \<in> snd ` set []; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps

goal (1 subgoal):
 1. crdt_ops (xs @ [] @ [(oid, oper)]) deps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ [] @ [(oid, oper)]) deps

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ ys) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set ys; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ ys @ [(oid, oper)]) deps
crdt_ops (xs @ [(oid, oper)] @ ys @ [y]) deps
\<lbrakk>?op2.0 \<in> snd ` set (ys @ [y]); ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ ys) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set ys; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ ys @ [(oid, oper)]) deps
crdt_ops (xs @ [(oid, oper)] @ ys @ [y]) deps
\<lbrakk>?op2.0 \<in> snd ` set (ys @ [y]); ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid
[PROOF STEP]
obtain yi yo where y_pair: "y = (yi, yo)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ ys) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set ys; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ ys @ [(oid, oper)]) deps
crdt_ops (xs @ [(oid, oper)] @ ys @ [y]) deps
\<lbrakk>?op2.0 \<in> snd ` set (ys @ [y]); ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

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

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
have IH: "crdt_ops (xs @ ys @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
have "crdt_ops (xs @ [(oid, oper)] @ ys) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ [(oid, oper)] @ ys) deps
[PROOF STEP]
by (metis snoc(2) append.assoc crdt_ops_rem_last)
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
thus "crdt_ops (xs @ ys @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
using snoc.IH snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, oper)] @ ys) deps
\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ ys) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set ys; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ ys @ [(oid, oper)]) deps
\<lbrakk>?op2.0 \<in> snd ` set (ys @ [y]); ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ ys @ [(oid, oper)]) deps

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ ys @ [(oid, oper)]) deps

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
have "crdt_ops (xs @ ys @ [y]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
have "yi \<notin> fst ` set (xs @ [(oid, oper)] @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yi \<notin> fst ` set (xs @ [(oid, oper)] @ ys)
[PROOF STEP]
by (metis y_pair append_assoc crdt_ops_unique_last set_map snoc.prems(1))
[PROOF STATE]
proof (state)
this:
yi \<notin> fst ` set (xs @ [(oid, oper)] @ ys)

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
hence "yi \<notin> fst ` set (xs @ ys)"
[PROOF STATE]
proof (prove)
using this:
yi \<notin> fst ` set (xs @ [(oid, oper)] @ ys)

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

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yi \<notin> fst ` set (xs @ ys)

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
have "\<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
have "\<And>r. r \<in> deps yo \<Longrightarrow> r \<noteq> oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
using snoc.prems(2) y_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?op2.0 \<in> snd ` set (ys @ [y]); ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid
y = (yi, yo)

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
have "\<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ [(oid, oper)] @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ [(oid, oper)] @ ys)
[PROOF STEP]
by (metis y_pair append_assoc snoc.prems(1) crdt_ops_ref_exists)
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ [(oid, oper)] @ ys)

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ [(oid, oper)] @ ys)

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
have "\<And>r. r \<in> deps yo \<Longrightarrow> r < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r < yi
[PROOF STEP]
using crdt_ops_ref_less snoc.prems(1) y_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>crdt_ops ?xs ?deps; (?oid, ?oper) \<in> set ?xs; ?r \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?r < ?oid
crdt_ops (xs @ [(oid, oper)] @ ys @ [y]) deps
y = (yi, yo)

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r < yi
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r < yi

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?r \<in> deps yo \<Longrightarrow> ?r \<noteq> oid
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ [(oid, oper)] @ ys)
?r \<in> deps yo \<Longrightarrow> ?r < yi
[PROOF STEP]
show "\<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi"
[PROOF STATE]
proof (prove)
using this:
?r \<in> deps yo \<Longrightarrow> ?r \<noteq> oid
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ [(oid, oper)] @ ys)
?r \<in> deps yo \<Longrightarrow> ?r < yi

goal (1 subgoal):
 1. \<And>r. r \<in> deps yo \<Longrightarrow> r \<in> fst ` set (xs @ ys) \<and> r < yi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ ys) \<and> ?r < yi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ ys) \<and> ?r < yi

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ ys) \<and> ?r < yi

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
crdt_ops (xs @ ys @ [(oid, oper)]) deps
[PROOF STEP]
have "crdt_ops (xs @ ys) deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ ys @ [(oid, oper)]) deps

goal (1 subgoal):
 1. crdt_ops (xs @ ys) deps
[PROOF STEP]
using crdt_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ ys @ [(oid, oper)]) deps
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps

goal (1 subgoal):
 1. crdt_ops (xs @ ys) deps
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ ys) deps

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
yi \<notin> fst ` set (xs @ ys)
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ ys) \<and> ?r < yi
crdt_ops (xs @ ys) deps
[PROOF STEP]
show "crdt_ops (xs @ ys @ [y]) deps"
[PROOF STATE]
proof (prove)
using this:
yi \<notin> fst ` set (xs @ ys)
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ ys) \<and> ?r < yi
crdt_ops (xs @ ys) deps

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
using y_pair crdt_ops_intro
[PROOF STATE]
proof (prove)
using this:
yi \<notin> fst ` set (xs @ ys)
?r \<in> deps yo \<Longrightarrow> ?r \<in> fst ` set (xs @ ys) \<and> ?r < yi
crdt_ops (xs @ ys) deps
y = (yi, yo)
\<lbrakk>\<And>r. r \<in> ?deps ?oper \<Longrightarrow> r \<in> fst ` set ?xs \<and> r < ?oid; ?oid \<notin> fst ` set ?xs; crdt_ops ?xs ?deps\<rbrakk> \<Longrightarrow> crdt_ops (?xs @ [(?oid, ?oper)]) ?deps

goal (1 subgoal):
 1. crdt_ops (xs @ ys @ [y]) deps
[PROOF STEP]
by (metis append.assoc)
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ ys @ [y]) deps

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ ys @ [y]) deps

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ ys @ [y]) deps

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
have "oid \<notin> fst ` set (xs @ ys @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<notin> fst ` set (xs @ ys @ [y])
[PROOF STEP]
using crdt_ops_unique_mid
[PROOF STATE]
proof (prove)
using this:
crdt_ops (?xs @ [(?oid, ?oper)] @ ?ys) ?deps \<Longrightarrow> ?oid \<notin> set (map fst ?xs) \<and> ?oid \<notin> set (map fst ?ys)

goal (1 subgoal):
 1. oid \<notin> fst ` set (xs @ ys @ [y])
[PROOF STEP]
by (metis (no_types, lifting) UnE image_Un
        image_set set_append snoc.prems(1))
[PROOF STATE]
proof (state)
this:
oid \<notin> fst ` set (xs @ ys @ [y])

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
oid \<notin> fst ` set (xs @ ys @ [y])

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
have "\<And>r. r \<in> deps oper \<Longrightarrow> r \<in> fst ` set (xs @ ys @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> deps oper \<Longrightarrow> r \<in> fst ` set (xs @ ys @ [y])
[PROOF STEP]
using crdt_ops_ref_exists
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>crdt_ops (?pre @ (?oid, ?oper) # ?suf) ?deps; ?ref \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?ref \<in> fst ` set ?pre

goal (1 subgoal):
 1. \<And>r. r \<in> deps oper \<Longrightarrow> r \<in> fst ` set (xs @ ys @ [y])
[PROOF STEP]
by (metis UnCI append_Cons image_Un set_append snoc.prems(1))
[PROOF STATE]
proof (state)
this:
?r \<in> deps oper \<Longrightarrow> ?r \<in> fst ` set (xs @ ys @ [y])

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?r \<in> deps oper \<Longrightarrow> ?r \<in> fst ` set (xs @ ys @ [y])

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
have "\<And>r. r \<in> deps oper \<Longrightarrow> r < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<in> deps oper \<Longrightarrow> r < oid
[PROOF STEP]
using IH crdt_ops_ref_less
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ ys @ [(oid, oper)]) deps
\<lbrakk>crdt_ops ?xs ?deps; (?oid, ?oper) \<in> set ?xs; ?r \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?r < ?oid

goal (1 subgoal):
 1. \<And>r. r \<in> deps oper \<Longrightarrow> r < oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?r \<in> deps oper \<Longrightarrow> ?r < oid

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>crdt_ops (xs @ [(oid, oper)] @ xsa) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xsa; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ xsa @ [(oid, oper)]) deps; crdt_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set (xsa @ [x]); r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid\<rbrakk> \<Longrightarrow> crdt_ops (xs @ (xsa @ [x]) @ [(oid, oper)]) deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
crdt_ops (xs @ ys @ [y]) deps
oid \<notin> fst ` set (xs @ ys @ [y])
?r \<in> deps oper \<Longrightarrow> ?r \<in> fst ` set (xs @ ys @ [y])
?r \<in> deps oper \<Longrightarrow> ?r < oid
[PROOF STEP]
show "crdt_ops (xs @ (ys @ [y]) @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ ys @ [y]) deps
oid \<notin> fst ` set (xs @ ys @ [y])
?r \<in> deps oper \<Longrightarrow> ?r \<in> fst ` set (xs @ ys @ [y])
?r \<in> deps oper \<Longrightarrow> ?r < oid

goal (1 subgoal):
 1. crdt_ops (xs @ (ys @ [y]) @ [(oid, oper)]) deps
[PROOF STEP]
using crdt_ops_intro
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ ys @ [y]) deps
oid \<notin> fst ` set (xs @ ys @ [y])
?r \<in> deps oper \<Longrightarrow> ?r \<in> fst ` set (xs @ ys @ [y])
?r \<in> deps oper \<Longrightarrow> ?r < oid
\<lbrakk>\<And>r. r \<in> ?deps ?oper \<Longrightarrow> r \<in> fst ` set ?xs \<and> r < ?oid; ?oid \<notin> fst ` set ?xs; crdt_ops ?xs ?deps\<rbrakk> \<Longrightarrow> crdt_ops (?xs @ [(?oid, ?oper)]) ?deps

goal (1 subgoal):
 1. crdt_ops (xs @ (ys @ [y]) @ [(oid, oper)]) deps
[PROOF STEP]
by (metis append_assoc)
[PROOF STATE]
proof (state)
this:
crdt_ops (xs @ (ys @ [y]) @ [(oid, oper)]) deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_rem_middle:
  assumes "crdt_ops (xs @ [(oid, ref)] @ ys) deps"
    and "\<And>op2 r. op2 \<in> snd ` set ys \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r \<noteq> oid"
  shows "crdt_ops (xs @ ys) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (xs @ ys) deps
[PROOF STEP]
using assms crdt_ops_rem_last crdt_ops_reorder append_assoc
[PROOF STATE]
proof (prove)
using this:
crdt_ops (xs @ [(oid, ref)] @ ys) deps
\<lbrakk>?op2.0 \<in> snd ` set ys; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps
\<lbrakk>crdt_ops (?xs @ [(?oid, ?oper)] @ ?ys) ?deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set ?ys; r \<in> ?deps op2\<rbrakk> \<Longrightarrow> r \<noteq> ?oid\<rbrakk> \<Longrightarrow> crdt_ops (?xs @ ?ys @ [(?oid, ?oper)]) ?deps
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs

goal (1 subgoal):
 1. crdt_ops (xs @ ys) deps
[PROOF STEP]
by metis


[STATEMENT]
lemma crdt_ops_independent_suf:
  assumes "spec_ops (xs @ [(oid, oper)]) deps"
    and "crdt_ops (ys @ [(oid, oper)] @ zs) deps"
    and "set (xs @ [(oid, oper)]) = set (ys @ [(oid, oper)] @ zs)"
  shows "\<And>op2 r. op2 \<in> snd ` set zs \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r \<noteq> oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
have "\<And>op2 r. op2 \<in> snd ` set xs \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < oid
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < oid
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
have "\<And>i. i \<in> fst ` set xs \<Longrightarrow> i < oid"
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)]) deps

goal (1 subgoal):
 1. \<And>i. i \<in> fst ` set xs \<Longrightarrow> i < oid
[PROOF STEP]
using spec_ops_id_inc
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)]) deps
\<lbrakk>spec_ops (?xs @ [(?oid, ?oper)]) ?deps; ?x \<in> set (map fst ?xs)\<rbrakk> \<Longrightarrow> ?x < ?oid

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

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < oid
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i \<in> fst ` set xs \<Longrightarrow> ?i < oid

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < oid
[PROOF STEP]
have "\<And>i2 op2 r. (i2, op2) \<in> set xs \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r < i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i2 op2 r. \<lbrakk>(i2, op2) \<in> set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < i2
[PROOF STEP]
using assms(1) spec_ops_ref_less spec_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)]) deps
\<lbrakk>spec_ops ?xs ?deps; (?oid, ?oper) \<in> set ?xs; ?r \<in> ?deps ?oper\<rbrakk> \<Longrightarrow> ?r < ?oid
spec_ops (?xs @ [?x]) ?deps \<Longrightarrow> spec_ops ?xs ?deps

goal (1 subgoal):
 1. \<And>i2 op2 r. \<lbrakk>(i2, op2) \<in> set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < i2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?i2.0, ?op2.0) \<in> set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < ?i2.0

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < oid
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i \<in> fst ` set xs \<Longrightarrow> ?i < oid
\<lbrakk>(?i2.0, ?op2.0) \<in> set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < ?i2.0
[PROOF STEP]
show "\<And>op2 r. op2 \<in> snd ` set xs \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r < oid"
[PROOF STATE]
proof (prove)
using this:
?i \<in> fst ` set xs \<Longrightarrow> ?i < oid
\<lbrakk>(?i2.0, ?op2.0) \<in> set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < ?i2.0

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set xs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r < oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op2.0 \<in> snd ` set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < oid

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op2.0 \<in> snd ` set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < oid

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op2.0 \<in> snd ` set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < oid

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
have "set zs \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set zs \<subseteq> set xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set zs \<subseteq> set xs
[PROOF STEP]
have "distinct (xs @ [(oid, oper)])" and "distinct (ys @ [(oid, oper)] @ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (xs @ [(oid, oper)]) &&& distinct (ys @ [(oid, oper)] @ zs)
[PROOF STEP]
using assms spec_ops_distinct crdt_ops_distinct
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)]) deps
crdt_ops (ys @ [(oid, oper)] @ zs) deps
set (xs @ [(oid, oper)]) = set (ys @ [(oid, oper)] @ zs)
spec_ops ?ops ?deps \<Longrightarrow> distinct ?ops
crdt_ops ?xs ?deps \<Longrightarrow> distinct ?xs

goal (1 subgoal):
 1. distinct (xs @ [(oid, oper)]) &&& distinct (ys @ [(oid, oper)] @ zs)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
distinct (xs @ [(oid, oper)])
distinct (ys @ [(oid, oper)] @ zs)

goal (1 subgoal):
 1. set zs \<subseteq> set xs
[PROOF STEP]
hence "set xs = set (ys @ zs)"
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ [(oid, oper)])
distinct (ys @ [(oid, oper)] @ zs)

goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
by (meson append_set_rem_last assms(3))
[PROOF STATE]
proof (state)
this:
set xs = set (ys @ zs)

goal (1 subgoal):
 1. set zs \<subseteq> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set xs = set (ys @ zs)
[PROOF STEP]
show "set zs \<subseteq> set xs"
[PROOF STATE]
proof (prove)
using this:
set xs = set (ys @ zs)

goal (1 subgoal):
 1. set zs \<subseteq> set xs
[PROOF STEP]
using append_subset(2)
[PROOF STATE]
proof (prove)
using this:
set xs = set (ys @ zs)
set ?xs = set (?ys @ ?zs) \<Longrightarrow> set ?zs \<subseteq> set ?xs

goal (1 subgoal):
 1. set zs \<subseteq> set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set zs \<subseteq> set xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set zs \<subseteq> set xs

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?op2.0 \<in> snd ` set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < oid
set zs \<subseteq> set xs
[PROOF STEP]
show "\<And>op2 r. op2 \<in> snd ` set zs \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r \<noteq> oid"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?op2.0 \<in> snd ` set xs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r < oid
set zs \<subseteq> set xs

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op2.0 \<in> snd ` set zs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_reorder_spec:
  assumes "spec_ops (xs @ [x]) deps"
    and "crdt_ops (ys @ [x] @ zs) deps"
    and "set (xs @ [x]) = set (ys @ [x] @ zs)"
  shows "crdt_ops (ys @ zs @ [x]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (ys @ zs @ [x]) deps
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [x]) deps
crdt_ops (ys @ [x] @ zs) deps
set (xs @ [x]) = set (ys @ [x] @ zs)

goal (1 subgoal):
 1. crdt_ops (ys @ zs @ [x]) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>spec_ops (xs @ [x]) deps; crdt_ops (ys @ [x] @ zs) deps; set (xs @ [x]) = set (ys @ [x] @ zs)\<rbrakk> \<Longrightarrow> crdt_ops (ys @ zs @ [x]) deps
[PROOF STEP]
obtain oid oper where x_pair: "x = (oid, oper)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid oper. x = (oid, oper) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (oid, oper)

goal (1 subgoal):
 1. \<lbrakk>spec_ops (xs @ [x]) deps; crdt_ops (ys @ [x] @ zs) deps; set (xs @ [x]) = set (ys @ [x] @ zs)\<rbrakk> \<Longrightarrow> crdt_ops (ys @ zs @ [x]) deps
[PROOF STEP]
hence "\<And>op2 r. op2 \<in> snd ` set zs \<Longrightarrow> r \<in> deps op2 \<Longrightarrow> r \<noteq> oid"
[PROOF STATE]
proof (prove)
using this:
x = (oid, oper)

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
using assms crdt_ops_independent_suf
[PROOF STATE]
proof (prove)
using this:
x = (oid, oper)
spec_ops (xs @ [x]) deps
crdt_ops (ys @ [x] @ zs) deps
set (xs @ [x]) = set (ys @ [x] @ zs)
\<lbrakk>spec_ops (?xs @ [(?oid, ?oper)]) ?deps; crdt_ops (?ys @ [(?oid, ?oper)] @ ?zs) ?deps; set (?xs @ [(?oid, ?oper)]) = set (?ys @ [(?oid, ?oper)] @ ?zs); ?op2.0 \<in> snd ` set ?zs; ?r \<in> ?deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> ?oid

goal (1 subgoal):
 1. \<And>op2 r. \<lbrakk>op2 \<in> snd ` set zs; r \<in> deps op2\<rbrakk> \<Longrightarrow> r \<noteq> oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op2.0 \<in> snd ` set zs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. \<lbrakk>spec_ops (xs @ [x]) deps; crdt_ops (ys @ [x] @ zs) deps; set (xs @ [x]) = set (ys @ [x] @ zs)\<rbrakk> \<Longrightarrow> crdt_ops (ys @ zs @ [x]) deps
[PROOF STEP]
thus "crdt_ops (ys @ zs @ [x]) deps"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?op2.0 \<in> snd ` set zs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid

goal (1 subgoal):
 1. crdt_ops (ys @ zs @ [x]) deps
[PROOF STEP]
using assms(2) crdt_ops_reorder x_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?op2.0 \<in> snd ` set zs; ?r \<in> deps ?op2.0\<rbrakk> \<Longrightarrow> ?r \<noteq> oid
crdt_ops (ys @ [x] @ zs) deps
\<lbrakk>crdt_ops (?xs @ [(?oid, ?oper)] @ ?ys) ?deps; \<And>op2 r. \<lbrakk>op2 \<in> snd ` set ?ys; r \<in> ?deps op2\<rbrakk> \<Longrightarrow> r \<noteq> ?oid\<rbrakk> \<Longrightarrow> crdt_ops (?xs @ ?ys @ [(?oid, ?oper)]) ?deps
x = (oid, oper)

goal (1 subgoal):
 1. crdt_ops (ys @ zs @ [x]) deps
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
crdt_ops (ys @ zs @ [x]) deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crdt_ops_rem_spec:
  assumes "spec_ops (xs @ [x]) deps"
    and "crdt_ops (ys @ [x] @ zs) deps"
    and "set (xs @ [x]) = set (ys @ [x] @ zs)"
  shows "crdt_ops (ys @ zs) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crdt_ops (ys @ zs) deps
[PROOF STEP]
using assms crdt_ops_rem_last crdt_ops_reorder_spec append_assoc
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [x]) deps
crdt_ops (ys @ [x] @ zs) deps
set (xs @ [x]) = set (ys @ [x] @ zs)
crdt_ops (?xs @ [?x]) ?deps \<Longrightarrow> crdt_ops ?xs ?deps
\<lbrakk>spec_ops (?xs @ [?x]) ?deps; crdt_ops (?ys @ [?x] @ ?zs) ?deps; set (?xs @ [?x]) = set (?ys @ [?x] @ ?zs)\<rbrakk> \<Longrightarrow> crdt_ops (?ys @ ?zs @ [?x]) ?deps
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs

goal (1 subgoal):
 1. crdt_ops (ys @ zs) deps
[PROOF STEP]
by metis