[STATEMENT]
lemma card_multiset_only_sets':
  assumes "finite A"
  shows "card {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = card A choose k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = card A choose k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = card A choose k
[PROOF STEP]
from \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} =
    {M. M \<subseteq># mset_set A \<and> size M = k}"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
using msubset_mset_set_iff
[PROOF STATE]
proof (prove)
using this:
finite A
finite ?A \<Longrightarrow> (set_mset ?M \<subseteq> ?A \<and> (\<forall>x. count ?M x \<le> 1)) = (?M \<subseteq># mset_set ?A)

goal (1 subgoal):
 1. {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = {M. M \<subseteq># mset_set A \<and> size M = k}

goal (1 subgoal):
 1. card {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = card A choose k
[PROOF STEP]
from this \<open>finite A\<close> card_multiset_only_sets
[PROOF STATE]
proof (chain)
picking this:
{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = {M. M \<subseteq># mset_set A \<and> size M = k}
finite A
finite ?A \<Longrightarrow> card {M. M \<subseteq># mset_set ?A \<and> size M = ?k} = card ?A choose ?k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = {M. M \<subseteq># mset_set A \<and> size M = k}
finite A
finite ?A \<Longrightarrow> card {M. M \<subseteq># mset_set ?A \<and> size M = ?k} = card ?A choose ?k

goal (1 subgoal):
 1. card {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = card A choose k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} = card A choose k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma opset_subset:
  assumes "opset Y deps"
    and "X \<subseteq> Y"
  shows "opset X deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opset X deps
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> X; (oid, op2) \<in> X\<rbrakk> \<Longrightarrow> op1 = op2
 2. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> X; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
 3. finite X
[PROOF STEP]
fix oid op1 op2
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> X; (oid, op2) \<in> X\<rbrakk> \<Longrightarrow> op1 = op2
 2. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> X; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
 3. finite X
[PROOF STEP]
assume "(oid, op1) \<in> X" and "(oid, op2) \<in> X"
[PROOF STATE]
proof (state)
this:
(oid, op1) \<in> X
(oid, op2) \<in> X

goal (3 subgoals):
 1. \<And>oid op1 op2. \<lbrakk>(oid, op1) \<in> X; (oid, op2) \<in> X\<rbrakk> \<Longrightarrow> op1 = op2
 2. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> X; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
 3. finite X
[PROOF STEP]
thus "op1 = op2"
[PROOF STATE]
proof (prove)
using this:
(oid, op1) \<in> X
(oid, op2) \<in> X

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(oid, op1) \<in> X
(oid, op2) \<in> X
opset Y deps
X \<subseteq> Y

goal (1 subgoal):
 1. op1 = op2
[PROOF STEP]
by (meson opset.unique_oid subsetD)
[PROOF STATE]
proof (state)
this:
op1 = op2

goal (2 subgoals):
 1. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> X; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
 2. finite X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> X; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
 2. finite X
[PROOF STEP]
fix oid oper ref
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> X; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
 2. finite X
[PROOF STEP]
assume "(oid, oper) \<in> X" and "ref \<in> deps oper"
[PROOF STATE]
proof (state)
this:
(oid, oper) \<in> X
ref \<in> deps oper

goal (2 subgoals):
 1. \<And>oid oper ref. \<lbrakk>(oid, oper) \<in> X; ref \<in> deps oper\<rbrakk> \<Longrightarrow> ref < oid
 2. finite X
[PROOF STEP]
thus "ref < oid"
[PROOF STATE]
proof (prove)
using this:
(oid, oper) \<in> X
ref \<in> deps oper

goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(oid, oper) \<in> X
ref \<in> deps oper
opset Y deps
X \<subseteq> Y

goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
by (meson opset.ref_older rev_subsetD)
[PROOF STATE]
proof (state)
this:
ref < oid

goal (1 subgoal):
 1. finite X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite X
[PROOF STEP]
show "finite X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X
[PROOF STEP]
using assms opset.finite_opset finite_subset
[PROOF STATE]
proof (prove)
using this:
opset Y deps
X \<subseteq> Y
opset ?opset ?deps \<Longrightarrow> finite ?opset
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma opset_insert:
  assumes "opset (insert x ops) deps"
  shows "opset ops deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opset ops deps
[PROOF STEP]
using assms opset_subset
[PROOF STATE]
proof (prove)
using this:
opset (insert x ops) deps
\<lbrakk>opset ?Y ?deps; ?X \<subseteq> ?Y\<rbrakk> \<Longrightarrow> opset ?X ?deps

goal (1 subgoal):
 1. opset ops deps
[PROOF STEP]
by blast


[STATEMENT]
lemma opset_sublist:
  assumes "opset (set (xs @ ys @ zs)) deps"
  shows "opset (set (xs @ zs)) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opset (set (xs @ zs)) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. opset (set (xs @ zs)) deps
[PROOF STEP]
have "set (xs @ zs) \<subseteq> set (xs @ ys @ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs @ zs) \<subseteq> set (xs @ ys @ zs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (xs @ zs) \<subseteq> set (xs @ ys @ zs)

goal (1 subgoal):
 1. opset (set (xs @ zs)) deps
[PROOF STEP]
thus "opset (set (xs @ zs)) deps"
[PROOF STATE]
proof (prove)
using this:
set (xs @ zs) \<subseteq> set (xs @ ys @ zs)

goal (1 subgoal):
 1. opset (set (xs @ zs)) deps
[PROOF STEP]
using assms opset_subset
[PROOF STATE]
proof (prove)
using this:
set (xs @ zs) \<subseteq> set (xs @ ys @ zs)
opset (set (xs @ ys @ zs)) deps
\<lbrakk>opset ?Y ?deps; ?X \<subseteq> ?Y\<rbrakk> \<Longrightarrow> opset ?X ?deps

goal (1 subgoal):
 1. opset (set (xs @ zs)) deps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
opset (set (xs @ zs)) deps

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. distinct (xs @ ys)
[PROOF STEP]
by (induction ys rule: rev_induct, simp_all)


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

goal (1 subgoal):
 1. x \<notin> set (map fst ys)
[PROOF STEP]
by (induction ys, force+)


[STATEMENT]
lemma distinct_set_remove_last:
  assumes "distinct (xs @ [x])"
  shows "set xs = set (xs @ [x]) - {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs = set (xs @ [x]) - {x}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ [x])

goal (1 subgoal):
 1. set xs = set (xs @ [x]) - {x}
[PROOF STEP]
by force


[STATEMENT]
lemma distinct_set_remove_mid:
  assumes "distinct (xs @ [x] @ ys)"
  shows "set (xs @ ys) = set (xs @ [x] @ ys) - {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs @ ys) = set (xs @ [x] @ ys) - {x}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ [x] @ ys)

goal (1 subgoal):
 1. set (xs @ ys) = set (xs @ [x] @ ys) - {x}
[PROOF STEP]
by force


[STATEMENT]
lemma distinct_list_split:
  assumes "distinct xs"
    and "xs = xa @ x # ya"
    and "xs = xb @ x # yb"
  shows "xa = xb \<and> ya = yb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa = xb \<and> ya = yb
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct xs
xs = xa @ x # ya
xs = xb @ x # yb

goal (1 subgoal):
 1. xa = xb \<and> ya = yb
[PROOF STEP]
proof(induction xs arbitrary: xa xb x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa xb x. \<lbrakk>distinct []; [] = xa @ x # ya; [] = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
 2. \<And>a xs xa xb x. \<lbrakk>\<And>xa xb x. \<lbrakk>distinct xs; xs = xa @ x # ya; xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb; distinct (a # xs); a # xs = xa @ x # ya; a # xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
[PROOF STEP]
fix xa xb x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa xb x. \<lbrakk>distinct []; [] = xa @ x # ya; [] = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
 2. \<And>a xs xa xb x. \<lbrakk>\<And>xa xb x. \<lbrakk>distinct xs; xs = xa @ x # ya; xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb; distinct (a # xs); a # xs = xa @ x # ya; a # xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
[PROOF STEP]
assume "[] = xa @ x # ya"
[PROOF STATE]
proof (state)
this:
[] = xa @ x # ya

goal (2 subgoals):
 1. \<And>xa xb x. \<lbrakk>distinct []; [] = xa @ x # ya; [] = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
 2. \<And>a xs xa xb x. \<lbrakk>\<And>xa xb x. \<lbrakk>distinct xs; xs = xa @ x # ya; xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb; distinct (a # xs); a # xs = xa @ x # ya; a # xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
[PROOF STEP]
thus "xa = xb \<and> ya = yb"
[PROOF STATE]
proof (prove)
using this:
[] = xa @ x # ya

goal (1 subgoal):
 1. xa = xb \<and> ya = yb
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xa = xb \<and> ya = yb

goal (1 subgoal):
 1. \<And>a xs xa xb x. \<lbrakk>\<And>xa xb x. \<lbrakk>distinct xs; xs = xa @ x # ya; xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb; distinct (a # xs); a # xs = xa @ x # ya; a # xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs xa xb x. \<lbrakk>\<And>xa xb x. \<lbrakk>distinct xs; xs = xa @ x # ya; xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb; distinct (a # xs); a # xs = xa @ x # ya; a # xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
[PROOF STEP]
fix a xs xa xb x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs xa xb x. \<lbrakk>\<And>xa xb x. \<lbrakk>distinct xs; xs = xa @ x # ya; xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb; distinct (a # xs); a # xs = xa @ x # ya; a # xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
[PROOF STEP]
assume IH: "\<And>xa xb x. distinct xs \<Longrightarrow> xs = xa @ x # ya \<Longrightarrow> xs = xb @ x # yb \<Longrightarrow> xa = xb \<and> ya = yb"
    and "distinct (a # xs)" and "a # xs = xa @ x # ya" and "a # xs = xb @ x # yb"
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct xs; xs = ?xa @ ?x # ya; xs = ?xb @ ?x # yb\<rbrakk> \<Longrightarrow> ?xa = ?xb \<and> ya = yb
distinct (a # xs)
a # xs = xa @ x # ya
a # xs = xb @ x # yb

goal (1 subgoal):
 1. \<And>a xs xa xb x. \<lbrakk>\<And>xa xb x. \<lbrakk>distinct xs; xs = xa @ x # ya; xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb; distinct (a # xs); a # xs = xa @ x # ya; a # xs = xb @ x # yb\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb
[PROOF STEP]
thus "xa = xb \<and> ya = yb"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct xs; xs = ?xa @ ?x # ya; xs = ?xb @ ?x # yb\<rbrakk> \<Longrightarrow> ?xa = ?xb \<and> ya = yb
distinct (a # xs)
a # xs = xa @ x # ya
a # xs = xb @ x # yb

goal (1 subgoal):
 1. xa = xb \<and> ya = yb
[PROOF STEP]
by(case_tac xa; case_tac xb) auto
[PROOF STATE]
proof (state)
this:
xa = xb \<and> ya = yb

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. distinct (ys @ xs)
[PROOF STEP]
by (induction ys, auto)


[STATEMENT]
lemma append_subset:
  assumes "set xs = set (ys @ zs)"
  shows "set ys \<subseteq> set xs" and "set zs \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys \<subseteq> set xs &&& set zs \<subseteq> set xs
[PROOF STEP]
by (metis Un_iff assms set_append subsetI)+


[STATEMENT]
lemma append_set_rem_last:
  assumes "set (xs @ [x]) = set (ys @ [x] @ zs)"
    and "distinct (xs @ [x])" and "distinct (ys @ [x] @ zs)"
  shows "set xs = set (ys @ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
have "distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
using assms distinct_append
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set (ys @ [x] @ zs)
distinct (xs @ [x])
distinct (ys @ [x] @ zs)
distinct (?xs @ ?ys) = (distinct ?xs \<and> distinct ?ys \<and> set ?xs \<inter> set ?ys = {})

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

goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct xs

goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
distinct xs
[PROOF STEP]
have "set xs = set (xs @ [x]) - {x}"
[PROOF STATE]
proof (prove)
using this:
distinct xs

goal (1 subgoal):
 1. set xs = set (xs @ [x]) - {x}
[PROOF STEP]
by (meson assms distinct_set_remove_last)
[PROOF STATE]
proof (state)
this:
set xs = set (xs @ [x]) - {x}

goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set xs = set (xs @ [x]) - {x}

goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
have "distinct (ys @ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (ys @ zs)
[PROOF STEP]
using assms distinct_rem_mid
[PROOF STATE]
proof (prove)
using this:
set (xs @ [x]) = set (ys @ [x] @ zs)
distinct (xs @ [x])
distinct (ys @ [x] @ zs)
distinct (?xs @ [?x] @ ?ys) \<Longrightarrow> distinct (?xs @ ?ys)

goal (1 subgoal):
 1. distinct (ys @ zs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (ys @ zs)

goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct xs
set xs = set (xs @ [x]) - {x}
distinct (ys @ zs)
[PROOF STEP]
show "set xs = set (ys @ zs)"
[PROOF STATE]
proof (prove)
using this:
distinct xs
set xs = set (xs @ [x]) - {x}
distinct (ys @ zs)

goal (1 subgoal):
 1. set xs = set (ys @ zs)
[PROOF STEP]
using assms distinct_set_remove_mid
[PROOF STATE]
proof (prove)
using this:
distinct xs
set xs = set (xs @ [x]) - {x}
distinct (ys @ zs)
set (xs @ [x]) = set (ys @ [x] @ zs)
distinct (xs @ [x])
distinct (ys @ [x] @ zs)
distinct (?xs @ [?x] @ ?ys) \<Longrightarrow> set (?xs @ ?ys) = set (?xs @ [?x] @ ?ys) - {?x}

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
proof(cases "a = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct (map fst (remove1 x xs)); a = x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
 2. \<lbrakk>distinct (map fst (remove1 x xs)); a \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = x

goal (2 subgoals):
 1. \<lbrakk>distinct (map fst (remove1 x xs)); a = x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
 2. \<lbrakk>distinct (map fst (remove1 x xs)); a \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = x

goal (1 subgoal):
 1. distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
a = x
distinct (map fst (a # xs))

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

goal (1 subgoal):
 1. \<lbrakk>distinct (map fst (remove1 x xs)); a \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst (remove1 x xs)); a \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> x

goal (1 subgoal):
 1. \<lbrakk>distinct (map fst (remove1 x xs)); a \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<noteq> x

goal (1 subgoal):
 1. \<lbrakk>distinct (map fst (remove1 x xs)); a \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
have "fst a \<notin> fst ` set (remove1 x xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst a \<notin> fst ` set (remove1 x xs)
[PROOF STEP]
by (metis (no_types, lifting) Cons.prems distinct.simps(2) image_iff
          list.simps(9) notin_set_remove1 set_map)
[PROOF STATE]
proof (state)
this:
fst a \<notin> fst ` set (remove1 x xs)

goal (1 subgoal):
 1. \<lbrakk>distinct (map fst (remove1 x xs)); a \<noteq> x\<rbrakk> \<Longrightarrow> distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> x
fst a \<notin> fst ` set (remove1 x xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x
fst a \<notin> fst ` set (remove1 x xs)

goal (1 subgoal):
 1. distinct (map fst (remove1 x (a # xs)))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
a \<noteq> x
fst a \<notin> fst ` set (remove1 x xs)
distinct (map fst (remove1 x xs))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (map fst (remove1 x (a # xs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_empty:
  shows "spec_ops [] deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops [] deps
[PROOF STEP]
by (simp add: spec_ops_def)


[STATEMENT]
lemma spec_ops_distinct:
  assumes "spec_ops ops deps"
  shows "distinct ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct ops
[PROOF STEP]
using assms distinct_map spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops ops deps
distinct (map ?f ?xs) = (distinct ?xs \<and> inj_on ?f (set ?xs))
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 ops
[PROOF STEP]
by blast


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

goal (1 subgoal):
 1. distinct (map fst ops)
[PROOF STEP]
by (simp add: spec_ops_def)


[STATEMENT]
lemma spec_ops_sorted:
  assumes "spec_ops ops deps"
  shows "sorted (map fst ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map fst ops)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
spec_ops ops deps

goal (1 subgoal):
 1. sorted (map fst ops)
[PROOF STEP]
by (simp add: spec_ops_def)


[STATEMENT]
lemma spec_ops_rem_cons:
  assumes "spec_ops (x # xs) deps"
  shows "spec_ops xs deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
have "sorted (map fst (x # xs))" and "distinct (map fst (x # xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map fst (x # xs)) &&& distinct (map fst (x # xs))
[PROOF STEP]
using assms spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops (x # xs) 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. sorted (map fst (x # xs)) &&& distinct (map fst (x # xs))
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
sorted (map fst (x # xs))
distinct (map fst (x # xs))

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (map fst (x # xs))
distinct (map fst (x # xs))

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
sorted (map fst (x # xs))
distinct (map fst (x # xs))
[PROOF STEP]
have "sorted (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (x # xs))
distinct (map fst (x # xs))

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

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (map fst xs)

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
have "\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid
[PROOF STEP]
by (meson assms set_subset_Cons spec_ops_def subsetCE)
[PROOF STATE]
proof (state)
this:
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted (map fst (x # xs))
distinct (map fst (x # xs))
sorted (map fst xs)
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid
[PROOF STEP]
show "spec_ops xs deps"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (x # xs))
distinct (map fst (x # xs))
sorted (map fst xs)
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
by (simp add: spec_ops_def)
[PROOF STATE]
proof (state)
this:
spec_ops xs deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_rem_last:
  assumes "spec_ops (xs @ [x]) deps"
  shows "spec_ops xs deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
have "sorted (map fst (xs @ [x]))" and "distinct (map fst (xs @ [x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map fst (xs @ [x])) &&& distinct (map fst (xs @ [x]))
[PROOF STEP]
using assms spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [x]) 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. sorted (map fst (xs @ [x])) &&& distinct (map fst (xs @ [x]))
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
sorted (map fst (xs @ [x]))
distinct (map fst (xs @ [x]))

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (map fst (xs @ [x]))
distinct (map fst (xs @ [x]))

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
sorted (map fst (xs @ [x]))
distinct (map fst (xs @ [x]))
[PROOF STEP]
have "sorted (map fst xs)" and "distinct xs"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (xs @ [x]))
distinct (map fst (xs @ [x]))

goal (1 subgoal):
 1. sorted (map fst xs) &&& distinct xs
[PROOF STEP]
by (auto simp add: sorted_append distinct_butlast distinct_map)
[PROOF STATE]
proof (state)
this:
sorted (map fst xs)
distinct xs

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (map fst xs)
distinct xs

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
have "\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid
[PROOF STEP]
by (metis assms butlast_snoc in_set_butlastD spec_ops_def)
[PROOF STATE]
proof (state)
this:
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted (map fst (xs @ [x]))
distinct (map fst (xs @ [x]))
sorted (map fst xs)
distinct xs
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid
[PROOF STEP]
show "spec_ops xs deps"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (xs @ [x]))
distinct (map fst (xs @ [x]))
sorted (map fst xs)
distinct xs
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid

goal (1 subgoal):
 1. spec_ops xs deps
[PROOF STEP]
by (simp add: spec_ops_def)
[PROOF STATE]
proof (state)
this:
spec_ops xs deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_remove1:
  assumes "spec_ops xs deps"
  shows "spec_ops (remove1 x xs) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops (remove1 x xs) deps
[PROOF STEP]
using assms distinct_map_fst_remove1 spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops xs deps
distinct (map fst ?xs) \<Longrightarrow> distinct (map fst (remove1 ?x ?xs))
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. spec_ops (remove1 x xs) deps
[PROOF STEP]
by (metis notin_set_remove1 sorted_map_remove1 spec_ops_def)


[STATEMENT]
lemma spec_ops_ref_less:
  assumes "spec_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 spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops xs deps
(oid, oper) \<in> set xs
r \<in> deps oper
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. r < oid
[PROOF STEP]
by force


[STATEMENT]
lemma spec_ops_ref_less_last:
  assumes "spec_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 spec_ops_ref_less
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)]) deps
r \<in> deps oper
\<lbrakk>spec_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 spec_ops_id_inc:
  assumes "spec_ops (xs @ [(oid, oper)]) deps"
    and "x \<in> set (map fst xs)"
  shows "x < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < oid
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x < oid
[PROOF STEP]
have "sorted ((map fst xs) @ (map fst [(oid, oper)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map fst xs @ map fst [(oid, oper)])
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)]) deps

goal (1 subgoal):
 1. sorted (map fst xs @ map fst [(oid, oper)])
[PROOF STEP]
by (simp add: spec_ops_def)
[PROOF STATE]
proof (state)
this:
sorted (map fst xs @ map fst [(oid, oper)])

goal (1 subgoal):
 1. x < oid
[PROOF STEP]
hence "\<forall>i \<in> set (map fst xs). i \<le> oid"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst xs @ map fst [(oid, oper)])

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

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

goal (1 subgoal):
 1. x < oid
[PROOF STEP]
have "distinct ((map fst xs) @ (map fst [(oid, oper)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs @ map fst [(oid, oper)])
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)]) deps

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

goal (1 subgoal):
 1. x < oid
[PROOF STEP]
hence "\<forall>i \<in> set (map fst xs). i \<noteq> oid"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst xs @ map fst [(oid, oper)])

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

goal (1 subgoal):
 1. x < oid
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>set (map fst xs). i \<le> oid
\<forall>i\<in>set (map fst xs). i \<noteq> oid
[PROOF STEP]
show "x < oid"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (map fst xs). i \<le> oid
\<forall>i\<in>set (map fst xs). i \<noteq> oid

goal (1 subgoal):
 1. x < oid
[PROOF STEP]
using assms(2) le_neq_trans
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (map fst xs). i \<le> oid
\<forall>i\<in>set (map fst xs). i \<noteq> oid
x \<in> set (map fst xs)
\<lbrakk>?a \<le> ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_add_last:
  assumes "spec_ops xs deps"
    and "\<forall>i \<in> set (map fst xs). i < oid"
    and "\<forall>ref \<in> deps oper. ref < oid"
  shows "spec_ops (xs @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
have "sorted ((map fst xs) @ [oid])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map fst xs @ [oid])
[PROOF STEP]
using assms sorted_append spec_ops_sorted
[PROOF STATE]
proof (prove)
using this:
spec_ops xs deps
\<forall>i\<in>set (map fst xs). i < oid
\<forall>ref\<in>deps oper. ref < oid
sorted (?xs @ ?ys) = (sorted ?xs \<and> sorted ?ys \<and> (\<forall>x\<in>set ?xs. \<forall>y\<in>set ?ys. x \<le> y))
spec_ops ?ops ?deps \<Longrightarrow> sorted (map fst ?ops)

goal (1 subgoal):
 1. sorted (map fst xs @ [oid])
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sorted (map fst xs @ [oid])

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (map fst xs @ [oid])

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
have "distinct ((map fst xs) @ [oid])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs @ [oid])
[PROOF STEP]
using assms spec_ops_distinct_fst
[PROOF STATE]
proof (prove)
using this:
spec_ops xs deps
\<forall>i\<in>set (map fst xs). i < oid
\<forall>ref\<in>deps oper. ref < oid
spec_ops ?ops ?deps \<Longrightarrow> distinct (map fst ?ops)

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

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map fst xs @ [oid])

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
have "\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid
[PROOF STEP]
using assms(1) spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops xs 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. \<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
hence "\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)]) \<and> r \<in> deps opr \<longrightarrow> r < i"
[PROOF STATE]
proof (prove)
using this:
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid

goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>oid oper ref. (oid, oper) \<in> set xs \<and> ref \<in> deps oper \<longrightarrow> ref < oid
\<forall>ref\<in>deps oper. ref < oid

goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)]) \<and> r \<in> deps opr \<longrightarrow> r < i

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted (map fst xs @ [oid])
distinct (map fst xs @ [oid])
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
show "spec_ops (xs @ [(oid, oper)]) deps"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst xs @ [oid])
distinct (map fst xs @ [oid])
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)]) \<and> r \<in> deps opr \<longrightarrow> r < i

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)]) deps
[PROOF STEP]
by (simp add: spec_ops_def)
[PROOF STATE]
proof (state)
this:
spec_ops (xs @ [(oid, oper)]) deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_add_any:
  assumes "spec_ops (xs @ ys) deps"
    and "\<forall>i \<in> set (map fst xs). i < oid"
    and "\<forall>i \<in> set (map fst ys). oid < i"
    and "\<forall>ref \<in> deps oper. ref < oid"
  shows "spec_ops (xs @ [(oid, oper)] @ ys) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)] @ ys) deps
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
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

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

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

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)] @ []) deps
[PROOF STEP]
by (simp add: spec_ops_add_last)
[PROOF STATE]
proof (state)
this:
spec_ops (xs @ [(oid, oper)] @ []) deps

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>spec_ops (xs @ ys) deps; \<forall>i\<in>set (map fst xs). i < oid; \<forall>a\<in>set (map fst ys). oid < a; \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ ys) deps
spec_ops (xs @ ys @ [y]) deps
\<forall>i\<in>set (map fst xs). i < oid
\<forall>a\<in>set (map fst (ys @ [y])). oid < a
\<forall>ref\<in>deps oper. ref < oid

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
have IH: "spec_ops (xs @ [(oid, oper)] @ ys) deps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)] @ ys) deps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)] @ ys) deps
[PROOF STEP]
from snoc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>spec_ops (xs @ ys) deps; \<forall>i\<in>set (map fst xs). i < oid; \<forall>a\<in>set (map fst ys). oid < a; \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ ys) deps
spec_ops (xs @ ys @ [y]) deps
\<forall>i\<in>set (map fst xs). i < oid
\<forall>a\<in>set (map fst (ys @ [y])). oid < a
\<forall>ref\<in>deps oper. ref < oid
[PROOF STEP]
have "spec_ops (xs @ ys) deps"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>spec_ops (xs @ ys) deps; \<forall>i\<in>set (map fst xs). i < oid; \<forall>a\<in>set (map fst ys). oid < a; \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ ys) deps
spec_ops (xs @ ys @ [y]) deps
\<forall>i\<in>set (map fst xs). i < oid
\<forall>a\<in>set (map fst (ys @ [y])). oid < a
\<forall>ref\<in>deps oper. ref < oid

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

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

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)] @ ys) deps
[PROOF STEP]
using assms(2) snoc
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ ys) deps
\<forall>i\<in>set (map fst xs). i < oid
\<lbrakk>spec_ops (xs @ ys) deps; \<forall>i\<in>set (map fst xs). i < oid; \<forall>a\<in>set (map fst ys). oid < a; \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ ys) deps
spec_ops (xs @ ys @ [y]) deps
\<forall>i\<in>set (map fst xs). i < oid
\<forall>a\<in>set (map fst (ys @ [y])). oid < a
\<forall>ref\<in>deps oper. ref < oid

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

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

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
obtain yi yo where y_pair: "y = (yi, yo)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>yi yo. y = (yi, yo) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y = (yi, yo)

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
have oid_yi: "oid < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid < yi
[PROOF STEP]
by (simp add: snoc.prems(3) y_pair)
[PROOF STATE]
proof (state)
this:
oid < yi

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
have yi_biggest: "\<forall>i \<in> set (map fst (xs @ [(oid, oper)] @ ys)). i < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi
[PROOF STEP]
have "\<forall>i \<in> set (map fst xs). i < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst xs). i < yi
[PROOF STEP]
using oid_yi assms(2) less_trans
[PROOF STATE]
proof (prove)
using this:
oid < yi
\<forall>i\<in>set (map fst xs). i < oid
\<lbrakk>?x < ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

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

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst xs). i < yi

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi
[PROOF STEP]
have "\<forall>i \<in> set (map fst ys). i < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>set (map fst ys). i < yi
[PROOF STEP]
by (metis UnCI append_assoc map_append set_append snoc.prems(1) spec_ops_id_inc y_pair)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst ys). i < yi

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>set (map fst xs). i < yi
\<forall>i\<in>set (map fst ys). i < yi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (map fst xs). i < yi
\<forall>i\<in>set (map fst ys). i < yi

goal (1 subgoal):
 1. \<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi
[PROOF STEP]
using oid_yi
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (map fst xs). i < yi
\<forall>i\<in>set (map fst ys). i < yi
oid < yi

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
have "sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
spec_ops (xs @ [(oid, oper)] @ ys) deps
[PROOF STEP]
have "sorted (map fst (xs @ [(oid, oper)] @ ys))"
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)] @ ys) deps

goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys))
[PROOF STEP]
using spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)] @ ys) 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. sorted (map fst (xs @ [(oid, oper)] @ ys))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sorted (map fst (xs @ [(oid, oper)] @ ys))

goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
hence "sorted (map fst (xs @ [(oid, oper)] @ ys) @ [yi])"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (xs @ [(oid, oper)] @ ys))

goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys) @ [yi])
[PROOF STEP]
using yi_biggest
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (xs @ [(oid, oper)] @ ys))
\<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi

goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys) @ [yi])
[PROOF STEP]
by (simp add: sorted_append dual_order.strict_implies_order)
[PROOF STATE]
proof (state)
this:
sorted (map fst (xs @ [(oid, oper)] @ ys) @ [yi])

goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
thus "sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (xs @ [(oid, oper)] @ ys) @ [yi])

goal (1 subgoal):
 1. sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
by (simp add: y_pair)
[PROOF STATE]
proof (state)
this:
sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
have "distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
have "distinct (map fst (xs @ [(oid, oper)] @ ys) @ [yi])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (xs @ [(oid, oper)] @ ys) @ [yi])
[PROOF STEP]
using IH yi_biggest spec_ops_def
[PROOF STATE]
proof (prove)
using this:
spec_ops (xs @ [(oid, oper)] @ ys) deps
\<forall>i\<in>set (map fst (xs @ [(oid, oper)] @ ys)). i < yi
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 (xs @ [(oid, oper)] @ ys) @ [yi])
[PROOF STEP]
by (metis distinct.simps(2) distinct1_rotate order_less_irrefl rotate1.simps(2))
[PROOF STATE]
proof (state)
this:
distinct (map fst (xs @ [(oid, oper)] @ ys) @ [yi])

goal (1 subgoal):
 1. distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))
[PROOF STEP]
thus "distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (xs @ [(oid, oper)] @ ys) @ [yi])

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
have "\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y])
                     \<and> r \<in> deps opr \<longrightarrow> r < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
have "\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys) \<and> r \<in> deps opr \<longrightarrow> r < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
by (meson IH spec_ops_def)
[PROOF STATE]
proof (state)
this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys) \<and> r \<in> deps opr \<longrightarrow> r < i

goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys) \<and> r \<in> deps opr \<longrightarrow> r < i

goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
have "\<forall>ref. ref \<in> deps yo \<longrightarrow> ref < yi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ref. ref \<in> deps yo \<longrightarrow> ref < yi
[PROOF STEP]
by (metis spec_ops_ref_less append_is_Nil_conv last_appendR last_in_set last_snoc
          list.simps(3) snoc.prems(1) y_pair)
[PROOF STATE]
proof (state)
this:
\<forall>ref. ref \<in> deps yo \<longrightarrow> ref < yi

goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys) \<and> r \<in> deps opr \<longrightarrow> r < i
\<forall>ref. ref \<in> deps yo \<longrightarrow> ref < yi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys) \<and> r \<in> deps opr \<longrightarrow> r < i
\<forall>ref. ref \<in> deps yo \<longrightarrow> ref < yi

goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
using y_pair
[PROOF STATE]
proof (prove)
using this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys) \<and> r \<in> deps opr \<longrightarrow> r < i
\<forall>ref. ref \<in> deps yo \<longrightarrow> ref < yi
y = (yi, yo)

goal (1 subgoal):
 1. \<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>\<lbrakk>spec_ops (xs @ xsa) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst xsa)) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa) deps; spec_ops (xs @ xsa @ [x]) deps; \<forall>i\<in>set (map fst xs). i < oid; Ball (set (map fst (xsa @ [x]))) ((<) oid); \<forall>ref\<in>deps oper. ref < oid\<rbrakk> \<Longrightarrow> spec_ops (xs @ [(oid, oper)] @ xsa @ [x]) deps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
[PROOF STEP]
show "spec_ops (xs @ [(oid, oper)] @ ys @ [y]) deps"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i

goal (1 subgoal):
 1. spec_ops (xs @ [(oid, oper)] @ ys @ [y]) deps
[PROOF STEP]
using spec_ops_def
[PROOF STATE]
proof (prove)
using this:
sorted (map fst (xs @ [(oid, oper)] @ ys @ [y]))
distinct (map fst (xs @ [(oid, oper)] @ ys @ [y]))
\<forall>i opr r. (i, opr) \<in> set (xs @ [(oid, oper)] @ ys @ [y]) \<and> r \<in> deps opr \<longrightarrow> r < i
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. spec_ops (xs @ [(oid, oper)] @ ys @ [y]) deps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
spec_ops (xs @ [(oid, oper)] @ ys @ [y]) deps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spec_ops_split:
  assumes "spec_ops xs deps"
    and "oid \<notin> set (map fst xs)"
  shows "\<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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
spec_ops xs deps
oid \<notin> set (map fst xs)

goal (1 subgoal):
 1. \<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)
[PROOF STEP]
proof(induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>spec_ops [] deps; oid \<notin> set (map fst [])\<rbrakk> \<Longrightarrow> \<exists>pre suf. [] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
 2. \<And>x xs. \<lbrakk>\<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> Ball (set (map fst suf)) ((<) oid); spec_ops (xs @ [x]) deps; oid \<notin> set (map fst (xs @ [x]))\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
spec_ops [] deps
oid \<notin> set (map fst [])

goal (2 subgoals):
 1. \<lbrakk>spec_ops [] deps; oid \<notin> set (map fst [])\<rbrakk> \<Longrightarrow> \<exists>pre suf. [] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
 2. \<And>x xs. \<lbrakk>\<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> Ball (set (map fst suf)) ((<) oid); spec_ops (xs @ [x]) deps; oid \<notin> set (map fst (xs @ [x]))\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
spec_ops [] deps
oid \<notin> set (map fst [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
spec_ops [] deps
oid \<notin> set (map fst [])

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

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>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> Ball (set (map fst suf)) ((<) oid); spec_ops (xs @ [x]) deps; oid \<notin> set (map fst (xs @ [x]))\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>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> Ball (set (map fst suf)) ((<) oid); spec_ops (xs @ [x]) deps; oid \<notin> set (map fst (xs @ [x]))\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>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>a\<in>set (map fst suf). oid < a)
spec_ops (xs @ [x]) deps
oid \<notin> set (map fst (xs @ [x]))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<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> Ball (set (map fst suf)) ((<) oid); spec_ops (xs @ [x]) deps; oid \<notin> set (map fst (xs @ [x]))\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
obtain xi xr where y_pair: "x = (xi, xr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi xr. x = (xi, xr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (xi, xr)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<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> Ball (set (map fst suf)) ((<) oid); spec_ops (xs @ [x]) deps; oid \<notin> set (map fst (xs @ [x]))\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
obtain pre suf where IH: "xs = pre @ suf \<and>
               (\<forall>a\<in>set (map fst pre). a < oid) \<and>
               (\<forall>a\<in>set (map fst suf). oid < a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pre suf. xs = pre @ suf \<and> (\<forall>a\<in>set (map fst pre). a < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis UnCI map_append set_append snoc spec_ops_rem_last)
[PROOF STATE]
proof (state)
this:
xs = pre @ suf \<and> (\<forall>a\<in>set (map fst pre). a < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<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> Ball (set (map fst suf)) ((<) oid); spec_ops (xs @ [x]) deps; oid \<notin> set (map fst (xs @ [x]))\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> Ball (set (map fst suf)) ((<) oid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = pre @ suf \<and> (\<forall>a\<in>set (map fst pre). a < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xs = pre @ suf \<and> (\<forall>a\<in>set (map fst pre). a < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)

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

goal (2 subgoals):
 1. \<lbrakk>xs = pre @ suf \<and> (\<forall>a\<in>set (map fst pre). a < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
 2. \<lbrakk>xs = pre @ suf \<and> (\<forall>a\<in>set (map fst pre). a < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a); \<not> xi < oid\<rbrakk> \<Longrightarrow> \<exists>pre suf. xs @ [x] = pre @ suf \<and> (\<forall>i\<in>set (map fst pre). i < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
[PROOF STEP]
have "\<forall>x \<in> set (map fst (pre @ suf)). x < xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (map fst (pre @ suf)). x < xi
[PROOF STEP]
using IH spec_ops_id_inc snoc.prems(1) y_pair
[PROOF STATE]
proof (prove)
using this:
xs = pre @ suf \<and> (\<forall>a\<in>set (map fst pre). a < oid) \<and> (\<forall>a\<in>set (map fst suf). oid < a)
\<lbrakk>spec_ops (?xs @ [(?oid, ?oper)]) ?deps; ?x \<in> set (map fst ?xs)\<rbrakk> \<Longrightarrow> ?x < ?oid
spec_ops (xs @ [x]) deps
x = (xi, xr)

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

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

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

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

goal (1 subgoal):
 1. \<forall>x\<in>set suf. fst x < oid
[PROOF STEP]
using xi_less
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set suf. fst x < xi
xi < oid

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. oid < xi
[PROOF STEP]
using snoc.prems(2) y_pair
[PROOF STATE]
proof (prove)
using this:
\<not> xi < oid
oid \<notin> set (map fst (xs @ [x]))
x = (xi, xr)

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed