theory GraphLangLemmas

lemma rev_drop_step:
  "(stack, stack') \<in> exec_graph_step Gamma
    \<Longrightarrow> continuing (rev (drop k (rev stack)))
    \<Longrightarrow> (rev (drop k (rev stack)), rev (drop k (rev stack'))) \<in> exec_graph_step Gamma" apply (subgoal_tac "\<exists>xs ys. stack = xs @ ys \<and> k = length ys") apply clarsimp apply (frule(1) exec_graph_step_stack_extend[THEN iffD1]) apply clarsimp apply (rule_tac x="take (length stack - k) stack" in exI) apply (rule_tac x="drop (length stack - k) stack" in exI) apply (cases "length (rev (drop k (rev stack)))") apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack)))\<rbrakk> \<Longrightarrow> (rev (drop k (rev stack)), rev (drop k (rev stack'))) \<in> exec_graph_step Gamma proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack))); \<exists>xs ys. stack = xs @ ys \<and> k = length ys\<rbrakk> \<Longrightarrow> (rev (drop k (rev stack)), rev (drop k (rev stack'))) \<in> exec_graph_step Gamma
 2. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack)))\<rbrakk> \<Longrightarrow> \<exists>xs ys. stack = xs @ ys \<and> k = length ys proof (prove)
goal (2 subgoals):
 1. \<And>xs ys. \<lbrakk>(xs @ ys, stack') \<in> exec_graph_step Gamma; continuing xs; k = length ys; stack = xs @ ys\<rbrakk> \<Longrightarrow> (xs, rev (drop (length ys) (rev stack'))) \<in> exec_graph_step Gamma
 2. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack)))\<rbrakk> \<Longrightarrow> \<exists>xs ys. stack = xs @ ys \<and> k = length ys proof (prove)
goal (2 subgoals):
 1. \<And>xs ys. \<lbrakk>(xs @ ys, stack') \<in> exec_graph_step Gamma; continuing xs; k = length ys; stack = xs @ ys; \<exists>stack''. stack' = stack'' @ ys \<and> (xs, stack'') \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> (xs, rev (drop (length ys) (rev stack'))) \<in> exec_graph_step Gamma
 2. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack)))\<rbrakk> \<Longrightarrow> \<exists>xs ys. stack = xs @ ys \<and> k = length ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack)))\<rbrakk> \<Longrightarrow> \<exists>xs ys. stack = xs @ ys \<and> k = length ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack)))\<rbrakk> \<Longrightarrow> \<exists>ys. stack = take (length stack - k) stack @ ys \<and> k = length ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack)))\<rbrakk> \<Longrightarrow> stack = take (length stack - k) stack @ drop (length stack - k) stack \<and> k = length (drop (length stack - k) stack) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack))); length (rev (drop k (rev stack))) = 0\<rbrakk> \<Longrightarrow> stack = take (length stack - k) stack @ drop (length stack - k) stack \<and> k = length (drop (length stack - k) stack)
 2. \<And>nat. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack))); length (rev (drop k (rev stack))) = Suc nat\<rbrakk> \<Longrightarrow> stack = take (length stack - k) stack @ drop (length stack - k) stack \<and> k = length (drop (length stack - k) stack) proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; continuing (rev (drop k (rev stack))); length (rev (drop k (rev stack))) = Suc nat\<rbrakk> \<Longrightarrow> stack = take (length stack - k) stack @ drop (length stack - k) stack \<and> k = length (drop (length stack - k) stack) proof (prove)
goal:
No subgoals!