[STATEMENT]
lemma pop_list_current [simp]: "\<lbrakk>invar small; 0 < size small; Small.pop small = (x, small')\<rbrakk>
  \<Longrightarrow> x # list_current small' = list_current small"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar small; 0 < size small; Small.pop small = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current small
[PROOF STEP]
proof(induction small arbitrary: x rule: pop.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>state x. \<lbrakk>invar (Common state); 0 < size (Common state); Small.pop (Common state) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Common state)
 2. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 3. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
case (1 state)
[PROOF STATE]
proof (state)
this:
invar (Common state)
0 < size (Common state)
Small.pop (Common state) = (x, small')

goal (3 subgoals):
 1. \<And>state x. \<lbrakk>invar (Common state); 0 < size (Common state); Small.pop (Common state) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Common state)
 2. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 3. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Common state)
0 < size (Common state)
Small.pop (Common state) = (x, small')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Common state)
0 < size (Common state)
Small.pop (Common state) = (x, small')

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Common state)
[PROOF STEP]
by(auto simp: pop_list_current split: prod.splits)
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Common state)

goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
case (2 current small auxS)
[PROOF STATE]
proof (state)
this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')

goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')
[PROOF STEP]
have "invar current"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')

goal (1 subgoal):
 1. invar current
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
invar current

goal (2 subgoals):
 1. \<And>current small auxS x. \<lbrakk>invar (Reverse1 current small auxS); 0 < size (Reverse1 current small auxS); Small.pop (Reverse1 current small auxS) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
 2. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')
invar current
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse1 current small auxS)
0 < size (Reverse1 current small auxS)
Small.pop (Reverse1 current small auxS) = (x, small')
invar current

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse1 current small auxS)

goal (1 subgoal):
 1. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
case (3 current auxS big newS count)
[PROOF STATE]
proof (state)
this:
invar (Reverse2 current auxS big newS count)
0 < size (Reverse2 current auxS big newS count)
Small.pop (Reverse2 current auxS big newS count) = (x, small')

goal (1 subgoal):
 1. \<And>current auxS big newS count x. \<lbrakk>invar (Reverse2 current auxS big newS count); 0 < size (Reverse2 current auxS big newS count); Small.pop (Reverse2 current auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 current auxS big newS count)
0 < size (Reverse2 current auxS big newS count)
Small.pop (Reverse2 current auxS big newS count) = (x, small')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 current auxS big newS count)
0 < size (Reverse2 current auxS big newS count)
Small.pop (Reverse2 current auxS big newS count) = (x, small')

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)
[PROOF STEP]
proof(induction current rule: Current.pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Reverse2 (Current [] added old remained) auxS big newS count); 0 < size (Reverse2 (Current [] added old remained) auxS big newS count); Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
 2. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
case (1 added old remained)
[PROOF STATE]
proof (state)
this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')

goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Reverse2 (Current [] added old remained) auxS big newS count); 0 < size (Reverse2 (Current [] added old remained) auxS big newS count); Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
 2. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')
[PROOF STEP]
have "\<not>is_empty old"
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')

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 (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (Reverse2 (Current [] added old remained) auxS big newS count); 0 < size (Reverse2 (Current [] added old remained) auxS big newS count); Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
 2. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')
\<not> is_empty old
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 (Current [] added old remained) auxS big newS count)
0 < size (Reverse2 (Current [] added old remained) auxS big newS count)
Small.pop (Reverse2 (Current [] added old remained) auxS big newS count) = (x, small')
\<not> is_empty old

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)
[PROOF STEP]
by(auto simp: rev_take drop_Suc drop_tl)
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse2 (Current [] added old remained) auxS big newS count)

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
invar (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
0 < size (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
Small.pop (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count) = (x, small')

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (Reverse2 (Current (x # xs) added old remained) auxS big newS count); 0 < size (Reverse2 (Current (x # xs) added old remained) auxS big newS count); Small.pop (Reverse2 (Current (x # xs) added old remained) auxS big newS count) = (x, small')\<rbrakk> \<Longrightarrow> x # Small.list_current small' = Small.list_current (Reverse2 (Current (x # xs) added old remained) auxS big newS count)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
0 < size (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
Small.pop (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count) = (x, small')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
0 < size (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
Small.pop (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count) = (x, small')

goal (1 subgoal):
 1. x # Small.list_current small' = Small.list_current (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse2 (Current (x_ # xs_) added_ old_ remained_) auxS big newS count)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # Small.list_current small' = Small.list_current (Reverse2 current auxS big newS count)

goal:
No subgoals!
[PROOF STEP]
qed