diff --git a/thys/Real_Time_Deque/Big.thy b/thys/Real_Time_Deque/Big.thy
--- a/thys/Real_Time_Deque/Big.thy
+++ b/thys/Real_Time_Deque/Big.thy
@@ -1,47 +1,47 @@
 section \<open>Bigger End of Deque\<close>
 
 theory Big
 imports Common
 begin
 
 text \<open>\<^noindent> The bigger end of the deque during transformation can be in two phases:
 
  \<^descr> \<open>Reverse\<close>: Using the \<open>step\<close> function the originally contained elements, 
     which will be kept in this end, are reversed.
  \<^descr> \<open>Common\<close>: Specified in theory \<open>Common\<close>. Is used to reverse the elements from the previous phase 
     again to get them in the original order.
 
 \<^noindent> Each phase contains a \<open>current\<close> state, which holds the original elements of the deque end. 
 \<close>
 
 datatype (plugins del: size) 'a big_state = 
      Reverse "'a current" "'a stack" "'a list" nat
-   | Common "'a Common.state"
+   | Common "'a common_state"
 
 text \<open>\<^noindent> Functions:
 
 \<^descr> \<open>push\<close>, \<open>pop\<close>: Add and remove elements using the \<open>current\<close> state.
 \<^descr> \<open>step\<close>: Executes one step of the transformation\<close>
 
 instantiation big_state ::(type) step
 begin
 
 fun step_big_state :: "'a big_state \<Rightarrow> 'a big_state" where
   "step (Common state) = Common (step state)"
 | "step (Reverse current _ aux 0) = Common (normalize (Copy current aux [] 0))"
 | "step (Reverse current big aux count) = 
      Reverse current (Stack.pop big) ((Stack.first big)#aux) (count - 1)"
 
 instance..
 end
 
 fun push :: "'a \<Rightarrow> 'a big_state \<Rightarrow> 'a big_state" where
   "push x (Common state) = Common (Common.push x state)"
 | "push x (Reverse current big aux count) = Reverse (Current.push x current) big aux count"
 
 fun pop :: "'a big_state \<Rightarrow> 'a * 'a big_state" where
   "pop (Common state) = (let (x, state) = Common.pop state in (x, Common state))"
 | "pop (Reverse current big aux count) = 
     (first current, Reverse (drop_first current) big aux count)"
 
 end
diff --git a/thys/Real_Time_Deque/Common.thy b/thys/Real_Time_Deque/Common.thy
--- a/thys/Real_Time_Deque/Common.thy
+++ b/thys/Real_Time_Deque/Common.thy
@@ -1,63 +1,63 @@
 section \<open>Common\<close>
 
 theory Common
 imports Current Idle
 begin
 
 text \<open>
 \<^noindent> The last two phases of both deque ends during transformation:
 
  \<^descr> \<open>Copy\<close>: Using the \<open>step\<close> function the new elements of this deque end are brought back into the original order.
  \<^descr> \<open>Idle\<close>: The transformation of the deque end is finished.
 
 \<^noindent> Each phase contains a \<open>current\<close> state, that holds the original elements of the deque end.
 \<close>
 
-datatype (plugins del: size)'a state = 
+datatype (plugins del: size)'a common_state = 
       Copy "'a current" "'a list" "'a list" nat
     | Idle "'a current" "'a idle"
 
 text\<open>
 \<^noindent> Functions:
 
 \<^descr> \<open>push\<close>, \<open>pop\<close>: Add and remove elements using the \<open>current\<close> state.
 \<^descr> \<open>step\<close>: Executes one step of the transformation, while keeping the invariant.\<close>
 
 (* TODO: Maybe inline function? *)
-fun normalize :: "'a state \<Rightarrow> 'a state" where
+fun normalize :: "'a common_state \<Rightarrow> 'a common_state" where
   "normalize (Copy current old new moved) = (
     case current of Current extra added _ remained \<Rightarrow> 
       if moved \<ge> remained
       then Idle current (idle.Idle (Stack extra new) (added + moved))
       else Copy current old new moved
   )"
 
 
-instantiation state ::(type) step
+instantiation common_state ::(type) step
 begin
 
-fun step_state :: "'a state \<Rightarrow> 'a state" where
+fun step_common_state :: "'a common_state \<Rightarrow> 'a common_state" where
   "step (Idle current idle) = Idle current idle"
 | "step (Copy current aux new moved) = (
     case current of Current _ _ _ remained \<Rightarrow>
       normalize (
         if moved < remained
         then Copy current (tl aux) ((hd aux)#new) (moved + 1)
         else Copy current aux new moved
       )
   )"
 
 instance..
 end
 
-fun push :: "'a \<Rightarrow> 'a state \<Rightarrow> 'a state" where
+fun push :: "'a \<Rightarrow> 'a common_state \<Rightarrow> 'a common_state" where
   "push x (Idle current (idle.Idle stack stackSize)) = 
       Idle (Current.push x current) (idle.Idle (Stack.push x stack) (Suc stackSize))"
 | "push x (Copy current aux new moved) = Copy (Current.push x current) aux new moved"
 
-fun pop :: "'a state \<Rightarrow> 'a * 'a state" where
+fun pop :: "'a common_state \<Rightarrow> 'a * 'a common_state" where
   "pop (Idle current idle) = (let (x, idle) = Idle.pop idle in (x, Idle (drop_first current) idle))"
 | "pop (Copy current aux new moved) = 
       (first current, normalize (Copy (drop_first current) aux new moved))"
 
 end
diff --git a/thys/Real_Time_Deque/Common_Aux.thy b/thys/Real_Time_Deque/Common_Aux.thy
--- a/thys/Real_Time_Deque/Common_Aux.thy
+++ b/thys/Real_Time_Deque/Common_Aux.thy
@@ -1,79 +1,79 @@
 theory Common_Aux
 imports Common Current_Aux Idle_Aux
 begin
 
 text\<open>
 \<^noindent> Functions:
 
 \<^descr> \<open>list\<close>: List abstraction of the elements which this end will contain after the transformation is finished
 \<^descr> \<open>list_current\<close>: List abstraction of the elements currently in this deque end.
 \<^descr> \<open>remaining_steps\<close>: Returns how many steps are left until the transformation is finished.
 \<^descr> \<open>size_new\<close>: Returns the size, that the deque end will have after the transformation is finished.
 \<^descr> \<open>size\<close>: Minimum of \<open>size_new\<close> and the number of elements contained in the \<open>current\<close> state.\<close>
 
 definition take_rev where 
 [simp]:  "take_rev n xs = rev (take n xs)"
 
-fun list :: "'a state \<Rightarrow> 'a list" where
+fun list :: "'a common_state \<Rightarrow> 'a list" where
   "list (Idle _ idle) = Idle_Aux.list idle"
 | "list (Copy (Current extra _ _ remained) old new moved) 
    = extra @ take_rev (remained - moved) old @ new"
 
-fun list_current :: "'a state \<Rightarrow> 'a list" where
+fun list_current :: "'a common_state \<Rightarrow> 'a list" where
   "list_current (Idle current _) = Current_Aux.list current"
 | "list_current (Copy current _ _ _) = Current_Aux.list current"
 
-instantiation state::(type) invar
+instantiation common_state::(type) invar
 begin
 
-fun invar_state :: "'a state \<Rightarrow> bool" where
+fun invar_common_state :: "'a common_state \<Rightarrow> bool" where
   "invar (Idle current idle) \<longleftrightarrow>
       invar idle 
     \<and> invar current 
     \<and> size_new current = size idle
     \<and> take (size idle) (Current_Aux.list current) = 
       take (size current) (Idle_Aux.list idle)"
 | "invar (Copy current aux new moved) \<longleftrightarrow> (
     case current of Current _ _ old remained \<Rightarrow>
       moved < remained
     \<and> moved = length new
     \<and> remained \<le> length aux + moved
     \<and> invar current
     \<and> take remained (Stack_Aux.list old) = take (size old) (take_rev (remained - moved) aux @ new)
  )"
 
 instance..
 end
 
-instantiation state::(type) size
+instantiation common_state::(type) size
 begin
 
-fun size_state :: "'a state \<Rightarrow> nat" where
+fun size_common_state :: "'a common_state \<Rightarrow> nat" where
   "size (Idle current idle) = min (size current) (size idle)"
 | "size (Copy current _ _ _) = min (size current) (size_new current)"
 
 instance..
 end
 
-instantiation state::(type) size_new
+instantiation common_state::(type) size_new
 begin
 
-fun size_new_state :: "'a state \<Rightarrow> nat" where
+fun size_new_common_state :: "'a common_state \<Rightarrow> nat" where
   "size_new (Idle current _) = size_new current"
 | "size_new (Copy current _ _ _) = size_new current"
 
 instance..
 end
 
-instantiation state::(type) remaining_steps
+instantiation common_state::(type) remaining_steps
 begin
 
-fun remaining_steps_state :: "'a state \<Rightarrow> nat" where
+fun remaining_steps_common_state :: "'a common_state \<Rightarrow> nat" where
   "remaining_steps (Idle _ _) = 0"
 | "remaining_steps (Copy (Current _ _ _ remained) aux new moved) = remained - moved"
 
 instance..
 end
 
 
 end
diff --git a/thys/Real_Time_Deque/Common_Proof.thy b/thys/Real_Time_Deque/Common_Proof.thy
--- a/thys/Real_Time_Deque/Common_Proof.thy
+++ b/thys/Real_Time_Deque/Common_Proof.thy
@@ -1,475 +1,479 @@
 section "Common Proofs"
 
 theory Common_Proof
 imports Common_Aux Idle_Proof Current_Proof
 begin
 
 lemma take_rev_drop: "take_rev n xs @ acc = drop (length xs - n) (rev xs) @ acc"
   unfolding take_rev_def using rev_take by blast
 
 lemma take_rev_step: "xs \<noteq> [] \<Longrightarrow> take_rev n (tl xs) @ (hd xs # acc) = take_rev (Suc n) xs @ acc"
   by (simp add: take_Suc)
 
 lemma take_rev_empty [simp]: "take_rev n [] = []"
   by simp
 
 lemma take_rev_tl_hd: 
     "0 < n \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> take_rev  n xs @ ys = take_rev (n - (Suc 0)) (tl xs) @ (hd xs #ys)"
   by (simp add: take_rev_step del: take_rev_def)
 
 lemma take_rev_nth: 
     "n < length xs \<Longrightarrow> x = xs ! n \<Longrightarrow> x # take_rev n xs @ ys = take_rev (Suc n) xs @ ys"
   by (simp add: take_Suc_conv_app_nth)
 
 lemma step_list [simp]: "invar common \<Longrightarrow> list (step common) = list common"
-proof(induction common rule: step_state.induct)
+proof(induction common rule: step_common_state.induct)
   case (1 idle)
   then show ?case by auto
 next
   case (2 current aux new moved)
 
   then show ?case 
   proof(cases current)
     case (Current extra added old remained)
     
     with 2 have aux_not_empty: "aux \<noteq> []"
         by auto
 
     from 2 Current show ?thesis 
     proof(cases "remained \<le> Suc moved")
       case True
      
       with 2 Current have "remained - length new = 1"
         by auto
 
       with True Current 2 aux_not_empty show ?thesis 
-        by(auto simp: )
+        by auto
     next
       case False
       with Current show ?thesis 
         by(auto simp: aux_not_empty take_rev_step Suc_diff_Suc simp del: take_rev_def)
     qed
   qed
 qed
 
 lemma step_list_current [simp]: "invar common \<Longrightarrow> list_current (step common) = list_current common"
   by(cases common)(auto split: current.splits)
 
 lemma push_list [simp]: "list (push x common) = x # list common"
 proof(induction x common rule: push.induct)
   case (1 x stack stackSize)
   then show ?case 
     by auto
 next
   case (2 x current aux new moved)
   then show ?case 
     by(induction x current rule: Current.push.induct) auto
 qed
 
-lemma invar_step: "invar (common :: 'a state) \<Longrightarrow> invar (step common)" 
-proof(induction "common" rule: invar_state.induct)
+lemma invar_step: "invar (common :: 'a common_state) \<Longrightarrow> invar (step common)" 
+proof(induction "common" rule: invar_common_state.induct)
   case (1 idle)
   then show ?case
     by auto
 next
   case (2 current aux new moved)
   then show ?case
   proof(cases current)
     case (Current extra added old remained)
     then show ?thesis
     proof(cases "aux = []")
       case True
       with 2 Current show ?thesis by auto 
     next
       case False
       note AUX_NOT_EMPTY = False
 
       then show ?thesis
       proof(cases "remained \<le> Suc (length new)")
         case True
         with 2 Current False 
           have "take (Suc (length new)) (Stack_Aux.list old) = take (size old) (hd aux # new)"
             by(auto simp: le_Suc_eq take_Cons')
          
         with 2 Current True show ?thesis 
           by auto
       next
         case False
         with 2 Current AUX_NOT_EMPTY show ?thesis 
           by(auto simp: take_rev_step Suc_diff_Suc simp del: take_rev_def)
       qed
     qed
   qed
 qed
 
 lemma invar_push: "invar common \<Longrightarrow> invar (push x common)"
 proof(induction x common rule: push.induct)
   case (1 x current stack stackSize)
   then show ?case
   proof(induction x current rule: Current.push.induct)
     case (1 x extra added old remained)
     then show ?case
     proof(induction x stack rule: Stack.push.induct)
       case (1 x left right)
       then show ?case by auto
     qed
   qed
 next
   case (2 x current aux new moved)
   then show ?case
   proof(induction x current rule: Current.push.induct)
     case (1 x extra added old remained)
     then show ?case by auto
   qed
 qed
 
 lemma invar_pop: "\<lbrakk>
   0 < size common; 
   invar common;
   pop common = (x, common')
 \<rbrakk> \<Longrightarrow> invar common'"
 proof(induction common arbitrary: x rule: pop.induct)
   case (1 current idle)
   then obtain idle' where idle: "Idle.pop idle = (x, idle')"
     by(auto split: prod.splits)
 
   obtain current' where current: "drop_first current = current'"
     by auto
 
   from 1 current idle show ?case 
     using Idle_Proof.size_pop[of idle x idle', symmetric] 
         size_new_pop[of current] 
         size_pop_sub[of current _ current']
     by(auto simp: Idle_Proof.invar_pop invar_pop eq_snd_iff take_tl size_not_empty)
 next
   case (2 current aux new moved)
   then show ?case 
   proof(induction current rule: Current.pop.induct)
     case (1 added old remained)
     then show ?case
     proof(cases "remained - Suc 0 \<le> length new")
       case True
 
       with 1 have [simp]: 
           "0 < size old" 
           "Stack_Aux.list old \<noteq> []" 
           "aux \<noteq> []"
           "length new = remained - Suc 0"
         by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
 
       then have [simp]: "Suc 0 \<le> size old" 
         by linarith
 
       from 1 have "0 < remained"
         by auto
 
       then have "take remained (Stack_Aux.list old)
           = hd (Stack_Aux.list old) # take (remained - Suc 0) (tl (Stack_Aux.list old))"
         by (metis Suc_pred \<open>Stack_Aux.list old \<noteq> []\<close> list.collapse take_Suc_Cons)
 
       with 1 True show ?thesis 
         using Stack_Proof.pop_list[of old] 
         by(auto simp: Stack_Proof.size_not_empty)
     next
       case False
       with 1 have "remained - Suc 0 \<le> length aux + length new" by auto
 
       with 1 False show ?thesis 
         using Stack_Proof.pop_list[of old]
         apply(auto simp: Suc_diff_Suc take_tl Stack_Proof.size_not_empty tl_append_if)
         by (simp add: Suc_diff_le rev_take tl_drop_2 tl_take)
     qed
    next
     case (2 x xs added old remained)
     then show ?case by auto
   qed
 qed
 
 lemma push_list_current [simp]: "list_current (push x left) = x # list_current left"
   by(induction x left rule: push.induct) auto
 
 lemma pop_list [simp]: "invar common \<Longrightarrow> 0 < size common \<Longrightarrow> pop common = (x, common') \<Longrightarrow>
    x # list common' = list common"
 proof(induction common arbitrary: x rule: pop.induct)
   case 1
   then show ?case
     by(auto simp: size_not_empty split: prod.splits)
 next
   case (2 current aux new moved)
   then show ?case
   proof(induction current rule: Current.pop.induct)
     case (1 added old remained)
     then show ?case
     proof(cases "remained - Suc 0 \<le> length new")
       case True
 
       from 1 True have [simp]: 
           "aux \<noteq> []" "0 < remained" 
           "Stack_Aux.list old \<noteq> []" "remained - length new = 1"
         by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
 
       then have "take remained (Stack_Aux.list old) = hd aux # take (size old - Suc 0) new
              \<Longrightarrow> Stack.first old = hd aux"
         by (metis first_hd hd_take list.sel(1))
      
       with 1 True take_hd[of aux] show ?thesis 
         by(auto simp: Suc_leI)
     next
       case False
       then show ?thesis 
       proof(cases "remained - length new = length aux")
         case True
 
         then have length_minus_1: "remained - Suc (length new) = length aux - 1"
           by simp
 
         from 1 have not_empty: "0 < remained" "0 < size old"  "aux \<noteq> []" "\<not> is_empty old"
           by(auto simp: Stack_Proof.size_not_empty)
 
         from 1 True not_empty have "take 1 (Stack_Aux.list old) = take 1 (rev aux)"
           using take_1[of 
                 remained 
                 "size old" 
                 "Stack_Aux.list old"  
                 "(rev aux) @ take (size old + length new - remained) new"
                 ] 
           by(simp)
          
         then have "[last aux] = [Stack.first old]"
           using take_last first_take not_empty
           by fastforce
 
         then have "last aux = Stack.first old"
           by auto
 
         with 1 True False show ?thesis 
           using not_empty last_drop_rev[of aux]
           by(auto simp: take_rev_drop length_minus_1 simp del: take_rev_def)
        next
         case False
 
         with 1 have a: "take (remained - length new) aux \<noteq> []"
           by auto
 
         from 1 False have b: "\<not> is_empty old"
           by(auto simp: Stack_Proof.size_not_empty)
 
         from 1 have c: "remained - Suc (length new) < length aux"
           by auto
 
-        from 1 have not_empty: "0 < remained" "0 < size old" "0 < remained - length new" "0 < length aux" 
+        from 1 have not_empty: 
+            "0 < remained" 
+            "0 < size old" 
+            "0 < remained - length new" 
+            "0 < length aux" 
           by auto
 
         with False have 
            "take remained (Stack_Aux.list old) =
             take (size old) (take_rev (remained - length new) aux @ new)
             \<Longrightarrow> take (Suc 0) (Stack_Aux.list old) =
                 take (Suc 0) (rev (take (remained - length new) aux))"
           using take_1[of
                 remained 
                 "size old" 
                 "Stack_Aux.list old" 
                 " (take_rev (remained - length new) aux @ new)"
               ]
           by(auto simp: not_empty Suc_le_eq)
 
         with 1 False have 
             "take 1 (Stack_Aux.list old) = take 1 (rev (take (remained - length new) aux))"
           by auto
           
         then have d: "[Stack.first old] = [last (take (remained - length new) aux)]"
           using take_last first_take a b
           by metis
 
         have "last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) 
             = rev (take (remained - length new) aux)"
           using Suc_diff_Suc c not_empty
           by (metis a drop_drop last_drop_rev plus_1_eq_Suc rev_take zero_less_diff)
           
         with 1(1) 1(3) False not_empty d show ?thesis 
           by(cases "remained - length new = 1") (auto)
       qed
     qed
   next
     case 2
     then show ?case by auto
   qed
 qed
 
 lemma pop_list_current: "invar common \<Longrightarrow> 0 < size common \<Longrightarrow> pop common = (x, common')
    \<Longrightarrow> x # list_current common' = list_current common"
 proof(induction common arbitrary: x rule: pop.induct)
   case (1 current idle)
   then show ?case 
   proof(induction idle rule: Idle.pop.induct)
     case (1 stack stackSize)
     then show ?case
     proof(induction current rule: Current.pop.induct)
       case (1 added old remained)
       then have "Stack.first old = Stack.first stack"
         using take_first[of old stack]
         by auto
 
       with 1 show ?case 
         by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
     next
       case (2 x xs added old remained)
       then have "0 < size stack" 
         by auto
 
       with Stack_Proof.size_not_empty Stack_Proof.list_not_empty
       have not_empty: "\<not> is_empty stack" "Stack_Aux.list stack \<noteq> []"
         by auto
 
       with 2 have "hd (Stack_Aux.list stack) = x"
         using take_hd'[of "Stack_Aux.list stack" x "xs @ Stack_Aux.list old"]
         by auto
        
       with 2 show ?case 
         using first_list[of stack] not_empty
         by auto
     qed
   qed
 next
   case (2 current)
   then show ?case
   proof(induction current rule: Current.pop.induct)
     case (1 added old remained)
     then have "\<not> is_empty old"
       by(auto simp: Stack_Proof.size_not_empty)
 
     with 1 show ?case
       using first_pop
       by(auto simp: Stack_Proof.list_not_empty)
   next
     case 2
     then show ?case by auto
   qed
 qed
 
 lemma list_current_size [simp]: 
   "\<lbrakk>0 < size common; list_current common = []; invar common\<rbrakk> \<Longrightarrow> False"
-proof(induction common rule: invar_state.induct)
+proof(induction common rule: invar_common_state.induct)
   case 1
   then show ?case
     using list_size by auto
 next
   case (2 current)
   then have "invar current" 
             "Current_Aux.list current = []"  
             "0 < size current" 
     by(auto split: current.splits)
  
   then show ?case using list_size by auto
 qed
 
 lemma list_size [simp]: "\<lbrakk>0 < size common; list common = []; invar common\<rbrakk> \<Longrightarrow> False"
-proof(induction common rule: invar_state.induct)
+proof(induction common rule: invar_common_state.induct)
   case 1
   then show ?case
     using list_size Idle_Proof.size_empty
     by auto
 next
   case (2 current aux new moved)
   then have "invar current" 
             "Current_Aux.list current = []"  
             "0 < size current" 
     by(auto split: current.splits)
  
   then show ?case using list_size by auto
 qed
   
-lemma step_size [simp]: "invar (common :: 'a state) \<Longrightarrow> size (step common) = size common"
-proof(induction common rule: step_state.induct)
+lemma step_size [simp]: "invar (common :: 'a common_state) \<Longrightarrow> size (step common) = size common"
+proof(induction common rule: step_common_state.induct)
   case 1
   then show ?case by auto
 next
   case 2
   then show ?case 
     by(auto simp: min_def split: current.splits)
 qed
 
-lemma step_size_new [simp]: "invar (common :: 'a state)
+lemma step_size_new [simp]: "invar (common :: 'a common_state)
    \<Longrightarrow> size_new (step common) = size_new common"
-proof(induction common rule: step_state.induct)
+proof(induction common rule: step_common_state.induct)
   case (1 current idle)
   then show ?case by auto
 next
   case (2 current aux new moved)
   then show ?case by(auto split: current.splits)
 qed
 
-lemma remaining_steps_step [simp]: "\<lbrakk>invar (common :: 'a state); remaining_steps common > 0\<rbrakk>
+lemma remaining_steps_step [simp]: "\<lbrakk>invar (common :: 'a common_state); remaining_steps common > 0\<rbrakk>
    \<Longrightarrow> Suc (remaining_steps (step common)) = remaining_steps common"
   by(induction common)(auto split: current.splits)
 
-lemma remaining_steps_step_sub [simp]: "\<lbrakk>invar (common :: 'a state)\<rbrakk>
+lemma remaining_steps_step_sub [simp]: "\<lbrakk>invar (common :: 'a common_state)\<rbrakk>
  \<Longrightarrow> remaining_steps (step common) = remaining_steps common - 1"
   by(induction common)(auto split: current.splits)
 
-lemma remaining_steps_step_0 [simp]: "\<lbrakk>invar (common :: 'a state); remaining_steps common = 0\<rbrakk>
+lemma remaining_steps_step_0 [simp]: "\<lbrakk>invar (common :: 'a common_state); remaining_steps common = 0\<rbrakk>
    \<Longrightarrow> remaining_steps (step common) = 0"
   by(induction common)(auto split: current.splits)
 
 lemma remaining_steps_push [simp]: "invar common
    \<Longrightarrow> remaining_steps (push x common) = remaining_steps common"
   by(induction x common rule: Common.push.induct)(auto split: current.splits)
 
 lemma remaining_steps_pop: "\<lbrakk>invar common; pop common = (x, common')\<rbrakk> 
   \<Longrightarrow> remaining_steps common' \<le> remaining_steps common"
 proof(induction common rule: pop.induct)
   case (1 current idle)
   then show ?case 
   proof(induction idle rule: Idle.pop.induct)
     case 1
     then show ?case  
       by(induction current rule: Current.pop.induct) auto
   qed
 next
   case (2 current aux new moved)
   then show ?case 
     by(induction current rule: Current.pop.induct) auto
 qed
 
 lemma size_push [simp]: "invar common \<Longrightarrow> size (push x common) = Suc (size common)"
   by(induction x common rule: push.induct) (auto split: current.splits)
  
 lemma size_new_push [simp]: "invar common \<Longrightarrow> size_new (push x common) = Suc (size_new common)"
   by(induction x common rule: Common.push.induct) (auto split: current.splits)
 
 lemma size_pop [simp]: "\<lbrakk>invar common; 0 < size common; pop common = (x, common')\<rbrakk>
    \<Longrightarrow> Suc (size common') = size common"
 proof(induction common rule: Common.pop.induct)
   case (1 current idle)
   then show ?case 
     using size_drop_first_sub[of current] Idle_Proof.size_pop_sub[of idle]
     by(auto simp: size_not_empty split: prod.splits)
 next
   case (2 current aux new moved)
   then show ?case 
     by(induction current rule: Current.pop.induct) auto
 qed
 
 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(induction common rule: Common.pop.induct)
   case (1 current idle)
   then show ?case
     using size_new_pop[of current]
     by(auto split: prod.splits)
 next
   case (2 current aux new moved)
   then show ?case 
   proof(induction current rule: Current.pop.induct)
     case (1 added old remained)
     then show ?case by auto
   next
     case (2 x xs added old remained)
     then show ?case by auto
   qed
 qed
 
-lemma size_size_new: "\<lbrakk>invar (common :: 'a state); 0 < size common\<rbrakk> \<Longrightarrow> 0 < size_new common"
+lemma size_size_new: "\<lbrakk>invar (common :: 'a common_state); 0 < size common\<rbrakk> \<Longrightarrow> 0 < size_new common"
   by(cases common) auto
 
 end
\ No newline at end of file
diff --git a/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy
--- a/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy
+++ b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy
@@ -1,471 +1,471 @@
 section "Dequeue Proofs"
 
 theory RealTimeDeque_Dequeue_Proof
 imports Deque RealTimeDeque_Aux States_Proof
 begin
  
 lemma list_deqL' [simp]: "\<lbrakk>invar deque; listL deque \<noteq> []; deqL' deque = (x, deque')\<rbrakk>
    \<Longrightarrow> x # listL deque' = listL deque"
 proof(induction deque arbitrary: x rule: deqL'.induct)
   case (4 left right length_right)
 
   then obtain left' where pop_left[simp]: "Idle.pop left = (x, left')"
     by(auto simp: Let_def split: if_splits stack.splits prod.splits idle.splits)
 
   then obtain stack_left' length_left' 
     where left'[simp]: "left' = idle.Idle stack_left' length_left'"
     using idle.exhaust by blast
 
   from 4 have invar_left': "invar left'"
     using Idle_Proof.invar_pop[of left]
     by auto
 
   then have size_left' [simp]: "size stack_left' = length_left'"
     by auto
 
   have size_left'_size_left [simp]: "size stack_left' = (size left) - 1"
     using Idle_Proof.size_pop_sub[of left x left']
     by auto
 
   show ?case
   proof(cases "3 * length_left' \<ge> length_right")
     case True
     with 4 pop_left show ?thesis
       using Idle_Proof.pop_list[of left x left']
       by auto
   next
     case False
     note Start_Transformation = False
 
     then show ?thesis
     proof(cases "length_left' \<ge> 1")
       case True
       let ?big = "Reverse (Current [] 0 right (size right - Suc length_left')) 
                            right [] (size right - Suc length_left')"
       let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []"
       let ?states = "States Left ?big ?small"
 
       from 4 Start_Transformation True invar_left' have invar: "invar ?states"
         by(auto simp: Let_def rev_take rev_drop)
 
       with 4 Start_Transformation True invar_left'
       have "States_Aux.listL ?states = tl (Idle_Aux.list left) @ rev (Stack_Aux.list right)"
         using pop_list_tl'[of left x left'] 
         by (auto simp del: take_rev_def)
     
       with invar 
       have "States_Aux.listL ((step^^6) ?states) = 
             tl (Idle_Aux.list left) @ rev (Stack_Aux.list right)"
         using step_n_listL[of ?states 6]
         by presburger
       
       with 4 Start_Transformation True show ?thesis 
         by(auto simp: Let_def)
     next
       case False
       from False Start_Transformation 4 have [simp]:"size left = 1"
         using size_left' size_left'_size_left by auto
         
       with False Start_Transformation 4 have [simp]: "Idle_Aux.list left = [x]"
         by(induction left)(auto simp: length_one_hd split: stack.splits)
 
       obtain right1 right2 where "right = Stack right1 right2"
         using Stack_Aux.list.cases by blast
 
       with False Start_Transformation 4 show ?thesis 
         by(induction right1 right2 rule: small_deque.induct) auto
     qed 
   qed
 next
   case (5 big small)
 
   then have start_invar: "invar (States Left big small)"
     by auto
 
   from 5 have small_invar: "invar small"
     by auto
 
   from 5 have small_size: "0 < size small"
     by auto
 
   with 5(3) obtain small' where pop: "Small.pop small = (x, small')"
     by(cases small)
       (auto simp: Let_def split: states.splits direction.splits state_splits prod.splits)
 
   let ?states_new = "States Left big small'"
   let ?states_stepped = "(step^^4) ?states_new"
 
   have invar: "invar ?states_new"
     using pop start_invar small_size invar_pop_small[of Left big small x small']
     by auto
 
   have "x # Small_Aux.list_current small' = Small_Aux.list_current small"
     using small_invar small_size pop Small_Proof.pop_list_current[of small x small'] by auto
     
   then have listL: 
       "x # States_Aux.listL ?states_new = 
        Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     using invar small_size Small_Proof.pop_list_current[of small x small'] 5(1)
     by auto      
 
   from invar have "invar ?states_stepped"
     using invar_step_n by blast
 
   then have states_listL_list_current [simp]: "x # States_Aux.listL ?states_stepped = 
                 Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     using States_Proof.step_n_listL invar listL by metis
 
   then have "listL (deqL (Transforming (States Left big small))) = States_Aux.listL ?states_stepped"
     by(auto simp: Let_def pop split: prod.splits direction.splits states.splits state_splits)
 
   then have states_listL_list_current: 
       "x # listL (deqL (Transforming (States Left big small))) =
        Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     by auto
 
   with 5(1) have "listL (Transforming (States Left big small)) = 
                   Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     by auto
 
   with states_listL_list_current 
   have "x # listL (deqL (Transforming (States Left big small))) = 
         listL (Transforming (States Left big small))"
     by auto
 
   with 5 show ?case by auto
 next
   case (6 big small)
   then have start_invar: "invar (States Right big small)"
     by auto
 
   from 6 have big_invar: "invar big"
     by auto
 
   from 6 have big_size: "0 < size big"
     by auto
 
   with 6(3) obtain big' where pop: "Big.pop big = (x, big')"
     by(cases big)
       (auto simp: Let_def split: prod.splits direction.splits states.splits state_splits)
 
   let ?states_new = "States Right big' small"
   let ?states_stepped = "(step^^4) ?states_new"
 
   have invar: "invar ?states_new"
     using pop start_invar big_size invar_pop_big[of Right big small]
     by auto
 
   have big_list_current: "x # Big_Aux.list_current big' = Big_Aux.list_current big"
     using big_invar big_size pop by auto
     
   then have listL: 
     "x # States_Aux.listL ?states_new = 
      Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     proof(cases "States_Aux.lists ?states_new")
       case (Pair bigs smalls)
       with invar big_list_current show ?thesis
         using app_rev[of smalls bigs]
         by(auto split: prod.splits)
     qed
 
   from invar have four_steps: "invar ?states_stepped"
     using invar_step_n by blast
 
   then have [simp]: 
       "x # States_Aux.listL ?states_stepped = 
        Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     using States_Proof.step_n_listL[of ?states_new 4] invar listL
     by auto
 
   then have "listL (deqL (Transforming (States Right big small))) = 
               States_Aux.listL ?states_stepped"
     by(auto simp: Let_def pop split: prod.splits direction.splits states.splits state_splits)
 
   then have listL_list_current: 
       "x # listL (deqL (Transforming (States Right big small))) = 
        Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     by auto
 
   with 6(1) have "listL (Transforming (States Right big small)) = 
                   Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     using invar_list_big_first[of "States Right big small"] by fastforce
 
   with listL_list_current have 
     "x # listL (deqL (Transforming (States Right big small))) = 
      listL (Transforming (States Right big small))"
     by auto
 
   with 6 show ?case by auto
 qed auto
 
 lemma list_deqL [simp]:
     "\<lbrakk>invar deque; listL deque \<noteq> []\<rbrakk> \<Longrightarrow> listL (deqL deque) = tl (listL deque)"
   using cons_tl[of "fst (deqL' deque)" "listL (deqL deque)" "listL deque"]
   by(auto split: prod.splits)
 
 lemma list_firstL [simp]:
     "\<lbrakk>invar deque; listL deque \<noteq> []\<rbrakk> \<Longrightarrow> firstL deque = hd (listL deque)"
   using cons_hd[of "fst (deqL' deque)" "listL (deqL deque)" "listL deque"] 
   by(auto split: prod.splits)
 
 lemma invar_deqL:
     "\<lbrakk>invar deque; \<not> is_empty deque\<rbrakk> \<Longrightarrow> invar (deqL deque)"
 proof(induction deque rule: deqL'.induct)
   case (4 left right length_right)
   then obtain x left' where pop_left[simp]: "Idle.pop left = (x, left')"
     by fastforce
 
   then obtain stack_left' length_left' 
     where left'[simp]: "left' = idle.Idle stack_left' length_left'"
     using idle.exhaust by blast
 
   from 4 have invar_left': "invar left'" "invar left"
     using Idle_Proof.invar_pop by fastforce+
 
   have [simp]: "size stack_left' = size left - 1" 
     by (metis Idle_Proof.size_pop_sub left' pop_left size_idle.simps)
 
   have [simp]: "length_left' = size left - 1" 
     using invar_left' by auto
 
   from 4 have list: "x # Idle_Aux.list left' = Idle_Aux.list left"
     using Idle_Proof.pop_list[of left x left']
     by auto
 
   show ?case 
   proof(cases "length_right \<le> 3 * size left'")
     case True
     with 4 invar_left' show ?thesis
       by(auto simp: Stack_Proof.size_empty[symmetric])
   next
     case False
     note Start_Transformation = False
     then show ?thesis 
     proof(cases "1 \<le> size left'")
       case True
       let ?big = 
         "Reverse 
             (Current [] 0 right (size right - Suc length_left')) 
             right [] (size right - Suc length_left')"
       let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []"
       let ?states = "States Left ?big ?small"
 
       from 4 Start_Transformation True invar_left' 
       have invar: "invar ?states"
         by(auto simp: Let_def rev_take rev_drop)
 
       then have invar_stepped: "invar ((step^^6) ?states)"
         using invar_step_n by blast
 
       from 4 Start_Transformation True 
       have remaining_steps: "6 < remaining_steps ?states"
         by auto
 
       then have remaining_steps_end: "0 < remaining_steps ((step^^6) ?states)"
         by(simp only: remaining_steps_n_steps_sub[of ?states 6] invar)
 
       from 4 Start_Transformation True  
       have size_ok': "size_ok' ?states (remaining_steps ?states - 6)"
         by auto
          
       then have size_ok: "size_ok ((step^^6) ?states)"
         using invar remaining_steps size_ok_steps by blast
 
       from True Start_Transformation 4 show ?thesis
         using remaining_steps_end size_ok invar_stepped
         by(auto simp: Let_def)
     next
       case False
       from False Start_Transformation 4 have [simp]: "size left = 1"
         by auto
         
       with False Start_Transformation 4 have [simp]: "Idle_Aux.list left = [x]"  
         using list[symmetric]
         by(auto simp: list Stack_Proof.list_empty_size)
      
       obtain right1 right2 where "right = Stack right1 right2"
         using Stack_Aux.list.cases by blast
 
       with False Start_Transformation 4 show ?thesis 
         by(induction right1 right2 rule: small_deque.induct) auto
     qed
   qed
 next
   case (5 big small)
   
   obtain x small' where small' [simp]: "Small.pop small = (x, small')"
     by fastforce
 
   let ?states = "States Left big small'"
   let ?states_stepped = "(step^^4) ?states"
 
   obtain big_stepped small_stepped where stepped [simp]: 
        "?states_stepped = States Left big_stepped small_stepped"
      by (metis remaining_steps_states.cases step_n_same)
 
   from 5 have invar: "invar ?states"
     using invar_pop_small[of Left big small x small']
     by auto
 
   then have invar_stepped: "invar ?states_stepped"
     using invar_step_n by blast
 
   show ?case
   proof(cases "4 < remaining_steps ?states")
     case True
 
     then have remaining_steps: "0 < remaining_steps ?states_stepped"
       using invar remaining_steps_n_steps_sub[of ?states 4]
       by simp
 
     from True have size_ok: "size_ok ?states_stepped"
       using step_4_pop_small_size_ok[of Left big small x small'] 5(1)
       by auto
 
     from remaining_steps size_ok invar_stepped show ?thesis
-      by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: Common.state.split)
+      by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: common_state.split)
   next
     case False
     then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0"
       using invar by(auto simp del: stepped)
 
     then obtain small_current small_idle big_current big_idle where idle [simp]: "
       States Left big_stepped small_stepped = 
       States Left 
-          (big_state.Common (state.Idle big_current big_idle))
-          (small_state.Common (state.Idle small_current small_idle))
+          (big_state.Common (common_state.Idle big_current big_idle))
+          (small_state.Common (common_state.Idle small_current small_idle))
       "
       using remaining_steps_idle' invar_stepped remaining_steps_stepped
       by fastforce
 
     have size_new_small : "1 < size_new small" 
       using 5 by auto
 
     have [simp]: "size_new small = Suc (size_new small')" 
       using 5 by auto
 
     have [simp]: "size_new small' = size_new small_stepped"
       using invar step_n_size_new_small stepped
       by metis
 
     have [simp]: "size_new small_stepped = size small_idle" 
       using idle invar_stepped
       by(cases small_stepped) auto
 
     have [simp]: "\<not>is_empty small_idle"
       using size_new_small
       by (simp add: Idle_Proof.size_not_empty)
 
     have [simp]: "size_new big = size_new big_stepped"
       by (metis invar step_n_size_new_big stepped)
 
     have [simp]: "size_new big_stepped = size big_idle" 
       using idle invar_stepped
       by(cases big_stepped) auto
       
     have "0 < size big_idle" 
       using 5 by auto
   
     then have [simp]: "\<not>is_empty big_idle"
       by (auto simp: Idle_Proof.size_not_empty)
 
     have [simp]: "size small_idle \<le> 3 * size big_idle"
       using 5 by auto
 
     have [simp]: "size big_idle \<le> 3 * size small_idle"
       using 5 by auto
 
     show ?thesis
       using invar_stepped by auto 
   qed
 next
   case (6 big small)
   
   obtain x big' where big' [simp]: "Big.pop big = (x, big')"
     by fastforce
 
   let ?states = "States Right big' small"
   let ?states_stepped = "(step^^4) ?states"
 
   obtain big_stepped small_stepped where stepped [simp]: 
        "?states_stepped = States Right big_stepped small_stepped"
      by (metis remaining_steps_states.cases step_n_same)
 
   from 6 have invar: "invar ?states"
     using invar_pop_big[of Right big small x big']
     by auto
 
   then have invar_stepped: "invar ?states_stepped"
     using invar_step_n by blast
 
   show ?case
   proof(cases "4 < remaining_steps ?states")
     case True
 
     then have remaining_steps: "0 < remaining_steps ?states_stepped"
       using invar remaining_steps_n_steps_sub[of ?states 4]
       by simp
 
     from True have size_ok: "size_ok ?states_stepped"
       using step_4_pop_big_size_ok[of Right big small x big'] 6(1)
       by auto
 
     from remaining_steps size_ok invar_stepped show ?thesis
-      by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: Common.state.split)
+      by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: common_state.split)
   next
     case False
     then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0"
       using invar by(auto simp del: stepped)
 
     then obtain small_current small_idle big_current big_idle where idle [simp]: "
       States Right big_stepped small_stepped = 
       States Right 
-          (big_state.Common (state.Idle big_current big_idle))
-          (small_state.Common (state.Idle small_current small_idle))
+          (big_state.Common (common_state.Idle big_current big_idle))
+          (small_state.Common (common_state.Idle small_current small_idle))
       "
       using remaining_steps_idle' invar_stepped remaining_steps_stepped
       by fastforce
 
     have size_new_big : "1 < size_new big" 
       using 6 by auto
 
     have [simp]: "size_new big = Suc (size_new big')" 
       using 6 by auto
 
     have [simp]: "size_new big' = size_new big_stepped"
       using invar step_n_size_new_big stepped
       by metis
 
     have [simp]: "size_new big_stepped = size big_idle" 
       using idle invar_stepped
       by(cases big_stepped) auto
 
     have [simp]: "\<not>is_empty big_idle"
       using size_new_big
       by (simp add: Idle_Proof.size_not_empty)
 
     have [simp]: "size_new small = size_new small_stepped"
       by (metis invar step_n_size_new_small stepped)
 
     have [simp]: "size_new small_stepped = size small_idle" 
       using idle invar_stepped
       by(cases small_stepped) auto
       
     have "0 < size small_idle" 
       using 6 by auto
   
     then have [simp]: "\<not>is_empty small_idle"
       by (auto simp: Idle_Proof.size_not_empty)
 
     have [simp]: "size big_idle \<le> 3 * size small_idle"
       using 6 by auto
 
     have [simp]: "size small_idle \<le> 3 * size big_idle"
       using 6 by auto
 
     show ?thesis
       using invar_stepped by auto 
   qed
 qed auto
 
 end
diff --git a/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy
--- a/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy
+++ b/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy
@@ -1,324 +1,324 @@
 section "Enqueue Proofs"
 
 theory RealTimeDeque_Enqueue_Proof
 imports Deque RealTimeDeque_Aux States_Proof
 begin
 
 lemma list_enqL: "invar deque \<Longrightarrow> listL (enqL x deque) = x # listL deque"
 proof(induction x deque rule: enqL.induct)
   case (5 x left right length_right)
 
   obtain left' length_left' where pushed [simp]: 
       "Idle.push x left = idle.Idle left' length_left'"
     using is_empty_idle.cases by blast
 
   then have invar_left': "invar (idle.Idle left' length_left')"
     using Idle_Proof.invar_push[of left x] 5 by auto
 
   show ?case
   proof(cases "length_left' \<le> 3 * length_right")
     case True
     then show ?thesis 
       using Idle_Proof.push_list[of x left]
       by(auto simp: Let_def)
   next
     case False
     let ?length_left = "length_left' - length_right - 1"
     let ?length_right = "2 * length_right + 1"
     let ?big = "Reverse  (Current [] 0 left' ?length_left) left' [] ?length_left"
     let ?small = "Reverse1 (Current [] 0 right ?length_right) right []"
     let ?states = "States Right ?big ?small"
     let ?states_stepped = "(step^^6) ?states"
 
     from False 5 invar_left' have invar: "invar ?states"
       by(auto simp: rev_drop rev_take)
 
     then have "States_Aux.listL ?states = x # Idle_Aux.list left @ rev (Stack_Aux.list right)"
       using Idle_Proof.push_list[of x left]
       by(auto)
 
     then have "States_Aux.listL ?states_stepped = x # Idle_Aux.list left @ rev (Stack_Aux.list right)"
       by (metis invar step_n_listL)
 
     with False show ?thesis 
       by(auto simp: Let_def)
   qed
 next
   case (6 x big small)
   let ?small = "Small.push x small"
   let ?states = "States Left big ?small"
   let ?states_stepped = "(step^^4) ?states"
 
   obtain big_stepped small_stepped where stepped:
       "?states_stepped = States Left big_stepped small_stepped"
     by (metis remaining_steps_states.cases step_n_same)
 
   from 6 have "invar ?states"
     using invar_push_small[of Left big small x]
     by auto
                         
   then have 
       "States_Aux.listL ?states_stepped = 
        x # Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     using step_n_listL by fastforce
 
   with 6 show ?case
     by(cases big_stepped; cases small_stepped)
-      (auto simp: Let_def stepped split!: Common.state.split)
+      (auto simp: Let_def stepped split!: common_state.split)
 next
   case (7 x big small)
 
   let ?big = "Big.push x big"
   let ?states = "States Right ?big small"
   let ?states_stepped = "(step^^4) ?states"
 
   obtain big_stepped small_stepped where stepped:
       "?states_stepped = States Right big_stepped small_stepped"
     by (metis remaining_steps_states.cases step_n_same)
 
    from 7 have list_invar:
     "list_current_small_first (States Right big small) = list_small_first (States Right big small)"
     by auto
 
   from 7 have invar: "invar ?states"
     using invar_push_big[of Right big small x]
     by auto
                         
   then have
       "States_Aux.listL ?states = x # Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     using app_rev[of _ _ _ "x # Big_Aux.list_current big"]
     by(auto split: prod.split)
 
   then have 
       "States_Aux.listL ?states_stepped = 
        x # Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     by (metis invar step_n_listL)
 
   with list_invar show ?case
     using app_rev[of "Small_Aux.list_current small" "Big_Aux.list_current big"]
     by(cases big_stepped; cases small_stepped)   
-      (auto simp: Let_def stepped split!: prod.split Common.state.split)
+      (auto simp: Let_def stepped split!: prod.split common_state.split)
 qed auto
 
 lemma invar_enqL: "invar deque \<Longrightarrow> invar (enqL x deque)"
 proof(induction x deque rule: enqL.induct)
   case (5 x left right length_right)
   obtain left' length_left' where pushed [simp]: 
       "Idle.push x left = idle.Idle left' length_left'"
     using is_empty_idle.cases by blast
 
   then have invar_left': "invar (idle.Idle left' length_left')"
     using Idle_Proof.invar_push[of left x] 5 by auto 
 
   have [simp]: "size left' = Suc (size left)"
     using Idle_Proof.size_push[of x left] 
     by auto 
 
   show ?case
   proof(cases "length_left' \<le> 3 * length_right")
     case True
     with 5 show ?thesis 
       using invar_left' Idle_Proof.size_push[of x left] Stack_Proof.size_not_empty[of left']
       by auto
   next
     case False
     let ?length_left = "length_left' - length_right - 1"
     let ?length_right = "Suc (2 * length_right)"
     let ?states = "States Right 
           (Reverse (Current [] 0 left' ?length_left) left' [] ?length_left)
           (Reverse1 (Current [] 0 right ?length_right) right [])"
     let ?states_stepped = "(step^^6) ?states"
 
     from invar_left' 5 False have invar: "invar ?states" 
       by(auto simp: rev_drop rev_take)
 
     then have invar_stepped: "invar ?states_stepped"
       using invar_step_n by blast 
 
     from False invar_left' 5 have remaining_steps: "6 < remaining_steps ?states" 
       using Stack_Proof.size_not_empty[of right]
       by auto
 
     then have remaining_steps_stepped: "0 < remaining_steps ?states_stepped" 
       using invar remaining_steps_n_steps_sub
       by (metis zero_less_diff)
 
     from False invar_left' 5 have "size_ok' ?states (remaining_steps ?states - 6)"
       using Stack_Proof.size_not_empty[of right] 
             size_not_empty
       by auto
 
     then have size_ok_stepped: "size_ok ?states_stepped" 
       using size_ok_steps[of ?states 6] remaining_steps invar
       by blast
    
     from False show ?thesis 
       using invar_stepped remaining_steps_stepped size_ok_stepped
       by(auto simp: Let_def)
   qed
 next
   case (6 x big small)
   let ?small = "Small.push x small"
   let ?states = "States Left big ?small"
   let ?states_stepped = "(step^^4) ?states"
 
   from 6 have invar: "invar ?states"
     using invar_push_small[of Left big small x]
     by auto
 
   then have invar_stepped: "invar ?states_stepped"
     using invar_step_n by blast
 
   show ?case
    proof(cases "4 < remaining_steps ?states")
      case True
 
      obtain big_stepped small_stepped where stepped [simp]: 
        "?states_stepped = States Left big_stepped small_stepped"
        by (metis remaining_steps_states.cases step_n_same)
       
      from True have remaining_steps: "0 < remaining_steps ?states_stepped"
        using invar remaining_steps_n_steps_sub[of ?states 4]
        by simp
 
      from True 6(1) have size_ok: "size_ok ?states_stepped"
        using 
           step_4_push_small_size_ok[of Left big small x] 
           remaining_steps_push_small[of Left big small x]
        by auto
 
      from remaining_steps size_ok invar_stepped show ?thesis
        by(cases big_stepped; cases small_stepped) 
-         (auto simp: Let_def split!: Common.state.split)
+         (auto simp: Let_def split!: common_state.split)
    next
      case False
      then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0"
        using invar by auto
 
      then obtain small_current small_idle big_current big_idle where idle [simp]: "
       ?states_stepped = 
       States Left 
-          (big_state.Common (state.Idle big_current big_idle))
-          (small_state.Common (state.Idle small_current small_idle))
+          (big_state.Common (common_state.Idle big_current big_idle))
+          (small_state.Common (common_state.Idle small_current small_idle))
       "
        using remaining_steps_idle' invar_stepped remaining_steps_stepped step_n_same
        by (smt (verit) invar_states.elims(2))
 
      from 6 have [simp]: "size_new (Small.push x small) = Suc (size_new small)"
        using Small_Proof.size_new_push by auto
 
      have [simp]: "size small_idle = size_new (Small.push x small)"
        using invar invar_stepped step_n_size_new_small[of Left big "Small.push x small" 4]
        by auto
 
      then have [simp]: "\<not>is_empty small_idle" 
        using Idle_Proof.size_not_empty[of small_idle]
        by auto
 
      have size_new_big [simp]: "0 < size_new big"
        using 6
        by auto
 
      then have [simp]: "size big_idle = size_new big"
        using invar invar_stepped step_n_size_new_big[of Left big "Small.push x small" 4]
        by auto
       
      then have [simp]: "\<not>is_empty big_idle" 
        using Idle_Proof.size_not_empty size_new_big
        by metis
 
      have size_ok_1: "size small_idle \<le> 3 * size big_idle"
        using 6 by auto
 
      have size_ok_2: "size big_idle \<le> 3 * size small_idle"
       using 6 by auto
 
      from False show ?thesis 
        using invar_stepped size_ok_1 size_ok_2
        by auto
    qed
 next
   case (7 x big small)
   let ?big = "Big.push x big"
   let ?states = "States Right ?big small"
   let ?states_stepped = "(step^^4) ?states"
 
   from 7 have invar: "invar ?states"
     using invar_push_big[of Right big small x]
     by auto
 
   then have invar_stepped: "invar ?states_stepped"
     using invar_step_n by blast
 
   show ?case
    proof(cases "4 < remaining_steps ?states")
      case True
      
      obtain big_stepped small_stepped where stepped [simp]:
        "?states_stepped = States Right big_stepped small_stepped"
        by (metis remaining_steps_states.cases step_n_same)
       
      from True have remaining_steps: "0 < remaining_steps ?states_stepped"
        using invar remaining_steps_n_steps_sub[of ?states 4]
        by simp
 
      from True 7(1) have size_ok: "size_ok ?states_stepped"
        using 
           step_4_push_big_size_ok[of Right big small x] 
           remaining_steps_push_big[of Right big small x]
        by auto
 
      from remaining_steps size_ok invar_stepped show ?thesis
        by(cases big_stepped; cases small_stepped) 
-         (auto simp: Let_def split!: Common.state.split)
+         (auto simp: Let_def split!: common_state.split)
    next
      case False
      then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0"
        using invar by auto
 
      then obtain small_current small_idle big_current big_idle where idle [simp]: "
       ?states_stepped = 
       States Right 
-          (big_state.Common (state.Idle big_current big_idle))
-          (small_state.Common (state.Idle small_current small_idle))
+          (big_state.Common (common_state.Idle big_current big_idle))
+          (small_state.Common (common_state.Idle small_current small_idle))
       "
        using remaining_steps_idle' invar_stepped remaining_steps_stepped step_n_same
        by (smt (verit) invar_states.elims(2))
 
      from 7 have [simp]: "size_new (Big.push x big) = Suc (size_new big)"
        using Big_Proof.size_new_push by auto
 
      have [simp]: "size big_idle = size_new (Big.push x big)"
        using invar invar_stepped step_n_size_new_big[of Right "Big.push x big" small 4]
        by auto
 
      then have [simp]: "\<not>is_empty big_idle" 
        using Idle_Proof.size_not_empty[of big_idle]
        by auto
 
      have size_new_small [simp]: "0 < size_new small"
        using 7
        by auto
 
      then have [simp]: "size small_idle = size_new small"
        using invar invar_stepped step_n_size_new_small[of Right "Big.push x big" small 4]
        by auto
       
      then have [simp]: "\<not>is_empty small_idle" 
        using Idle_Proof.size_not_empty size_new_small
        by metis
 
      have size_ok_1: "size small_idle \<le> 3 * size big_idle"
        using 7 by auto
 
      have size_ok_2: "size big_idle \<le> 3 * size small_idle"
       using 7 by auto
 
      from False show ?thesis 
        using invar_stepped size_ok_1 size_ok_2
        by auto
    qed
 qed auto
 
 end
 
diff --git a/thys/Real_Time_Deque/Small.thy b/thys/Real_Time_Deque/Small.thy
--- a/thys/Real_Time_Deque/Small.thy
+++ b/thys/Real_Time_Deque/Small.thy
@@ -1,62 +1,62 @@
 section \<open>Smaller End of Deque\<close>
 
 theory Small
 imports Common
 begin
 
 text \<open>
 \<^noindent> The smaller end of the deque during \<open>transformation\<close> can be in one three phases:
 
  \<^descr> \<open>Reverse1\<close>: Using the \<open>step\<close> function the originally contained elements are reversed.
  \<^descr> \<open>Reverse2\<close>: Using the \<open>step\<close> function the newly obtained elements from the bigger end are reversed on top of the ones reversed in the previous phase.
  \<^descr> \<open>Common\<close>: See theory \<open>Common\<close>. Is used to reverse the elements from the two previous phases again to get them again in the original order.
 
 \<^noindent> Each phase contains a \<open>current\<close> state, which holds the original elements of the deque end. 
 \<close>
 
 datatype (plugins del: size) 'a small_state =
    Reverse1 "'a current" "'a stack" "'a list"
  | Reverse2 "'a current" "'a list" "'a stack" "'a list" nat
- | Common "'a Common.state"
+ | Common "'a common_state"
 
 text \<open>\<^noindent> Functions:
 
  \<^descr> \<open>push\<close>, \<open>pop\<close>: Add and remove elements using the \<open>current\<close> state.
  \<^descr> \<open>step\<close>: Executes one step of the transformation, while keeping the invariant.\<close>
 
 instantiation small_state::(type) step
 begin
 
 fun step_small_state :: "'a small_state \<Rightarrow> 'a small_state" where
   "step (Common state) = Common (step state)"
 | "step (Reverse1 current small auxS) = (
     if is_empty small 
     then Reverse1 current small auxS 
     else Reverse1 current (Stack.pop small) ((Stack.first small)#auxS)
   )"
 | "step (Reverse2 current auxS big newS count) = (
     if is_empty big
     then Common (normalize (Copy current auxS newS count))
     else Reverse2 current auxS (Stack.pop big) ((Stack.first big)#newS) (count + 1)
   )"
 
 instance..
 end
 
 fun push :: "'a \<Rightarrow> 'a small_state \<Rightarrow> 'a small_state" where
   "push x (Common state) = Common (Common.push x state)"
 | "push x (Reverse1 current small auxS) = Reverse1 (Current.push x current) small auxS"
 | "push x (Reverse2 current auxS big newS count) = 
     Reverse2 (Current.push x current) auxS big newS count"
 
 fun pop :: "'a small_state \<Rightarrow> 'a * 'a small_state" where
   "pop (Common state) = (
     let (x, state) = Common.pop state 
     in (x, Common state)
   )"
 | "pop (Reverse1 current small auxS) = 
     (first current, Reverse1 (drop_first current) small auxS)"
 | "pop (Reverse2 current auxS big newS count) = 
     (first current, Reverse2 (drop_first current) auxS big newS count)"
 
 end
\ No newline at end of file
diff --git a/thys/Real_Time_Deque/States_Proof.thy b/thys/Real_Time_Deque/States_Proof.thy
--- a/thys/Real_Time_Deque/States_Proof.thy
+++ b/thys/Real_Time_Deque/States_Proof.thy
@@ -1,1203 +1,1203 @@
 section "Big + Small Proofs"
 
 theory States_Proof
 imports States_Aux Big_Proof Small_Proof
 begin
 
-lemmas state_splits = idle.splits Common.state.splits small_state.splits big_state.splits
+lemmas state_splits = idle.splits common_state.splits small_state.splits big_state.splits
 lemmas invar_steps = Big_Proof.invar_step Common_Proof.invar_step Small_Proof.invar_step
 
 lemma invar_list_big_first: 
     "invar states \<Longrightarrow> list_big_first states = list_current_big_first states"
   using app_rev
   by(cases states)(auto split: prod.splits)
 
 lemma step_lists [simp]: "invar states \<Longrightarrow> lists (step states) = lists states"
 proof(induction states rule: lists.induct)
   case (1 dir currentB big auxB count currentS small auxS)
   then show ?case 
   proof(induction 
       "(States dir (Reverse currentB big auxB count) (Reverse1 currentS small auxS))" 
       rule: step_states.induct)
     case 1
     then show ?case 
       by(cases currentB) auto
   next
     case ("2_1" count')
     then have "0 < size big"
       by(cases currentB) auto
 
     then have big_not_empty: "Stack_Aux.list big \<noteq> []"
       by (simp add: Stack_Proof.size_not_empty Stack_Proof.list_empty)
 
     with "2_1" show ?case 
       using 
           take_rev_step[of "Stack_Aux.list big" count' auxB] 
           Stack_Proof.list_empty[symmetric, of small]       
       apply (cases currentB)
       by(auto simp: first_hd funpow_swap1 take_rev_step simp del: take_rev_def)
     qed
 next
   case ("2_1" dir common small)
   then show ?case 
     using Small_Proof.step_list_reverse2[of small]
     by(auto split: small_state.splits)
 next
   case ("2_2" dir big current auxS big newS count)
   then show ?case 
     using Small_Proof.step_list_reverse2[of "Reverse2 current auxS big newS count"]
     by auto
 next
   case ("2_3" dir big common)
   then show ?case 
     by auto
 qed
   
 lemma step_lists_current [simp]: 
     "invar states \<Longrightarrow> lists_current (step states) = lists_current states"
   by(induction states rule: step_states.induct)(auto split: current.splits)
 
 lemma push_big: "lists (States dir big small) = (big', small')
    \<Longrightarrow> lists (States dir (Big.push x big) small) = (x # big', small')"
 proof(induction "States dir (Big.push x big) small" rule: lists.induct)
   case 1
   then show ?case
   proof(induction x big rule: Big.push.induct)
     case 1
     then show ?case 
       by auto
   next
     case (2 x current big aux count)
     then show ?case 
       by(cases current) auto
   qed
 next
   case "2_1"
   then show ?case 
     by(cases big) auto
 qed auto
 
 lemma push_small_lists: "
   invar (States dir big small)
    \<Longrightarrow> lists (States dir big (Small.push x small)) = (big', x # small') \<longleftrightarrow> 
        lists (States dir big small) = (big', small')"
   apply(induction "States dir big (Small.push x small)" rule: lists.induct)
   by (auto split: current.splits small_state.splits)
 
 lemma list_small_big: "
     list_small_first (States dir big small) = list_current_small_first (States dir big small) \<longleftrightarrow>
     list_big_first (States dir big small) = list_current_big_first (States dir big small)"
   using app_rev 
   by(auto split: prod.splits)
 
 lemma list_big_first_pop_big [simp]: "\<lbrakk>
   invar (States dir big small);
   0 < size big;
   Big.pop big = (x, big')\<rbrakk>
  \<Longrightarrow> x # list_big_first (States dir big' small) = list_big_first (States dir big small)"
   by(induction "States dir big small" rule: lists.induct)(auto split: prod.splits)
 
 lemma list_current_big_first_pop_big [simp]: "\<lbrakk>
   invar (States dir big small);
   0 < size big;
   Big.pop big = (x, big')\<rbrakk>
  \<Longrightarrow> x # list_current_big_first (States dir big' small) =
     list_current_big_first (States dir big small)"
   by auto
 
 lemma lists_big_first_pop_big: "\<lbrakk>
   invar (States dir big small);
    0 < size big;
   Big.pop big = (x, big')\<rbrakk>
  \<Longrightarrow> list_big_first (States dir big' small) = list_current_big_first (States dir big' small)"
   by (metis invar_list_big_first list_big_first_pop_big list_current_big_first_pop_big list.sel(3))
 
 lemma lists_small_first_pop_big: "\<lbrakk>
   invar (States dir big small);
   0 < size big;
   Big.pop big = (x, big')\<rbrakk>
  \<Longrightarrow> list_small_first (States dir big' small) = list_current_small_first (States dir big' small)"
   by (meson lists_big_first_pop_big list_small_big)
 
 lemma list_small_first_pop_small [simp]: "\<lbrakk>
   invar (States dir big small);
    0 < size small;
   Small.pop small = (x, small')\<rbrakk>
  \<Longrightarrow> x # list_small_first (States dir big small') = list_small_first (States dir big small)"
 proof(induction "States dir big small" rule: lists.induct)
   case (1 currentB big auxB count currentS small auxS) 
   then show ?case
     by(cases currentS)(auto simp: Cons_eq_appendI)
 next
   case ("2_1" common)
   then show ?case  
   proof(induction small rule: Small.pop.induct)
     case (1 common)
     then show ?case 
       by(cases "Common.pop common")(auto simp: Cons_eq_appendI)
   next
     case 2
     then show ?case by auto
   next
     case 3
     then show ?case 
       by(cases "Common.pop common")(auto simp: Cons_eq_appendI)
   qed
 next
   case ("2_2" current)
   then show ?case 
     by(induction current rule: Current.pop.induct)
       (auto simp: first_hd rev_take Suc_diff_le)
 next
   case ("2_3" common)
   then show ?case 
     by(cases "Common.pop common")(auto simp: Cons_eq_appendI)
 qed
 
 lemma list_current_small_first_pop_small [simp]: "\<lbrakk>
   invar (States dir big small);
   0 < size small;
   Small.pop small = (x, small')\<rbrakk>
  \<Longrightarrow> x # list_current_small_first (States dir big small') =
      list_current_small_first (States dir big small)"
   by auto
 
 lemma lists_small_first_pop_small: "\<lbrakk>
   invar (States dir big small);
   0 < size small;
   Small.pop small = (x, small')\<rbrakk>
  \<Longrightarrow> list_small_first (States dir big small') = list_current_small_first (States dir big small')"
   by (metis (no_types, opaque_lifting) invar_states.simps list.sel(3) 
       list_current_small_first_pop_small list_small_first_pop_small)
 
 lemma invars_pop_big: "\<lbrakk>
   invar (States dir big small);
   0 < size big;
   Big.pop big = (x, big')\<rbrakk>
  \<Longrightarrow> invar big' \<and> invar small"
   by(auto simp: Big_Proof.invar_pop)
 
 lemma invar_pop_big_aux: "\<lbrakk>
   invar (States dir big small);
   0 < size big;
   Big.pop big = (x, big')\<rbrakk>
  \<Longrightarrow> (case (big', small) of 
         (Reverse _ big _ count, Reverse1 (Current _ _ old remained) small _) \<Rightarrow> 
           size big - count = remained - size old \<and> count \<ge> size small
       | (_, Reverse1 _ _ _) \<Rightarrow> False
       | (Reverse _ _ _ _, _) \<Rightarrow> False
       | _ \<Rightarrow> True
       )"
   by(auto split: big_state.splits small_state.splits prod.splits)
 
 lemma invar_pop_big: "\<lbrakk>
   invar (States dir big small);
   0 < size big;
   Big.pop big = (x, big')\<rbrakk>
  \<Longrightarrow> invar (States dir big' small)"
   using invars_pop_big[of dir big small x big']  
         lists_small_first_pop_big[of dir big small x big']
         invar_pop_big_aux[of dir big small x big']
   by auto
 
 lemma invars_pop_small: "\<lbrakk>
   invar (States dir big small);
   0 < size small;
   Small.pop small = (x, small')\<rbrakk>
  \<Longrightarrow>  invar big  \<and> invar small'"
   by(auto simp: Small_Proof.invar_pop)
 
 lemma invar_pop_small_aux: "\<lbrakk>
   invar (States dir big small);
   0 < size small;
   Small.pop small = (x, small')\<rbrakk>
  \<Longrightarrow> (case (big, small') of 
         (Reverse _ big _ count, Reverse1 (Current _ _ old remained) small _) \<Rightarrow> 
           size big - count = remained - size old \<and> count \<ge> size small
       | (_, Reverse1 _ _ _) \<Rightarrow> False
       | (Reverse _ _ _ _, _) \<Rightarrow> False
       | _ \<Rightarrow> True
       )"
 proof(induction small rule: Small.pop.induct)
   case 1
   then show ?case
     by(auto split: big_state.splits small_state.splits prod.splits)
 next
   case (2 current)
   then show ?case 
   proof(induction current rule: Current.pop.induct)
     case 1
     then show ?case 
       by(auto split: big_state.splits)
   next
     case 2
     then show ?case 
       by(auto split: big_state.splits)
   qed
 next
   case 3
   then show ?case 
     by(auto split: big_state.splits)
 qed
   
 lemma invar_pop_small: "\<lbrakk>
     invar (States dir big small);
     0 < size small;
     Small.pop small = (x, small')
   \<rbrakk> \<Longrightarrow> invar (States dir big small')"
   using invars_pop_small[of dir big small x small']  
         lists_small_first_pop_small[of dir big small x small']
         invar_pop_small_aux[of dir big small x small']
   by fastforce  
 
 lemma invar_push_big: "invar (States dir big small) \<Longrightarrow> invar (States dir (Big.push x big) small)"
 proof(induction x big arbitrary: small rule: Big.push.induct)
   case 1
   then show ?case
     by(auto simp: Common_Proof.invar_push)
 next
   case (2 x current big aux count)
   then show ?case 
     by(cases current)(auto split: prod.splits small_state.splits)
 qed
 
 lemma invar_push_small: "invar (States dir big small)
    \<Longrightarrow> invar (States dir big (Small.push x small))"
 proof(induction x small arbitrary: big rule: Small.push.induct)
   case (1 x state)
   then show ?case 
     by(auto simp: Common_Proof.invar_push split: big_state.splits)
 next
   case (2 x current small auxS)
   then show ?case
     by(induction x current rule: Current.push.induct)(auto split: big_state.splits)
 next
   case (3 x current auxS big newS count)
   then show ?case 
     by(induction x current rule: Current.push.induct)(auto split: big_state.splits)
 qed
 
 lemma step_invars:"\<lbrakk>invar states; step states = States dir big small\<rbrakk> \<Longrightarrow> invar big \<and> invar small"
 proof(induction states rule: step_states.induct)
   case (1 dir currentB big' auxB currentS small' auxS)
   with Big_Proof.invar_step have "invar (Reverse currentB big' auxB 0)"
     by auto
   with 1 have invar_big: "invar big"
     using Big_Proof.invar_step[of "Reverse currentB big' auxB 0"]
     by auto
 
   from 1 have invar_small: "invar small"
     using Stack_Proof.list_empty_size[of small']
     by(cases currentS) auto
   
   from invar_small invar_big show ?case
     by simp
 next
   case ("2_1" dir current big aux count small)
   then show ?case 
     using Big_Proof.invar_step[of "(Reverse current big aux (Suc count))"]  
           Small_Proof.invar_step[of small]
     by simp
 next
   case "2_2"
   then show ?case 
     by(auto simp: Common_Proof.invar_step Small_Proof.invar_step)
 next
   case ("2_3" dir big current auxS big' newS count)
   then show ?case 
     using Big_Proof.invar_step[of big] 
           Small_Proof.invar_step[of "Reverse2 current auxS big' newS count"]
     by auto
 next
   case "2_4"
   then show ?case 
     by(auto simp: Common_Proof.invar_step Big_Proof.invar_step)
 qed
 
 lemma step_lists_small_first: "invar states \<Longrightarrow>
    list_small_first (step states) = list_current_small_first (step states)"
   using step_lists_current step_lists  invar_states.elims(2)
   by fastforce
 
 lemma invar_step_aux: "invar states \<Longrightarrow>(case step states of 
         (States _ (Reverse _ big _ count) (Reverse1 (Current _ _ old remained) small _)) \<Rightarrow> 
           size big - count = remained - size old \<and> count \<ge> size small
       | (States _ _  (Reverse1 _ _ _)) \<Rightarrow> False
       | (States _ (Reverse _ _ _ _) _) \<Rightarrow> False
       | _ \<Rightarrow> True
       )"
 proof(induction states rule: step_states.induct)
   case ("2_1" dir current big aux count small)
   then show ?case
   proof(cases small)
     case (Reverse1 current small auxS)
     with "2_1" show ?thesis 
       using Stack_Proof.size_empty[symmetric, of small]
       by(auto split: current.splits)
   qed auto 
 qed (auto split: big_state.splits small_state.splits) 
 
 lemma invar_step: "invar (states :: 'a states) \<Longrightarrow> invar (step states)" 
   using invar_step_aux[of states] step_lists_small_first[of states]
   by(cases "step states")(auto simp: step_invars)
 
 lemma step_consistent [simp]: 
   "\<lbrakk>\<And>states. invar (states :: 'a states) \<Longrightarrow>  P (step states) = P states; invar states\<rbrakk>
    \<Longrightarrow> P states = P ((step ^^n) states)" 
   by(induction n arbitrary: states)
     (auto simp: States_Proof.invar_step funpow_swap1)
 
 lemma step_consistent_2: 
   "\<lbrakk>\<And>states. \<lbrakk>invar (states :: 'a states); P states\<rbrakk> \<Longrightarrow>  P (step states); invar states;  P states\<rbrakk>
    \<Longrightarrow> P ((step ^^n) states)" 
   by(induction n arbitrary: states)
     (auto simp: States_Proof.invar_step funpow_swap1)
 
 lemma size_ok'_Suc: "size_ok' states (Suc steps) \<Longrightarrow> size_ok' states steps"
   by(induction states steps rule: size_ok'.induct) auto
 
 lemma size_ok'_decline: "size_ok' states x \<Longrightarrow> x \<ge> y \<Longrightarrow> size_ok' states y"
   by(induction states x rule: size_ok'.induct) auto
 
 lemma remaining_steps_0 [simp]: "\<lbrakk>invar (states :: 'a states); remaining_steps states = 0\<rbrakk>
    \<Longrightarrow> remaining_steps (step states) = 0"
   by(induction states rule: step_states.induct) 
     (auto split: current.splits small_state.splits)
 
 lemma remaining_steps_0': "\<lbrakk>invar (states :: 'a states); remaining_steps states = 0\<rbrakk>
    \<Longrightarrow> remaining_steps ((step ^^ n) states) = 0"
   by(induction n arbitrary: states)(auto simp: invar_step funpow_swap1)
 
 lemma remaining_steps_decline_Suc: 
   "\<lbrakk>invar (states :: 'a states); 0 < remaining_steps states\<rbrakk>
      \<Longrightarrow> Suc (remaining_steps (step states)) = remaining_steps states"
 proof(induction states rule: step_states.induct)
   case 1
   then show ?case 
      by(auto simp: max_def split: big_state.splits small_state.splits current.splits)
 next
   case ("2_1" _ _ _ _ _ small)
   then show ?case 
     by(cases small)(auto split: current.splits)
 next
   case ("2_2" dir big small)
   then show ?case 
   proof(cases small)
     case (Reverse2 current auxS big newS count)
     with "2_2" show ?thesis 
       using Stack_Proof.size_empty_2[of big]
       by(cases current) auto
   qed auto
 next
   case ("2_3" dir big current auxS big' newS count)
   then show ?case 
   proof(induction big)
     case Reverse
     then show ?case by auto
   next
     case Common
     then show ?case 
       using Stack_Proof.size_empty_2[of big']
       by(cases current) auto
   qed
 next
   case ("2_4" _ big)
   then show ?case 
     by(cases big) auto
 qed
 
 lemma remaining_steps_decline_sub [simp]: "invar (states :: 'a states)
      \<Longrightarrow> remaining_steps (step states) = remaining_steps states - 1"
   using Suc_sub[of "remaining_steps (step states)" "remaining_steps states"]
   by(cases "0 < remaining_steps states") (auto simp: remaining_steps_decline_Suc)
 
 lemma remaining_steps_decline: "invar (states :: 'a states)
    \<Longrightarrow> remaining_steps (step states) \<le> remaining_steps states"
   using remaining_steps_decline_sub[of states] by auto
 
 lemma remaining_steps_decline_n_steps [simp]: 
   "\<lbrakk>invar (states :: 'a states); remaining_steps states \<le> n\<rbrakk>
    \<Longrightarrow> remaining_steps ((step ^^ n) states) = 0"
   by(induction n arbitrary: states)(auto simp: funpow_swap1 invar_step)
 
 lemma remaining_steps_n_steps_plus [simp]: 
   "\<lbrakk>n \<le> remaining_steps states; invar (states :: 'a states)\<rbrakk>
     \<Longrightarrow> remaining_steps ((step ^^ n) states) + n = remaining_steps states" 
   by(induction n arbitrary: states)(auto simp: funpow_swap1 invar_step)
 
 lemma remaining_steps_n_steps_sub [simp]: "invar (states :: 'a states)
     \<Longrightarrow> remaining_steps ((step ^^ n) states) = remaining_steps states - n"
   by(induction n arbitrary: states)(auto simp: funpow_swap1 invar_step)
 
 lemma step_size_new_small [simp]: 
   "\<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'\<rbrakk>
    \<Longrightarrow> size_new small' = size_new small"
 proof(induction "States dir big small" rule: step_states.induct)
   case 1
   then show ?case 
     by auto
 next
   case "2_1"
   then show ?case 
     by(auto split: small_state.splits)
 next
   case "2_2"
   then show ?case 
     by(auto split: small_state.splits current.splits)
 next
   case "2_3"
   then show ?case 
     by(auto split: current.splits)
 next
   case "2_4"
   then show ?case 
     by auto
 qed
 
 lemma step_size_new_small_2 [simp]:
  "invar states \<Longrightarrow> size_new_small (step states) = size_new_small states"
   by(cases states; cases "step states") auto
 
 lemma step_size_new_big [simp]:
  "\<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'\<rbrakk>
    \<Longrightarrow> size_new big' = size_new big"
 proof(induction "States dir big small" rule: step_states.induct)
   case 1
   then show ?case 
     by(auto split: current.splits)
 next
   case "2_1"
   then show ?case 
     by auto
 next
   case "2_2"
   then show ?case 
     by auto
 next
   case "2_3"
   then show ?case 
     by(auto split: big_state.splits)
 next
   case "2_4"
   then show ?case 
     by(auto split: big_state.splits)
 qed
 
 lemma step_size_new_big_2 [simp]:
  "invar states \<Longrightarrow> size_new_big (step states) = size_new_big states"
   by(cases states; cases "step states") auto
 
 lemma step_size_small [simp]:
  "\<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'\<rbrakk>
     \<Longrightarrow> size small' = size small"
 proof(induction "States dir big small" rule: step_states.induct)
   case "2_3"
   then show ?case 
     by(auto split: current.splits)
 qed auto
 
 lemma step_size_small_2 [simp]:
  "invar states \<Longrightarrow> size_small (step states) = size_small states"
   by(cases states; cases "step states") auto
 
 lemma step_size_big [simp]: 
   "\<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'\<rbrakk>
      \<Longrightarrow> size big' = size big"
 proof(induction "States dir big small" rule: step_states.induct)
   case 1
   then show ?case 
     by(auto split: current.splits)
 next
   case "2_1"
   then show ?case 
     by(auto split: small_state.splits current.splits)
 next
   case "2_2"
   then show ?case 
     by(auto split: small_state.splits current.splits)
 next
   case "2_3"
   then show ?case 
     by(auto split: current.splits big_state.splits)
 next
   case "2_4"
   then show ?case 
     by(auto split: big_state.splits)
 qed
 
 lemma step_size_big_2 [simp]:
  "invar states \<Longrightarrow> size_big (step states) = size_big states"
   by(cases states; cases "step states") auto
 
 lemma step_size_ok_1: "\<lbrakk>
     invar (States dir big small);
     step (States dir big small) = States dir' big' small';
     size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small
 \<rbrakk> \<Longrightarrow> size_new big' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new small'"
   using step_size_new_small step_size_new_big remaining_steps_decline
   by (smt (verit, ccfv_SIG) add.commute le_trans nat_add_left_cancel_le)
 
 lemma step_size_ok_2: "\<lbrakk>
   invar (States dir big small); 
   step (States dir big small) = States dir' big' small';
   size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big
 \<rbrakk> \<Longrightarrow> size_new small' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new big'"
   using remaining_steps_decline step_size_new_small step_size_new_big
   by (smt (verit, best) add_le_mono le_refl le_trans)
 
 lemma step_size_ok_3: "\<lbrakk>
   invar (States dir big small); 
   step (States dir big small) = States dir' big' small';
   remaining_steps (States dir big small) + 1 \<le> 4 * size small
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'"
   using remaining_steps_decline step_size_small
   by (metis Suc_eq_plus1 Suc_le_mono le_trans)
 
 lemma step_size_ok_4: "\<lbrakk>
   invar (States dir big small); 
   step (States dir big small) = States dir' big' small';
   remaining_steps (States dir big small) + 1 \<le> 4 * size big
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size big'"
   using remaining_steps_decline step_size_big
   by (metis (no_types, lifting) add_mono_thms_linordered_semiring(3) order.trans)
 
 lemma step_size_ok: "\<lbrakk>invar states; size_ok states\<rbrakk> \<Longrightarrow> size_ok (step states)"
   using step_size_ok_1 step_size_ok_2 step_size_ok_3 step_size_ok_4
   by (smt (verit) invar_states.elims(1) size_ok'.elims(3) size_ok'.simps)
 
 lemma step_n_size_ok: "\<lbrakk>invar states; size_ok states\<rbrakk> \<Longrightarrow> size_ok ((step ^^ n) states)"
   using step_consistent_2[of size_ok states n] step_size_ok by blast
  
 lemma step_push_size_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   step (States dir big (Small.push x small)) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size small' = Suc (size small)"
   using 
     invar_push_small[of dir big small x]
     step_size_small[of dir big "Small.push x small" dir' big' small']
     size_push[of small x]
   by simp
 
 lemma step_push_size_new_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   step (States dir big (Small.push x small)) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size_new small' = Suc (size_new small)"
   using 
     invar_push_small[of dir big small x]
     step_size_new_small[of dir big "Small.push x small" dir' big' small']
     size_new_push[of small x]
   by simp
 
 lemma step_push_size_big [simp]: "\<lbrakk>
   invar (States dir big small); 
   step (States dir (Big.push x big) small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size big' = Suc (size big)"
   using 
     invar_push_big[of dir big small x]
     Big_Proof.size_push[of big]
     step_size_big[of dir "Big.push x big" small dir' big' small']
   by simp
 
 lemma step_push_size_new_big [simp]: "\<lbrakk>
   invar (States dir big small); 
   step (States dir (Big.push x big) small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size_new big' = Suc (size_new big)"
   using 
     invar_push_big[of dir big small x] 
     step_size_new_big[of dir "Big.push x big" small dir' big' small']
     Big_Proof.size_new_push[of big x]
   by simp
 
 lemma step_pop_size_big [simp]: "\<lbrakk>
   invar (States dir big small); 
   0 < size big; 
   Big.pop big = (x, bigP); 
   step (States dir bigP small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> Suc (size big') = size big"
   using 
     invar_pop_big[of dir big small x bigP] 
     step_size_big[of dir bigP small dir' big' small']  
     Big_Proof.size_pop[of big x bigP]
   by simp
 
 lemma step_pop_size_new_big [simp]: "\<lbrakk>
   invar (States dir big small);
   0 < size big; Big.pop big = (x, bigP); 
   step (States dir bigP small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> Suc (size_new big') = size_new big"
   using 
     invar_pop_big[of dir big small x bigP] 
     Big_Proof.size_size_new[of big]
     step_size_new_big[of dir bigP small dir' big' small']  
     Big_Proof.size_new_pop[of big x bigP]
   by simp
 
 lemma step_n_size_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   (step ^^ n) (States dir big small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size small' = size small"
   using step_consistent[of size_small "States dir big small" n]
   by simp
 
 lemma step_n_size_big [simp]: 
   "\<lbrakk>invar (States dir big small); (step ^^ n) (States dir big small) = States dir' big' small'\<rbrakk>
     \<Longrightarrow> size big' = size big"
   using step_consistent[of size_big "States dir big small" n]
   by simp
 
 lemma step_n_size_new_small [simp]: 
   "\<lbrakk>invar (States dir big small); (step ^^ n) (States dir big small) = States dir' big' small'\<rbrakk>
     \<Longrightarrow> size_new small' = size_new small"
   using step_consistent[of size_new_small "States dir big small" n]
   by simp
 
 lemma step_n_size_new_big [simp]: 
   "\<lbrakk>invar (States dir big small); (step ^^ n) (States dir big small) = States dir' big' small'\<rbrakk>
    \<Longrightarrow> size_new big' = size_new big"
   using step_consistent[of size_new_big "States dir big small" n]
   by simp
 
 lemma step_n_push_size_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   (step ^^ n) (States dir big (Small.push x small)) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size small' = Suc (size small)"
   using step_n_size_small invar_push_small Small_Proof.size_push
   by (metis invar_states.simps)
 
 lemma step_n_push_size_new_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   (step ^^ n) (States dir big (Small.push x small)) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size_new small' = Suc (size_new small)"
   by (metis Small_Proof.size_new_push invar_states.simps invar_push_small step_n_size_new_small)
 
 lemma step_n_push_size_big [simp]: "\<lbrakk>
   invar (States dir big small); 
   (step ^^ n) (States dir (Big.push x big) small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size big' = Suc (size big)"
   by (metis Big_Proof.size_push invar_states.simps invar_push_big step_n_size_big)
 
 lemma step_n_push_size_new_big [simp]: "\<lbrakk>
   invar (States dir big small); 
   (step ^^ n) (States dir (Big.push x big) small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> size_new big' = Suc (size_new big)"
   by (metis Big_Proof.size_new_push invar_states.simps invar_push_big step_n_size_new_big)
 
 lemma step_n_pop_size_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   0 < size small; 
   Small.pop small = (x, smallP);
   (step ^^ n) (States dir big smallP) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> Suc (size small') = size small"
   using invar_pop_small size_pop step_n_size_small
   by (metis (no_types, opaque_lifting) invar_states.simps)
 
 lemma step_n_pop_size_new_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   0 < size small; 
   Small.pop small = (x, smallP);
   (step ^^ n) (States dir big smallP) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> Suc (size_new small') = size_new small"
   using invar_pop_small size_new_pop step_n_size_new_small size_size_new
   by (metis (no_types, lifting) invar_states.simps)
 
 lemma step_n_pop_size_big [simp]: "\<lbrakk>
   invar (States dir big small);
   0 < size big; Big.pop big = (x, bigP);
   (step ^^ n) (States dir bigP small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> Suc (size big') = size big"
   using invar_pop_big Big_Proof.size_pop step_n_size_big 
   by fastforce
 
 lemma step_n_pop_size_new_big: "\<lbrakk>
   invar (States dir big small);
   0 < size big; Big.pop big = (x, bigP);
   (step ^^ n) (States dir bigP small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> Suc (size_new big') = size_new big"
   using invar_pop_big Big_Proof.size_new_pop step_n_size_new_big Big_Proof.size_size_new
   by (metis (no_types, lifting)  invar_states.simps)
 
 lemma remaining_steps_push_small [simp]: "invar (States dir big small)
     \<Longrightarrow> remaining_steps (States dir big small) = 
         remaining_steps (States dir big (Small.push x small))"
   by(induction x small rule: Small.push.induct)(auto split: current.splits)   
 
 lemma remaining_steps_pop_small: 
   "\<lbrakk>invar (States dir big small); 0 < size small; Small.pop small = (x, smallP)\<rbrakk>
     \<Longrightarrow> remaining_steps (States dir big smallP) \<le> remaining_steps (States dir big small)"
 proof(induction small rule: Small.pop.induct)
   case 1
   then show ?case 
     by(auto simp: Common_Proof.remaining_steps_pop max.coboundedI2 split: prod.splits)
 next
   case (2 current small auxS)
   then show ?case
     by(induction current rule: Current.pop.induct)(auto split: big_state.splits) 
 next
   case (3 current auxS big newS count)
   then show ?case 
     by(induction current rule: Current.pop.induct) auto
 qed
 
 lemma remaining_steps_pop_big: 
   "\<lbrakk>invar (States dir big small); 0 < size big; Big.pop big = (x, bigP)\<rbrakk>
     \<Longrightarrow> remaining_steps (States dir bigP small) \<le> remaining_steps (States dir big small)"
 proof(induction big rule: Big.pop.induct)
   case (1 state)
   then show ?case
   proof(induction state rule: Common.pop.induct)
     case (1 current idle)
     then show ?case 
       by(cases idle)(auto split: small_state.splits)
   next
     case (2 current aux new moved)
     then show ?case 
       by(induction current rule: Current.pop.induct)(auto split: small_state.splits)
   qed
 next
   case (2 current big aux count)
   then show ?case
   proof(induction current rule: Current.pop.induct)
     case 1
     then show ?case 
       by(auto split: small_state.splits current.splits)
   next
     case 2
     then show ?case 
       by(auto split: small_state.splits current.splits)
   qed
 qed
 
 lemma remaining_steps_push_big [simp]: "invar (States dir big small)
    \<Longrightarrow> remaining_steps (States dir (Big.push x big) small) = 
        remaining_steps (States dir big small)"
   by(induction x big rule: Big.push.induct)(auto split: small_state.splits current.splits)
 
 lemma step_4_remaining_steps_push_big [simp]: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir (Big.push x big) small) = States dir' big' small'\<rbrakk>
     \<Longrightarrow> remaining_steps (States dir' big' small') = remaining_steps (States dir big small) - 4"
   by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big )
 
 lemma step_4_remaining_steps_push_small [simp]: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
  (step^^4) (States dir big (Small.push x small)) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') = remaining_steps (States dir big small) - 4"
   by (metis invar_push_small remaining_steps_n_steps_sub remaining_steps_push_small)
 
 lemma step_4_remaining_steps_pop_big: "\<lbrakk>
   invar (States dir big small); 
   0 < size big; 
   Big.pop big = (x, bigP); 
   4 \<le> remaining_steps (States dir bigP small);
   (step^^4) (States dir bigP small) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') \<le> remaining_steps (States dir big small) - 4"
   by (metis add_le_imp_le_diff invar_pop_big remaining_steps_pop_big remaining_steps_n_steps_plus)
 
 lemma step_4_remaining_steps_pop_small: "\<lbrakk>
   invar (States dir big small); 
   0 < size small; 
   Small.pop small = (x, smallP); 
   4 \<le> remaining_steps (States dir big smallP);
   (step^^4) (States dir big smallP) = States dir' big' small'
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') \<le> remaining_steps (States dir big small) - 4"
   by (metis add_le_imp_le_diff invar_pop_small remaining_steps_n_steps_plus remaining_steps_pop_small)
 
 lemma step_4_pop_small_size_ok_1: "\<lbrakk>
   invar (States dir big small);
   0 < size small; 
   Small.pop small = (x, smallP); 
   4 \<le> remaining_steps (States dir big smallP);
   (step^^4) (States dir big smallP) = States dir' big' small'; 
   remaining_steps (States dir big small) + 1 \<le> 4 * size small
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'"
   by (smt (verit, ccfv_SIG) add.left_commute add.right_neutral add_le_cancel_left distrib_left_numeral dual_order.trans invar_pop_small le_add_diff_inverse2 mult.right_neutral plus_1_eq_Suc remaining_steps_n_steps_sub remaining_steps_pop_small step_n_pop_size_small)
   
 lemma step_4_pop_big_size_ok_1: "\<lbrakk>
   invar (States dir big small); 
   0 < size big; Big.pop big = (x, bigP); 
   4 \<le> remaining_steps (States dir bigP small);
   (step^^4) (States dir bigP small) = States dir' big' small'; 
   remaining_steps (States dir big small) + 1 \<le> 4 * size small
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'"
   by (smt (verit, ccfv_SIG) add_leE add_le_cancel_right invar_pop_big order_trans remaining_steps_pop_big step_n_size_small remaining_steps_n_steps_plus)
 
 lemma step_4_pop_small_size_ok_2: "\<lbrakk>
   invar (States dir big small); 
   0 < size small; 
   Small.pop small = (x, smallP); 
   4 \<le> remaining_steps (States dir big smallP);
   (step^^4) (States dir big smallP) = States dir' big' small'; 
   remaining_steps (States dir big small) + 1 \<le> 4 * size big
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size big'"
   by (smt (z3) add.commute add_leE invar_pop_small le_add_diff_inverse2 nat_add_left_cancel_le remaining_steps_n_steps_sub step_n_size_big remaining_steps_pop_small)
 
 lemma step_4_pop_big_size_ok_2: 
   assumes
     "invar (States dir big small)"
     "0 < size big"
     "Big.pop big = (x, bigP)"
     "remaining_steps (States dir bigP small) \<ge> 4"
     "((step ^^ 4) (States dir bigP small)) =  States dir' big' small'"
     "remaining_steps (States dir big small) + 1 \<le> 4 * size big"
   shows
     "remaining_steps (States dir' big' small') + 1 \<le> 4 * size big'"
 proof -
   from assms have "remaining_steps  (States dir bigP small) + 1 \<le> 4 * size big"
     by (meson add_le_cancel_right order.trans remaining_steps_pop_big)
 
   with assms show ?thesis
     by (smt (z3) Suc_diff_le Suc_eq_plus1 add_mult_distrib2 diff_diff_add diff_is_0_eq invar_pop_big mult_numeral_1_right numerals(1) plus_1_eq_Suc remaining_steps_n_steps_sub step_n_pop_size_big)
 qed
 
 lemma step_4_pop_small_size_ok_3: 
   assumes
     "invar (States dir big small)"
     "0 < size small"
     "Small.pop small = (x, smallP)"
     "remaining_steps (States dir big smallP) \<ge> 4"
     "((step ^^ 4) (States dir big smallP)) = States dir' big' small'"
     "size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big" 
   shows
     "size_new small' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new big'"
   by (smt (verit, best) add_leD2 add_mono_thms_linordered_semiring(1) add_mono_thms_linordered_semiring(3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) invar_pop_small le_add2 le_add_diff_inverse order_trans plus_1_eq_Suc remaining_steps_n_steps_sub remaining_steps_pop_small step_n_pop_size_new_small step_n_size_new_big)
 
 lemma step_4_pop_big_size_ok_3_aux: "\<lbrakk>
   0 < size big; 
   4 \<le> remaining_steps (States dir big small);
   size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big
 \<rbrakk> \<Longrightarrow> size_new small + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * (size_new big - 1)"
   by linarith
 
 lemma step_4_pop_big_size_ok_3: 
     assumes
       "invar (States dir big small)"
       "0 < size big" 
       "Big.pop big = (x, bigP) "
       "remaining_steps (States dir bigP small) \<ge> 4"
       "((step ^^ 4) (States dir bigP small)) = (States dir' big' small')"
       "size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big"
     shows
       "size_new small' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new big'"
 proof-
   from assms 
   have "size_new small + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * (size_new big - 1)"
     by (meson dual_order.trans remaining_steps_pop_big step_4_pop_big_size_ok_3_aux)
 
   then 
   have "size_new small + remaining_steps (States dir' big' small') + 2 \<le> 3 * (size_new big - 1)"
     by (smt (verit, ccfv_SIG) add_le_mono assms(1) assms(2) assms(3) assms(4) assms(5) dual_order.trans le_antisym less_or_eq_imp_le nat_less_le step_4_remaining_steps_pop_big)
 
   with assms show ?thesis 
     by (metis diff_Suc_1 invar_pop_big step_n_size_new_small step_n_pop_size_new_big)
 qed
 
 lemma step_4_pop_small_size_ok_4_aux: "\<lbrakk>
   0 < size small; 
   4 \<le> remaining_steps (States dir big small);
   size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small
 \<rbrakk> \<Longrightarrow> size_new big + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * (size_new small - 1)"
   by linarith
 
 lemma step_4_pop_small_size_ok_4:
     assumes
       "invar (States dir big small)"
       "0 < size small"
       "Small.pop small = (x, smallP)"
       "remaining_steps (States dir big smallP) \<ge> 4"
       "((step ^^ 4) (States dir big smallP)) = (States dir' big' small')"
       "size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small"
     shows
        "size_new big' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new small'"
 proof-
   from assms step_4_pop_small_size_ok_4_aux 
   have "size_new big + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * (size_new small - 1)"
     by (smt (verit, best) add_leE le_add_diff_inverse remaining_steps_pop_small)
 
   with assms 
   have "size_new big + remaining_steps (States dir' big' small') + 2 \<le> 3 * (size_new small - 1)"
     by (smt (verit, best) add_le_cancel_left add_mono_thms_linordered_semiring(3) diff_le_mono invar_pop_small order_trans remaining_steps_n_steps_sub remaining_steps_pop_small)
 
   with assms show ?thesis 
     by (metis diff_Suc_1 invar_pop_small step_n_size_new_big step_n_pop_size_new_small)
 qed
 
 lemma step_4_pop_big_size_ok_4_aux: "\<lbrakk>
   0 < size big; 
   4 \<le> remaining_steps (States dir big small);
   size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small
 \<rbrakk> \<Longrightarrow> size_new big - 1 + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * size_new small"
   by linarith
 
 lemma step_4_pop_big_size_ok_4: 
   assumes
     "invar (States dir big small)"
     "0 < size big "
     "Big.pop big = (x, bigP)"
     "remaining_steps (States dir bigP small) \<ge> 4"
     "((step ^^ 4) (States dir bigP small)) = (States dir' big' small')"
     "size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small"
   shows
     "size_new big' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new small'"
 proof -
   from assms step_4_pop_big_size_ok_4_aux
   have "(size_new big - 1) + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * size_new small"
     by linarith
 
   with assms 
   have "(size_new big - 1) + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new small"
     by (meson add_le_mono dual_order.eq_iff order_trans step_4_remaining_steps_pop_big)
 
   with assms show ?thesis 
     by (metis diff_Suc_1 invar_pop_big step_n_size_new_small step_n_pop_size_new_big)
 qed
 
 lemma step_4_push_small_size_ok_1: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir big (Small.push x small)) = States dir' big' small';
   remaining_steps (States dir big small) + 1 \<le> 4 * size small
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'"
   by (smt (z3) add.commute add_leD1 add_le_mono le_add1 le_add_diff_inverse2 mult_Suc_right nat_1_add_1 numeral_Bit0 step_n_push_size_small step_4_remaining_steps_push_small)
 
 lemma step_4_push_big_size_ok_1: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir (Big.push x big) small) = States dir' big' small';
   remaining_steps (States dir big small) + 1 \<le> 4 * size small
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'"
   by (smt (verit, ccfv_SIG) Nat.le_diff_conv2 add_leD2 invar_push_big le_add1 le_add_diff_inverse2 remaining_steps_n_steps_sub remaining_steps_push_big step_n_size_small)
 
 lemma step_4_push_small_size_ok_2: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir big (Small.push x small)) = States dir' big' small';
   remaining_steps (States dir big small) + 1 \<le> 4 * size big
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size big'"
   by (metis (full_types) Suc_diff_le Suc_eq_plus1 invar_push_small less_Suc_eq_le less_imp_diff_less step_4_remaining_steps_push_small step_n_size_big)
 
 lemma step_4_push_big_size_ok_2: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir (Big.push x big) small) = States dir' big' small';
   remaining_steps (States dir big small) + 1 \<le> 4 * size big
 \<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size big'"
   by (smt (verit, ccfv_SIG) add.commute add_diff_cancel_left' add_leD1 add_le_mono invar_push_big mult_Suc_right nat_le_iff_add one_le_numeral remaining_steps_n_steps_sub remaining_steps_push_big step_n_push_size_big)
 
 lemma step_4_push_small_size_ok_3_aux: "\<lbrakk>
   4 \<le> remaining_steps (States dir big small); 
   size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big
 \<rbrakk> \<Longrightarrow> Suc (size_new small) + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * size_new big"
   using distrib_left dual_order.trans le_add_diff_inverse2 by force
 
 lemma step_4_push_small_size_ok_3: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir big (Small.push x small)) = States dir' big' small';
   size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big
 \<rbrakk> \<Longrightarrow> size_new small' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new big'"
   using step_n_size_new_big step_n_push_size_new_small step_4_remaining_steps_push_small
   by (metis invar_push_small step_4_push_small_size_ok_3_aux)
 
 lemma step_4_push_big_size_ok_3_aux: "\<lbrakk>
   4 \<le> remaining_steps (States dir big small); 
   size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big
 \<rbrakk> \<Longrightarrow> size_new small + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * Suc (size_new big)"
   using distrib_left dual_order.trans le_add_diff_inverse2 by force
 
 lemma step_4_push_big_size_ok_3: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir (Big.push x big) small) = States dir' big' small';
   size_new small + remaining_steps (States dir big small) + 2 \<le> 3 * size_new big
 \<rbrakk> \<Longrightarrow> size_new small' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new big'"
   by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big step_4_push_big_size_ok_3_aux step_n_push_size_new_big step_n_size_new_small)
 
 lemma step_4_push_small_size_ok_4_aux: "\<lbrakk>
   4 \<le> remaining_steps (States dir big small); 
   size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small
 \<rbrakk> \<Longrightarrow> size_new big + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * Suc (size_new small)"
   using distrib_left dual_order.trans le_add_diff_inverse2 by force
 
 lemma step_4_push_small_size_ok_4: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir big (Small.push x small)) = States dir' big' small';
   size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small
 \<rbrakk> \<Longrightarrow> size_new big' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new small'"
   by (metis invar_push_small step_n_size_new_big step_n_push_size_new_small step_4_remaining_steps_push_small step_4_push_small_size_ok_4_aux)
 
 lemma step_4_push_big_size_ok_4_aux: "\<lbrakk>
   4 \<le> remaining_steps (States dir big small); 
   size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small
 \<rbrakk> \<Longrightarrow> Suc (size_new big) + (remaining_steps (States dir big small) - 4) + 2 \<le> 3 * size_new small"
   using distrib_left dual_order.trans le_add_diff_inverse2 by force
 
 lemma step_4_push_big_size_ok_4: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small);
   (step^^4) (States dir (Big.push x big) small) = States dir' big' small';
   size_new big + remaining_steps (States dir big small) + 2 \<le> 3 * size_new small
 \<rbrakk> \<Longrightarrow> size_new big' + remaining_steps (States dir' big' small') + 2 \<le> 3 * size_new small'"
   by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big step_4_push_big_size_ok_4_aux step_n_push_size_new_big step_n_size_new_small)
 
 lemma step_4_push_small_size_ok: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small); 
   size_ok (States dir big small)
 \<rbrakk> \<Longrightarrow> size_ok ((step^^4) (States dir big (Small.push x small)))"
   using step_4_push_small_size_ok_1 step_4_push_small_size_ok_2 step_4_push_small_size_ok_3 step_4_push_small_size_ok_4 
   by (smt (verit) size_ok'.elims(3) size_ok'.simps)
 
 lemma step_4_push_big_size_ok: "\<lbrakk>
   invar (States dir big small); 
   4 \<le> remaining_steps (States dir big small); 
   size_ok (States dir big small)
 \<rbrakk> \<Longrightarrow> size_ok ((step^^4) (States dir (Big.push x big) small))"
   using step_4_push_big_size_ok_1 step_4_push_big_size_ok_2 step_4_push_big_size_ok_3 step_4_push_big_size_ok_4
   by (smt (verit) size_ok'.elims(3) size_ok'.simps)
 
 lemma step_4_pop_small_size_ok: "\<lbrakk>
   invar (States dir big small); 
   0 < size small; 
   Small.pop small = (x, smallP); 
   4 \<le> remaining_steps (States dir big smallP);
   size_ok (States dir big small)
 \<rbrakk> \<Longrightarrow> size_ok ((step^^4) (States dir big smallP))"
   by (smt (verit) size_ok'.elims(3) size_ok'.simps step_4_pop_small_size_ok_1 step_4_pop_small_size_ok_2 step_4_pop_small_size_ok_3 step_4_pop_small_size_ok_4)
 
 lemma step_4_pop_big_size_ok: "\<lbrakk>
   invar (States dir big small); 
   0 < size big; Big.pop big = (x, bigP); 
   4 \<le> remaining_steps (States dir bigP small);
   size_ok (States dir big small)
 \<rbrakk> \<Longrightarrow> size_ok ((step^^4) (States dir bigP small))"
   using step_4_pop_big_size_ok_1 step_4_pop_big_size_ok_2 step_4_pop_big_size_ok_3 step_4_pop_big_size_ok_4
   by (smt (verit) size_ok'.elims(3) size_ok'.simps)
 
 lemma size_ok_size_small: "size_ok (States dir big small) \<Longrightarrow> 0 < size small"
   by auto
 
 lemma size_ok_size_big: "size_ok (States dir big small) \<Longrightarrow> 0 < size big"
   by auto
 
 lemma size_ok_size_new_small: "size_ok (States dir big small) \<Longrightarrow> 0 < size_new small"
   by auto
 
 lemma size_ok_size_new_big: "size_ok (States dir big small) \<Longrightarrow> 0 < size_new big"
   by auto
 
 lemma step_size_ok': "\<lbrakk>invar states; size_ok' states n\<rbrakk> \<Longrightarrow> size_ok' (step states) n"
   by (smt (verit, ccfv_SIG) size_ok'.elims(2) size_ok'.elims(3) step_size_big step_size_new_big step_size_new_small step_size_small)
 
 lemma step_same: "step (States dir big small) = States dir' big' small' \<Longrightarrow> dir = dir'"
   by(induction "States dir big small" rule: step_states.induct) auto
 
 lemma step_n_same: "(step^^n) (States dir big small) = States dir' big' small' \<Longrightarrow> dir = dir'"
 proof(induction n arbitrary: big small big' small')
   case 0
   then show ?case
     by simp
 next
   case (Suc n)
   obtain big'' small'' where "step (States dir big small) = States dir big'' small''"
     by (metis states.exhaust step_same)
 
   with Suc show ?case
     by(auto simp: funpow_swap1)
 qed
   
 lemma step_listL: "invar states \<Longrightarrow> listL (step states) = listL states"
 proof(induction states rule: listL.induct)
   case (1 big small)
   then have "list_small_first (States Left big small) = 
              Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     by auto
 
   then have "list_small_first (step (States Left big small)) = 
              Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     using 1 step_lists by fastforce
 
   then have "listL (step (States Left big small)) =
              Small_Aux.list_current small @ rev (Big_Aux.list_current big)"
     by (smt (verit, ccfv_SIG) "1" invar_states.elims(2) States_Proof.invar_step listL.simps(1) step_same)
 
   with 1 show ?case 
     by auto
 next
   case (2 big small)
   then have a: "list_big_first (States Right big small) = 
              Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
      using invar_list_big_first[of "States Right big small"]
      by auto
 
    then have "list_big_first (step (States Right big small)) = 
               Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     using 2 step_lists by fastforce
 
   then have "listL (step (States Right big small)) =
              Big_Aux.list_current big @ rev (Small_Aux.list_current small)"
     by (metis(full_types) listL.cases listL.simps(2) step_same)
 
   with 2 show ?case 
     using a by force
 qed
 
 lemma step_n_listL: "invar states \<Longrightarrow> listL ((step^^n) states) = listL states"
   using step_consistent[of listL states] step_listL
   by metis
 
 lemma listL_remaining_steps: 
   assumes
     "listL states = []"
     "0 < remaining_steps states"
     "invar states"
     "size_ok states"
   shows
     "False"
 proof(cases states)
   case (States dir big small)
   with assms show ?thesis 
     using Small_Proof.list_current_size size_ok_size_small
     by(cases dir; cases "lists (States dir big small)") auto
 qed
    
 lemma invar_step_n: "invar (states :: 'a states) \<Longrightarrow> invar ((step^^n) states)"
   by (simp add: invar_step step_consistent_2)
 
 lemma step_n_size_ok': "\<lbrakk>invar states; size_ok' states x\<rbrakk> \<Longrightarrow> size_ok' ((step ^^ n) states) x"
 proof(induction n arbitrary: states x)
   case 0
   then show ?case by auto
 next
   case Suc
   then show ?case  
     using invar_step_n step_size_ok'
     by fastforce
 qed
 
 lemma size_ok_steps: "\<lbrakk>
   invar states;
   size_ok' states (remaining_steps states - n)
 \<rbrakk> \<Longrightarrow> size_ok ((step ^^ n) states)"
   by (simp add: step_n_size_ok')
 
 lemma remaining_steps_idle: "invar states
   \<Longrightarrow> remaining_steps states = 0 \<longleftrightarrow> (
     case states of 
        States _ (Big.Common (Common.Idle _ _)) (Small.Common (Common.Idle _ _))  \<Rightarrow> True 
     | _ \<Rightarrow> False) "
   by(cases states)
-    (auto split: big_state.split small_state.split Common.state.split current.splits)
+    (auto split: big_state.split small_state.split common_state.split current.splits)
 
 lemma remaining_steps_idle': 
   "\<lbrakk>invar (States dir big small); remaining_steps (States dir big small) = 0\<rbrakk>
     \<Longrightarrow> \<exists>big_current big_idle small_current small_idle. States dir big small = 
           States dir 
-            (big_state.Common (state.Idle big_current big_idle)) 
-            (small_state.Common (state.Idle small_current small_idle))"
+            (big_state.Common (common_state.Idle big_current big_idle)) 
+            (small_state.Common (common_state.Idle small_current small_idle))"
   using remaining_steps_idle[of "States dir big small"]
-  by(cases big; cases small) (auto split!: Common.state.splits)
+  by(cases big; cases small) (auto split!: common_state.splits)
 
 end