[STATEMENT]
lemma pop_list_current: "invar common \<Longrightarrow> 0 < size common \<Longrightarrow> pop common = (x, common')
   \<Longrightarrow> x # list_current common' = list_current common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; 0 < size common; Common.pop common = (x, common')\<rbrakk> \<Longrightarrow> x # list_current common' = list_current 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 # list_current common' = list_current (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 # list_current common' = list_current (Copy current aux new moved)
[PROOF STEP]
case (1 current idle)
[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 # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (state.Idle current idle)
[PROOF STEP]
proof(induction idle rule: Idle.pop.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>stack stackSize. \<lbrakk>invar (state.Idle current (idle.Idle stack stackSize)); 0 < size (state.Idle current (idle.Idle stack stackSize)); Common.pop (state.Idle current (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> x # list_current common' = list_current (state.Idle current (idle.Idle stack stackSize))
[PROOF STEP]
case (1 stack stackSize)
[PROOF STATE]
proof (state)
this:
invar (state.Idle current (idle.Idle stack stackSize))
0 < size (state.Idle current (idle.Idle stack stackSize))
Common.pop (state.Idle current (idle.Idle stack stackSize)) = (x, common')

goal (1 subgoal):
 1. \<And>stack stackSize. \<lbrakk>invar (state.Idle current (idle.Idle stack stackSize)); 0 < size (state.Idle current (idle.Idle stack stackSize)); Common.pop (state.Idle current (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> x # list_current common' = list_current (state.Idle current (idle.Idle stack stackSize))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle current (idle.Idle stack stackSize))
0 < size (state.Idle current (idle.Idle stack stackSize))
Common.pop (state.Idle current (idle.Idle stack stackSize)) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle current (idle.Idle stack stackSize))
0 < size (state.Idle current (idle.Idle stack stackSize))
Common.pop (state.Idle current (idle.Idle stack stackSize)) = (x, common')

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

goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> x # list_current common' = list_current (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
 2. \<And>x xs added old remained. \<lbrakk>invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> x # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)) = (x, common')
[PROOF STEP]
have "Stack.first old = Stack.first stack"
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)) = (x, common')

goal (1 subgoal):
 1. Stack.first old = Stack.first stack
[PROOF STEP]
using take_first[of old stack]
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)) = (x, common')
\<lbrakk>0 < size old; 0 < size stack; take (size old) (Stack.list stack) = take (size stack) (Stack.list old)\<rbrakk> \<Longrightarrow> Stack.first old = Stack.first stack

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

goal (2 subgoals):
 1. \<And>added old remained. \<lbrakk>invar (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> x # list_current common' = list_current (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
 2. \<And>x xs added old remained. \<lbrakk>invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> x # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)) = (x, common')
Stack.first old = Stack.first stack
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current [] added old remained) (idle.Idle stack stackSize)) = (x, common')
Stack.first old = Stack.first stack

goal (1 subgoal):
 1. x # list_current common' = list_current (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
[PROOF STATE]
proof (state)
this:
x # list_current common' = list_current (state.Idle (Current [] added old remained) (idle.Idle stack stackSize))

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

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')\<rbrakk> \<Longrightarrow> xa__ # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')
[PROOF STEP]
have "0 < size stack"
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')

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

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')\<rbrakk> \<Longrightarrow> xa__ # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
with Stack_Proof.size_not_empty Stack_Proof.list_not_empty
[PROOF STATE]
proof (chain)
picking this:
(0 < size ?stack) = (\<not> is_empty ?stack)
(Stack.list ?stack \<noteq> []) = (\<not> is_empty ?stack)
0 < size stack
[PROOF STEP]
have not_empty: "\<not> is_empty stack" "Stack.list stack \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
(0 < size ?stack) = (\<not> is_empty ?stack)
(Stack.list ?stack \<noteq> []) = (\<not> is_empty ?stack)
0 < size stack

goal (1 subgoal):
 1. \<not> is_empty stack &&& Stack.list stack \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_empty stack
Stack.list stack \<noteq> []

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')\<rbrakk> \<Longrightarrow> xa__ # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')
\<not> is_empty stack
Stack.list stack \<noteq> []
[PROOF STEP]
have "hd (Stack.list stack) = x"
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')
\<not> is_empty stack
Stack.list stack \<noteq> []

goal (1 subgoal):
 1. hd (Stack.list stack) = x
[PROOF STEP]
using take_hd'[of "Stack.list stack" x "xs @ Stack.list old"]
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')
\<not> is_empty stack
Stack.list stack \<noteq> []
\<lbrakk>Stack.list stack \<noteq> []; take (length (Stack.list stack)) (x # xs @ Stack.list old) = take (Suc (length (xs @ Stack.list old))) (Stack.list stack)\<rbrakk> \<Longrightarrow> hd (Stack.list stack) = x

goal (1 subgoal):
 1. hd (Stack.list stack) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd (Stack.list stack) = x

goal (1 subgoal):
 1. \<And>x xs added old remained. \<lbrakk>invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); 0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)); Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')\<rbrakk> \<Longrightarrow> xa__ # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')
hd (Stack.list stack) = x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')
hd (Stack.list stack) = x

goal (1 subgoal):
 1. xa__ # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
using first_list[of stack] not_empty
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
0 < size (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
Common.pop (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize)) = (xa__, common')
hd (Stack.list stack) = x
\<not> is_empty stack \<Longrightarrow> Stack.first stack = hd (Stack.list stack)
\<not> is_empty stack
Stack.list stack \<noteq> []

goal (1 subgoal):
 1. xa__ # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xa__ # list_current common' = list_current (state.Idle (Current (x # xs) added old remained) (idle.Idle stack stackSize))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # list_current common' = list_current (state.Idle current (idle.Idle stack stackSize))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (Copy current aux new moved)
[PROOF STEP]
case (2 current)
[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 # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (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]
have "\<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. \<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 (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 # list_current common' = list_current (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 # list_current common' = list_current (Copy (Current (x # xs) 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')
\<not> is_empty old
[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')
\<not> is_empty old

goal (1 subgoal):
 1. x # list_current common' = list_current (Copy (Current [] added old remained) aux_ new_ moved_)
[PROOF STEP]
using first_pop
[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')
\<not> is_empty old
\<not> is_empty ?stack \<Longrightarrow> Stack.first ?stack # Stack.list (Stack.pop ?stack) = Stack.list ?stack

goal (1 subgoal):
 1. x # list_current common' = list_current (Copy (Current [] added old remained) aux_ new_ moved_)
[PROOF STEP]
by(auto simp: Stack_Proof.list_not_empty)
[PROOF STATE]
proof (state)
this:
x # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (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 # list_current common' = list_current (Copy (Current (x_ # xs_) added_ old_ remained_) aux_ new_ moved_)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # list_current common' = list_current (Copy (Current (x_ # xs_) added_ old_ remained_) aux_ new_ moved_)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # list_current common' = list_current (Copy current aux_ new_ moved_)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_current_size [simp]:
  "\<lbrakk>0 < size common; list_current common = []; invar common\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size common; list_current common = []; invar common\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof(induction common rule: invar_state.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle. \<lbrakk>0 < size (state.Idle current idle); list_current (state.Idle current idle) = []; invar (state.Idle current idle)\<rbrakk> \<Longrightarrow> False
 2. \<And>current aux new moved. \<lbrakk>0 < size (Copy current aux new moved); list_current (Copy current aux new moved) = []; invar (Copy current aux new moved)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
0 < size (state.Idle current_ idle_)
list_current (state.Idle current_ idle_) = []
invar (state.Idle current_ idle_)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using list_size
[PROOF STATE]
proof (prove)
using this:
0 < size (state.Idle current_ idle_)
list_current (state.Idle current_ idle_) = []
invar (state.Idle current_ idle_)
\<lbrakk>invar ?current; Current.list ?current = []; 0 < size ?current\<rbrakk> \<Longrightarrow> False

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

goal (1 subgoal):
 1. \<And>current aux new moved. \<lbrakk>0 < size (Copy current aux new moved); list_current (Copy current aux new moved) = []; invar (Copy current aux new moved)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved. \<lbrakk>0 < size (Copy current aux new moved); list_current (Copy current aux new moved) = []; invar (Copy current aux new moved)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (2 current)
[PROOF STATE]
proof (state)
this:
0 < size (Copy current aux_ new_ moved_)
list_current (Copy current aux_ new_ moved_) = []
invar (Copy current aux_ new_ moved_)

goal (1 subgoal):
 1. \<And>current aux new moved. \<lbrakk>0 < size (Copy current aux new moved); list_current (Copy current aux new moved) = []; invar (Copy current aux new moved)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy current aux_ new_ moved_)
list_current (Copy current aux_ new_ moved_) = []
invar (Copy current aux_ new_ moved_)
[PROOF STEP]
have "invar current"
            "Current.list current = []"
            "0 < size current"
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy current aux_ new_ moved_)
list_current (Copy current aux_ new_ moved_) = []
invar (Copy current aux_ new_ moved_)

goal (1 subgoal):
 1. invar current &&& Current.list current = [] &&& 0 < size current
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
invar current
Current.list current = []
0 < size current

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using list_size
[PROOF STATE]
proof (prove)
using this:
invar current
Current.list current = []
0 < size current
\<lbrakk>invar ?current; Current.list ?current = []; 0 < size ?current\<rbrakk> \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using list_size Idle_Proof.size_empty
[PROOF STATE]
proof (prove)
using this:
0 < size (state.Idle current_ idle_)
Common.list (state.Idle current_ idle_) = []
invar (state.Idle current_ idle_)
\<lbrakk>invar ?current; Current.list ?current = []; 0 < size ?current\<rbrakk> \<Longrightarrow> False
(size ?idle = 0) = is_empty ?idle

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

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

goal (1 subgoal):
 1. \<And>current aux new moved. \<lbrakk>0 < size (Copy current aux new moved); Common.list (Copy current aux new moved) = []; invar (Copy current aux new moved)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Copy current aux new moved)
Common.list (Copy current aux new moved) = []
invar (Copy current aux new moved)
[PROOF STEP]
have "invar current"
            "Current.list current = []"
            "0 < size current"
[PROOF STATE]
proof (prove)
using this:
0 < size (Copy current aux new moved)
Common.list (Copy current aux new moved) = []
invar (Copy current aux new moved)

goal (1 subgoal):
 1. invar current &&& Current.list current = [] &&& 0 < size current
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
invar current
Current.list current = []
0 < size current

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using list_size
[PROOF STATE]
proof (prove)
using this:
invar current
Current.list current = []
0 < size current
\<lbrakk>invar ?current; Current.list ?current = []; 0 < size ?current\<rbrakk> \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_empty: "invar (common :: 'a state) \<Longrightarrow> size common = 0 \<Longrightarrow> is_empty common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; size common = 0\<rbrakk> \<Longrightarrow> is_empty common
[PROOF STEP]
proof(induction common rule: is_empty_state.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle. \<lbrakk>invar (state.Idle current idle); size (state.Idle current idle) = 0\<rbrakk> \<Longrightarrow> is_empty (state.Idle current idle)
 2. \<And>current uu_ uv_ uw_. \<lbrakk>invar (Copy current uu_ uv_ uw_); size (Copy current uu_ uv_ uw_) = 0\<rbrakk> \<Longrightarrow> is_empty (Copy current uu_ uv_ uw_)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
invar (state.Idle current_ idle_)
size (state.Idle current_ idle_) = 0

goal (2 subgoals):
 1. \<And>current idle. \<lbrakk>invar (state.Idle current idle); size (state.Idle current idle) = 0\<rbrakk> \<Longrightarrow> is_empty (state.Idle current idle)
 2. \<And>current uu_ uv_ uw_. \<lbrakk>invar (Copy current uu_ uv_ uw_); size (Copy current uu_ uv_ uw_) = 0\<rbrakk> \<Longrightarrow> is_empty (Copy current uu_ uv_ uw_)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle current_ idle_)
size (state.Idle current_ idle_) = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle current_ idle_)
size (state.Idle current_ idle_) = 0

goal (1 subgoal):
 1. is_empty (state.Idle current_ idle_)
[PROOF STEP]
by(auto simp: min_def size_empty size_new_empty split: if_splits)
[PROOF STATE]
proof (state)
this:
is_empty (state.Idle current_ idle_)

goal (1 subgoal):
 1. \<And>current uu_ uv_ uw_. \<lbrakk>invar (Copy current uu_ uv_ uw_); size (Copy current uu_ uv_ uw_) = 0\<rbrakk> \<Longrightarrow> is_empty (Copy current uu_ uv_ uw_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current uu_ uv_ uw_. \<lbrakk>invar (Copy current uu_ uv_ uw_); size (Copy current uu_ uv_ uw_) = 0\<rbrakk> \<Longrightarrow> is_empty (Copy current uu_ uv_ uw_)
[PROOF STEP]
case (2 current)
[PROOF STATE]
proof (state)
this:
invar (Copy current uu_ uv_ uw_)
size (Copy current uu_ uv_ uw_) = 0

goal (1 subgoal):
 1. \<And>current uu_ uv_ uw_. \<lbrakk>invar (Copy current uu_ uv_ uw_); size (Copy current uu_ uv_ uw_) = 0\<rbrakk> \<Longrightarrow> is_empty (Copy current uu_ uv_ uw_)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current uu_ uv_ uw_)
size (Copy current uu_ uv_ uw_) = 0
[PROOF STEP]
have "invar current"
[PROOF STATE]
proof (prove)
using this:
invar (Copy current uu_ uv_ uw_)
size (Copy current uu_ uv_ uw_) = 0

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

goal (1 subgoal):
 1. \<And>current uu_ uv_ uw_. \<lbrakk>invar (Copy current uu_ uv_ uw_); size (Copy current uu_ uv_ uw_) = 0\<rbrakk> \<Longrightarrow> is_empty (Copy current uu_ uv_ uw_)
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current uu_ uv_ uw_)
size (Copy current uu_ uv_ uw_) = 0
invar current
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy current uu_ uv_ uw_)
size (Copy current uu_ uv_ uw_) = 0
invar current

goal (1 subgoal):
 1. is_empty (Copy current uu_ uv_ uw_)
[PROOF STEP]
by(auto simp: min_def size_empty size_new_empty split: if_splits)
[PROOF STATE]
proof (state)
this:
is_empty (Copy current uu_ uv_ uw_)

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> size (step (Copy current aux new moved)) = size (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> size (step (Copy current aux new moved)) = size (Copy current aux new moved)
[PROOF STEP]
case 2
[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> size (step (Copy current aux new moved)) = size (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. size (step (Copy current_ aux_ new_ moved_)) = size (Copy current_ aux_ new_ moved_)
[PROOF STEP]
by(auto simp: min_def split: current.splits)
[PROOF STATE]
proof (state)
this:
size (step (Copy current_ aux_ new_ moved_)) = size (Copy current_ aux_ new_ moved_)

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> size_new (step (Copy current aux new moved)) = size_new (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> size_new (step (Copy current aux new moved)) = size_new (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> size_new (step (Copy current aux new moved)) = size_new (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. size_new (step (Copy current aux new moved)) = size_new (Copy current aux new moved)
[PROOF STEP]
by(auto split: current.splits)
[PROOF STATE]
proof (state)
this:
size_new (step (Copy current aux new moved)) = size_new (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma remaining_steps_step [simp]: "\<lbrakk>invar (common :: 'a state); remaining_steps common > 0\<rbrakk>
   \<Longrightarrow> Suc (remaining_steps (step common)) = remaining_steps common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; 0 < remaining_steps common\<rbrakk> \<Longrightarrow> Suc (remaining_steps (step common)) = remaining_steps common
[PROOF STEP]
by(induction common)(auto split: current.splits)


[STATEMENT]
lemma remaining_steps_step_0 [simp]: "\<lbrakk>invar (common :: 'a state); remaining_steps common = 0\<rbrakk>
   \<Longrightarrow> remaining_steps (step common) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; remaining_steps common = 0\<rbrakk> \<Longrightarrow> remaining_steps (step common) = 0
[PROOF STEP]
by(induction common)(auto split: current.splits)


[STATEMENT]
lemma remaining_steps_push [simp]: "invar common
   \<Longrightarrow> remaining_steps (push x common) = remaining_steps common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> remaining_steps (Common.push x common) = remaining_steps common
[PROOF STEP]
by(induction x common rule: Common.push.induct)(auto split: current.splits)


[STATEMENT]
lemma remaining_steps_pop: "\<lbrakk>invar common; 0 < size common; pop common = (x, common')\<rbrakk>
  \<Longrightarrow> remaining_steps common' \<le> remaining_steps common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; 0 < size common; Common.pop common = (x, common')\<rbrakk> \<Longrightarrow> remaining_steps common' \<le> remaining_steps common
[PROOF STEP]
proof(induction common rule: pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle. \<lbrakk>invar (state.Idle current idle); 0 < size (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> remaining_steps common' \<le> remaining_steps (state.Idle current idle)
 2. \<And>current aux new moved. \<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> remaining_steps common' \<le> remaining_steps (Copy current aux new moved)
[PROOF STEP]
case (1 current idle)
[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. \<lbrakk>invar (state.Idle current idle); 0 < size (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> remaining_steps common' \<le> remaining_steps (state.Idle current idle)
 2. \<And>current aux new moved. \<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> remaining_steps common' \<le> remaining_steps (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. remaining_steps common' \<le> remaining_steps (state.Idle current idle)
[PROOF STEP]
proof(induction idle rule: Idle.pop.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>stack stackSize. \<lbrakk>invar (state.Idle current (idle.Idle stack stackSize)); 0 < size (state.Idle current (idle.Idle stack stackSize)); Common.pop (state.Idle current (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> remaining_steps common' \<le> remaining_steps (state.Idle current (idle.Idle stack stackSize))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
invar (state.Idle current (idle.Idle stack_ stackSize_))
0 < size (state.Idle current (idle.Idle stack_ stackSize_))
Common.pop (state.Idle current (idle.Idle stack_ stackSize_)) = (x, common')

goal (1 subgoal):
 1. \<And>stack stackSize. \<lbrakk>invar (state.Idle current (idle.Idle stack stackSize)); 0 < size (state.Idle current (idle.Idle stack stackSize)); Common.pop (state.Idle current (idle.Idle stack stackSize)) = (x, common')\<rbrakk> \<Longrightarrow> remaining_steps common' \<le> remaining_steps (state.Idle current (idle.Idle stack stackSize))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle current (idle.Idle stack_ stackSize_))
0 < size (state.Idle current (idle.Idle stack_ stackSize_))
Common.pop (state.Idle current (idle.Idle stack_ stackSize_)) = (x, common')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle current (idle.Idle stack_ stackSize_))
0 < size (state.Idle current (idle.Idle stack_ stackSize_))
Common.pop (state.Idle current (idle.Idle stack_ stackSize_)) = (x, common')

goal (1 subgoal):
 1. remaining_steps common' \<le> remaining_steps (state.Idle current (idle.Idle stack_ stackSize_))
[PROOF STEP]
by(induction current rule: Current.pop.induct) auto
[PROOF STATE]
proof (state)
this:
remaining_steps common' \<le> remaining_steps (state.Idle current (idle.Idle stack_ stackSize_))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
remaining_steps common' \<le> remaining_steps (state.Idle current idle)

goal (1 subgoal):
 1. \<And>current aux new moved. \<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> remaining_steps common' \<le> remaining_steps (Copy current aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved. \<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> remaining_steps common' \<le> remaining_steps (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. \<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> remaining_steps common' \<le> remaining_steps (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. remaining_steps common' \<le> remaining_steps (Copy current aux new moved)
[PROOF STEP]
by(induction current rule: Current.pop.induct) auto
[PROOF STATE]
proof (state)
this:
remaining_steps common' \<le> remaining_steps (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_push [simp]: "invar common \<Longrightarrow> size (push x common) = Suc (size common)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> size (Common.push x common) = Suc (size common)
[PROOF STEP]
by(induction x common rule: push.induct) (auto split: current.splits)


[STATEMENT]
lemma size_new_push [simp]: "invar common \<Longrightarrow> size_new (push x common) = Suc (size_new common)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> size_new (Common.push x common) = Suc (size_new common)
[PROOF STEP]
by(induction x common rule: Common.push.induct) (auto split: current.splits)


[STATEMENT]
lemma size_pop [simp]: "\<lbrakk>invar common; 0 < size common; pop common = (x, common')\<rbrakk>
   \<Longrightarrow> Suc (size common') = size common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; 0 < size common; Common.pop common = (x, common')\<rbrakk> \<Longrightarrow> Suc (size common') = size common
[PROOF STEP]
proof(induction common rule: Common.pop.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle. \<lbrakk>invar (state.Idle current idle); 0 < size (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size common') = size (state.Idle current idle)
 2. \<And>current aux new moved. \<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> Suc (size common') = size (Copy current aux new moved)
[PROOF STEP]
case (1 current idle)
[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. \<lbrakk>invar (state.Idle current idle); 0 < size (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size common') = size (state.Idle current idle)
 2. \<And>current aux new moved. \<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> Suc (size common') = size (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. Suc (size common') = size (state.Idle current idle)
[PROOF STEP]
using size_drop_first_sub[of current] Idle_Proof.size_pop_sub[of idle]
[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')
\<lbrakk>0 < size current; invar current\<rbrakk> \<Longrightarrow> size (drop_first current) = size current - 1
Idle.pop idle = (?x, ?idle') \<Longrightarrow> size ?idle' = size idle - 1

goal (1 subgoal):
 1. Suc (size common') = size (state.Idle current idle)
[PROOF STEP]
by(auto simp: size_not_empty split: prod.splits)
[PROOF STATE]
proof (state)
this:
Suc (size common') = size (state.Idle current idle)

goal (1 subgoal):
 1. \<And>current aux new moved. \<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> Suc (size common') = size (Copy current aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved. \<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> Suc (size common') = size (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. \<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> Suc (size common') = size (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. Suc (size common') = size (Copy current aux new moved)
[PROOF STEP]
by(induction current rule: Current.pop.induct) auto
[PROOF STATE]
proof (state)
this:
Suc (size common') = size (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (2 subgoals):
 1. \<And>current idle. \<lbrakk>invar (state.Idle current idle); 0 < size_new (state.Idle current idle); Common.pop (state.Idle current idle) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (state.Idle current idle)
 2. \<And>current aux new moved. \<lbrakk>invar (Copy current aux new moved); 0 < size_new (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle current idle)
0 < size_new (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_new (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')

goal (1 subgoal):
 1. Suc (size_new common') = size_new (state.Idle current idle)
[PROOF STEP]
using size_new_pop[of current]
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle current idle)
0 < size_new (state.Idle current idle)
Common.pop (state.Idle current idle) = (x, common')
\<lbrakk>0 < size_new current; invar current\<rbrakk> \<Longrightarrow> Suc (size_new (drop_first current)) = size_new current

goal (1 subgoal):
 1. Suc (size_new common') = size_new (state.Idle current idle)
[PROOF STEP]
by(auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
Suc (size_new common') = size_new (state.Idle current idle)

goal (1 subgoal):
 1. \<And>current aux new moved. \<lbrakk>invar (Copy current aux new moved); 0 < size_new (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy current aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved. \<lbrakk>invar (Copy current aux new moved); 0 < size_new (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (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_new (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')

goal (1 subgoal):
 1. \<And>current aux new moved. \<lbrakk>invar (Copy current aux new moved); 0 < size_new (Copy current aux new moved); Common.pop (Copy current aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
0 < size_new (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_new (Copy current aux new moved)
Common.pop (Copy current aux new moved) = (x, common')

goal (1 subgoal):
 1. Suc (size_new common') = size_new (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_new (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy (Current [] added old remained) aux new moved)
 2. \<And>xa xs added old remained. \<lbrakk>invar (Copy (Current (xa # xs) added old remained) aux new moved); 0 < size_new (Copy (Current (xa # xs) added old remained) aux new moved); Common.pop (Copy (Current (xa # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy (Current (xa # 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_new (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_new (Copy (Current [] added old remained) aux new moved); Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy (Current [] added old remained) aux new moved)
 2. \<And>xa xs added old remained. \<lbrakk>invar (Copy (Current (xa # xs) added old remained) aux new moved); 0 < size_new (Copy (Current (xa # xs) added old remained) aux new moved); Common.pop (Copy (Current (xa # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy (Current (xa # 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_new (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_new (Copy (Current [] added old remained) aux new moved)
Common.pop (Copy (Current [] added old remained) aux new moved) = (x, common')

goal (1 subgoal):
 1. Suc (size_new common') = size_new (Copy (Current [] added old remained) aux new moved)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (size_new common') = size_new (Copy (Current [] added old remained) aux new moved)

goal (1 subgoal):
 1. \<And>xa xs added old remained. \<lbrakk>invar (Copy (Current (xa # xs) added old remained) aux new moved); 0 < size_new (Copy (Current (xa # xs) added old remained) aux new moved); Common.pop (Copy (Current (xa # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy (Current (xa # xs) added old remained) aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs added old remained. \<lbrakk>invar (Copy (Current (xa # xs) added old remained) aux new moved); 0 < size_new (Copy (Current (xa # xs) added old remained) aux new moved); Common.pop (Copy (Current (xa # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy (Current (xa # xs) added old remained) aux new moved)
[PROOF STEP]
case (2 x xs added old remained)
[PROOF STATE]
proof (state)
this:
invar (Copy (Current (x # xs) added old remained) aux new moved)
0 < size_new (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>xa xs added old remained. \<lbrakk>invar (Copy (Current (xa # xs) added old remained) aux new moved); 0 < size_new (Copy (Current (xa # xs) added old remained) aux new moved); Common.pop (Copy (Current (xa # xs) added old remained) aux new moved) = (x, common')\<rbrakk> \<Longrightarrow> Suc (size_new common') = size_new (Copy (Current (xa # 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_new (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_new (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. Suc (size_new common') = size_new (Copy (Current (x # xs) added old remained) aux new moved)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (size_new common') = size_new (Copy (Current (x # xs) added old remained) aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc (size_new common') = size_new (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_size_new: "\<lbrakk>invar (common :: 'a state); 0 < size common\<rbrakk> \<Longrightarrow> 0 < size_new common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar common; 0 < size common\<rbrakk> \<Longrightarrow> 0 < size_new common
[PROOF STEP]
by(cases common) auto


[STATEMENT]
lemma conv_isotone:
  "x \<le> y \<Longrightarrow> x\<^sup>T \<le> y\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x\<^sup>T \<le> y\<^sup>T
[PROOF STEP]
by (metis conv_dist_sup le_iff_sup)


[STATEMENT]
lemma conv_order:
  "x \<le> y \<longleftrightarrow> x\<^sup>T \<le> y\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> y) = (x\<^sup>T \<le> y\<^sup>T)
[PROOF STEP]
using conv_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x\<^sup>T \<le> ?y\<^sup>T

goal (1 subgoal):
 1. (x \<le> y) = (x\<^sup>T \<le> y\<^sup>T)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma conv_bot [simp]:
  "bot\<^sup>T = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric bot
[PROOF STEP]
using conv_order bot_unique
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
(?a \<le> bot) = (?a = bot)

goal (1 subgoal):
 1. symmetric bot
[PROOF STEP]
by force


[STATEMENT]
lemma conv_top [simp]:
  "top\<^sup>T = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric top
[PROOF STEP]
by (metis conv_involutive conv_order order.eq_iff top_greatest)


[STATEMENT]
lemma conv_dist_inf:
  "(x \<sqinter> y)\<^sup>T = x\<^sup>T \<sqinter> y\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y)\<^sup>T = x\<^sup>T \<sqinter> y\<^sup>T
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (x \<sqinter> y)\<^sup>T \<le> x\<^sup>T \<sqinter> y\<^sup>T
 2. x\<^sup>T \<sqinter> y\<^sup>T \<le> (x \<sqinter> y)\<^sup>T
[PROOF STEP]
using conv_order
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)

goal (2 subgoals):
 1. (x \<sqinter> y)\<^sup>T \<le> x\<^sup>T \<sqinter> y\<^sup>T
 2. x\<^sup>T \<sqinter> y\<^sup>T \<le> (x \<sqinter> y)\<^sup>T
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T \<sqinter> y\<^sup>T \<le> (x \<sqinter> y)\<^sup>T
[PROOF STEP]
by (metis conv_order conv_involutive inf.boundedI inf.cobounded1 inf.cobounded2)


[STATEMENT]
lemma conv_inf_bot_iff:
  "bot = x\<^sup>T \<sqinter> y \<longleftrightarrow> bot = x \<sqinter> y\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bot = x\<^sup>T \<sqinter> y) = (bot = x \<sqinter> y\<^sup>T)
[PROOF STEP]
using conv_dist_inf conv_bot
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> ?y)\<^sup>T = ?x\<^sup>T \<sqinter> ?y\<^sup>T
symmetric bot

goal (1 subgoal):
 1. (bot = x\<^sup>T \<sqinter> y) = (bot = x \<sqinter> y\<^sup>T)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma conv_one [simp]:
  "1\<^sup>T = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric (1::'a)
[PROOF STEP]
by (metis comp_left_one conv_dist_comp conv_involutive)


[STATEMENT]
lemma comp_left_dist_sup:
  "(x * y) \<squnion> (x * z) = x * (y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<squnion> x * z = x * (y \<squnion> z)
[PROOF STEP]
by (metis comp_right_dist_sup conv_involutive conv_dist_sup conv_dist_comp)


[STATEMENT]
lemma comp_right_isotone:
  "x \<le> y \<Longrightarrow> z * x \<le> z * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> z * x \<le> z * y
[PROOF STEP]
by (simp add: comp_left_dist_sup sup.absorb_iff1)


[STATEMENT]
lemma comp_left_isotone:
  "x \<le> y \<Longrightarrow> x * z \<le> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x * z \<le> y * z
[PROOF STEP]
by (metis comp_right_dist_sup le_iff_sup)


[STATEMENT]
lemma comp_isotone:
  "x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> x * w \<le> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; w \<le> z\<rbrakk> \<Longrightarrow> x * w \<le> y * z
[PROOF STEP]
using comp_left_isotone comp_right_isotone order.trans
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; w \<le> z\<rbrakk> \<Longrightarrow> x * w \<le> y * z
[PROOF STEP]
by blast


[STATEMENT]
lemma comp_left_subdist_inf:
  "(x \<sqinter> y) * z \<le> x * z \<sqinter> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> y) * z \<le> x * z \<sqinter> y * z
[PROOF STEP]
by (simp add: comp_left_isotone)


[STATEMENT]
lemma comp_left_increasing_sup:
  "x * y \<le> (x \<squnion> z) * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<le> (x \<squnion> z) * y
[PROOF STEP]
by (simp add: comp_left_isotone)


[STATEMENT]
lemma comp_right_subdist_inf:
  "x * (y \<sqinter> z) \<le> x * y \<sqinter> x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y \<sqinter> z) \<le> x * y \<sqinter> x * z
[PROOF STEP]
by (simp add: comp_right_isotone)


[STATEMENT]
lemma comp_right_increasing_sup:
  "x * y \<le> x * (y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<le> x * (y \<squnion> z)
[PROOF STEP]
by (simp add: comp_right_isotone)


[STATEMENT]
lemma comp_right_zero [simp]:
  "x * bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * bot = bot
[PROOF STEP]
by (metis comp_left_zero conv_dist_comp conv_involutive)


[STATEMENT]
lemma comp_right_one [simp]:
  "x * 1 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (1::'a) = x
[PROOF STEP]
by (metis comp_left_one conv_dist_comp conv_involutive)


[STATEMENT]
lemma comp_left_conjugate:
  "conjugate (\<lambda>y . x * y) (\<lambda>y . x\<^sup>T * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate ((*) x) ((*) (x\<^sup>T))
[PROOF STEP]
apply (unfold conjugate_def, intro allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa y. (x * xa \<sqinter> y = bot) = (xa \<sqinter> x\<^sup>T * y = bot)
[PROOF STEP]
by (metis comp_right_zero bot.extremum_unique conv_involutive dedekind_1 inf.commute)


[STATEMENT]
lemma comp_right_conjugate:
  "conjugate (\<lambda>y . y * x) (\<lambda>y . y * x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (\<lambda>y. y * x) (\<lambda>y. y * x\<^sup>T)
[PROOF STEP]
apply (unfold conjugate_def, intro allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa y. (xa * x \<sqinter> y = bot) = (xa \<sqinter> y * x\<^sup>T = bot)
[PROOF STEP]
by (metis comp_left_conjugate[unfolded conjugate_def] conv_inf_bot_iff conv_dist_comp conv_involutive)


[STATEMENT]
lemma schroeder_1:
  "x * y \<sqinter> z = bot \<longleftrightarrow> x\<^sup>T * z \<sqinter> y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y \<sqinter> z = bot) = (x\<^sup>T * z \<sqinter> y = bot)
[PROOF STEP]
using abel_semigroup.commute comp_left_conjugate conjugate_def inf.abel_semigroup_axioms
[PROOF STATE]
proof (prove)
using this:
abel_semigroup ?f \<Longrightarrow> ?f ?a ?b = ?f ?b ?a
conjugate ((*) ?x) ((*) (?x\<^sup>T))
conjugate ?f ?g \<equiv> \<forall>x y. (?f x \<sqinter> y = bot) = (x \<sqinter> ?g y = bot)
abel_semigroup (\<sqinter>)

goal (1 subgoal):
 1. (x * y \<sqinter> z = bot) = (x\<^sup>T * z \<sqinter> y = bot)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma schroeder_2:
  "x * y \<sqinter> z = bot \<longleftrightarrow> z * y\<^sup>T \<sqinter> x = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y \<sqinter> z = bot) = (z * y\<^sup>T \<sqinter> x = bot)
[PROOF STEP]
by (metis comp_right_conjugate conjugate_def inf_commute)


[STATEMENT]
lemma comp_additive:
  "additive (\<lambda>y . x * y) \<and> additive (\<lambda>y . x\<^sup>T * y) \<and> additive (\<lambda>y . y * x) \<and> additive (\<lambda>y . y * x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. additive ((*) x) \<and> additive ((*) (x\<^sup>T)) \<and> additive (\<lambda>y. y * x) \<and> additive (\<lambda>y. y * x\<^sup>T)
[PROOF STEP]
by (simp add: comp_left_dist_sup additive_def comp_right_dist_sup)


[STATEMENT]
lemma dedekind_2:
  "y * x \<sqinter> z \<le> (y \<sqinter> (z * x\<^sup>T)) * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * x \<sqinter> z \<le> (y \<sqinter> z * x\<^sup>T) * x
[PROOF STEP]
by (metis conv_dist_inf conv_order conv_dist_comp dedekind_1)


[STATEMENT]
lemma vector_inf_comp:
  "vector x \<Longrightarrow> (x \<sqinter> y) * z = x \<sqinter> (y * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> (x \<sqinter> y) * z = x \<sqinter> y * z
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. vector x \<Longrightarrow> (x \<sqinter> y) * z \<le> x \<sqinter> y * z
 2. vector x \<Longrightarrow> x \<sqinter> y * z \<le> (x \<sqinter> y) * z
[PROOF STEP]
apply (metis comp_left_subdist_inf comp_right_isotone inf.sup_left_isotone order_lesseq_imp top_greatest)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> x \<sqinter> y * z \<le> (x \<sqinter> y) * z
[PROOF STEP]
by (metis comp_left_isotone comp_right_isotone dedekind_2 inf_commute inf_mono order_refl order_trans top_greatest)


[STATEMENT]
lemma vector_inf_closed:
  "vector x \<Longrightarrow> vector y \<Longrightarrow> vector (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector x; vector y\<rbrakk> \<Longrightarrow> vector (x \<sqinter> y)
[PROOF STEP]
by (simp add: vector_inf_comp)


[STATEMENT]
lemma vector_inf_one_comp:
  "vector x \<Longrightarrow> (x \<sqinter> 1) * y = x \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> (x \<sqinter> (1::'a)) * y = x \<sqinter> y
[PROOF STEP]
by (simp add: vector_inf_comp)


[STATEMENT]
lemma covector_inf_comp_1:
  assumes "vector x"
    shows "(y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
have "(y \<sqinter> x\<^sup>T) * z \<le> (y \<sqinter> x\<^sup>T) * (z \<sqinter> ((y\<^sup>T \<sqinter> x) * top))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * z \<le> (y \<sqinter> x\<^sup>T) * (z \<sqinter> (y\<^sup>T \<sqinter> x) * top)
[PROOF STEP]
by (metis inf_top_right dedekind_1 conv_dist_inf conv_involutive)
[PROOF STATE]
proof (state)
this:
(y \<sqinter> x\<^sup>T) * z \<le> (y \<sqinter> x\<^sup>T) * (z \<sqinter> (y\<^sup>T \<sqinter> x) * top)

goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y \<sqinter> x\<^sup>T) * z \<le> (y \<sqinter> x\<^sup>T) * (z \<sqinter> (y\<^sup>T \<sqinter> x) * top)

goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
have "... \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * (z \<sqinter> (y\<^sup>T \<sqinter> x) * top) \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
by (metis assms comp_left_isotone comp_right_isotone inf_le2 inf_mono order_refl inf_commute)
[PROOF STATE]
proof (state)
this:
(y \<sqinter> x\<^sup>T) * (z \<sqinter> (y\<^sup>T \<sqinter> x) * top) \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)

goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(y \<sqinter> x\<^sup>T) * z \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(y \<sqinter> x\<^sup>T) * z \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)

goal (1 subgoal):
 1. (y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
by (simp add: comp_right_isotone order.antisym)
[PROOF STATE]
proof (state)
this:
(y \<sqinter> x\<^sup>T) * z = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma covector_inf_comp_2:
  assumes "vector x"
    shows "y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
have "y * (x \<sqinter> z) \<le> (y \<sqinter> (top * (x \<sqinter> z)\<^sup>T)) * (x \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * (x \<sqinter> z) \<le> (y \<sqinter> top * (x \<sqinter> z)\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
by (metis dedekind_2 inf_top_right)
[PROOF STATE]
proof (state)
this:
y * (x \<sqinter> z) \<le> (y \<sqinter> top * (x \<sqinter> z)\<^sup>T) * (x \<sqinter> z)

goal (1 subgoal):
 1. y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y * (x \<sqinter> z) \<le> (y \<sqinter> top * (x \<sqinter> z)\<^sup>T) * (x \<sqinter> z)

goal (1 subgoal):
 1. y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
have "... \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<sqinter> top * (x \<sqinter> z)\<^sup>T) * (x \<sqinter> z) \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
by (metis assms comp_left_isotone conv_dist_comp conv_order conv_top eq_refl inf_le1 inf_mono)
[PROOF STATE]
proof (state)
this:
(y \<sqinter> top * (x \<sqinter> z)\<^sup>T) * (x \<sqinter> z) \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)

goal (1 subgoal):
 1. y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y * (x \<sqinter> z) \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y * (x \<sqinter> z) \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)

goal (1 subgoal):
 1. y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
using comp_left_subdist_inf order.antisym
[PROOF STATE]
proof (prove)
using this:
y * (x \<sqinter> z) \<le> (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
(?x \<sqinter> ?y) * ?z \<le> ?x * ?z \<sqinter> ?y * ?z
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * (x \<sqinter> z) = (y \<sqinter> x\<^sup>T) * (x \<sqinter> z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma covector_inf_comp_3:
  "vector x \<Longrightarrow> (y \<sqinter> x\<^sup>T) * z = y * (x \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> (y \<sqinter> x\<^sup>T) * z = y * (x \<sqinter> z)
[PROOF STEP]
by (metis covector_inf_comp_1 covector_inf_comp_2)


[STATEMENT]
lemma covector_inf_closed:
  "covector x \<Longrightarrow> covector y \<Longrightarrow> covector (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>covector x; covector y\<rbrakk> \<Longrightarrow> covector (x \<sqinter> y)
[PROOF STEP]
by (metis comp_right_subdist_inf order.antisym top_left_mult_increasing)


[STATEMENT]
lemma vector_conv_covector:
  "vector v \<longleftrightarrow> covector (v\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector v = covector (v\<^sup>T)
[PROOF STEP]
by (metis conv_dist_comp conv_involutive conv_top)


[STATEMENT]
lemma covector_conv_vector:
  "covector v \<longleftrightarrow> vector (v\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector v = vector (v\<^sup>T)
[PROOF STEP]
by (simp add: vector_conv_covector)


[STATEMENT]
lemma covector_comp_inf:
  "covector z \<Longrightarrow> x * (y \<sqinter> z) = x * y \<sqinter> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector z \<Longrightarrow> x * (y \<sqinter> z) = x * y \<sqinter> z
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. covector z \<Longrightarrow> x * (y \<sqinter> z) \<le> x * y \<sqinter> z
 2. covector z \<Longrightarrow> x * y \<sqinter> z \<le> x * (y \<sqinter> z)
[PROOF STEP]
apply (metis comp_isotone comp_right_subdist_inf inf.boundedE inf.boundedI inf.cobounded2 top.extremum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector z \<Longrightarrow> x * y \<sqinter> z \<le> x * (y \<sqinter> z)
[PROOF STEP]
by (metis comp_left_isotone comp_right_isotone dedekind_1 inf_commute inf_mono order_refl order_trans top_greatest)


[STATEMENT]
lemma vector_restrict_comp_conv:
  "vector x \<Longrightarrow> x \<sqinter> y \<le> x\<^sup>T * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector x \<Longrightarrow> x \<sqinter> y \<le> x\<^sup>T * y
[PROOF STEP]
by (metis covector_inf_comp_3 eq_refl inf.sup_monoid.add_commute inf_top_right le_supE sup.orderE top_left_mult_increasing)


[STATEMENT]
lemma covector_restrict_comp_conv:
  "covector x \<Longrightarrow> y \<sqinter> x \<le> y * x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector x \<Longrightarrow> y \<sqinter> x \<le> y * x\<^sup>T
[PROOF STEP]
by (metis conv_dist_comp conv_dist_inf conv_order conv_top inf.sup_monoid.add_commute vector_restrict_comp_conv)


[STATEMENT]
lemma covector_comp_inf_1:
  "covector x \<Longrightarrow> (y \<sqinter> x) * z = y * (x\<^sup>T \<sqinter> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector x \<Longrightarrow> (y \<sqinter> x) * z = y * (x\<^sup>T \<sqinter> z)
[PROOF STEP]
using covector_conv_vector covector_inf_comp_3
[PROOF STATE]
proof (prove)
using this:
covector ?v = vector (?v\<^sup>T)
vector ?x \<Longrightarrow> (?y \<sqinter> ?x\<^sup>T) * ?z = ?y * (?x \<sqinter> ?z)

goal (1 subgoal):
 1. covector x \<Longrightarrow> (y \<sqinter> x) * z = y * (x\<^sup>T \<sqinter> z)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma surjective_var:
  "surjective x \<longleftrightarrow> surjective_var x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective x = surjective_var x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. surjective x \<Longrightarrow> surjective_var x
 2. surjective_var x \<Longrightarrow> surjective x
[PROOF STEP]
assume "surjective x"
[PROOF STATE]
proof (state)
this:
surjective x

goal (2 subgoals):
 1. surjective x \<Longrightarrow> surjective_var x
 2. surjective_var x \<Longrightarrow> surjective x
[PROOF STEP]
thus "surjective_var x"
[PROOF STATE]
proof (prove)
using this:
surjective x

goal (1 subgoal):
 1. surjective_var x
[PROOF STEP]
by (metis dedekind_2 comp_left_one inf_absorb2 top_greatest)
[PROOF STATE]
proof (state)
this:
surjective_var x

goal (1 subgoal):
 1. surjective_var x \<Longrightarrow> surjective x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. surjective_var x \<Longrightarrow> surjective x
[PROOF STEP]
assume "surjective_var x"
[PROOF STATE]
proof (state)
this:
surjective_var x

goal (1 subgoal):
 1. surjective_var x \<Longrightarrow> surjective x
[PROOF STEP]
hence "x\<^sup>T * (x * top) = top"
[PROOF STATE]
proof (prove)
using this:
surjective_var x

goal (1 subgoal):
 1. x\<^sup>T * (x * top) = top
[PROOF STEP]
by (metis comp_left_isotone comp_associative comp_left_one top_le)
[PROOF STATE]
proof (state)
this:
x\<^sup>T * (x * top) = top

goal (1 subgoal):
 1. surjective_var x \<Longrightarrow> surjective x
[PROOF STEP]
thus "surjective x"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T * (x * top) = top

goal (1 subgoal):
 1. surjective x
[PROOF STEP]
by (metis comp_right_isotone conv_top conv_dist_comp conv_involutive top_greatest top_le)
[PROOF STATE]
proof (state)
this:
surjective x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma total_var:
  "total x \<longleftrightarrow> total_var x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total x = total_var x
[PROOF STEP]
by (metis conv_top conv_dist_comp conv_involutive surjective_var)


[STATEMENT]
lemma surjective_conv_total:
  "surjective x \<longleftrightarrow> total (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective x = times_top_class.total (x\<^sup>T)
[PROOF STEP]
by (metis conv_top conv_dist_comp conv_involutive)


[STATEMENT]
lemma total_conv_surjective:
  "total x \<longleftrightarrow> surjective (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total x = surjective (x\<^sup>T)
[PROOF STEP]
by (simp add: surjective_conv_total)


[STATEMENT]
lemma injective_conv_univalent:
  "injective x \<longleftrightarrow> univalent (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective x = univalent (x\<^sup>T)
[PROOF STEP]
by simp


[STATEMENT]
lemma univalent_conv_injective:
  "univalent x \<longleftrightarrow> injective (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent x = injective (x\<^sup>T)
[PROOF STEP]
by simp


[STATEMENT]
lemma univalent_bot_closed:
  "univalent bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent bot
[PROOF STEP]
by simp


[STATEMENT]
lemma univalent_one_closed:
  "univalent 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma univalent_inf_closed:
  "univalent x \<Longrightarrow> univalent (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent x \<Longrightarrow> univalent (x \<sqinter> y)
[PROOF STEP]
by (metis comp_left_subdist_inf comp_right_subdist_inf conv_dist_inf inf.cobounded1 order_lesseq_imp)


[STATEMENT]
lemma univalent_mult_closed:
  assumes "univalent x"
      and "univalent y"
    shows "univalent (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent (x * y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. univalent (x * y)
[PROOF STEP]
have "(x * y)\<^sup>T * x \<le> y\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y)\<^sup>T * x \<le> y\<^sup>T
[PROOF STEP]
by (metis assms(1) comp_left_isotone comp_right_one conv_one conv_order comp_associative conv_dist_comp conv_involutive)
[PROOF STATE]
proof (state)
this:
(x * y)\<^sup>T * x \<le> y\<^sup>T

goal (1 subgoal):
 1. univalent (x * y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * y)\<^sup>T * x \<le> y\<^sup>T

goal (1 subgoal):
 1. univalent (x * y)
[PROOF STEP]
by (metis assms(2) comp_left_isotone comp_associative dual_order.trans)
[PROOF STATE]
proof (state)
this:
univalent (x * y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma injective_bot_closed:
  "injective bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective bot
[PROOF STEP]
by simp


[STATEMENT]
lemma injective_one_closed:
  "injective 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma injective_inf_closed:
  "injective x \<Longrightarrow> injective (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective x \<Longrightarrow> injective (x \<sqinter> y)
[PROOF STEP]
by (metis conv_dist_inf injective_conv_univalent univalent_inf_closed)


[STATEMENT]
lemma injective_mult_closed:
  "injective x \<Longrightarrow> injective y \<Longrightarrow> injective (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>injective x; injective y\<rbrakk> \<Longrightarrow> injective (x * y)
[PROOF STEP]
by (metis injective_conv_univalent conv_dist_comp univalent_mult_closed)


[STATEMENT]
lemma mapping_one_closed:
  "mapping 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma mapping_mult_closed:
  "mapping x \<Longrightarrow> mapping y \<Longrightarrow> mapping (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mapping x; mapping y\<rbrakk> \<Longrightarrow> mapping (x * y)
[PROOF STEP]
by (simp add: comp_associative univalent_mult_closed)


[STATEMENT]
lemma bijective_one_closed:
  "bijective 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bijective (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma bijective_mult_closed:
  "bijective x \<Longrightarrow> bijective y \<Longrightarrow> bijective (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bijective x; bijective y\<rbrakk> \<Longrightarrow> bijective (x * y)
[PROOF STEP]
by (metis injective_mult_closed comp_associative)


[STATEMENT]
lemma bijective_conv_mapping:
  "bijective x \<longleftrightarrow> mapping (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bijective x = mapping (x\<^sup>T)
[PROOF STEP]
by (simp add: surjective_conv_total)


[STATEMENT]
lemma mapping_conv_bijective:
  "mapping x \<longleftrightarrow> bijective (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping x = bijective (x\<^sup>T)
[PROOF STEP]
by (simp add: total_conv_surjective)


[STATEMENT]
lemma reflexive_inf_closed:
  "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive x; reflexive y\<rbrakk> \<Longrightarrow> reflexive (x \<sqinter> y)
[PROOF STEP]
by simp


[STATEMENT]
lemma reflexive_conv_closed:
  "reflexive x \<Longrightarrow> reflexive (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive x \<Longrightarrow> reflexive (x\<^sup>T)
[PROOF STEP]
using conv_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x\<^sup>T \<le> ?y\<^sup>T

goal (1 subgoal):
 1. reflexive x \<Longrightarrow> reflexive (x\<^sup>T)
[PROOF STEP]
by force


[STATEMENT]
lemma coreflexive_inf_closed:
  "coreflexive x \<Longrightarrow> coreflexive (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> coreflexive (x \<sqinter> y)
[PROOF STEP]
by (simp add: le_infI1)


[STATEMENT]
lemma coreflexive_conv_closed:
  "coreflexive x \<Longrightarrow> coreflexive (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> coreflexive (x\<^sup>T)
[PROOF STEP]
using conv_order
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)

goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> coreflexive (x\<^sup>T)
[PROOF STEP]
by force


[STATEMENT]
lemma coreflexive_symmetric:
  "coreflexive x \<Longrightarrow> symmetric x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> symmetric x
[PROOF STEP]
by (metis comp_right_one comp_right_subdist_inf conv_dist_inf conv_dist_comp conv_involutive dedekind_1 inf.absorb1 inf_absorb2)


[STATEMENT]
lemma transitive_conv_closed:
  "transitive x \<Longrightarrow> transitive (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive x \<Longrightarrow> transitive (x\<^sup>T)
[PROOF STEP]
using conv_order conv_dist_comp
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T

goal (1 subgoal):
 1. transitive x \<Longrightarrow> transitive (x\<^sup>T)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma dense_conv_closed:
  "dense_rel x \<Longrightarrow> dense_rel (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel x \<Longrightarrow> dense_rel (x\<^sup>T)
[PROOF STEP]
using conv_order conv_dist_comp
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)
(?x * ?y)\<^sup>T = ?y\<^sup>T * ?x\<^sup>T

goal (1 subgoal):
 1. dense_rel x \<Longrightarrow> dense_rel (x\<^sup>T)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma idempotent_conv_closed:
  "idempotent x \<Longrightarrow> idempotent (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent x \<Longrightarrow> idempotent (x\<^sup>T)
[PROOF STEP]
by (metis conv_dist_comp)


[STATEMENT]
lemma preorder_inf_closed:
  "preorder x \<Longrightarrow> preorder y \<Longrightarrow> preorder (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preorder x; preorder y\<rbrakk> \<Longrightarrow> preorder (x \<sqinter> y)
[PROOF STEP]
using transitive_inf_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>transitive ?x; transitive ?y\<rbrakk> \<Longrightarrow> transitive (?x \<sqinter> ?y)

goal (1 subgoal):
 1. \<lbrakk>preorder x; preorder y\<rbrakk> \<Longrightarrow> preorder (x \<sqinter> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma preorder_conv_closed:
  "preorder x \<Longrightarrow> preorder (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preorder x \<Longrightarrow> preorder (x\<^sup>T)
[PROOF STEP]
by (simp add: reflexive_conv_closed transitive_conv_closed)


[STATEMENT]
lemma symmetric_bot_closed:
  "symmetric bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric bot
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_one_closed:
  "symmetric 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_top_closed:
  "symmetric top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric top
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_inf_closed:
  "symmetric x \<Longrightarrow> symmetric y \<Longrightarrow> symmetric (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>symmetric x; symmetric y\<rbrakk> \<Longrightarrow> symmetric (x \<sqinter> y)
[PROOF STEP]
by (simp add: conv_dist_inf)


[STATEMENT]
lemma symmetric_sup_closed:
  "symmetric x \<Longrightarrow> symmetric y \<Longrightarrow> symmetric (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>symmetric x; symmetric y\<rbrakk> \<Longrightarrow> symmetric (x \<squnion> y)
[PROOF STEP]
by (simp add: conv_dist_sup)


[STATEMENT]
lemma symmetric_conv_closed:
  "symmetric x \<Longrightarrow> symmetric (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric x \<Longrightarrow> symmetric (x\<^sup>T)
[PROOF STEP]
by simp


[STATEMENT]
lemma one_inf_conv:
  "1 \<sqinter> x = 1 \<sqinter> x\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<sqinter> x = (1::'a) \<sqinter> x\<^sup>T
[PROOF STEP]
by (metis conv_dist_inf coreflexive_symmetric inf.cobounded1 symmetric_one_closed)


[STATEMENT]
lemma antisymmetric_bot_closed:
  "antisymmetric bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisymmetric bot
[PROOF STEP]
by simp


[STATEMENT]
lemma antisymmetric_one_closed:
  "antisymmetric 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisymmetric (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma antisymmetric_inf_closed:
  "antisymmetric x \<Longrightarrow> antisymmetric (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisymmetric x \<Longrightarrow> antisymmetric (x \<sqinter> y)
[PROOF STEP]
by (rule order_trans[where y="x \<sqinter> x\<^sup>T"]) (simp_all add: conv_isotone inf.coboundedI2 inf.sup_assoc)


[STATEMENT]
lemma antisymmetric_conv_closed:
  "antisymmetric x \<Longrightarrow> antisymmetric (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisymmetric x \<Longrightarrow> antisymmetric (x\<^sup>T)
[PROOF STEP]
by (simp add: inf_commute)


[STATEMENT]
lemma asymmetric_bot_closed:
  "asymmetric bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asymmetric bot
[PROOF STEP]
by simp


[STATEMENT]
lemma asymmetric_inf_closed:
  "asymmetric x \<Longrightarrow> asymmetric (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asymmetric x \<Longrightarrow> asymmetric (x \<sqinter> y)
[PROOF STEP]
by (metis conv_dist_inf inf.mult_zero_left inf.left_commute inf_assoc)


[STATEMENT]
lemma asymmetric_conv_closed:
  "asymmetric x \<Longrightarrow> asymmetric (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asymmetric x \<Longrightarrow> asymmetric (x\<^sup>T)
[PROOF STEP]
by (simp add: inf_commute)


[STATEMENT]
lemma linear_top_closed:
  "linear top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear top
[PROOF STEP]
by simp