[STATEMENT]
lemma observable_moves_preserves_stack:
  assumes "S,f \<turnstile> (m#ms,s) =as\<Rightarrow> (m'#ms',s')"
  and "valid_node m" and "valid_call_list cs m"
  and "\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)" and "valid_return_list rs m"
  and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "\<forall>i < length rs'. rs'!i \<in> get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'"
  and "ms' = targetnodes rs'" and "upd_cs cs as = cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs' rs'. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs as = cs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
from \<open>S,f \<turnstile> (m#ms,s) =as\<Rightarrow> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (m' # ms',s')
[PROOF STEP]
obtain msx s'' as' a'
    where "as = as'@[a']" and "S,f \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (msx,s'')"
    and "S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m'#ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>as' a' msx s''. \<lbrakk>as = as' @ [a']; S,f \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (msx,s''); S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:observable_moves.cases)
[PROOF STATE]
proof (state)
this:
as = as' @ [a']
S,f \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (msx,s'')
S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m' # ms',s')

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
from \<open>S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m' # ms',s')
[PROOF STEP]
obtain m'' ms''
    where [simp]:"msx = m''#ms''"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>m'' ms''. msx = m'' # ms'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases msx)(auto elim:observable_move.cases)
[PROOF STATE]
proof (state)
this:
msx = m'' # ms''

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
from \<open>S,f \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (msx,s'')\<close> \<open>valid_node m\<close> \<open>valid_call_list cs m\<close>
    \<open>\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)\<close> \<open>valid_return_list rs m\<close>
    \<open>length rs = length cs\<close> \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (msx,s'')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
[PROOF STEP]
obtain cs'' rs'' where "valid_node m''" and "valid_call_list cs'' m''"
    and "\<forall>i < length rs''. rs''!i \<in> get_return_edges (cs''!i)"
    and "valid_return_list rs'' m''" and "length rs'' = length cs''"
    and "ms'' = targetnodes rs''" and "upd_cs cs as' = cs''"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (msx,s'')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. (\<And>cs'' rs''. \<lbrakk>valid_node m''; valid_call_list cs'' m''; \<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i); valid_return_list rs'' m''; length rs'' = length cs''; ms'' = targetnodes rs''; upd_cs cs as' = cs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim!:silent_moves_preserves_stacks)
[PROOF STATE]
proof (state)
this:
valid_node m''
valid_call_list cs'' m''
\<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i)
valid_return_list rs'' m''
length rs'' = length cs''
ms'' = targetnodes rs''
upd_cs cs as' = cs''

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
with \<open>S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m' # ms',s')
valid_node m''
valid_call_list cs'' m''
\<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i)
valid_return_list rs'' m''
length rs'' = length cs''
ms'' = targetnodes rs''
upd_cs cs as' = cs''
[PROOF STEP]
obtain cs' rs' where results:"valid_node m'" "valid_call_list cs' m'"
    "\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)"
    "valid_return_list rs' m'" "length rs' = length cs'" "ms' = targetnodes rs'"
    and "upd_cs cs'' [a'] = cs'"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (msx,s'') -a'\<rightarrow> (m' # ms',s')
valid_node m''
valid_call_list cs'' m''
\<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i)
valid_return_list rs'' m''
length rs'' = length cs''
ms'' = targetnodes rs''
upd_cs cs as' = cs''

goal (1 subgoal):
 1. (\<And>cs' rs'. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs'' [a'] = cs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim!:observable_move_preserves_stacks)
[PROOF STATE]
proof (state)
this:
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'
upd_cs cs'' [a'] = cs'

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
from \<open>upd_cs cs as' = cs''\<close> \<open>upd_cs cs'' [a'] = cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs cs as' = cs''
upd_cs cs'' [a'] = cs'
[PROOF STEP]
have "upd_cs cs (as'@[a']) = cs'"
[PROOF STATE]
proof (prove)
using this:
upd_cs cs as' = cs''
upd_cs cs'' [a'] = cs'

goal (1 subgoal):
 1. upd_cs cs (as' @ [a']) = cs'
[PROOF STEP]
by(rule upd_cs_Append)
[PROOF STATE]
proof (state)
this:
upd_cs cs (as' @ [a']) = cs'

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
with \<open>as = as'@[a']\<close> results
[PROOF STATE]
proof (chain)
picking this:
as = as' @ [a']
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'
upd_cs cs (as' @ [a']) = cs'
[PROOF STEP]
show "\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and>
    (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and>
    valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and>
    upd_cs cs as = cs'"
[PROOF STATE]
proof (prove)
using this:
as = as' @ [a']
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'
upd_cs cs (as' @ [a']) = cs'

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
apply(rule_tac x="cs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>as = as' @ [a']; valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs (as' @ [a']) = cs'\<rbrakk> \<Longrightarrow> \<exists>rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
apply(rule_tac x="rs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>as = as' @ [a']; valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs (as' @ [a']) = cs'\<rbrakk> \<Longrightarrow> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'

goal:
No subgoals!
[PROOF STEP]
qed