[STATEMENT]
lemma succ_rel_insert_alt:
  assumes "a \<noteq> ref"
    and "distinct (oid # a # b # list)"
  shows "insert_alt (succ_rel (a # b # list)) (oid, ref) =
         {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
proof(cases "\<exists>n. (ref, n) \<in> succ_rel (a # b # list)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>n. (ref, n) \<in> succ_rel (a # b # list)

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
hence "insert_alt (succ_rel (a # b # list)) (oid, ref) =
           {(p, n) \<in> succ_rel (a # b # list). p \<noteq> ref} \<union> {(ref, Some oid)} \<union>
           {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)}"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. (ref, n) \<in> succ_rel (a # b # list)

goal (1 subgoal):
 1. insert_alt (succ_rel (a # b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (a # b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)}

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (a # b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)}

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
have "{(p, n) \<in> succ_rel (a # b # list). p \<noteq> ref} =
                 {(a, Some b)} \<union> {(p, n) \<in> succ_rel (b # list). p \<noteq> ref}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} = {(a, Some b)} \<union> {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<noteq> ref

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} = {(a, Some b)} \<union> {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} = {(a, Some b)} \<union> {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref}

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} = {(a, Some b)} \<union> {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref}

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
have "insert_alt (succ_rel (b # list)) (oid, ref) =
           {(p, n) \<in> succ_rel (b # list). p \<noteq> ref} \<union> {(ref, Some oid)} \<union>
           {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
[PROOF STEP]
have "\<exists>n. (ref, n) \<in> succ_rel (b # list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. (ref, n) \<in> succ_rel (b # list)
[PROOF STEP]
using assms(1) True
[PROOF STATE]
proof (prove)
using this:
a \<noteq> ref
\<exists>n. (ref, n) \<in> succ_rel (a # b # list)

goal (1 subgoal):
 1. \<exists>n. (ref, n) \<in> succ_rel (b # list)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. (ref, n) \<in> succ_rel (b # list)

goal (1 subgoal):
 1. insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n. (ref, n) \<in> succ_rel (b # list)

goal (1 subgoal):
 1. insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
have "{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)} =
                 {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)} = {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<noteq> ref

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

goal (2 subgoals):
 1. \<exists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
 2. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert_alt (succ_rel (a # b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)}
{(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} = {(a, Some b)} \<union> {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref}
insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)} = {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insert_alt (succ_rel (a # b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)}
{(p, n). (p, n) \<in> succ_rel (a # b # list) \<and> p \<noteq> ref} = {(a, Some b)} \<union> {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref}
insert_alt (succ_rel (b # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (b # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}
{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (a # b # list)} = {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (b # list)}

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

goal (1 subgoal):
 1. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>n. (ref, n) \<in> succ_rel (a # b # list) \<Longrightarrow> insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>n. (ref, n) \<in> succ_rel (a # b # list)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_rel_insert_head:
  assumes "distinct (ref # list)"
  shows "succ_rel (insert_spec (ref # list) (oid, Some ref)) =
         insert_alt (succ_rel (ref # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
obtain n where ref_in_rel: "(ref, n) \<in> succ_rel (ref # list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. (ref, n) \<in> succ_rel (ref # list) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases list, auto)
[PROOF STATE]
proof (state)
this:
(ref, n) \<in> succ_rel (ref # list)

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ref, n) \<in> succ_rel (ref # list)

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(ref, n) \<in> succ_rel (ref # list)
[PROOF STEP]
have "{(p, n) \<in> succ_rel (ref # list). p \<noteq> ref} = succ_rel list"
[PROOF STATE]
proof (prove)
using this:
(ref, n) \<in> succ_rel (ref # list)

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} = succ_rel list
[PROOF STEP]
using assms succ_rel_rem_head
[PROOF STATE]
proof (prove)
using this:
(ref, n) \<in> succ_rel (ref # list)
distinct (ref # list)
distinct (?x # ?xs) \<Longrightarrow> {(p, n). (p, n) \<in> succ_rel (?x # ?xs) \<and> p \<noteq> ?x} = succ_rel ?xs

goal (1 subgoal):
 1. {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} = succ_rel list
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
{(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} = succ_rel list

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} = succ_rel list

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
have "{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
[PROOF STEP]
have "\<And>nx. (ref, nx) \<in> succ_rel (ref # list) \<Longrightarrow> nx = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nx. (ref, nx) \<in> succ_rel (ref # list) \<Longrightarrow> nx = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (ref # list)

goal (1 subgoal):
 1. \<And>nx. (ref, nx) \<in> succ_rel (ref # list) \<Longrightarrow> nx = n
[PROOF STEP]
by (simp add: succ_rel_functional ref_in_rel)
[PROOF STATE]
proof (state)
this:
(ref, ?nx) \<in> succ_rel (ref # list) \<Longrightarrow> ?nx = n

goal (1 subgoal):
 1. {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
[PROOF STEP]
hence "{(i, n) \<in> succ_rel (ref # list). i = ref} \<subseteq> {(ref, n)}"
[PROOF STATE]
proof (prove)
using this:
(ref, ?nx) \<in> succ_rel (ref # list) \<Longrightarrow> ?nx = n

goal (1 subgoal):
 1. {(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref} \<subseteq> {(ref, n)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref} \<subseteq> {(ref, n)}

goal (1 subgoal):
 1. {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref} \<subseteq> {(ref, n)}

goal (1 subgoal):
 1. {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
[PROOF STEP]
have "{(ref, n)} \<subseteq> {(i, n) \<in> succ_rel (ref # list). i = ref}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(ref, n)} \<subseteq> {(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref}
[PROOF STEP]
by (simp add: ref_in_rel)
[PROOF STATE]
proof (state)
this:
{(ref, n)} \<subseteq> {(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref}

goal (1 subgoal):
 1. {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref} \<subseteq> {(ref, n)}
{(ref, n)} \<subseteq> {(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref} \<subseteq> {(ref, n)}
{(ref, n)} \<subseteq> {(i, n). (i, n) \<in> succ_rel (ref # list) \<and> i = ref}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
have "insert_alt (succ_rel (ref # list)) (oid, ref) =
                   {(p, n) \<in> succ_rel (ref # list). p \<noteq> ref} \<union> {(ref, Some oid)} \<union>
                   {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}
[PROOF STEP]
have "\<exists>n. (ref, n) \<in> succ_rel (ref # list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. (ref, n) \<in> succ_rel (ref # list)
[PROOF STEP]
using ref_in_rel
[PROOF STATE]
proof (prove)
using this:
(ref, n) \<in> succ_rel (ref # list)

goal (1 subgoal):
 1. \<exists>n. (ref, n) \<in> succ_rel (ref # list)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. (ref, n) \<in> succ_rel (ref # list)

goal (1 subgoal):
 1. insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n. (ref, n) \<in> succ_rel (ref # list)

goal (1 subgoal):
 1. insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(ref, n) \<in> succ_rel (ref # list)
{(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} = succ_rel list
{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}
[PROOF STEP]
have "insert_alt (succ_rel (ref # list)) (oid, ref) =
                   succ_rel list \<union> {(ref, Some oid)} \<union> {(oid, n)}"
[PROOF STATE]
proof (prove)
using this:
(ref, n) \<in> succ_rel (ref # list)
{(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} = succ_rel list
{(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)} = {(oid, n)}
insert_alt (succ_rel (ref # list)) (oid, ref) = {(p, n). (p, n) \<in> succ_rel (ref # list) \<and> p \<noteq> ref} \<union> {(ref, Some oid)} \<union> {(i, n). i = oid \<and> (ref, n) \<in> succ_rel (ref # list)}

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

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

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
have "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]
using assms ref_in_rel succ_rel_swap_head
[PROOF STATE]
proof (prove)
using this:
distinct (ref # list)
(ref, n) \<in> succ_rel (ref # list)
\<lbrakk>distinct (?ref # ?list); (?ref, ?n) \<in> succ_rel (?ref # ?list)\<rbrakk> \<Longrightarrow> succ_rel (?oid # ?list) = {(?oid, ?n)} \<union> succ_rel ?list

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

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
hence "succ_rel (ref # oid # list) = {(ref, Some oid), (oid, n)} \<union> succ_rel list"
[PROOF STATE]
proof (prove)
using this:
succ_rel (oid # list) = {(oid, n)} \<union> succ_rel list

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

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert_alt (succ_rel (ref # list)) (oid, ref) = succ_rel list \<union> {(ref, Some oid)} \<union> {(oid, n)}
succ_rel (ref # oid # list) = {(ref, Some oid), (oid, n)} \<union> succ_rel list
[PROOF STEP]
show "succ_rel (insert_spec (ref # list) (oid, Some ref)) =
                   insert_alt (succ_rel (ref # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
insert_alt (succ_rel (ref # list)) (oid, ref) = succ_rel list \<union> {(ref, Some oid)} \<union> {(oid, n)}
succ_rel (ref # oid # list) = {(ref, Some oid), (oid, n)} \<union> succ_rel list

goal (1 subgoal):
 1. succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (ref # list) (oid, Some ref)) = insert_alt (succ_rel (ref # list)) (oid, ref)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_rel_insert_later:
  assumes "succ_rel (insert_spec (b # list) (oid, Some ref)) =
           insert_alt (succ_rel (b # list)) (oid, ref)"
    and "a \<noteq> ref"
    and "distinct (a # b # list)"
  shows "succ_rel (insert_spec (a # b # list) (oid, Some ref)) =
         insert_alt (succ_rel (a # b # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
have "succ_rel (a # b # list) = {(a, Some b)} \<union> succ_rel (b # list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (a # b # list) = {(a, Some b)} \<union> succ_rel (b # list)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
succ_rel (a # b # list) = {(a, Some b)} \<union> succ_rel (b # list)

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
succ_rel (a # b # list) = {(a, Some b)} \<union> succ_rel (b # list)

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
have "insert_spec (a # b # list) (oid, Some ref) =
                 a # (insert_spec (b # list) (oid, Some ref))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (a # b # list) (oid, Some ref) = a # insert_spec (b # list) (oid, Some ref)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
a \<noteq> ref

goal (1 subgoal):
 1. insert_spec (a # b # list) (oid, Some ref) = a # insert_spec (b # list) (oid, Some ref)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_spec (a # b # list) (oid, Some ref) = a # insert_spec (b # list) (oid, Some ref)

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
hence "succ_rel (insert_spec (a # b # list) (oid, Some ref)) =
         {(a, Some b)} \<union> succ_rel (insert_spec (b # list) (oid, Some ref))"
[PROOF STATE]
proof (prove)
using this:
insert_spec (a # b # list) (oid, Some ref) = a # insert_spec (b # list) (oid, Some ref)

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

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
hence "succ_rel (insert_spec (a # b # list) (oid, Some ref)) =
         {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
succ_rel (insert_spec (a # b # list) (oid, Some ref)) = {(a, Some b)} \<union> succ_rel (insert_spec (b # list) (oid, Some ref))

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
succ_rel (insert_spec (a # b # list) (oid, Some ref)) = {(a, Some b)} \<union> succ_rel (insert_spec (b # list) (oid, Some ref))
succ_rel (insert_spec (b # list) (oid, Some ref)) = insert_alt (succ_rel (b # list)) (oid, ref)

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

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (a # b # list) (oid, Some ref)) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
have "insert_alt (succ_rel (a # b # list)) (oid, ref) =
                 {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (succ_rel (a # b # list)) (oid, ref) = {(a, Some b)} \<union> insert_alt (succ_rel (b # list)) (oid, ref)
[PROOF STEP]
using succ_rel_insert_alt assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<noteq> ?ref; distinct (?oid # ?a # ?b # ?list)\<rbrakk> \<Longrightarrow> insert_alt (succ_rel (?a # ?b # ?list)) (?oid, ?ref) = {(?a, Some ?b)} \<union> insert_alt (succ_rel (?b # ?list)) (?oid, ?ref)
a \<noteq> ref

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

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

goal (1 subgoal):
 1. succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (a # b # list) (oid, Some ref)) = insert_alt (succ_rel (a # b # list)) (oid, ref)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_rel_insert_Some:
  assumes "distinct list"
  shows "succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct list

goal (1 subgoal):
 1. succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
[PROOF STEP]
proof(induction list)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct [] \<Longrightarrow> succ_rel (insert_spec [] (oid, Some ref)) = insert_alt (succ_rel []) (oid, ref)
 2. \<And>a list. \<lbrakk>distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref); distinct (a # list)\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
distinct []

goal (2 subgoals):
 1. distinct [] \<Longrightarrow> succ_rel (insert_spec [] (oid, Some ref)) = insert_alt (succ_rel []) (oid, ref)
 2. \<And>a list. \<lbrakk>distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref); distinct (a # list)\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct []
[PROOF STEP]
show "succ_rel (insert_spec [] (oid, Some ref)) = insert_alt (succ_rel []) (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
distinct []

goal (1 subgoal):
 1. succ_rel (insert_spec [] (oid, Some ref)) = insert_alt (succ_rel []) (oid, ref)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec [] (oid, Some ref)) = insert_alt (succ_rel []) (oid, ref)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref); distinct (a # list)\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref); distinct (a # list)\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
case (Cons a list)
[PROOF STATE]
proof (state)
this:
distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
distinct (a # list)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref); distinct (a # list)\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
hence "distinct (a # list)"
[PROOF STATE]
proof (prove)
using this:
distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
distinct (a # list)

goal (1 subgoal):
 1. distinct (a # list)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (a # list)

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref); distinct (a # list)\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (a # list)
[PROOF STEP]
show "succ_rel (insert_spec (a # list) (oid, Some ref)) =
             insert_alt (succ_rel (a # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
distinct (a # list)

goal (1 subgoal):
 1. succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
proof(cases "a = ref")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct (a # list); a = ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
 2. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = ref

goal (2 subgoals):
 1. \<lbrakk>distinct (a # list); a = ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
 2. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = ref
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = ref

goal (1 subgoal):
 1. succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
using succ_rel_insert_head \<open>distinct (a # list)\<close>
[PROOF STATE]
proof (prove)
using this:
a = ref
distinct (?ref # ?list) \<Longrightarrow> succ_rel (insert_spec (?ref # ?list) (?oid, Some ?ref)) = insert_alt (succ_rel (?ref # ?list)) (?oid, ?ref)
distinct (a # list)

goal (1 subgoal):
 1. succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)

goal (1 subgoal):
 1. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> ref

goal (1 subgoal):
 1. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
hence "a \<noteq> ref"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> ref

goal (1 subgoal):
 1. a \<noteq> ref
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<noteq> ref

goal (1 subgoal):
 1. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<noteq> ref

goal (1 subgoal):
 1. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
have "succ_rel (insert_spec list (oid, Some ref)) =
                   insert_alt (succ_rel list) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
[PROOF STEP]
using Cons.IH Cons.prems
[PROOF STATE]
proof (prove)
using this:
distinct list \<Longrightarrow> succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
distinct (a # list)

goal (1 subgoal):
 1. succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)

goal (1 subgoal):
 1. \<lbrakk>distinct (a # list); a \<noteq> ref\<rbrakk> \<Longrightarrow> succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> ref
succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)
[PROOF STEP]
show "succ_rel (insert_spec (a # list) (oid, Some ref)) =
                     insert_alt (succ_rel (a # list)) (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> ref
succ_rel (insert_spec list (oid, Some ref)) = insert_alt (succ_rel list) (oid, ref)

goal (1 subgoal):
 1. succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)
[PROOF STEP]
by (cases list, force, metis Cons.prems succ_rel_insert_later)
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (a # list) (oid, Some ref)) = insert_alt (succ_rel (a # list)) (oid, ref)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem insert_alt_equivalent:
  assumes "insert_ops ops"
    and "head \<notin> fst ` set ops"
    and "\<And>r. Some r \<in> snd ` set ops \<Longrightarrow> r \<noteq> head"
  shows "succ_rel (head # interp_ins ops) = interp_alt head ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (head # interp_ins ops) = interp_alt head ops
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
head \<notin> fst ` set ops
Some ?r \<in> snd ` set ops \<Longrightarrow> ?r \<noteq> head

goal (1 subgoal):
 1. succ_rel (head # interp_ins ops) = interp_alt head ops
[PROOF STEP]
proof(induction ops rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>insert_ops []; head \<notin> fst ` set []; \<And>r. Some r \<in> snd ` set [] \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins []) = interp_alt head []
 2. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops []
head \<notin> fst ` set []
Some ?r \<in> snd ` set [] \<Longrightarrow> ?r \<noteq> head

goal (2 subgoals):
 1. \<lbrakk>insert_ops []; head \<notin> fst ` set []; \<And>r. Some r \<in> snd ` set [] \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins []) = interp_alt head []
 2. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops []
head \<notin> fst ` set []
Some ?r \<in> snd ` set [] \<Longrightarrow> ?r \<noteq> head
[PROOF STEP]
show "succ_rel (head # interp_ins []) = interp_alt head []"
[PROOF STATE]
proof (prove)
using this:
insert_ops []
head \<notin> fst ` set []
Some ?r \<in> snd ` set [] \<Longrightarrow> ?r \<noteq> head

goal (1 subgoal):
 1. succ_rel (head # interp_ins []) = interp_alt head []
[PROOF STEP]
by (simp add: interp_ins_def interp_alt_def)
[PROOF STATE]
proof (state)
this:
succ_rel (head # interp_ins []) = interp_alt head []

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs
insert_ops (xs @ [x])
head \<notin> fst ` set (xs @ [x])
Some ?r \<in> snd ` set (xs @ [x]) \<Longrightarrow> ?r \<noteq> head

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have IH: "succ_rel (head # interp_ins xs) = interp_alt head xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (head # interp_ins xs) = interp_alt head xs
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs
insert_ops (xs @ [x])
head \<notin> fst ` set (xs @ [x])
Some ?r \<in> snd ` set (xs @ [x]) \<Longrightarrow> ?r \<noteq> head

goal (1 subgoal):
 1. succ_rel (head # interp_ins xs) = interp_alt head xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ_rel (head # interp_ins xs) = interp_alt head xs

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have distinct_list: "distinct (head # interp_ins xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (head # interp_ins xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (head # interp_ins xs)
[PROOF STEP]
have "distinct (interp_ins xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (interp_ins xs)
[PROOF STEP]
using interp_ins_distinct snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
insert_ops ?op_list \<Longrightarrow> distinct (interp_ins ?op_list)
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. distinct (head # interp_ins xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (interp_ins xs)

goal (1 subgoal):
 1. distinct (head # interp_ins xs)
[PROOF STEP]
have "set (interp_ins xs) \<subseteq> fst ` set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (interp_ins xs) \<subseteq> fst ` set xs
[PROOF STEP]
using interp_ins_subset snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
set (interp_ins ?op_list) \<subseteq> set (map fst ?op_list)
insert_ops (xs @ [x])

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

goal (1 subgoal):
 1. distinct (head # interp_ins xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (interp_ins xs)
set (interp_ins xs) \<subseteq> fst ` set xs
[PROOF STEP]
show "distinct (head # interp_ins xs)"
[PROOF STATE]
proof (prove)
using this:
distinct (interp_ins xs)
set (interp_ins xs) \<subseteq> fst ` set xs

goal (1 subgoal):
 1. distinct (head # interp_ins xs)
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
distinct (interp_ins xs)
set (interp_ins xs) \<subseteq> fst ` set xs
head \<notin> fst ` set (xs @ [x])

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (head # interp_ins xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
obtain oid r where x_pair: "x = (oid, r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid r. x = (oid, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = (oid, r)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>insert_ops xs; head \<notin> fst ` set xs; \<And>r. Some r \<in> snd ` set xs \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins xs) = interp_alt head xs; insert_ops (xs @ [x]); head \<notin> fst ` set (xs @ [x]); \<And>r. Some r \<in> snd ` set (xs @ [x]) \<Longrightarrow> r \<noteq> head\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (oid, r)
[PROOF STEP]
show "succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])"
[PROOF STATE]
proof (prove)
using this:
x = (oid, r)

goal (1 subgoal):
 1. succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
proof(cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
r = None

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, head)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, head)
[PROOF STEP]
by (simp add: interp_alt_def None x_pair)
[PROOF STATE]
proof (state)
this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, head)

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, head)

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (interp_alt head xs) (oid, head) = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)
[PROOF STEP]
by (simp add: IH)
[PROOF STATE]
proof (state)
this:
insert_alt (interp_alt head xs) (oid, head) = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_alt (interp_alt head xs) (oid, head) = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (succ_rel (head # interp_ins xs)) (oid, head) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))
[PROOF STEP]
using distinct_list succ_rel_insert_Some
[PROOF STATE]
proof (prove)
using this:
distinct (head # interp_ins xs)
distinct ?list \<Longrightarrow> succ_rel (insert_spec ?list (?oid, Some ?ref)) = insert_alt (succ_rel ?list) (?oid, ?ref)

goal (1 subgoal):
 1. insert_alt (succ_rel (head # interp_ins xs)) (oid, head) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (head # interp_ins xs)) (oid, head) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (head # interp_ins xs)) (oid, head) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = succ_rel (head # (insert_spec (interp_ins xs) (oid, None)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (insert_spec (head # interp_ins xs) (oid, Some head)) = succ_rel (head # insert_spec (interp_ins xs) (oid, None))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (head # interp_ins xs) (oid, Some head)) = succ_rel (head # insert_spec (interp_ins xs) (oid, None))

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (head # interp_ins xs) (oid, Some head)) = succ_rel (head # insert_spec (interp_ins xs) (oid, None))

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = succ_rel (head # (interp_ins (xs @ [x])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (head # insert_spec (interp_ins xs) (oid, None)) = succ_rel (head # interp_ins (xs @ [x]))
[PROOF STEP]
by (simp add: interp_ins_tail_unfold None x_pair)
[PROOF STATE]
proof (state)
this:
succ_rel (head # insert_spec (interp_ins xs) (oid, None)) = succ_rel (head # interp_ins (xs @ [x]))

goal (2 subgoals):
 1. \<lbrakk>x = (oid, r); r = None\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
 2. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, head)
insert_alt (interp_alt head xs) (oid, head) = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)
insert_alt (succ_rel (head # interp_ins xs)) (oid, head) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))
succ_rel (insert_spec (head # interp_ins xs) (oid, Some head)) = succ_rel (head # insert_spec (interp_ins xs) (oid, None))
succ_rel (head # insert_spec (interp_ins xs) (oid, None)) = succ_rel (head # interp_ins (xs @ [x]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, head)
insert_alt (interp_alt head xs) (oid, head) = insert_alt (succ_rel (head # interp_ins xs)) (oid, head)
insert_alt (succ_rel (head # interp_ins xs)) (oid, head) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some head))
succ_rel (insert_spec (head # interp_ins xs) (oid, Some head)) = succ_rel (head # insert_spec (interp_ins xs) (oid, None))
succ_rel (head # insert_spec (interp_ins xs) (oid, None)) = succ_rel (head # interp_ins (xs @ [x]))

goal (1 subgoal):
 1. succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
case (Some ref)
[PROOF STATE]
proof (state)
this:
r = Some ref

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "ref \<noteq> head"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref \<noteq> head
[PROOF STEP]
by (simp add: Some snoc.prems(3) x_pair)
[PROOF STATE]
proof (state)
this:
ref \<noteq> head

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, ref)
[PROOF STEP]
by (simp add: interp_alt_def Some x_pair)
[PROOF STATE]
proof (state)
this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, ref)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, ref)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = insert_alt (succ_rel (head # interp_ins xs)) (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (interp_alt head xs) (oid, ref) = insert_alt (succ_rel (head # interp_ins xs)) (oid, ref)
[PROOF STEP]
by (simp add: IH)
[PROOF STATE]
proof (state)
this:
insert_alt (interp_alt head xs) (oid, ref) = insert_alt (succ_rel (head # interp_ins xs)) (oid, ref)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_alt (interp_alt head xs) (oid, ref) = insert_alt (succ_rel (head # interp_ins xs)) (oid, ref)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_alt (succ_rel (head # interp_ins xs)) (oid, ref) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))
[PROOF STEP]
using distinct_list succ_rel_insert_Some
[PROOF STATE]
proof (prove)
using this:
distinct (head # interp_ins xs)
distinct ?list \<Longrightarrow> succ_rel (insert_spec ?list (?oid, Some ?ref)) = insert_alt (succ_rel ?list) (?oid, ?ref)

goal (1 subgoal):
 1. insert_alt (succ_rel (head # interp_ins xs)) (oid, ref) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (head # interp_ins xs)) (oid, ref) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_alt (succ_rel (head # interp_ins xs)) (oid, ref) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = succ_rel (head # (insert_spec (interp_ins xs) (oid, Some ref)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref)) = succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref))
[PROOF STEP]
using \<open>ref \<noteq> head\<close>
[PROOF STATE]
proof (prove)
using this:
ref \<noteq> head

goal (1 subgoal):
 1. succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref)) = succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref)) = succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref)) = succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
have "... = succ_rel (head # (interp_ins (xs @ [x])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref)) = succ_rel (head # interp_ins (xs @ [x]))
[PROOF STEP]
by (simp add: interp_ins_tail_unfold Some x_pair)
[PROOF STATE]
proof (state)
this:
succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref)) = succ_rel (head # interp_ins (xs @ [x]))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = (oid, r); r = Some a\<rbrakk> \<Longrightarrow> succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, ref)
insert_alt (interp_alt head xs) (oid, ref) = insert_alt (succ_rel (head # interp_ins xs)) (oid, ref)
insert_alt (succ_rel (head # interp_ins xs)) (oid, ref) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))
succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref)) = succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref))
succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref)) = succ_rel (head # interp_ins (xs @ [x]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp_alt head (xs @ [x]) = insert_alt (interp_alt head xs) (oid, ref)
insert_alt (interp_alt head xs) (oid, ref) = insert_alt (succ_rel (head # interp_ins xs)) (oid, ref)
insert_alt (succ_rel (head # interp_ins xs)) (oid, ref) = succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref))
succ_rel (insert_spec (head # interp_ins xs) (oid, Some ref)) = succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref))
succ_rel (head # insert_spec (interp_ins xs) (oid, Some ref)) = succ_rel (head # interp_ins (xs @ [x]))

goal (1 subgoal):
 1. succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
succ_rel (head # interp_ins (xs @ [x])) = interp_alt head (xs @ [x])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_orderI:
  assumes "interp_ins ops = xs @ [x] @ ys @ [y] @ zs"
  shows "list_order ops x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order ops x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = xs @ [x] @ ys @ [y] @ zs

goal (1 subgoal):
 1. list_order ops x y
[PROOF STEP]
by (auto simp add: list_order_def)


[STATEMENT]
lemma list_orderE:
  assumes "list_order ops x y"
  shows "\<exists>xs ys zs. interp_ins ops = xs @ [x] @ ys @ [y] @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins ops = xs @ [x] @ ys @ [y] @ zs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_order ops x y

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins ops = xs @ [x] @ ys @ [y] @ zs
[PROOF STEP]
by (auto simp add: list_order_def)


[STATEMENT]
lemma list_order_memb1:
  assumes "list_order ops x y"
  shows "x \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (interp_ins ops)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_order ops x y

goal (1 subgoal):
 1. x \<in> set (interp_ins ops)
[PROOF STEP]
by (auto simp add: list_order_def)


[STATEMENT]
lemma list_order_memb2:
  assumes "list_order ops x y"
  shows "y \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> set (interp_ins ops)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_order ops x y

goal (1 subgoal):
 1. y \<in> set (interp_ins ops)
[PROOF STEP]
by (auto simp add: list_order_def)


[STATEMENT]
lemma list_order_trans:
  assumes "insert_ops op_list"
    and "list_order op_list x y"
    and "list_order op_list y z"
  shows "list_order op_list x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
obtain xxs xys xzs where 1: "interp_ins op_list = (xxs@[x]@xys)@(y#xzs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xxs xys xzs. interp_ins op_list = (xxs @ [x] @ xys) @ y # xzs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops op_list
list_order op_list x y
list_order op_list y z

goal (1 subgoal):
 1. (\<And>xxs xys xzs. interp_ins op_list = (xxs @ [x] @ xys) @ y # xzs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: list_order_def interp_ins_def)
[PROOF STATE]
proof (state)
this:
interp_ins op_list = (xxs @ [x] @ xys) @ y # xzs

goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
obtain yxs yys yzs where 2: "interp_ins op_list = yxs@y#(yys@[z]@yzs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>yxs yys yzs. interp_ins op_list = yxs @ y # yys @ [z] @ yzs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops op_list
list_order op_list x y
list_order op_list y z

goal (1 subgoal):
 1. (\<And>yxs yys yzs. interp_ins op_list = yxs @ y # yys @ [z] @ yzs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: list_order_def interp_ins_def)
[PROOF STATE]
proof (state)
this:
interp_ins op_list = yxs @ y # yys @ [z] @ yzs

goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
have 3: "distinct (interp_ins op_list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (interp_ins op_list)
[PROOF STEP]
using assms interp_ins_distinct
[PROOF STATE]
proof (prove)
using this:
insert_ops op_list
list_order op_list x y
list_order op_list y z
insert_ops ?op_list \<Longrightarrow> distinct (interp_ins ?op_list)

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

goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
hence "xzs = yys@[z]@yzs"
[PROOF STATE]
proof (prove)
using this:
distinct (interp_ins op_list)

goal (1 subgoal):
 1. xzs = yys @ [z] @ yzs
[PROOF STEP]
using distinct_list_split[OF 3, OF 2, OF 1]
[PROOF STATE]
proof (prove)
using this:
distinct (interp_ins op_list)
yxs = xxs @ [x] @ xys \<and> yys @ [z] @ yzs = xzs

goal (1 subgoal):
 1. xzs = yys @ [z] @ yzs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xzs = yys @ [z] @ yzs

goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
hence "interp_ins op_list = xxs@[x]@xys@[y]@yys@[z]@yzs"
[PROOF STATE]
proof (prove)
using this:
xzs = yys @ [z] @ yzs

goal (1 subgoal):
 1. interp_ins op_list = xxs @ [x] @ xys @ [y] @ yys @ [z] @ yzs
[PROOF STEP]
using 1 2 3
[PROOF STATE]
proof (prove)
using this:
xzs = yys @ [z] @ yzs
interp_ins op_list = (xxs @ [x] @ xys) @ y # xzs
interp_ins op_list = yxs @ y # yys @ [z] @ yzs
distinct (interp_ins op_list)

goal (1 subgoal):
 1. interp_ins op_list = xxs @ [x] @ xys @ [y] @ yys @ [z] @ yzs
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
interp_ins op_list = xxs @ [x] @ xys @ [y] @ yys @ [z] @ yzs

goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
thus "list_order op_list x z"
[PROOF STATE]
proof (prove)
using this:
interp_ins op_list = xxs @ [x] @ xys @ [y] @ yys @ [z] @ yzs

goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
interp_ins op_list = xxs @ [x] @ xys @ [y] @ yys @ [z] @ yzs
insert_ops op_list
list_order op_list x y
list_order op_list y z

goal (1 subgoal):
 1. list_order op_list x z
[PROOF STEP]
by (metis append.assoc list_orderI)
[PROOF STATE]
proof (state)
this:
list_order op_list x z

goal:
No subgoals!
[PROOF STEP]
qed