[STATEMENT]
lemma inserted_item_ident:
  assumes "a \<in> set (insert_spec xs (e, i))"
    and "a \<notin> set xs"
  shows "a = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> set (insert_spec xs (e, i))
a \<notin> set xs

goal (1 subgoal):
 1. a = e
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<in> set (insert_spec [] (e, i)); a \<notin> set []\<rbrakk> \<Longrightarrow> a = e
 2. \<And>aa xs. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (aa # xs) (e, i)); a \<notin> set (aa # xs)\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
a \<in> set (insert_spec [] (e, i))
a \<notin> set []

goal (2 subgoals):
 1. \<lbrakk>a \<in> set (insert_spec [] (e, i)); a \<notin> set []\<rbrakk> \<Longrightarrow> a = e
 2. \<And>aa xs. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (aa # xs) (e, i)); a \<notin> set (aa # xs)\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set (insert_spec [] (e, i))
a \<notin> set []
[PROOF STEP]
show "a = e"
[PROOF STATE]
proof (prove)
using this:
a \<in> set (insert_spec [] (e, i))
a \<notin> set []

goal (1 subgoal):
 1. a = e
[PROOF STEP]
by (cases i, auto)
[PROOF STATE]
proof (state)
this:
a = e

goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (aa # xs) (e, i)); a \<notin> set (aa # xs)\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (aa # xs) (e, i)); a \<notin> set (aa # xs)\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e
a \<in> set (insert_spec (x # xs) (e, i))
a \<notin> set (x # xs)

goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (aa # xs) (e, i)); a \<notin> set (aa # xs)\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e
a \<in> set (insert_spec (x # xs) (e, i))
a \<notin> set (x # xs)
[PROOF STEP]
show "a = e"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e
a \<in> set (insert_spec (x # xs) (e, i))
a \<notin> set (x # xs)

goal (1 subgoal):
 1. a = e
[PROOF STEP]
proof(cases i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (x # xs) (e, i)); a \<notin> set (x # xs); i = None\<rbrakk> \<Longrightarrow> a = e
 2. \<And>aa. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (x # xs) (e, i)); a \<notin> set (x # xs); i = Some aa\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
i = None

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (x # xs) (e, i)); a \<notin> set (x # xs); i = None\<rbrakk> \<Longrightarrow> a = e
 2. \<And>aa. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (x # xs) (e, i)); a \<notin> set (x # xs); i = Some aa\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = None
[PROOF STEP]
show "a = e"
[PROOF STATE]
proof (prove)
using this:
i = None

goal (1 subgoal):
 1. a = e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i = None
a \<in> set (insert_spec xs (e, i))
a \<notin> set xs

goal (1 subgoal):
 1. a = e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = e

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (x # xs) (e, i)); a \<notin> set (x # xs); i = Some aa\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (x # xs) (e, i)); a \<notin> set (x # xs); i = Some aa\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
case (Some ref)
[PROOF STATE]
proof (state)
this:
i = Some ref

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e; a \<in> set (insert_spec (x # xs) (e, i)); a \<notin> set (x # xs); i = Some aa\<rbrakk> \<Longrightarrow> a = e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = Some ref
[PROOF STEP]
show "a = e"
[PROOF STATE]
proof (prove)
using this:
i = Some ref

goal (1 subgoal):
 1. a = e
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
i = Some ref
\<lbrakk>a \<in> set (insert_spec xs (e, i)); a \<notin> set xs\<rbrakk> \<Longrightarrow> a = e
a \<in> set (insert_spec (x # xs) (e, i))
a \<notin> set (x # xs)

goal (1 subgoal):
 1. a = e
[PROOF STEP]
by (case_tac "x = ref", auto)
[PROOF STATE]
proof (state)
this:
a = e

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_spec_distinct [intro]:
  fixes oid :: "'oid::{linorder}"
  assumes "distinct xs"
    and "\<And>x. x \<in> set xs \<Longrightarrow> x < oid"
    and "ref = Some r \<longrightarrow> r < oid"
  shows "distinct (insert_spec xs (oid, ref))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (insert_spec xs (oid, ref))
[PROOF STEP]
using assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
distinct xs
?x \<in> set xs \<Longrightarrow> ?x < oid

goal (1 subgoal):
 1. distinct (insert_spec xs (oid, ref))
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct []; \<And>x. x \<in> set [] \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec [] (oid, ref))
 2. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<And>x. x \<in> set xs \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec xs (oid, ref)); distinct (a # xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
show "distinct (insert_spec [] (oid, ref))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (insert_spec [] (oid, ref))
[PROOF STEP]
by(cases ref, auto)
[PROOF STATE]
proof (state)
this:
distinct (insert_spec [] (oid, ref))

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<And>x. x \<in> set xs \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec xs (oid, ref)); distinct (a # xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<And>x. x \<in> set xs \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec xs (oid, ref)); distinct (a # xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
fix a xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<And>x. x \<in> set xs \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec xs (oid, ref)); distinct (a # xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
assume IH: "distinct xs \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> x < oid) \<Longrightarrow> distinct (insert_spec xs (oid, ref))"
    and D: "distinct (a#xs)"
    and L: "\<And>x. x \<in> set (a#xs) \<Longrightarrow> x < oid"
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct xs; \<And>x. x \<in> set xs \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec xs (oid, ref))
distinct (a # xs)
?x \<in> set (a # xs) \<Longrightarrow> ?x < oid

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<And>x. x \<in> set xs \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec xs (oid, ref)); distinct (a # xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x < oid\<rbrakk> \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
show "distinct (insert_spec (a#xs) (oid, ref))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
proof(cases "ref")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref = None \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
 2. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
assume "ref = None"
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. ref = None \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
 2. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
thus "distinct (insert_spec (a#xs) (oid, ref))"
[PROOF STATE]
proof (prove)
using this:
ref = None

goal (1 subgoal):
 1. distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
using D L
[PROOF STATE]
proof (prove)
using this:
ref = None
distinct (a # xs)
?x \<in> set (a # xs) \<Longrightarrow> ?x < oid

goal (1 subgoal):
 1. distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (insert_spec (a # xs) (oid, ref))

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
fix id
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
assume S: "ref = Some id"
[PROOF STATE]
proof (state)
this:
ref = Some id

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ref = Some id

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
assume EQ: "a = id"
[PROOF STATE]
proof (state)
this:
a = id

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
hence "id \<noteq> oid"
[PROOF STATE]
proof (prove)
using this:
a = id

goal (1 subgoal):
 1. id \<noteq> oid
[PROOF STEP]
using D L
[PROOF STATE]
proof (prove)
using this:
a = id
distinct (a # xs)
?x \<in> set (a # xs) \<Longrightarrow> ?x < oid

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

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
id \<noteq> oid

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
have "id \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id \<notin> set xs
[PROOF STEP]
using D EQ
[PROOF STATE]
proof (prove)
using this:
distinct (a # xs)
a = id

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

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
id \<notin> set xs

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
have "oid \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oid \<notin> set xs
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (a # xs) \<Longrightarrow> ?x < oid

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

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
id \<noteq> oid
id \<notin> set xs
oid \<notin> set xs
[PROOF STEP]
have "id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs"
[PROOF STATE]
proof (prove)
using this:
id \<noteq> oid
id \<notin> set xs
oid \<notin> set xs

goal (1 subgoal):
 1. id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
id \<noteq> oid
id \<notin> set xs
oid \<notin> set xs
distinct (a # xs)

goal (1 subgoal):
 1. id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
a = id \<Longrightarrow> id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
note T = this
[PROOF STATE]
proof (state)
this:
a = id \<Longrightarrow> id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a = id \<Longrightarrow> id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
assume NEQ: "a \<noteq> id"
[PROOF STATE]
proof (state)
this:
a \<noteq> id

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
have 0: "a \<notin> set (insert_spec xs (oid, Some id))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> set (insert_spec xs (oid, Some id))
[PROOF STEP]
using D L
[PROOF STATE]
proof (prove)
using this:
distinct (a # xs)
?x \<in> set (a # xs) \<Longrightarrow> ?x < oid

goal (1 subgoal):
 1. a \<notin> set (insert_spec xs (oid, Some id))
[PROOF STEP]
by(metis distinct.simps(2) insert_spec.simps(1) insert_spec_none insert_spec_nonex
            insert_spec_set insert_iff list.set(2) not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
a \<notin> set (insert_spec xs (oid, Some id))

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
have 1: "distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
distinct (a # xs)

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

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
have "\<And>x. x \<in> set xs \<Longrightarrow> x < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<Longrightarrow> x < oid
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (a # xs) \<Longrightarrow> ?x < oid

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

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
hence "distinct (insert_spec xs (oid, Some id))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> ?x < oid

goal (1 subgoal):
 1. distinct (insert_spec xs (oid, Some id))
[PROOF STEP]
using S IH[OF 1]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> ?x < oid
ref = Some id
(\<And>x. x \<in> set xs \<Longrightarrow> x < oid) \<Longrightarrow> distinct (insert_spec xs (oid, ref))

goal (1 subgoal):
 1. distinct (insert_spec xs (oid, Some id))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (insert_spec xs (oid, Some id))

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
hence "a \<notin> set (insert_spec xs (oid, Some id)) \<and> distinct (insert_spec xs (oid, Some id))"
[PROOF STATE]
proof (prove)
using this:
distinct (insert_spec xs (oid, Some id))

goal (1 subgoal):
 1. a \<notin> set (insert_spec xs (oid, Some id)) \<and> distinct (insert_spec xs (oid, Some id))
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
distinct (insert_spec xs (oid, Some id))
a \<notin> set (insert_spec xs (oid, Some id))

goal (1 subgoal):
 1. a \<notin> set (insert_spec xs (oid, Some id)) \<and> distinct (insert_spec xs (oid, Some id))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> set (insert_spec xs (oid, Some id)) \<and> distinct (insert_spec xs (oid, Some id))

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
a \<noteq> id \<Longrightarrow> a \<notin> set (insert_spec xs (oid, Some id)) \<and> distinct (insert_spec xs (oid, Some id))

goal (1 subgoal):
 1. \<And>aa. ref = Some aa \<Longrightarrow> distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
from this S T
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> id \<Longrightarrow> a \<notin> set (insert_spec xs (oid, Some id)) \<and> distinct (insert_spec xs (oid, Some id))
ref = Some id
a = id \<Longrightarrow> id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs
[PROOF STEP]
show "distinct (insert_spec (a # xs) (oid, ref))"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> id \<Longrightarrow> a \<notin> set (insert_spec xs (oid, Some id)) \<and> distinct (insert_spec xs (oid, Some id))
ref = Some id
a = id \<Longrightarrow> id \<noteq> oid \<and> id \<notin> set xs \<and> oid \<notin> set xs \<and> distinct xs

goal (1 subgoal):
 1. distinct (insert_spec (a # xs) (oid, ref))
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
distinct (insert_spec (a # xs) (oid, ref))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (insert_spec (a # xs) (oid, ref))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_after_ref:
  assumes "distinct (xs @ ref # ys)"
  shows "insert_spec (xs @ ref # ys) (oid, Some ref) = xs @ ref # oid # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (xs @ ref # ys) (oid, Some ref) = xs @ ref # oid # ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (xs @ ref # ys)

goal (1 subgoal):
 1. insert_spec (xs @ ref # ys) (oid, Some ref) = xs @ ref # oid # ys
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma insert_somewhere:
  assumes "ref = None \<or> (ref = Some r \<and> r \<in> set list)"
  shows "\<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ref = None \<or> ref = Some r \<and> r \<in> set list

goal (1 subgoal):
 1. \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys
[PROOF STEP]
proof(induction list)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref = None \<or> ref = Some r \<and> r \<in> set [] \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
 2. \<And>a list. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys; ref = None \<or> ref = Some r \<and> r \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume "ref = None \<or> ref = Some r \<and> r \<in> set []"
[PROOF STATE]
proof (state)
this:
ref = None \<or> ref = Some r \<and> r \<in> set []

goal (2 subgoals):
 1. ref = None \<or> ref = Some r \<and> r \<in> set [] \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
 2. \<And>a list. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys; ref = None \<or> ref = Some r \<and> r \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
thus "\<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
ref = None \<or> ref = Some r \<and> r \<in> set []

goal (1 subgoal):
 1. \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref = None \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
 2. ref = Some r \<and> r \<in> set [] \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume "ref = None"
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. ref = None \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
 2. ref = Some r \<and> r \<in> set [] \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
thus "\<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
ref = None

goal (1 subgoal):
 1. \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set [] \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set [] \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume "ref = Some r \<and> r \<in> set []"
[PROOF STATE]
proof (state)
this:
ref = Some r \<and> r \<in> set []

goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set [] \<Longrightarrow> \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
thus "\<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
ref = Some r \<and> r \<in> set []

goal (1 subgoal):
 1. \<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. [] = xs @ ys \<and> insert_spec [] (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys; ref = None \<or> ref = Some r \<and> r \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys; ref = None \<or> ref = Some r \<and> r \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
fix a list
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys; ref = None \<or> ref = Some r \<and> r \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume 1: "ref = None \<or> ref = Some r \<and> r \<in> set (a#list)"
    and IH: "ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow>
         \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (state)
this:
ref = None \<or> ref = Some r \<and> r \<in> set (a # list)
ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys; ref = None \<or> ref = Some r \<and> r \<in> set (a # list)\<rbrakk> \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
show "\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
proof(rule disjE[OF 1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref = None \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
 2. ref = Some r \<and> r \<in> set (a # list) \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume "ref = None"
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. ref = None \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
 2. ref = Some r \<and> r \<in> set (a # list) \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
thus "\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
ref = None

goal (1 subgoal):
 1. \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set (a # list) \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set (a # list) \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume "ref = Some r \<and> r \<in> set (a # list)"
[PROOF STATE]
proof (state)
this:
ref = Some r \<and> r \<in> set (a # list)

goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set (a # list) \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
hence 2: "r = a \<or> r \<in> set list" and 3: "ref = Some r"
[PROOF STATE]
proof (prove)
using this:
ref = Some r \<and> r \<in> set (a # list)

goal (1 subgoal):
 1. r = a \<or> r \<in> set list &&& ref = Some r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r = a \<or> r \<in> set list
ref = Some r

goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set (a # list) \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
show "\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
proof(rule disjE[OF 2])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = a \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
 2. r \<in> set list \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume "r = a"
[PROOF STATE]
proof (state)
this:
r = a

goal (2 subgoals):
 1. r = a \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
 2. r \<in> set list \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
thus "\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
r = a

goal (1 subgoal):
 1. \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
r = a
ref = Some r

goal (1 subgoal):
 1. \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
by(metis append_Cons append_Nil insert_spec.simps(3))
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. r \<in> set list \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> set list \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
assume "r \<in> set list"
[PROOF STATE]
proof (state)
this:
r \<in> set list

goal (1 subgoal):
 1. r \<in> set list \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
r \<in> set list
[PROOF STEP]
obtain xs ys
        where "list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
r \<in> set list

goal (1 subgoal):
 1. (\<And>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using IH 3
[PROOF STATE]
proof (prove)
using this:
r \<in> set list
ref = None \<or> ref = Some r \<and> r \<in> set list \<Longrightarrow> \<exists>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys
ref = Some r

goal (1 subgoal):
 1. (\<And>xs ys. list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. r \<in> set list \<Longrightarrow> \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
thus "\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
list = xs @ ys \<and> insert_spec list (oid, ref) = xs @ oid # ys
ref = Some r

goal (1 subgoal):
 1. \<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys
[PROOF STEP]
by clarsimp (metis append_Cons append_Nil)
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. a # list = xs @ ys \<and> insert_spec (a # list) (oid, ref) = xs @ oid # ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_first_part:
  assumes "ref = None \<or> (ref = Some r \<and> r \<in> set xs)"
  shows "insert_spec (xs @ ys) (oid, ref) = (insert_spec xs (oid, ref)) @ ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (xs @ ys) (oid, ref) = insert_spec xs (oid, ref) @ ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ref = None \<or> ref = Some r \<and> r \<in> set xs

goal (1 subgoal):
 1. insert_spec (xs @ ys) (oid, ref) = insert_spec xs (oid, ref) @ ys
[PROOF STEP]
proof(induction ys rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ []) (oid, ref) = insert_spec xs (oid, ref) @ []
 2. \<And>x xsa. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
[PROOF STEP]
assume "ref = None \<or> ref = Some r \<and> r \<in> set xs"
[PROOF STATE]
proof (state)
this:
ref = None \<or> ref = Some r \<and> r \<in> set xs

goal (2 subgoals):
 1. ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ []) (oid, ref) = insert_spec xs (oid, ref) @ []
 2. \<And>x xsa. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
[PROOF STEP]
thus "insert_spec (xs @ []) (oid, ref) = insert_spec xs (oid, ref) @ []"
[PROOF STATE]
proof (prove)
using this:
ref = None \<or> ref = Some r \<and> r \<in> set xs

goal (1 subgoal):
 1. insert_spec (xs @ []) (oid, ref) = insert_spec xs (oid, ref) @ []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ []) (oid, ref) = insert_spec xs (oid, ref) @ []

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
[PROOF STEP]
fix x xsa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
[PROOF STEP]
assume IH: "ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa"
    and "ref = None \<or> ref = Some r \<and> r \<in> set xs"
[PROOF STATE]
proof (state)
this:
ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa
ref = None \<or> ref = Some r \<and> r \<in> set xs

goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
[PROOF STEP]
thus "insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]"
[PROOF STATE]
proof (prove)
using this:
ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa
ref = None \<or> ref = Some r \<and> r \<in> set xs

goal (1 subgoal):
 1. insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set [] \<Longrightarrow> insert_spec ([] @ xsa) (oid, ref) = insert_spec [] (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set []\<rbrakk> \<Longrightarrow> insert_spec ([] @ xsa @ [x]) (oid, ref) = insert_spec [] (oid, ref) @ xsa @ [x]
 2. \<And>a xs. \<lbrakk>\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
assume "ref = None \<or> ref = Some r \<and> r \<in> set []"
[PROOF STATE]
proof (state)
this:
ref = None \<or> ref = Some r \<and> r \<in> set []

goal (2 subgoals):
 1. \<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set [] \<Longrightarrow> insert_spec ([] @ xsa) (oid, ref) = insert_spec [] (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set []\<rbrakk> \<Longrightarrow> insert_spec ([] @ xsa @ [x]) (oid, ref) = insert_spec [] (oid, ref) @ xsa @ [x]
 2. \<And>a xs. \<lbrakk>\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
thus "insert_spec ([] @ xsa @ [x]) (oid, ref) = insert_spec [] (oid, ref) @ xsa @ [x]"
[PROOF STATE]
proof (prove)
using this:
ref = None \<or> ref = Some r \<and> r \<in> set []

goal (1 subgoal):
 1. insert_spec ([] @ xsa @ [x]) (oid, ref) = insert_spec [] (oid, ref) @ xsa @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_spec ([] @ xsa @ [x]) (oid, ref) = insert_spec [] (oid, ref) @ xsa @ [x]

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
fix a xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
assume 1: "ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)"
      and 2: "((ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa) \<Longrightarrow>
             ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x])"
      and 3: "(ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa)"
[PROOF STATE]
proof (state)
this:
ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)
\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
show "insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
proof(rule disjE[OF 1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref = None \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
 2. ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
assume "ref = None"
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. ref = None \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
 2. ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
thus "insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]"
[PROOF STATE]
proof (prove)
using this:
ref = None

goal (1 subgoal):
 1. insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]

goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
assume "ref = Some r \<and> r \<in> set (a # xs)"
[PROOF STATE]
proof (state)
this:
ref = Some r \<and> r \<in> set (a # xs)

goal (1 subgoal):
 1. ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
thus "insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]"
[PROOF STATE]
proof (prove)
using this:
ref = Some r \<and> r \<in> set (a # xs)

goal (1 subgoal):
 1. insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
ref = Some r \<and> r \<in> set (a # xs)
\<lbrakk>ref = None \<or> ref = Some r \<and> r \<in> set xs \<Longrightarrow> insert_spec (xs @ xsa) (oid, ref) = insert_spec xs (oid, ref) @ xsa; ref = None \<or> ref = Some r \<and> r \<in> set xs\<rbrakk> \<Longrightarrow> insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]
ref = None \<or> ref = Some r \<and> r \<in> set (a # xs) \<Longrightarrow> insert_spec ((a # xs) @ xsa) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa

goal (1 subgoal):
 1. insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_spec ((a # xs) @ xsa @ [x]) (oid, ref) = insert_spec (a # xs) (oid, ref) @ xsa @ [x]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ xsa @ [x]) (oid, ref) = insert_spec xs (oid, ref) @ xsa @ [x]

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref)
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ref = Some r; r \<notin> set []; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ([] @ ys) (oid, ref) = [] @ insert_spec ys (oid, ref)
 2. \<And>a xs. \<lbrakk>\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref); ref = Some r; r \<notin> set (a # xs); r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)
[PROOF STEP]
assume "ref = Some r"
[PROOF STATE]
proof (state)
this:
ref = Some r

goal (2 subgoals):
 1. \<lbrakk>ref = Some r; r \<notin> set []; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ([] @ ys) (oid, ref) = [] @ insert_spec ys (oid, ref)
 2. \<And>a xs. \<lbrakk>\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref); ref = Some r; r \<notin> set (a # xs); r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)
[PROOF STEP]
thus "insert_spec ([] @ ys) (oid, ref) = [] @ insert_spec ys (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
ref = Some r

goal (1 subgoal):
 1. insert_spec ([] @ ys) (oid, ref) = [] @ insert_spec ys (oid, ref)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_spec ([] @ ys) (oid, ref) = [] @ insert_spec ys (oid, ref)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref); ref = Some r; r \<notin> set (a # xs); r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref); ref = Some r; r \<notin> set (a # xs); r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)
[PROOF STEP]
fix a xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref); ref = Some r; r \<notin> set (a # xs); r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)
[PROOF STEP]
assume "ref = Some r" and "r \<notin> set (a # xs)" and "r \<in> set ys"
    and "ref = Some r \<Longrightarrow> r \<notin> set xs \<Longrightarrow> r \<in> set ys \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref)"
[PROOF STATE]
proof (state)
this:
ref = Some r
r \<notin> set (a # xs)
r \<in> set ys
\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref); ref = Some r; r \<notin> set (a # xs); r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)
[PROOF STEP]
thus "insert_spec ((a # xs) @ ys) (oid, ref) = (a # xs) @ insert_spec ys (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
ref = Some r
r \<notin> set (a # xs)
r \<in> set ys
\<lbrakk>ref = Some r; r \<notin> set xs; r \<in> set ys\<rbrakk> \<Longrightarrow> insert_spec (xs @ ys) (oid, ref) = xs @ insert_spec ys (oid, ref)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_ins_empty [simp]:
  shows "interp_ins [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins [] = []
[PROOF STEP]
by (simp add: interp_ins_def)


[STATEMENT]
lemma interp_ins_tail_unfold:
  shows "interp_ins (xs @ [x]) = insert_spec (interp_ins xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins (xs @ [x]) = insert_spec (interp_ins xs) x
[PROOF STEP]
by (clarsimp simp add: interp_ins_def)


[STATEMENT]
lemma interp_ins_subset [simp]:
  shows "set (interp_ins op_list) \<subseteq> set (map fst op_list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (interp_ins op_list) \<subseteq> set (map fst op_list)
[PROOF STEP]
proof(induction op_list rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (interp_ins []) \<subseteq> set (map fst [])
 2. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. set (interp_ins []) \<subseteq> set (map fst [])
 2. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show "set (interp_ins []) \<subseteq> set (map fst [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (interp_ins []) \<subseteq> set (map fst [])
[PROOF STEP]
by (simp add: interp_ins_def)
[PROOF STATE]
proof (state)
this:
set (interp_ins []) \<subseteq> set (map fst [])

goal (1 subgoal):
 1. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
set (interp_ins xs) \<subseteq> set (map fst xs)

goal (1 subgoal):
 1. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
hence IH: "set (interp_ins xs) \<subseteq> set (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
set (interp_ins xs) \<subseteq> set (map fst xs)

goal (1 subgoal):
 1. set (interp_ins xs) \<subseteq> set (map fst xs)
[PROOF STEP]
using interp_ins_def
[PROOF STATE]
proof (prove)
using this:
set (interp_ins xs) \<subseteq> set (map fst xs)
interp_ins ?ops \<equiv> foldl insert_spec [] ?ops

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

goal (1 subgoal):
 1. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
obtain oid ref where x_pair: "x = (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid ref. x = (oid, ref) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = (oid, ref)

goal (1 subgoal):
 1. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
hence spec: "interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
x = (oid, ref)

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

goal (1 subgoal):
 1. \<And>x xs. set (interp_ins xs) \<subseteq> set (map fst xs) \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref)
[PROOF STEP]
show "set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref)

goal (1 subgoal):
 1. set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
proof(cases ref)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref); ref = None\<rbrakk> \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
 2. \<And>a. \<lbrakk>interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. \<lbrakk>interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref); ref = None\<rbrakk> \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
 2. \<And>a. \<lbrakk>interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ref = None
[PROOF STEP]
show "set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
ref = None

goal (1 subgoal):
 1. set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
using IH spec x_pair
[PROOF STATE]
proof (prove)
using this:
ref = None
set (interp_ins xs) \<subseteq> set (map fst xs)
interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref)
x = (oid, ref)

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

goal (1 subgoal):
 1. \<And>a. \<lbrakk>interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
ref = Some a

goal (1 subgoal):
 1. \<And>a. \<lbrakk>interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ref = Some a
[PROOF STEP]
show "set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))"
[PROOF STATE]
proof (prove)
using this:
ref = Some a

goal (1 subgoal):
 1. set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
using IH spec x_pair
[PROOF STATE]
proof (prove)
using this:
ref = Some a
set (interp_ins xs) \<subseteq> set (map fst xs)
interp_ins (xs @ [x]) = insert_spec (interp_ins xs) (oid, ref)
x = (oid, ref)

goal (1 subgoal):
 1. set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))
[PROOF STEP]
by (cases "a \<in> set (interp_ins xs)", auto)
[PROOF STATE]
proof (state)
this:
set (interp_ins (xs @ [x])) \<subseteq> set (map fst (xs @ [x]))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_ins_distinct:
  assumes "insert_ops op_list"
  shows "distinct (interp_ins op_list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (interp_ins op_list)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops op_list

goal (1 subgoal):
 1. distinct (interp_ins op_list)
[PROOF STEP]
proof(induction op_list rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. insert_ops [] \<Longrightarrow> distinct (interp_ins [])
 2. \<And>x xs. \<lbrakk>insert_ops xs \<Longrightarrow> distinct (interp_ins xs); insert_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_ins (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops []

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

goal (1 subgoal):
 1. distinct (interp_ins [])
[PROOF STEP]
by (simp add: interp_ins_def)
[PROOF STATE]
proof (state)
this:
distinct (interp_ins [])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>insert_ops xs \<Longrightarrow> distinct (interp_ins xs); insert_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_ins (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>insert_ops xs \<Longrightarrow> distinct (interp_ins xs); insert_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_ins (xs @ [x]))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
insert_ops xs \<Longrightarrow> distinct (interp_ins xs)
insert_ops (xs @ [x])

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

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

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>insert_ops xs \<Longrightarrow> distinct (interp_ins xs); insert_ops (xs @ [x])\<rbrakk> \<Longrightarrow> distinct (interp_ins (xs @ [x]))
[PROOF STEP]
obtain oid ref where x_pair: "x = (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid ref. x = (oid, ref) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (oid, ref)

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

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

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

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

goal (1 subgoal):
 1. \<forall>x\<in>set (interp_ins xs). x < oid
[PROOF STEP]
using interp_ins_subset
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (map fst xs). x < oid
set (interp_ins ?op_list) \<subseteq> set (map fst ?op_list)

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

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

goal (1 subgoal):
 1. distinct (insert_spec (interp_ins xs) (oid, ref))
[PROOF STEP]
using IH insert_spec_distinct insert_spec_nonex
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (interp_ins xs). x < oid
distinct (interp_ins xs)
\<lbrakk>distinct ?xs; \<And>x. x \<in> set ?xs \<Longrightarrow> x < ?oid; ?ref = Some ?r \<longrightarrow> ?r < ?oid\<rbrakk> \<Longrightarrow> distinct (insert_spec ?xs (?oid, ?ref))
?ref \<notin> set ?xs \<Longrightarrow> insert_spec ?xs (?oid, Some ?ref) = ?xs

goal (1 subgoal):
 1. distinct (insert_spec (interp_ins xs) (oid, ref))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distinct (insert_spec (interp_ins xs) (oid, ref))

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

goal (1 subgoal):
 1. distinct (interp_ins (xs @ [x]))
[PROOF STEP]
by (simp add: x_pair interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
distinct (interp_ins (xs @ [x]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_rel_set_fst:
  shows "fst ` (succ_rel xs) = set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` succ_rel xs = set xs
[PROOF STEP]
by (induction xs rule: succ_rel.induct, auto)


[STATEMENT]
lemma succ_rel_functional:
  assumes "(a, b1) \<in> succ_rel xs"
    and "(a, b2) \<in> succ_rel xs"
    and "distinct xs"
  shows "b1 = b2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(a, b1) \<in> succ_rel xs
(a, b2) \<in> succ_rel xs
distinct xs

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
proof(induction xs rule: succ_rel.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>(a, b1) \<in> succ_rel []; (a, b2) \<in> succ_rel []; distinct []\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<And>head. \<lbrakk>(a, b1) \<in> succ_rel [head]; (a, b2) \<in> succ_rel [head]; distinct [head]\<rbrakk> \<Longrightarrow> b1 = b2
 3. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
(a, b1) \<in> succ_rel []
(a, b2) \<in> succ_rel []
distinct []

goal (3 subgoals):
 1. \<lbrakk>(a, b1) \<in> succ_rel []; (a, b2) \<in> succ_rel []; distinct []\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<And>head. \<lbrakk>(a, b1) \<in> succ_rel [head]; (a, b2) \<in> succ_rel [head]; distinct [head]\<rbrakk> \<Longrightarrow> b1 = b2
 3. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a, b1) \<in> succ_rel []
(a, b2) \<in> succ_rel []
distinct []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(a, b1) \<in> succ_rel []
(a, b2) \<in> succ_rel []
distinct []

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b1 = b2

goal (2 subgoals):
 1. \<And>head. \<lbrakk>(a, b1) \<in> succ_rel [head]; (a, b2) \<in> succ_rel [head]; distinct [head]\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>head. \<lbrakk>(a, b1) \<in> succ_rel [head]; (a, b2) \<in> succ_rel [head]; distinct [head]\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
case (2 head)
[PROOF STATE]
proof (state)
this:
(a, b1) \<in> succ_rel [head]
(a, b2) \<in> succ_rel [head]
distinct [head]

goal (2 subgoals):
 1. \<And>head. \<lbrakk>(a, b1) \<in> succ_rel [head]; (a, b2) \<in> succ_rel [head]; distinct [head]\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a, b1) \<in> succ_rel [head]
(a, b2) \<in> succ_rel [head]
distinct [head]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(a, b1) \<in> succ_rel [head]
(a, b2) \<in> succ_rel [head]
distinct [head]

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b1 = b2

goal (1 subgoal):
 1. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
case (3 head x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
(a, b1) \<in> succ_rel (head # x # xs)
(a, b2) \<in> succ_rel (head # x # xs)
distinct (head # x # xs)

goal (1 subgoal):
 1. \<And>head x xs. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
(a, b1) \<in> succ_rel (head # x # xs)
(a, b2) \<in> succ_rel (head # x # xs)
distinct (head # x # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
(a, b1) \<in> succ_rel (head # x # xs)
(a, b2) \<in> succ_rel (head # x # xs)
distinct (head # x # xs)

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
proof(cases "a = head")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a = head\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = head

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a = head\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
hence "a \<notin> set (x#xs)"
[PROOF STATE]
proof (prove)
using this:
a = head

goal (1 subgoal):
 1. a \<notin> set (x # xs)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
a = head
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
(a, b1) \<in> succ_rel (head # x # xs)
(a, b2) \<in> succ_rel (head # x # xs)
distinct (head # x # xs)

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

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a = head\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
hence "a \<notin> fst ` (succ_rel (x#xs))"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set (x # xs)

goal (1 subgoal):
 1. a \<notin> fst ` succ_rel (x # xs)
[PROOF STEP]
using succ_rel_set_fst
[PROOF STATE]
proof (prove)
using this:
a \<notin> set (x # xs)
fst ` succ_rel ?xs = set ?xs

goal (1 subgoal):
 1. a \<notin> fst ` succ_rel (x # xs)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<notin> fst ` succ_rel (x # xs)

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a = head\<rbrakk> \<Longrightarrow> b1 = b2
 2. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<notin> fst ` succ_rel (x # xs)
[PROOF STEP]
show "b1 = b2"
[PROOF STATE]
proof (prove)
using this:
a \<notin> fst ` succ_rel (x # xs)

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
using 3 image_iff
[PROOF STATE]
proof (prove)
using this:
a \<notin> fst ` succ_rel (x # xs)
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
(a, b1) \<in> succ_rel (head # x # xs)
(a, b2) \<in> succ_rel (head # x # xs)
distinct (head # x # xs)
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> head

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
hence "{(a, b1), (a, b2)} \<subseteq> succ_rel (x#xs)"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> head

goal (1 subgoal):
 1. {(a, b1), (a, b2)} \<subseteq> succ_rel (x # xs)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
a \<noteq> head
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
(a, b1) \<in> succ_rel (head # x # xs)
(a, b2) \<in> succ_rel (head # x # xs)
distinct (head # x # xs)

goal (1 subgoal):
 1. {(a, b1), (a, b2)} \<subseteq> succ_rel (x # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(a, b1), (a, b2)} \<subseteq> succ_rel (x # xs)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(a, b1), (a, b2)} \<subseteq> succ_rel (x # xs)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
have "distinct (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (x # xs)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2
(a, b1) \<in> succ_rel (head # x # xs)
(a, b2) \<in> succ_rel (head # x # xs)
distinct (head # x # xs)

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2; (a, b1) \<in> succ_rel (head # x # xs); (a, b2) \<in> succ_rel (head # x # xs); distinct (head # x # xs); a \<noteq> head\<rbrakk> \<Longrightarrow> b1 = b2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(a, b1), (a, b2)} \<subseteq> succ_rel (x # xs)
distinct (x # xs)
[PROOF STEP]
show "b1 = b2"
[PROOF STATE]
proof (prove)
using this:
{(a, b1), (a, b2)} \<subseteq> succ_rel (x # xs)
distinct (x # xs)

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
using "3.IH"
[PROOF STATE]
proof (prove)
using this:
{(a, b1), (a, b2)} \<subseteq> succ_rel (x # xs)
distinct (x # xs)
\<lbrakk>(a, b1) \<in> succ_rel (x # xs); (a, b2) \<in> succ_rel (x # xs); distinct (x # xs)\<rbrakk> \<Longrightarrow> b1 = b2

goal (1 subgoal):
 1. b1 = b2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b1 = b2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_rel_rem_head:
  assumes "distinct (x # xs)"
  shows "{(p, n) \<in> succ_rel (x # xs). p \<noteq> x} = succ_rel xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
have head_notin: "x \<notin> fst ` succ_rel xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> fst ` succ_rel xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (x # xs)

goal (1 subgoal):
 1. x \<notin> fst ` succ_rel xs
[PROOF STEP]
by (simp add: succ_rel_set_fst)
[PROOF STATE]
proof (state)
this:
x \<notin> fst ` succ_rel xs

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> fst ` succ_rel xs

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
obtain y where "(x, y) \<in> succ_rel (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. (x, y) \<in> succ_rel (x # xs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases xs, auto)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> succ_rel (x # xs)

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, y) \<in> succ_rel (x # xs)

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
have "succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs
[PROOF STEP]
using calculation head_notin image_iff
[PROOF STATE]
proof (prove)
using this:
x \<notin> fst ` succ_rel xs
(x, y) \<in> succ_rel (x # xs)
x \<notin> fst ` succ_rel xs
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs
[PROOF STEP]
by (cases xs, fastforce+)
[PROOF STATE]
proof (state)
this:
succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs
[PROOF STEP]
have "\<And>n. (x, n) \<in> succ_rel (x # xs) \<Longrightarrow> n = y"
[PROOF STATE]
proof (prove)
using this:
succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs

goal (1 subgoal):
 1. \<And>n. (x, n) \<in> succ_rel (x # xs) \<Longrightarrow> n = y
[PROOF STEP]
by (metis Pair_inject fst_conv head_notin image_eqI insertE insert_is_Un)
[PROOF STATE]
proof (state)
this:
(x, ?n) \<in> succ_rel (x # xs) \<Longrightarrow> ?n = y

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
hence "{(p, n) \<in> succ_rel (x # xs). p \<noteq> x} = succ_rel (x # xs) - {(x, y)}"
[PROOF STATE]
proof (prove)
using this:
(x, ?n) \<in> succ_rel (x # xs) \<Longrightarrow> ?n = y

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel (x # xs) - {(x, y)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel (x # xs) - {(x, y)}

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel (x # xs) - {(x, y)}

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
have "succ_rel (x # xs) - {(x, y)} = succ_rel xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (x # xs) - {(x, y)} = succ_rel xs
[PROOF STEP]
using image_iff calculation
[PROOF STATE]
proof (prove)
using this:
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)
x \<notin> fst ` succ_rel xs
(x, y) \<in> succ_rel (x # xs)
succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs
{(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel (x # xs) - {(x, y)}

goal (1 subgoal):
 1. succ_rel (x # xs) - {(x, y)} = succ_rel xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
succ_rel (x # xs) - {(x, y)} = succ_rel xs

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> fst ` succ_rel xs
(x, y) \<in> succ_rel (x # xs)
succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs
{(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel (x # xs) - {(x, y)}
succ_rel (x # xs) - {(x, y)} = succ_rel xs
[PROOF STEP]
show "{(p, n) \<in> succ_rel (x # xs). p \<noteq> x} = succ_rel xs"
[PROOF STATE]
proof (prove)
using this:
x \<notin> fst ` succ_rel xs
(x, y) \<in> succ_rel (x # xs)
succ_rel (x # xs) = {(x, y)} \<union> succ_rel xs
{(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel (x # xs) - {(x, y)}
succ_rel (x # xs) - {(x, y)} = succ_rel xs

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{(p, n). (p, n) \<in> succ_rel (x # xs) \<and> p \<noteq> x} = succ_rel xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_rel_swap_head:
  assumes "distinct (ref # list)"
    and "(ref, n) \<in> succ_rel (ref # list)"
  shows "succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
proof(cases list)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list = [] \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
 2. \<And>a lista. list = a # lista \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
list = []

goal (2 subgoals):
 1. list = [] \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
 2. \<And>a lista. list = a # lista \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
list = []

goal (1 subgoal):
 1. succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list = []
distinct (ref # list)
(ref, n) \<in> succ_rel (ref # list)

goal (1 subgoal):
 1. succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list

goal (1 subgoal):
 1. \<And>a lista. list = a # lista \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lista. list = a # lista \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
case (Cons a list)
[PROOF STATE]
proof (state)
this:
list = a # list

goal (1 subgoal):
 1. \<And>a lista. list = a # lista \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list = a # list

goal (1 subgoal):
 1. \<And>a lista. list = a # lista \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
list = a # list
[PROOF STEP]
have "n = Some a"
[PROOF STATE]
proof (prove)
using this:
list = a # list

goal (1 subgoal):
 1. n = Some a
[PROOF STEP]
by (metis Un_iff assms singletonI succ_rel.simps(3) succ_rel_functional)
[PROOF STATE]
proof (state)
this:
n = Some a

goal (1 subgoal):
 1. \<And>a lista. list = a # lista \<Longrightarrow> succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list = a # list
n = Some a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
list = a # list
n = Some a

goal (1 subgoal):
 1. succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list

goal:
No subgoals!
[PROOF STEP]
qed