[STATEMENT]
lemma insert_preserves_order:
  assumes "insert_ops ops" and "insert_ops rest"
    and "rest = before @ after"
    and "ops  = before @ (oid, ref) # after"
  shows "\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
insert_ops rest
rest = before @ after
ops = before @ (oid, ref) # after

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
proof(induction after arbitrary: rest ops rule: List.rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ []; ops = before @ [(oid, ref)]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops ops
insert_ops rest
rest = before @ []
ops = before @ [(oid, ref)]

goal (2 subgoals):
 1. \<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ []; ops = before @ [(oid, ref)]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops ops
insert_ops rest
rest = before @ []
ops = before @ [(oid, ref)]
[PROOF STEP]
have 1: "interp_ins ops = insert_spec (interp_ins before) (oid, ref)"
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
insert_ops rest
rest = before @ []
ops = before @ [(oid, ref)]

goal (1 subgoal):
 1. interp_ins ops = insert_spec (interp_ins before) (oid, ref)
[PROOF STEP]
by (simp add: interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins ops = insert_spec (interp_ins before) (oid, ref)

goal (2 subgoals):
 1. \<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ []; ops = before @ [(oid, ref)]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins ops = insert_spec (interp_ins before) (oid, ref)
[PROOF STEP]
show "\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs"
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = insert_spec (interp_ins before) (oid, ref)

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
proof(cases ref)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
ref = None

goal (2 subgoals):
 1. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
hence "interp_ins rest = [] @ (interp_ins before) \<and>
           interp_ins ops = [] @ [oid] @ (interp_ins before)"
[PROOF STATE]
proof (prove)
using this:
ref = None

goal (1 subgoal):
 1. interp_ins rest = [] @ interp_ins before \<and> interp_ins ops = [] @ [oid] @ interp_ins before
[PROOF STEP]
using 1 Nil.prems(3)
[PROOF STATE]
proof (prove)
using this:
ref = None
interp_ins ops = insert_spec (interp_ins before) (oid, ref)
rest = before @ []

goal (1 subgoal):
 1. interp_ins rest = [] @ interp_ins before \<and> interp_ins ops = [] @ [oid] @ interp_ins before
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interp_ins rest = [] @ interp_ins before \<and> interp_ins ops = [] @ [oid] @ interp_ins before

goal (2 subgoals):
 1. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins rest = [] @ interp_ins before \<and> interp_ins ops = [] @ [oid] @ interp_ins before
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp_ins rest = [] @ interp_ins before \<and> interp_ins ops = [] @ [oid] @ interp_ins before

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
ref = Some a

goal (1 subgoal):
 1. \<And>a. \<lbrakk>interp_ins ops = insert_spec (interp_ins before) (oid, ref); ref = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ref = Some a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ref = Some a

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
proof(cases "a \<in> set (interp_ins before)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ref = Some a; a \<in> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> set (interp_ins before)

goal (2 subgoals):
 1. \<lbrakk>ref = Some a; a \<in> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set (interp_ins before)
[PROOF STEP]
obtain xs ys where "interp_ins before = xs @ ys \<and>
          insert_spec (interp_ins before) (oid, ref) = xs @ oid # ys"
[PROOF STATE]
proof (prove)
using this:
a \<in> set (interp_ins before)

goal (1 subgoal):
 1. (\<And>xs ys. interp_ins before = xs @ ys \<and> insert_spec (interp_ins before) (oid, ref) = xs @ oid # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert_somewhere Some
[PROOF STATE]
proof (prove)
using this:
a \<in> set (interp_ins before)
?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 a

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

goal (2 subgoals):
 1. \<lbrakk>ref = Some a; a \<in> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
hence "interp_ins rest = xs @ ys \<and> interp_ins ops = xs @ [oid] @ ys"
[PROOF STATE]
proof (prove)
using this:
interp_ins before = xs @ ys \<and> insert_spec (interp_ins before) (oid, ref) = xs @ oid # ys

goal (1 subgoal):
 1. interp_ins rest = xs @ ys \<and> interp_ins ops = xs @ [oid] @ ys
[PROOF STEP]
using 1 Nil.prems(3)
[PROOF STATE]
proof (prove)
using this:
interp_ins before = xs @ ys \<and> insert_spec (interp_ins before) (oid, ref) = xs @ oid # ys
interp_ins ops = insert_spec (interp_ins before) (oid, ref)
rest = before @ []

goal (1 subgoal):
 1. interp_ins rest = xs @ ys \<and> interp_ins ops = xs @ [oid] @ ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
interp_ins rest = xs @ ys \<and> interp_ins ops = xs @ [oid] @ ys

goal (2 subgoals):
 1. \<lbrakk>ref = Some a; a \<in> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins rest = xs @ ys \<and> interp_ins ops = xs @ [oid] @ ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp_ins rest = xs @ ys \<and> interp_ins ops = xs @ [oid] @ ys

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal (1 subgoal):
 1. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> set (interp_ins before)

goal (1 subgoal):
 1. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
hence "interp_ins ops = (interp_ins rest) @ [] @ []"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set (interp_ins before)

goal (1 subgoal):
 1. interp_ins ops = interp_ins rest @ [] @ []
[PROOF STEP]
using insert_spec_nonex 1 Nil.prems(3) Some
[PROOF STATE]
proof (prove)
using this:
a \<notin> set (interp_ins before)
?ref \<notin> set ?xs \<Longrightarrow> insert_spec ?xs (?oid, Some ?ref) = ?xs
interp_ins ops = insert_spec (interp_ins before) (oid, ref)
rest = before @ []
ref = Some a

goal (1 subgoal):
 1. interp_ins ops = interp_ins rest @ [] @ []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interp_ins ops = interp_ins rest @ [] @ []

goal (1 subgoal):
 1. \<lbrakk>ref = Some a; a \<notin> set (interp_ins before)\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins ops = interp_ins rest @ [] @ []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp_ins ops = interp_ins rest @ [] @ []

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal (1 subgoal):
 1. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case (snoc oper op_list)
[PROOF STATE]
proof (state)
this:
\<lbrakk>insert_ops ?ops; insert_ops ?rest; ?rest = before @ op_list; ?ops = before @ (oid, ref) # op_list\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins ?rest = xs @ zs \<and> interp_ins ?ops = xs @ ys @ zs
insert_ops ops
insert_ops rest
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]

goal (1 subgoal):
 1. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>insert_ops ?ops; insert_ops ?rest; ?rest = before @ op_list; ?ops = before @ (oid, ref) # op_list\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins ?rest = xs @ zs \<and> interp_ins ?ops = xs @ ys @ zs
insert_ops ops
insert_ops rest
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]
[PROOF STEP]
have "insert_ops ((before @ (oid, ref) # op_list) @ [oper])"
    and "insert_ops ((before @ op_list) @ [oper])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert_ops ?ops; insert_ops ?rest; ?rest = before @ op_list; ?ops = before @ (oid, ref) # op_list\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins ?rest = xs @ zs \<and> interp_ins ?ops = xs @ ys @ zs
insert_ops ops
insert_ops rest
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]

goal (1 subgoal):
 1. insert_ops ((before @ (oid, ref) # op_list) @ [oper]) &&& insert_ops ((before @ op_list) @ [oper])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_ops ((before @ (oid, ref) # op_list) @ [oper])
insert_ops ((before @ op_list) @ [oper])

goal (1 subgoal):
 1. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops ((before @ (oid, ref) # op_list) @ [oper])
insert_ops ((before @ op_list) @ [oper])
[PROOF STEP]
have ops1: "insert_ops (before @ op_list)"
    and ops2: "insert_ops (before @ (oid, ref) # op_list)"
[PROOF STATE]
proof (prove)
using this:
insert_ops ((before @ (oid, ref) # op_list) @ [oper])
insert_ops ((before @ op_list) @ [oper])

goal (1 subgoal):
 1. insert_ops (before @ op_list) &&& insert_ops (before @ (oid, ref) # op_list)
[PROOF STEP]
using insert_ops_appendD
[PROOF STATE]
proof (prove)
using this:
insert_ops ((before @ (oid, ref) # op_list) @ [oper])
insert_ops ((before @ op_list) @ [oper])
insert_ops (?xs @ ?ys) \<Longrightarrow> insert_ops ?xs

goal (1 subgoal):
 1. insert_ops (before @ op_list) &&& insert_ops (before @ (oid, ref) # op_list)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
insert_ops (before @ op_list)
insert_ops (before @ (oid, ref) # op_list)

goal (1 subgoal):
 1. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops (before @ op_list)
insert_ops (before @ (oid, ref) # op_list)
[PROOF STEP]
obtain xs ys zs where IH1: "interp_ins (before @ op_list) = xs @ zs"
    and IH2: "interp_ins (before @ (oid, ref) # op_list) = xs @ ys @ zs"
[PROOF STATE]
proof (prove)
using this:
insert_ops (before @ op_list)
insert_ops (before @ (oid, ref) # op_list)

goal (1 subgoal):
 1. (\<And>xs zs ys. \<lbrakk>interp_ins (before @ op_list) = xs @ zs; interp_ins (before @ (oid, ref) # op_list) = xs @ ys @ zs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
insert_ops (before @ op_list)
insert_ops (before @ (oid, ref) # op_list)
\<lbrakk>insert_ops ?ops; insert_ops ?rest; ?rest = before @ op_list; ?ops = before @ (oid, ref) # op_list\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins ?rest = xs @ zs \<and> interp_ins ?ops = xs @ ys @ zs

goal (1 subgoal):
 1. (\<And>xs zs ys. \<lbrakk>interp_ins (before @ op_list) = xs @ zs; interp_ins (before @ (oid, ref) # op_list) = xs @ ys @ zs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
interp_ins (before @ op_list) = xs @ zs
interp_ins (before @ (oid, ref) # op_list) = xs @ ys @ zs

goal (1 subgoal):
 1. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
obtain i2 r2 where "oper = (i2, r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i2 r2. oper = (i2, r2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
oper = (i2, r2)

goal (1 subgoal):
 1. \<And>x xs rest ops. \<lbrakk>\<And>rest ops. \<lbrakk>insert_ops ops; insert_ops rest; rest = before @ xs; ops = before @ (oid, ref) # xs\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs; insert_ops ops; insert_ops rest; rest = before @ xs @ [x]; ops = before @ (oid, ref) # xs @ [x]\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
oper = (i2, r2)
[PROOF STEP]
show "\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs"
[PROOF STATE]
proof (prove)
using this:
oper = (i2, r2)

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
proof(cases r2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>oper = (i2, r2); r2 = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
r2 = None

goal (2 subgoals):
 1. \<lbrakk>oper = (i2, r2); r2 = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
hence "interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs"
[PROOF STATE]
proof (prove)
using this:
r2 = None

goal (1 subgoal):
 1. interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs
[PROOF STEP]
by (metis IH1 \<open>oper = (i2, r2)\<close> append.assoc append_Cons insert_spec.simps(1)
          interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs

goal (2 subgoals):
 1. \<lbrakk>oper = (i2, r2); r2 = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs

goal (2 subgoals):
 1. \<lbrakk>oper = (i2, r2); r2 = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
have "interp_ins (before @ (oid, ref) # op_list @ [oper]) = (i2 # xs) @ ys @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins (before @ (oid, ref) # op_list @ [oper]) = (i2 # xs) @ ys @ zs
[PROOF STEP]
by (metis IH2 None \<open>oper = (i2, r2)\<close> append.assoc append_Cons insert_spec.simps(1)
          interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins (before @ (oid, ref) # op_list @ [oper]) = (i2 # xs) @ ys @ zs

goal (2 subgoals):
 1. \<lbrakk>oper = (i2, r2); r2 = None\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs
interp_ins (before @ (oid, ref) # op_list @ [oper]) = (i2 # xs) @ ys @ zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs
interp_ins (before @ (oid, ref) # op_list @ [oper]) = (i2 # xs) @ ys @ zs

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
using snoc.prems(3) snoc.prems(4)
[PROOF STATE]
proof (prove)
using this:
interp_ins (before @ op_list @ [oper]) = (i2 # xs) @ zs
interp_ins (before @ (oid, ref) # op_list @ [oper]) = (i2 # xs) @ ys @ zs
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case (Some r)
[PROOF STATE]
proof (state)
this:
r2 = Some r

goal (1 subgoal):
 1. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r2 = Some r
[PROOF STEP]
have 1: "interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) =
                  insert_spec (xs @ ys @ zs) (i2, Some r)"
[PROOF STATE]
proof (prove)
using this:
r2 = Some r

goal (1 subgoal):
 1. interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) = insert_spec (xs @ ys @ zs) (i2, Some r)
[PROOF STEP]
by (metis IH2 append.assoc append_Cons interp_ins_tail_unfold)
[PROOF STATE]
proof (state)
this:
interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) = insert_spec (xs @ ys @ zs) (i2, Some r)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
have 2: "interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)
[PROOF STEP]
by (metis IH1 append.assoc interp_ins_tail_unfold Some)
[PROOF STATE]
proof (state)
this:
interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
consider (r_xs) "r \<in> set xs" | (r_ys) "r \<in> set ys" | (r_zs) "r \<in> set zs" |
      (r_nonex) "r \<notin> set (xs @ ys @ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set xs \<Longrightarrow> thesis; r \<in> set ys \<Longrightarrow> thesis; r \<in> set zs \<Longrightarrow> thesis; r \<notin> set (xs @ ys @ zs) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>r \<in> set xs \<Longrightarrow> ?thesis; r \<in> set ys \<Longrightarrow> ?thesis; r \<in> set zs \<Longrightarrow> ?thesis; r \<notin> set (xs @ ys @ zs) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a. \<lbrakk>oper = (i2, r2); r2 = Some a\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>r \<in> set xs \<Longrightarrow> ?thesis; r \<in> set ys \<Longrightarrow> ?thesis; r \<in> set zs \<Longrightarrow> ?thesis; r \<notin> set (xs @ ys @ zs) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r \<in> set xs \<Longrightarrow> ?thesis; r \<in> set ys \<Longrightarrow> ?thesis; r \<in> set zs \<Longrightarrow> ?thesis; r \<notin> set (xs @ ys @ zs) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. r \<in> set xs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 4. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case r_xs
[PROOF STATE]
proof (state)
this:
r \<in> set xs

goal (4 subgoals):
 1. r \<in> set xs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 4. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
r \<in> set xs
[PROOF STEP]
have "insert_spec (xs @ ys @ zs) (i2, Some r) =
                      (insert_spec xs (i2, Some r)) @ ys @ zs"
[PROOF STATE]
proof (prove)
using this:
r \<in> set xs

goal (1 subgoal):
 1. insert_spec (xs @ ys @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ ys @ zs
[PROOF STEP]
by (meson insert_first_part)
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ ys @ zs

goal (4 subgoals):
 1. r \<in> set xs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 4. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ ys @ zs

goal (4 subgoals):
 1. r \<in> set xs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 4. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
have "insert_spec (xs @ zs) (i2, Some r) = (insert_spec xs (i2, Some r)) @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (xs @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ zs
[PROOF STEP]
by (meson r_xs insert_first_part)
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ zs

goal (4 subgoals):
 1. r \<in> set xs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 4. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert_spec (xs @ ys @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ ys @ zs
insert_spec (xs @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insert_spec (xs @ ys @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ ys @ zs
insert_spec (xs @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ zs

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
using 1 2 \<open>oper = (i2, r2)\<close> snoc.prems
[PROOF STATE]
proof (prove)
using this:
insert_spec (xs @ ys @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ ys @ zs
insert_spec (xs @ zs) (i2, Some r) = insert_spec xs (i2, Some r) @ zs
interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) = insert_spec (xs @ ys @ zs) (i2, Some r)
interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)
oper = (i2, r2)
insert_ops ops
insert_ops rest
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case r_ys
[PROOF STATE]
proof (state)
this:
r \<in> set ys

goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
hence "r \<notin> set xs" and "r \<notin> set zs"
[PROOF STATE]
proof (prove)
using this:
r \<in> set ys

goal (1 subgoal):
 1. r \<notin> set xs &&& r \<notin> set zs
[PROOF STEP]
using IH2 ops2 interp_ins_distinct
[PROOF STATE]
proof (prove)
using this:
r \<in> set ys
interp_ins (before @ (oid, ref) # op_list) = xs @ ys @ zs
insert_ops (before @ (oid, ref) # op_list)
insert_ops ?op_list \<Longrightarrow> distinct (interp_ins ?op_list)

goal (1 subgoal):
 1. r \<notin> set xs &&& r \<notin> set zs
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
r \<notin> set xs
r \<notin> set zs

goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<notin> set xs
r \<notin> set zs

goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
r \<notin> set xs
r \<notin> set zs
[PROOF STEP]
have "insert_spec (xs @ ys @ zs) (i2, Some r) =
                               xs @ (insert_spec ys (i2, Some r)) @ zs"
[PROOF STATE]
proof (prove)
using this:
r \<notin> set xs
r \<notin> set zs

goal (1 subgoal):
 1. insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ insert_spec ys (i2, Some r) @ zs
[PROOF STEP]
using insert_first_part insert_second_part insert_spec_nonex
[PROOF STATE]
proof (prove)
using this:
r \<notin> set xs
r \<notin> set zs
?ref = None \<or> ?ref = Some ?r \<and> ?r \<in> set ?xs \<Longrightarrow> insert_spec (?xs @ ?ys) (?oid, ?ref) = insert_spec ?xs (?oid, ?ref) @ ?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)
?ref \<notin> set ?xs \<Longrightarrow> insert_spec ?xs (?oid, Some ?ref) = ?xs

goal (1 subgoal):
 1. insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ insert_spec ys (i2, Some r) @ zs
[PROOF STEP]
by (metis Some UnE r_ys set_append)
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ insert_spec ys (i2, Some r) @ zs

goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ insert_spec ys (i2, Some r) @ zs

goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
have "insert_spec (xs @ zs) (i2, Some r) = xs @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (xs @ zs) (i2, Some r) = xs @ zs
[PROOF STEP]
by (simp add: Some calculation(1) calculation(2))
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ zs) (i2, Some r) = xs @ zs

goal (3 subgoals):
 1. r \<in> set ys \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 3. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<notin> set xs
r \<notin> set zs
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ insert_spec ys (i2, Some r) @ zs
insert_spec (xs @ zs) (i2, Some r) = xs @ zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<notin> set xs
r \<notin> set zs
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ insert_spec ys (i2, Some r) @ zs
insert_spec (xs @ zs) (i2, Some r) = xs @ zs

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
using 1 2 \<open>oper = (i2, r2)\<close> snoc.prems
[PROOF STATE]
proof (prove)
using this:
r \<notin> set xs
r \<notin> set zs
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ insert_spec ys (i2, Some r) @ zs
insert_spec (xs @ zs) (i2, Some r) = xs @ zs
interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) = insert_spec (xs @ ys @ zs) (i2, Some r)
interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)
oper = (i2, r2)
insert_ops ops
insert_ops rest
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case r_zs
[PROOF STATE]
proof (state)
this:
r \<in> set zs

goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
hence "r \<notin> set xs" and "r \<notin> set ys"
[PROOF STATE]
proof (prove)
using this:
r \<in> set zs

goal (1 subgoal):
 1. r \<notin> set xs &&& r \<notin> set ys
[PROOF STEP]
using IH2 ops2 interp_ins_distinct
[PROOF STATE]
proof (prove)
using this:
r \<in> set zs
interp_ins (before @ (oid, ref) # op_list) = xs @ ys @ zs
insert_ops (before @ (oid, ref) # op_list)
insert_ops ?op_list \<Longrightarrow> distinct (interp_ins ?op_list)

goal (1 subgoal):
 1. r \<notin> set xs &&& r \<notin> set ys
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
r \<notin> set xs
r \<notin> set ys

goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<notin> set xs
r \<notin> set ys

goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
r \<notin> set xs
r \<notin> set ys
[PROOF STEP]
have "insert_spec (xs @ ys @ zs) (i2, Some r) =
                               xs @ ys @ (insert_spec zs (i2, Some r))"
[PROOF STATE]
proof (prove)
using this:
r \<notin> set xs
r \<notin> set ys

goal (1 subgoal):
 1. insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ insert_spec zs (i2, Some r)
[PROOF STEP]
by (metis Some UnE insert_second_part insert_spec_nonex set_append)
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ insert_spec zs (i2, Some r)

goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ insert_spec zs (i2, Some r)

goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
have "insert_spec (xs @ zs) (i2, Some r) = xs @ (insert_spec zs (i2, Some r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (xs @ zs) (i2, Some r) = xs @ insert_spec zs (i2, Some r)
[PROOF STEP]
by (simp add: r_zs calculation(1) insert_second_part)
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ zs) (i2, Some r) = xs @ insert_spec zs (i2, Some r)

goal (2 subgoals):
 1. r \<in> set zs \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
 2. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<notin> set xs
r \<notin> set ys
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ insert_spec zs (i2, Some r)
insert_spec (xs @ zs) (i2, Some r) = xs @ insert_spec zs (i2, Some r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<notin> set xs
r \<notin> set ys
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ insert_spec zs (i2, Some r)
insert_spec (xs @ zs) (i2, Some r) = xs @ insert_spec zs (i2, Some r)

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
using 1 2 \<open>oper = (i2, r2)\<close> snoc.prems
[PROOF STATE]
proof (prove)
using this:
r \<notin> set xs
r \<notin> set ys
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ insert_spec zs (i2, Some r)
insert_spec (xs @ zs) (i2, Some r) = xs @ insert_spec zs (i2, Some r)
interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) = insert_spec (xs @ ys @ zs) (i2, Some r)
interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)
oper = (i2, r2)
insert_ops ops
insert_ops rest
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal (1 subgoal):
 1. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
case r_nonex
[PROOF STATE]
proof (state)
this:
r \<notin> set (xs @ ys @ zs)

goal (1 subgoal):
 1. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<notin> set (xs @ ys @ zs)
[PROOF STEP]
have "insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs"
[PROOF STATE]
proof (prove)
using this:
r \<notin> set (xs @ ys @ zs)

goal (1 subgoal):
 1. insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs

goal (1 subgoal):
 1. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs

goal (1 subgoal):
 1. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
have "insert_spec (xs @ zs) (i2, Some r) = xs @ zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec (xs @ zs) (i2, Some r) = xs @ zs
[PROOF STEP]
using r_nonex
[PROOF STATE]
proof (prove)
using this:
r \<notin> set (xs @ ys @ zs)

goal (1 subgoal):
 1. insert_spec (xs @ zs) (i2, Some r) = xs @ zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_spec (xs @ zs) (i2, Some r) = xs @ zs

goal (1 subgoal):
 1. r \<notin> set (xs @ ys @ zs) \<Longrightarrow> \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs
insert_spec (xs @ zs) (i2, Some r) = xs @ zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs
insert_spec (xs @ zs) (i2, Some r) = xs @ zs

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
using 1 2 \<open>oper = (i2, r2)\<close> snoc.prems
[PROOF STATE]
proof (prove)
using this:
insert_spec (xs @ ys @ zs) (i2, Some r) = xs @ ys @ zs
insert_spec (xs @ zs) (i2, Some r) = xs @ zs
interp_ins (before @ (oid, ref) # op_list @ [(i2, r2)]) = insert_spec (xs @ ys @ zs) (i2, Some r)
interp_ins (before @ op_list @ [(i2, r2)]) = insert_spec (xs @ zs) (i2, Some r)
oper = (i2, r2)
insert_ops ops
insert_ops rest
rest = before @ op_list @ [oper]
ops = before @ (oid, ref) # op_list @ [oper]

goal (1 subgoal):
 1. \<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xs ys zs. interp_ins rest = xs @ zs \<and> interp_ins ops = xs @ ys @ zs

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. distinct A
[PROOF STEP]
by (induction A) auto


[STATEMENT]
lemma subset_distinct_le:
  assumes "set A \<subseteq> set B" and "distinct A" and "distinct B"
  shows "length A \<le> length B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A \<le> length B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set A \<subseteq> set B
distinct A
distinct B

goal (1 subgoal):
 1. length A \<le> length B
[PROOF STEP]
proof(induction B arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>set A \<subseteq> set []; distinct A; distinct []\<rbrakk> \<Longrightarrow> length A \<le> length []
 2. \<And>a B A. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B)\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
set A \<subseteq> set []
distinct A
distinct []

goal (2 subgoals):
 1. \<And>A. \<lbrakk>set A \<subseteq> set []; distinct A; distinct []\<rbrakk> \<Longrightarrow> length A \<le> length []
 2. \<And>a B A. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B)\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set A \<subseteq> set []
distinct A
distinct []
[PROOF STEP]
show "length A \<le> length []"
[PROOF STATE]
proof (prove)
using this:
set A \<subseteq> set []
distinct A
distinct []

goal (1 subgoal):
 1. length A \<le> length []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length A \<le> length []

goal (1 subgoal):
 1. \<And>a B A. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B)\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a B A. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B)\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
case (Cons a B)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set ?A \<subseteq> set B; distinct ?A; distinct B\<rbrakk> \<Longrightarrow> length ?A \<le> length B
set A \<subseteq> set (a # B)
distinct A
distinct (a # B)

goal (1 subgoal):
 1. \<And>a B A. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B)\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set ?A \<subseteq> set B; distinct ?A; distinct B\<rbrakk> \<Longrightarrow> length ?A \<le> length B
set A \<subseteq> set (a # B)
distinct A
distinct (a # B)
[PROOF STEP]
show "length A \<le> length (a # B)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?A \<subseteq> set B; distinct ?A; distinct B\<rbrakk> \<Longrightarrow> length ?A \<le> length B
set A \<subseteq> set (a # B)
distinct A
distinct (a # B)

goal (1 subgoal):
 1. length A \<le> length (a # B)
[PROOF STEP]
proof(cases "a \<in> set A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<in> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
 2. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> set A

goal (2 subgoals):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<in> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
 2. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
have "set (remove1 a A) \<subseteq> set B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (remove1 a A) \<subseteq> set B
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
set A \<subseteq> set (a # B)
distinct A
distinct (a # B)

goal (1 subgoal):
 1. set (remove1 a A) \<subseteq> set B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (remove1 a A) \<subseteq> set B

goal (2 subgoals):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<in> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
 2. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
hence "length (remove1 a A) \<le> length B"
[PROOF STATE]
proof (prove)
using this:
set (remove1 a A) \<subseteq> set B

goal (1 subgoal):
 1. length (remove1 a A) \<le> length B
[PROOF STEP]
using Cons.IH Cons.prems
[PROOF STATE]
proof (prove)
using this:
set (remove1 a A) \<subseteq> set B
\<lbrakk>set ?A \<subseteq> set B; distinct ?A; distinct B\<rbrakk> \<Longrightarrow> length ?A \<le> length B
set A \<subseteq> set (a # B)
distinct A
distinct (a # B)

goal (1 subgoal):
 1. length (remove1 a A) \<le> length B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (remove1 a A) \<le> length B

goal (2 subgoals):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<in> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
 2. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (remove1 a A) \<le> length B
[PROOF STEP]
show "length A \<le> length (a # B)"
[PROOF STATE]
proof (prove)
using this:
length (remove1 a A) \<le> length B

goal (1 subgoal):
 1. length A \<le> length (a # B)
[PROOF STEP]
by (simp add: True length_remove1)
[PROOF STATE]
proof (state)
this:
length A \<le> length (a # B)

goal (1 subgoal):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> set A

goal (1 subgoal):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
hence "set A \<subseteq> set B"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set A

goal (1 subgoal):
 1. set A \<subseteq> set B
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
a \<notin> set A
set A \<subseteq> set (a # B)
distinct A
distinct (a # B)

goal (1 subgoal):
 1. set A \<subseteq> set B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set A \<subseteq> set B

goal (1 subgoal):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
hence "length A \<le> length B"
[PROOF STATE]
proof (prove)
using this:
set A \<subseteq> set B

goal (1 subgoal):
 1. length A \<le> length B
[PROOF STEP]
using Cons.IH Cons.prems
[PROOF STATE]
proof (prove)
using this:
set A \<subseteq> set B
\<lbrakk>set ?A \<subseteq> set B; distinct ?A; distinct B\<rbrakk> \<Longrightarrow> length ?A \<le> length B
set A \<subseteq> set (a # B)
distinct A
distinct (a # B)

goal (1 subgoal):
 1. length A \<le> length B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length A \<le> length B

goal (1 subgoal):
 1. \<lbrakk>\<And>A. \<lbrakk>set A \<subseteq> set B; distinct A; distinct B\<rbrakk> \<Longrightarrow> length A \<le> length B; set A \<subseteq> set (a # B); distinct A; distinct (a # B); a \<notin> set A\<rbrakk> \<Longrightarrow> length A \<le> length (a # B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length A \<le> length B
[PROOF STEP]
show "length A \<le> length (a # B)"
[PROOF STATE]
proof (prove)
using this:
length A \<le> length B

goal (1 subgoal):
 1. length A \<le> length (a # B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length A \<le> length (a # B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length A \<le> length (a # B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_subset_length_eq:
  assumes "set A \<subseteq> set B" and "length B \<le> length A"
    and "distinct A" and "distinct B"
  shows "set A = set B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set A = set B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set A = set B
[PROOF STEP]
have "length A \<le> length B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A \<le> length B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set A \<subseteq> set B
length B \<le> length A
distinct A
distinct B

goal (1 subgoal):
 1. length A \<le> length B
[PROOF STEP]
by (simp add: subset_distinct_le)
[PROOF STATE]
proof (state)
this:
length A \<le> length B

goal (1 subgoal):
 1. set A = set B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length A \<le> length B

goal (1 subgoal):
 1. set A = set B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
length A \<le> length B
[PROOF STEP]
have "card (set A) = card (set B)"
[PROOF STATE]
proof (prove)
using this:
length A \<le> length B

goal (1 subgoal):
 1. card (set A) = card (set B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length A \<le> length B
set A \<subseteq> set B
length B \<le> length A
distinct A
distinct B

goal (1 subgoal):
 1. card (set A) = card (set B)
[PROOF STEP]
by (simp add: distinct_card le_antisym)
[PROOF STATE]
proof (state)
this:
card (set A) = card (set B)

goal (1 subgoal):
 1. set A = set B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length A \<le> length B
card (set A) = card (set B)
[PROOF STEP]
show "set A = set B"
[PROOF STATE]
proof (prove)
using this:
length A \<le> length B
card (set A) = card (set B)

goal (1 subgoal):
 1. set A = set B
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
length A \<le> length B
card (set A) = card (set B)
set A \<subseteq> set B

goal (1 subgoal):
 1. set A = set B
[PROOF STEP]
by (simp add: card_subset_eq)
[PROOF STATE]
proof (state)
this:
set A = set B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_diff_Suc_exists:
  assumes "length xs - length ys = Suc m"
    and "set ys \<subseteq> set xs"
    and "distinct ys" and "distinct xs"
  shows "\<exists>e. e \<in> set xs \<and> e \<notin> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs - length ys = Suc m
set ys \<subseteq> set xs
distinct ys
distinct xs

goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set ys
[PROOF STEP]
proof(induction xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>length [] - length ys = Suc m; set ys \<subseteq> set []; distinct ys; distinct []\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set [] \<and> e \<notin> set ys
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
length [] - length ys = Suc m
set ys \<subseteq> set []
distinct ys
distinct []

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>length [] - length ys = Suc m; set ys \<subseteq> set []; distinct ys; distinct []\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set [] \<and> e \<notin> set ys
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length [] - length ys = Suc m
set ys \<subseteq> set []
distinct ys
distinct []
[PROOF STEP]
show "\<exists>e. e \<in> set [] \<and> e \<notin> set ys"
[PROOF STATE]
proof (prove)
using this:
length [] - length ys = Suc m
set ys \<subseteq> set []
distinct ys
distinct []

goal (1 subgoal):
 1. \<exists>e. e \<in> set [] \<and> e \<notin> set ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>e. e \<in> set [] \<and> e \<notin> set ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length xs - length ?ys = Suc m; set ?ys \<subseteq> set xs; distinct ?ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ?ys
length (a # xs) - length ys = Suc m
set ys \<subseteq> set (a # xs)
distinct ys
distinct (a # xs)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs)\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs - length ?ys = Suc m; set ?ys \<subseteq> set xs; distinct ?ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ?ys
length (a # xs) - length ys = Suc m
set ys \<subseteq> set (a # xs)
distinct ys
distinct (a # xs)
[PROOF STEP]
show "\<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs - length ?ys = Suc m; set ?ys \<subseteq> set xs; distinct ?ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ?ys
length (a # xs) - length ys = Suc m
set ys \<subseteq> set (a # xs)
distinct ys
distinct (a # xs)

goal (1 subgoal):
 1. \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
proof(cases "a \<in> set ys")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<in> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
 2. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> set ys

goal (2 subgoals):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<in> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
 2. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
have IH: "\<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
[PROOF STEP]
have "length xs - length (remove1 a ys) = Suc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs - length (remove1 a ys) = Suc m
[PROOF STEP]
by (metis Cons.prems(1) One_nat_def Suc_pred True diff_Suc_Suc length_Cons
            length_pos_if_in_set length_remove1)
[PROOF STATE]
proof (state)
this:
length xs - length (remove1 a ys) = Suc m

goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length xs - length (remove1 a ys) = Suc m

goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
[PROOF STEP]
have "set (remove1 a ys) \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (remove1 a ys) \<subseteq> set xs
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
length (a # xs) - length ys = Suc m
set ys \<subseteq> set (a # xs)
distinct ys
distinct (a # xs)

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

goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length xs - length (remove1 a ys) = Suc m
set (remove1 a ys) \<subseteq> set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs - length (remove1 a ys) = Suc m
set (remove1 a ys) \<subseteq> set xs

goal (1 subgoal):
 1. \<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
[PROOF STEP]
by (meson Cons.IH Cons.prems distinct.simps(2) distinct_remove1)
[PROOF STATE]
proof (state)
this:
\<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)

goal (2 subgoals):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<in> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
 2. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)

goal (2 subgoals):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<in> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
 2. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
have "set ys - {a} \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys - {a} \<subseteq> set xs
[PROOF STEP]
using Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> set (a # xs)

goal (1 subgoal):
 1. set ys - {a} \<subseteq> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ys - {a} \<subseteq> set xs

goal (2 subgoals):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<in> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
 2. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
set ys - {a} \<subseteq> set xs
[PROOF STEP]
show "\<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys"
[PROOF STATE]
proof (prove)
using this:
\<exists>e. e \<in> set xs \<and> e \<notin> set (remove1 a ys)
set ys - {a} \<subseteq> set xs

goal (1 subgoal):
 1. \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
by (metis Cons.prems(4) distinct.simps(2) in_set_remove1 set_subset_Cons subsetCE)
[PROOF STATE]
proof (state)
this:
\<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys

goal (1 subgoal):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> set ys

goal (1 subgoal):
 1. \<lbrakk>\<And>ys. \<lbrakk>length xs - length ys = Suc m; set ys \<subseteq> set xs; distinct ys; distinct xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set xs \<and> e \<notin> set ys; length (a # xs) - length ys = Suc m; set ys \<subseteq> set (a # xs); distinct ys; distinct (a # xs); a \<notin> set ys\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<notin> set ys
[PROOF STEP]
show "\<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set ys

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>e. e \<in> set (a # xs) \<and> e \<notin> set ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma app_length_lt_exists:
  assumes "xsa @ zsa = xs @ ys"
    and "length xsa \<le> length xs"
  shows "xsa @ (drop (length xsa) xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xsa @ drop (length xsa) xs = xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xsa @ zsa = xs @ ys
length xsa \<le> length xs

goal (1 subgoal):
 1. xsa @ drop (length xsa) xs = xs
[PROOF STEP]
by (induction xsa arbitrary: xs zsa ys, simp,
      metis append_eq_append_conv_if append_take_drop_id)