[STATEMENT]
lemma invar_step: "invar (common :: 'a state) \<Longrightarrow> invar (step common)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> invar (step common)
[PROOF STEP]
proof(induction "common" rule: invar_state.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle. invar (state.Idle current idle) \<Longrightarrow> invar (step (state.Idle current idle))
 2. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
case (1 idle)
[PROOF STATE]
proof (state)
this:
invar (state.Idle idle idle_)

goal (2 subgoals):
 1. \<And>current idle. invar (state.Idle current idle) \<Longrightarrow> invar (step (state.Idle current idle))
 2. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle idle idle_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle idle idle_)

goal (1 subgoal):
 1. invar (step (state.Idle idle idle_))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (step (state.Idle idle idle_))

goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
case (2 current aux new moved)
[PROOF STATE]
proof (state)
this:
invar (Copy current aux new moved)

goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)

goal (1 subgoal):
 1. invar (step (Copy current aux new moved))
[PROOF STEP]
proof(cases current)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>invar (Copy current aux new moved); current = Current x1 x2 x3 x4\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
case (Current extra added old remained)
[PROOF STATE]
proof (state)
this:
current = Current extra added old remained

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>invar (Copy current aux new moved); current = Current x1 x2 x3 x4\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
current = Current extra added old remained
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
current = Current extra added old remained

goal (1 subgoal):
 1. invar (step (Copy current aux new moved))
[PROOF STEP]
proof(cases "aux = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>current = Current extra added old remained; aux = []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
 2. \<lbrakk>current = Current extra added old remained; aux \<noteq> []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
aux = []

goal (2 subgoals):
 1. \<lbrakk>current = Current extra added old remained; aux = []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
 2. \<lbrakk>current = Current extra added old remained; aux \<noteq> []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
with 2 Current
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
current = Current extra added old remained
aux = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
current = Current extra added old remained
aux = []

goal (1 subgoal):
 1. invar (step (Copy current aux new moved))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (step (Copy current aux new moved))

goal (1 subgoal):
 1. \<lbrakk>current = Current extra added old remained; aux \<noteq> []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>current = Current extra added old remained; aux \<noteq> []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
aux \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>current = Current extra added old remained; aux \<noteq> []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
note AUX_NOT_EMPTY = False
[PROOF STATE]
proof (state)
this:
aux \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>current = Current extra added old remained; aux \<noteq> []\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
aux \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
aux \<noteq> []

goal (1 subgoal):
 1. invar (step (Copy current aux new moved))
[PROOF STEP]
proof(cases "remained \<le> Suc (length new)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>aux \<noteq> []; remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
 2. \<lbrakk>aux \<noteq> []; \<not> remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
remained \<le> Suc (length new)

goal (2 subgoals):
 1. \<lbrakk>aux \<noteq> []; remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
 2. \<lbrakk>aux \<noteq> []; \<not> remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
with 2 Current False
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
current = Current extra added old remained
aux \<noteq> []
remained \<le> Suc (length new)
[PROOF STEP]
have "take (Suc (length new)) (Stack.list old) = take (size old) (hd aux # new)"
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
current = Current extra added old remained
aux \<noteq> []
remained \<le> Suc (length new)

goal (1 subgoal):
 1. take (Suc (length new)) (Stack.list old) = take (size old) (hd aux # new)
[PROOF STEP]
by(auto simp: le_Suc_eq take_Cons')
[PROOF STATE]
proof (state)
this:
take (Suc (length new)) (Stack.list old) = take (size old) (hd aux # new)

goal (2 subgoals):
 1. \<lbrakk>aux \<noteq> []; remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
 2. \<lbrakk>aux \<noteq> []; \<not> remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
with 2 Current True
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
current = Current extra added old remained
remained \<le> Suc (length new)
take (Suc (length new)) (Stack.list old) = take (size old) (hd aux # new)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
current = Current extra added old remained
remained \<le> Suc (length new)
take (Suc (length new)) (Stack.list old) = take (size old) (hd aux # new)

goal (1 subgoal):
 1. invar (step (Copy current aux new moved))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (step (Copy current aux new moved))

goal (1 subgoal):
 1. \<lbrakk>aux \<noteq> []; \<not> remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>aux \<noteq> []; \<not> remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> remained \<le> Suc (length new)

goal (1 subgoal):
 1. \<lbrakk>aux \<noteq> []; \<not> remained \<le> Suc (length new)\<rbrakk> \<Longrightarrow> invar (step (Copy current aux new moved))
[PROOF STEP]
with 2 Current AUX_NOT_EMPTY
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
current = Current extra added old remained
aux \<noteq> []
\<not> remained \<le> Suc (length new)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
current = Current extra added old remained
aux \<noteq> []
\<not> remained \<le> Suc (length new)

goal (1 subgoal):
 1. invar (step (Copy current aux new moved))
[PROOF STEP]
by(auto simp: reverseN_step Suc_diff_Suc simp del: reverseN_def)
[PROOF STATE]
proof (state)
this:
invar (step (Copy current aux new moved))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (step (Copy current aux new moved))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (step (Copy current aux new moved))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (step (Copy current aux new moved))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invar_push: "invar common \<Longrightarrow> invar (push x common)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> invar (Common.push x common)
[PROOF STEP]
proof(induction x common rule: push.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x current stack stackSize. invar (state.Idle current (idle.Idle stack stackSize)) \<Longrightarrow> invar (Common.push x (state.Idle current (idle.Idle stack stackSize)))
 2. \<And>x current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (Common.push x (Copy current aux new moved))
[PROOF STEP]
case (1 x current stack stackSize)
[PROOF STATE]
proof (state)
this:
invar (state.Idle current (idle.Idle stack stackSize))

goal (2 subgoals):
 1. \<And>x current stack stackSize. invar (state.Idle current (idle.Idle stack stackSize)) \<Longrightarrow> invar (Common.push x (state.Idle current (idle.Idle stack stackSize)))
 2. \<And>x current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (Common.push x (Copy current aux new moved))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle current (idle.Idle stack stackSize))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle current (idle.Idle stack stackSize))

goal (1 subgoal):
 1. invar (Common.push x (state.Idle current (idle.Idle stack stackSize)))
[PROOF STEP]
proof(induction x current rule: Current.push.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x extra added old remained. invar (state.Idle (Current extra added old remained) (idle.Idle stack stackSize)) \<Longrightarrow> invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle stack stackSize)))
[PROOF STEP]
case (1 x extra added old remained)
[PROOF STATE]
proof (state)
this:
invar (state.Idle (Current extra added old remained) (idle.Idle stack stackSize))

goal (1 subgoal):
 1. \<And>x extra added old remained. invar (state.Idle (Current extra added old remained) (idle.Idle stack stackSize)) \<Longrightarrow> invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle stack stackSize)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle (Current extra added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current extra added old remained) (idle.Idle stack stackSize))

goal (1 subgoal):
 1. invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle stack stackSize)))
[PROOF STEP]
proof(induction x stack rule: Stack.push.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x left right. invar (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize)) \<Longrightarrow> invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize)))
[PROOF STEP]
case (1 x left right)
[PROOF STATE]
proof (state)
this:
invar (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize))

goal (1 subgoal):
 1. \<And>x left right. invar (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize)) \<Longrightarrow> invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize))

goal (1 subgoal):
 1. invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle (Stack left right) stackSize)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (Common.push x (state.Idle (Current extra added old remained) (idle.Idle stack stackSize)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (Common.push x (state.Idle current (idle.Idle stack stackSize)))

goal (1 subgoal):
 1. \<And>x current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (Common.push x (Copy current aux new moved))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (Common.push x (Copy current aux new moved))
[PROOF STEP]
case (2 x current aux new moved)
[PROOF STATE]
proof (state)
this:
invar (Copy current aux new moved)

goal (1 subgoal):
 1. \<And>x current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> invar (Common.push x (Copy current aux new moved))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)

goal (1 subgoal):
 1. invar (Common.push x (Copy current aux new moved))
[PROOF STEP]
proof(induction x current rule: Current.push.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x extra added old remained. invar (Copy (Current extra added old remained) aux new moved) \<Longrightarrow> invar (Common.push x (Copy (Current extra added old remained) aux new moved))
[PROOF STEP]
case (1 x extra added old remained)
[PROOF STATE]
proof (state)
this:
invar (Copy (Current extra added old remained) aux new moved)

goal (1 subgoal):
 1. \<And>x extra added old remained. invar (Copy (Current extra added old remained) aux new moved) \<Longrightarrow> invar (Common.push x (Copy (Current extra added old remained) aux new moved))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current extra added old remained) aux new moved)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current extra added old remained) aux new moved)

goal (1 subgoal):
 1. invar (Common.push x (Copy (Current extra added old remained) aux new moved))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (Common.push x (Copy (Current extra added old remained) aux new moved))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (Common.push x (Copy current aux new moved))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invar_pop: "\<lbrakk>
  0 < size common;
  invar common;
  pop common = (x, common')
\<rbrakk> \<Longrightarrow> invar common'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size common; invar common; Common.pop common = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
proof(induction common arbitrary: x rule: pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle x. \<lbrakk>0 < size (state.Idle current idle); invar (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
 2. \<And>current aux new moved x. \<lbrakk>0 < size (Copy current aux new moved); invar (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
case (1 current idle)
[PROOF STATE]
proof (state)
this:
0 < size (state.Idle current idle)
invar (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')

goal (2 subgoals):
 1. \<And>current idle x. \<lbrakk>0 < size (state.Idle current idle); invar (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
 2. \<And>current aux new moved x. \<lbrakk>0 < size (Copy current aux new moved); invar (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (state.Idle current idle)
invar (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')
[PROOF STEP]
obtain idle' where idle: "Idle.pop idle = (x, idle')"
[PROOF STATE]
proof (prove)
using this:
0 < size (state.Idle current idle)
invar (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')

goal (1 subgoal):
 1. (\<And>idle'. Idle.pop idle = (x, idle') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
Idle.pop idle = (x, idle')

goal (2 subgoals):
 1. \<And>current idle x. \<lbrakk>0 < size (state.Idle current idle); invar (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
 2. \<And>current aux new moved x. \<lbrakk>0 < size (Copy current aux new moved); invar (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
obtain current' where current: "drop_first current = current'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>current'. drop_first current = current' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
drop_first current = current'

goal (2 subgoals):
 1. \<And>current idle x. \<lbrakk>0 < size (state.Idle current idle); invar (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
 2. \<And>current aux new moved x. \<lbrakk>0 < size (Copy current aux new moved); invar (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
from 1 current idle
[PROOF STATE]
proof (chain)
picking this:
0 < size (state.Idle current idle)
invar (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')
drop_first current = current'
Idle.pop idle = (x, idle')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (state.Idle current idle)
invar (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')
drop_first current = current'
Idle.pop idle = (x, idle')

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
using Idle_Proof.size_pop[of idle x idle', symmetric]
        size_new_pop[of current]
        size_pop_sub[of current _ current']
[PROOF STATE]
proof (prove)
using this:
0 < size (state.Idle current idle)
invar (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')
drop_first current = current'
Idle.pop idle = (x, idle')
\<lbrakk>\<not> is_empty idle; Idle.pop idle = (x, idle')\<rbrakk> \<Longrightarrow> size idle = Suc (size idle')
\<lbrakk>0 < size_new current; invar current\<rbrakk> \<Longrightarrow> Suc (size_new (drop_first current)) = size_new current
\<lbrakk>0 < size current; invar current; Current.pop current = (?x, current')\<rbrakk> \<Longrightarrow> size current' = size current - 1

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
by(auto simp: Idle_Proof.invar_pop invar_size_pop eq_snd_iff take_tl size_not_empty)
[PROOF STATE]
proof (state)
this:
invar common'

goal (1 subgoal):
 1. \<And>current aux new moved x. \<lbrakk>0 < size (Copy current aux new moved); invar (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved x. \<lbrakk>0 < size (Copy current aux new moved); invar (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
case (2 current aux new moved)
[PROOF STATE]
proof (state)
this:
0 < size (Copy current aux new moved)
invar (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')

goal (1 subgoal):
 1. \<And>current aux new moved x. \<lbrakk>0 < size (Copy current aux new moved); invar (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy current aux new moved)
invar (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy current aux new moved)
invar (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
proof(induction current rule: Current.pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
 2. \<And>x xs added old remained. \<lbrakk>0 < size (Copy (Current (x # xs) added old remained) aux new moved); invar (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
case (1 added old remained)
[PROOF STATE]
proof (state)
this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
 2. \<And>x xs added old remained. \<lbrakk>0 < size (Copy (Current (x # xs) added old remained) aux new moved); invar (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
proof(cases "remained - Suc 0 \<le> length new")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
 2. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
remained - Suc 0 \<le> length new

goal (2 subgoals):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
 2. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new
[PROOF STEP]
have [simp]:
          "0 < size old"
          "Stack.list old \<noteq> []"
          "aux \<noteq> []"
          "length new = remained - Suc 0"
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new

goal (1 subgoal):
 1. (0 < size old &&& Stack.list old \<noteq> []) &&& aux \<noteq> [] &&& length new = remained - Suc 0
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
[PROOF STATE]
proof (state)
this:
0 < size old
Stack.list old \<noteq> []
aux \<noteq> []
length new = remained - Suc 0

goal (2 subgoals):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
 2. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size old
Stack.list old \<noteq> []
aux \<noteq> []
length new = remained - Suc 0
[PROOF STEP]
have [simp]: "Suc 0 \<le> size old"
[PROOF STATE]
proof (prove)
using this:
0 < size old
Stack.list old \<noteq> []
aux \<noteq> []
length new = remained - Suc 0

goal (1 subgoal):
 1. Suc 0 \<le> size old
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> size old

goal (2 subgoals):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
 2. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
[PROOF STEP]
have "0 < remained"
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

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

goal (2 subgoals):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
 2. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < remained
[PROOF STEP]
have "take remained (Stack.list old)
          = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))"
[PROOF STATE]
proof (prove)
using this:
0 < remained

goal (1 subgoal):
 1. take remained (Stack.list old) = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))
[PROOF STEP]
by (metis Suc_pred \<open>Stack.list old \<noteq> []\<close> list.collapse take_Suc_Cons)
[PROOF STATE]
proof (state)
this:
take remained (Stack.list old) = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))

goal (2 subgoals):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
 2. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
with 1 True
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new
take remained (Stack.list old) = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new
take remained (Stack.list old) = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
using Stack_Proof.pop_list[of old]
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new
take remained (Stack.list old) = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))
\<not> is_empty old \<Longrightarrow> Stack.list (Stack.pop old) = tl (Stack.list old)

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty)
[PROOF STATE]
proof (state)
this:
invar common'

goal (1 subgoal):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> remained - Suc 0 \<le> length new

goal (1 subgoal):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
\<not> remained - Suc 0 \<le> length new
[PROOF STEP]
have "remained - Suc 0 \<le> length aux + length new"
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
\<not> remained - Suc 0 \<le> length new

goal (1 subgoal):
 1. remained - Suc 0 \<le> length aux + length new
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remained - Suc 0 \<le> length aux + length new

goal (1 subgoal):
 1. \<lbrakk>0 < size (Copy (Current [] added old remained) aux new moved); invar (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
with 1 False
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
\<not> remained - Suc 0 \<le> length new
remained - Suc 0 \<le> length aux + length new
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
\<not> remained - Suc 0 \<le> length new
remained - Suc 0 \<le> length aux + length new

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
using Stack_Proof.pop_list[of old]
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current [] added old remained) aux new moved)
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
\<not> remained - Suc 0 \<le> length new
remained - Suc 0 \<le> length aux + length new
\<not> is_empty old \<Longrightarrow> Stack.list (Stack.pop old) = tl (Stack.list old)

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
apply(auto simp: Suc_diff_Suc take_tl Stack_Proof.size_not_empty tl_append_if)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_empty old; \<not> remained - Suc 0 \<le> length new; remained - Suc 0 \<le> length aux + length new; length new < remained; x = hd (Stack.list old); common' = Copy (Current [] 0 (Stack.pop old) (remained - Suc 0)) aux new (length new); moved = length new; remained \<le> length aux + length new; added = 0; take remained (Stack.list old) = take (size old) (rev (take (remained - length new) aux)) @ take (size old + length new - remained) new; aux \<noteq> []\<rbrakk> \<Longrightarrow> tl (take (size old) (rev (take (remained - length new) aux))) = take (size old - Suc 0) (rev (take (remained - Suc (length new)) aux))
[PROOF STEP]
by (simp add: Suc_diff_le rev_take tl_drop_2 tl_take)
[PROOF STATE]
proof (state)
this:
invar common'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar common'

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>0 < size (Copy (Current (x # xs) added old remained) aux new moved); invar (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>0 < size (Copy (Current (x # xs) added old remained) aux new moved); invar (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
case (2 x xs added old remained)
[PROOF STATE]
proof (state)
this:
0 < size (Copy (Current (x # xs) added old remained) aux new moved)
invar (Copy (Current (x # xs) added old remained) aux new moved)
Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (xa__, common')

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>0 < size (Copy (Current (x # xs) added old remained) aux new moved); invar (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (xa__, common')\<rbrakk> \<Longrightarrow> invar common'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy (Current (x # xs) added old remained) aux new moved)
invar (Copy (Current (x # xs) added old remained) aux new moved)
Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (xa__, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy (Current (x # xs) added old remained) aux new moved)
invar (Copy (Current (x # xs) added old remained) aux new moved)
Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (xa__, common')

goal (1 subgoal):
 1. invar common'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar common'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar common'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma push_list_current [simp]: "list_current (push x left) = x # list_current left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_current (Common.push x left) = x # list_current left
[PROOF STEP]
by(induction x left rule: push.induct) auto


[STATEMENT]
lemma pop_list [simp]: "invar common \<Longrightarrow> 0 < size common \<Longrightarrow> pop common = (x, common') \<Longrightarrow>
   x # list common' = list common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; 0 < size common; Common.pop common = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list common
[PROOF STEP]
proof(induction common arbitrary: x rule: pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle x. \<lbrakk>invar (state.Idle current idle); 0 < size (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (state.Idle current idle)
 2. \<And>current aux new moved x. \<lbrakk>invar (Copy current aux new moved); 0 < size (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy current aux new moved)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
invar (state.Idle current_ idle_)
0 < size (state.Idle current_ idle_)
Common.pop (state.Idle current_ idle_) = (x, common')

goal (2 subgoals):
 1. \<And>current idle x. \<lbrakk>invar (state.Idle current idle); 0 < size (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (state.Idle current idle)
 2. \<And>current aux new moved x. \<lbrakk>invar (Copy current aux new moved); 0 < size (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle current_ idle_)
0 < size (state.Idle current_ idle_)
Common.pop (state.Idle current_ idle_) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle current_ idle_)
0 < size (state.Idle current_ idle_)
Common.pop (state.Idle current_ idle_) = (x, common')

goal (1 subgoal):
 1. x # Common.list common' = Common.list (state.Idle current_ idle_)
[PROOF STEP]
by(auto simp: size_not_empty split: prod.splits)
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (state.Idle current_ idle_)

goal (1 subgoal):
 1. \<And>current aux new moved x. \<lbrakk>invar (Copy current aux new moved); 0 < size (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy current aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved x. \<lbrakk>invar (Copy current aux new moved); 0 < size (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy current aux new moved)
[PROOF STEP]
case (2 current aux new moved)
[PROOF STATE]
proof (state)
this:
invar (Copy current aux new moved)
0 < size (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')

goal (1 subgoal):
 1. \<And>current aux new moved x. \<lbrakk>invar (Copy current aux new moved); 0 < size (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
0 < size (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
0 < size (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy current aux new moved)
[PROOF STEP]
proof(induction current rule: Current.pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<And>x xs added old remained. \<lbrakk>invar (Copy (Current (x # xs) added old remained) aux new moved); 0 < size (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current (x # xs) added old remained) aux new moved)
[PROOF STEP]
case (1 added old remained)
[PROOF STATE]
proof (state)
this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<And>x xs added old remained. \<lbrakk>invar (Copy (Current (x # xs) added old remained) aux new moved); 0 < size (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current (x # xs) added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
proof(cases "remained - Suc 0 \<le> length new")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
remained - Suc 0 \<le> length new

goal (2 subgoals):
 1. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
from 1 True
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new
[PROOF STEP]
have [simp]:
          "aux \<noteq> []" "0 < remained"
          "Stack.list old \<noteq> []" "remained - length new = 1"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new

goal (1 subgoal):
 1. (aux \<noteq> [] &&& 0 < remained) &&& Stack.list old \<noteq> [] &&& remained - length new = 1
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
[PROOF STATE]
proof (state)
this:
aux \<noteq> []
0 < remained
Stack.list old \<noteq> []
remained - length new = 1

goal (2 subgoals):
 1. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
aux \<noteq> []
0 < remained
Stack.list old \<noteq> []
remained - length new = 1
[PROOF STEP]
have "take remained (Stack.list old) = hd aux # take (size old - Suc 0) new
             \<Longrightarrow> Stack.first old = hd aux"
[PROOF STATE]
proof (prove)
using this:
aux \<noteq> []
0 < remained
Stack.list old \<noteq> []
remained - length new = 1

goal (1 subgoal):
 1. take remained (Stack.list old) = hd aux # take (size old - Suc 0) new \<Longrightarrow> Stack.first old = hd aux
[PROOF STEP]
by (metis first_hd hd_take list.sel(1))
[PROOF STATE]
proof (state)
this:
take remained (Stack.list old) = hd aux # take (size old - Suc 0) new \<Longrightarrow> Stack.first old = hd aux

goal (2 subgoals):
 1. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
with 1 True take_hd[of aux]
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new
aux \<noteq> [] \<Longrightarrow> take (Suc 0) aux = [hd aux]
take remained (Stack.list old) = hd aux # take (size old - Suc 0) new \<Longrightarrow> Stack.first old = hd aux
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - Suc 0 \<le> length new
aux \<noteq> [] \<Longrightarrow> take (Suc 0) aux = [hd aux]
take remained (Stack.list old) = hd aux # take (size old - Suc 0) new \<Longrightarrow> Stack.first old = hd aux

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
by(auto simp: Suc_leI)
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)

goal (1 subgoal):
 1. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> remained - Suc 0 \<le> length new

goal (1 subgoal):
 1. \<lbrakk>invar (Copy (Current [] added old remained) aux new moved); 0 < size (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common'); \<not> remained - Suc 0 \<le> length new\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> remained - Suc 0 \<le> length new
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> remained - Suc 0 \<le> length new

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
proof(cases "remained - length new = length aux")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new = length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
remained - length new = length aux

goal (2 subgoals):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new = length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
remained - length new = length aux
[PROOF STEP]
have length_minus_1: "remained - Suc (length new) = length aux - 1"
[PROOF STATE]
proof (prove)
using this:
remained - length new = length aux

goal (1 subgoal):
 1. remained - Suc (length new) = length aux - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remained - Suc (length new) = length aux - 1

goal (2 subgoals):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new = length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
[PROOF STEP]
have not_empty: "0 < remained" "0 < size old"  "aux \<noteq> []" "\<not> is_empty old"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (1 subgoal):
 1. (0 < remained &&& 0 < size old) &&& aux \<noteq> [] &&& \<not> is_empty old
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty)
[PROOF STATE]
proof (state)
this:
0 < remained
0 < size old
aux \<noteq> []
\<not> is_empty old

goal (2 subgoals):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new = length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
from 1 True not_empty
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new = length aux
0 < remained
0 < size old
aux \<noteq> []
\<not> is_empty old
[PROOF STEP]
have "take 1 (Stack.list old) = take 1 (rev aux)"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new = length aux
0 < remained
0 < size old
aux \<noteq> []
\<not> is_empty old

goal (1 subgoal):
 1. take 1 (Stack.list old) = take 1 (rev aux)
[PROOF STEP]
using take_1[of
                remained
                "size old"
                "Stack.list old"
                "(rev aux) @ take (size old + length new - remained) new"
                ]
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new = length aux
0 < remained
0 < size old
aux \<noteq> []
\<not> is_empty old
\<lbrakk>0 < remained \<and> 0 < size old; take remained (Stack.list old) = take (size old) (rev aux @ take (size old + length new - remained) new)\<rbrakk> \<Longrightarrow> take 1 (Stack.list old) = take 1 (rev aux @ take (size old + length new - remained) new)

goal (1 subgoal):
 1. take 1 (Stack.list old) = take 1 (rev aux)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
take 1 (Stack.list old) = take 1 (rev aux)

goal (2 subgoals):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new = length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take 1 (Stack.list old) = take 1 (rev aux)
[PROOF STEP]
have "[last aux] = [Stack.first old]"
[PROOF STATE]
proof (prove)
using this:
take 1 (Stack.list old) = take 1 (rev aux)

goal (1 subgoal):
 1. [last aux] = [Stack.first old]
[PROOF STEP]
using take_last first_take not_empty
[PROOF STATE]
proof (prove)
using this:
take 1 (Stack.list old) = take 1 (rev aux)
?xs \<noteq> [] \<Longrightarrow> take 1 (rev ?xs) = [last ?xs]
\<not> is_empty ?stack \<Longrightarrow> [Stack.first ?stack] = take 1 (Stack.list ?stack)
0 < remained
0 < size old
aux \<noteq> []
\<not> is_empty old

goal (1 subgoal):
 1. [last aux] = [Stack.first old]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[last aux] = [Stack.first old]

goal (2 subgoals):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new = length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[last aux] = [Stack.first old]
[PROOF STEP]
have "last aux = Stack.first old"
[PROOF STATE]
proof (prove)
using this:
[last aux] = [Stack.first old]

goal (1 subgoal):
 1. last aux = Stack.first old
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last aux = Stack.first old

goal (2 subgoals):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new = length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
 2. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
with 1 True False
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new = length aux
\<not> remained - Suc 0 \<le> length new
last aux = Stack.first old
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new = length aux
\<not> remained - Suc 0 \<le> length new
last aux = Stack.first old

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
using not_empty last_drop_rev[of aux]
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new = length aux
\<not> remained - Suc 0 \<le> length new
last aux = Stack.first old
0 < remained
0 < size old
aux \<noteq> []
\<not> is_empty old
aux \<noteq> [] \<Longrightarrow> last aux # drop 1 (rev aux) = rev aux

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
by(auto simp: reverseN_drop length_minus_1 simp del: reverseN_def)
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
remained - length new \<noteq> length aux

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux
[PROOF STEP]
have a: "take (remained - length new) aux \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux

goal (1 subgoal):
 1. take (remained - length new) aux \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take (remained - length new) aux \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
from 1 False
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux
[PROOF STEP]
have b: "\<not> is_empty old"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux

goal (1 subgoal):
 1. \<not> is_empty old
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty)
[PROOF STATE]
proof (state)
this:
\<not> is_empty old

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
[PROOF STEP]
have c: "remained - Suc (length new) < length aux"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (1 subgoal):
 1. remained - Suc (length new) < length aux
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remained - Suc (length new) < length aux

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
[PROOF STEP]
have not_empty: "0 < remained" "0 < size old" "0 < remained - length new" "0 < length aux"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (1 subgoal):
 1. (0 < remained &&& 0 < size old) &&& 0 < remained - length new &&& 0 < length aux
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < remained
0 < size old
0 < remained - length new
0 < length aux

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
remained - length new \<noteq> length aux
0 < remained
0 < size old
0 < remained - length new
0 < length aux
[PROOF STEP]
have "
              take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new)
          \<Longrightarrow> take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))"
[PROOF STATE]
proof (prove)
using this:
remained - length new \<noteq> length aux
0 < remained
0 < size old
0 < remained - length new
0 < length aux

goal (1 subgoal):
 1. take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new) \<Longrightarrow> take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))
[PROOF STEP]
using take_1[of
                remained
                "size old"
                "Stack.list old"
                " (reverseN (remained - length new) aux new)"
              ]
[PROOF STATE]
proof (prove)
using this:
remained - length new \<noteq> length aux
0 < remained
0 < size old
0 < remained - length new
0 < length aux
\<lbrakk>0 < remained \<and> 0 < size old; take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new)\<rbrakk> \<Longrightarrow> take 1 (Stack.list old) = take 1 (reverseN (remained - length new) aux new)

goal (1 subgoal):
 1. take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new) \<Longrightarrow> take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))
[PROOF STEP]
by(auto simp: not_empty Suc_le_eq)
[PROOF STATE]
proof (state)
this:
take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new) \<Longrightarrow> take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
with 1 False
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux
take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new) \<Longrightarrow> take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))
[PROOF STEP]
have "take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))"
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
0 < size (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux
take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new) \<Longrightarrow> take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))

goal (1 subgoal):
 1. take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))
[PROOF STEP]
have d: "[Stack.first old] = [last (take (remained - length new) aux)]"
[PROOF STATE]
proof (prove)
using this:
take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))

goal (1 subgoal):
 1. [Stack.first old] = [last (take (remained - length new) aux)]
[PROOF STEP]
using take_last first_take a b
[PROOF STATE]
proof (prove)
using this:
take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))
?xs \<noteq> [] \<Longrightarrow> take 1 (rev ?xs) = [last ?xs]
\<not> is_empty ?stack \<Longrightarrow> [Stack.first ?stack] = take 1 (Stack.list ?stack)
take (remained - length new) aux \<noteq> []
\<not> is_empty old

goal (1 subgoal):
 1. [Stack.first old] = [last (take (remained - length new) aux)]
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[Stack.first old] = [last (take (remained - length new) aux)]

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
have "last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux)
            = rev (take (remained - length new) aux)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) = rev (take (remained - length new) aux)
[PROOF STEP]
using Suc_diff_Suc c not_empty
[PROOF STATE]
proof (prove)
using this:
?n < ?m \<Longrightarrow> Suc (?m - Suc ?n) = ?m - ?n
remained - Suc (length new) < length aux
0 < remained
0 < size old
0 < remained - length new
0 < length aux

goal (1 subgoal):
 1. last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) = rev (take (remained - length new) aux)
[PROOF STEP]
by (metis a drop_drop last_drop_rev plus_1_eq_Suc rev_take zero_less_diff)
[PROOF STATE]
proof (state)
this:
last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) = rev (take (remained - length new) aux)

goal (1 subgoal):
 1. \<lbrakk>\<not> remained - Suc 0 \<le> length new; remained - length new \<noteq> length aux\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
with 1(1) 1(3) False not_empty d
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux
0 < remained
0 < size old
0 < remained - length new
0 < length aux
[Stack.first old] = [last (take (remained - length new) aux)]
last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) = rev (take (remained - length new) aux)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')
remained - length new \<noteq> length aux
0 < remained
0 < size old
0 < remained - length new
0 < length aux
[Stack.first old] = [last (take (remained - length new) aux)]
last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) = rev (take (remained - length new) aux)

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
by(cases "remained - length new = 1") (auto)
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (Copy (Current [] added old remained) aux new moved)

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Copy (Current (x # xs) added old remained) aux new moved); 0 < size (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current (x # xs) added old remained) aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Copy (Current (x # xs) added old remained) aux new moved); 0 < size (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current (x # xs) added old remained) aux new moved)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
invar (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)
0 < size (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)
Common.pop (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved) = (x, common')

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Copy (Current (x # xs) added old remained) aux new moved); 0 < size (Copy (Current (x # xs) added old remained) aux new moved); Common.pop (Copy (Current (x # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> x # Common.list common' = Common.list (Copy (Current (x # xs) added old remained) aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)
0 < size (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)
Common.pop (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)
0 < size (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)
Common.pop (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved) = (x, common')

goal (1 subgoal):
 1. x # Common.list common' = Common.list (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (Copy (Current (x_ # xs_) added_ old_ remained_) aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # Common.list common' = Common.list (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed