theory GraphLang

lemma exec_graph_step_stack_extend:
  "continuing stack \<Longrightarrow>
    ((stack @ xs, stack') \<in> exec_graph_step Gamma)
    = (\<exists>stack''. stack' = stack'' @ xs
        \<and> (stack, stack'') \<in> exec_graph_step Gamma)" using exec_node_stack_extend[where stack'=stack' and stack=stack
            and Gamma=Gamma and xs=xs]
        exec_node_return_stack_extend[where stack'=stack' and stack="tl stack"
            and Gamma=Gamma and xs=xs] apply (simp add: exec_graph_step_def) apply (cases stack, simp_all) apply clarsimp apply (case_tac a, simp_all) apply (clarsimp split: option.split graph_function.split) apply (clarsimp simp: neq_Nil_conv split: list.split) apply (clarsimp split: next_node.split option.split graph_function.split) apply (clarsimp simp: neq_Nil_conv split: list.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma) = (\<exists>stack''. stack' = stack'' @ xs \<and> (stack, stack'') \<in> exec_graph_step Gamma) proof (prove)
using this:
continuing stack \<Longrightarrow> (stack' \<in> exec_node Gamma ?st ?node (stack @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma ?st ?node stack)
continuing (tl stack) \<Longrightarrow> (stack' \<in> exec_node_return Gamma ?st ?node (tl stack @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma ?st ?node (tl stack))

goal (1 subgoal):
 1. continuing stack \<Longrightarrow> ((stack @ xs, stack') \<in> exec_graph_step Gamma) = (\<exists>stack''. stack' = stack'' @ xs \<and> (stack, stack'') \<in> exec_graph_step Gamma) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>continuing stack; \<And>st node. (stack' \<in> exec_node Gamma st node (stack @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node stack); \<And>st node. continuing (tl stack) \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (tl stack @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node (tl stack))\<rbrakk> \<Longrightarrow> (case stack @ xs of [] \<Rightarrow> False | (NextNode nn, st, fname) # xa \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (stack @ xs) | Some node \<Rightarrow> stack' \<in> exec_node Gamma st node (stack @ xs) | [(Ret, st, x)] \<Rightarrow> False | (Ret, st, x) # (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (stack @ xs)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma st node (tl (stack @ xs)) | (Ret, st, x) # (_, b) # xb \<Rightarrow> stack' = upd_stack Err id (tl (stack @ xs)) | [(Err, b)] \<Rightarrow> False | (Err, b) # a # lista \<Rightarrow> stack' = upd_stack Err id (tl (stack @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case stack of [] \<Rightarrow> False | (NextNode nn, st, fname) # xa \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id stack | Some node \<Rightarrow> stack'' \<in> exec_node Gamma st node stack | [(Ret, st, x)] \<Rightarrow> False | (Ret, st, x) # (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id (tl stack) | Some node \<Rightarrow> stack'' \<in> exec_node_return Gamma st node (tl stack) | (Ret, st, x) # (_, b) # xb \<Rightarrow> stack'' = upd_stack Err id (tl stack) | [(Err, b)] \<Rightarrow> False | (Err, b) # a # lista \<Rightarrow> stack'' = upd_stack Err id (tl stack))) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>continuing (a # list); \<And>st node. (stack' \<in> exec_node Gamma st node (a # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node (a # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = a # list\<rbrakk> \<Longrightarrow> (case a of (NextNode nn, st, fname) \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (stack @ xs) | Some node \<Rightarrow> stack' \<in> exec_node Gamma st node (stack @ xs) | (Ret, st, x) \<Rightarrow> case list @ xs of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (stack @ xs)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma st node (tl (stack @ xs)) | (_, b) # xb \<Rightarrow> stack' = upd_stack Err id (tl (stack @ xs)) | (Err, b) \<Rightarrow> case list @ xs of [] \<Rightarrow> False | a # lista \<Rightarrow> stack' = upd_stack Err id (tl (stack @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case a of (NextNode nn, st, fname) \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id stack | Some node \<Rightarrow> stack'' \<in> exec_node Gamma st node stack | (Ret, st, x) \<Rightarrow> case list of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id (tl stack) | Some node \<Rightarrow> stack'' \<in> exec_node_return Gamma st node (tl stack) | (_, b) # xb \<Rightarrow> stack'' = upd_stack Err id (tl stack) | (Err, b) \<Rightarrow> case list of [] \<Rightarrow> False | a # lista \<Rightarrow> stack'' = upd_stack Err id (tl stack))) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b list. \<lbrakk>continuing ((a, aa, b) # list); \<And>st node. (stack' \<in> exec_node Gamma st node ((a, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((a, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (a, aa, b) # list\<rbrakk> \<Longrightarrow> (case a of NextNode nn \<Rightarrow> case Gamma b of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (((a, aa, b) # list) @ xs) | Some node \<Rightarrow> stack' \<in> exec_node Gamma aa node (((a, aa, b) # list) @ xs) | Ret \<Rightarrow> case list @ xs of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma aa node (tl (((a, aa, b) # list) @ xs)) | (_, ba) # xb \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs)) | Err \<Rightarrow> case list @ xs of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case a of NextNode nn \<Rightarrow> case Gamma b of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id ((a, aa, b) # list) | Some node \<Rightarrow> stack'' \<in> exec_node Gamma aa node ((a, aa, b) # list) | Ret \<Rightarrow> case list of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)) | Some node \<Rightarrow> stack'' \<in> exec_node_return Gamma aa node (tl ((a, aa, b) # list)) | (_, ba) # xb \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)) | Err \<Rightarrow> case list of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)))) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b list x1. \<lbrakk>\<And>st node. (stack' \<in> exec_node Gamma st node ((NextNode x1, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((NextNode x1, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (NextNode x1, aa, b) # list; a = NextNode x1\<rbrakk> \<Longrightarrow> (case Gamma b of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph x1 of None \<Rightarrow> stack' = upd_stack Err id (((a, aa, b) # list) @ xs) | Some node \<Rightarrow> stack' \<in> exec_node Gamma aa node (((a, aa, b) # list) @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case Gamma b of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph x1 of None \<Rightarrow> stack'' = upd_stack Err id ((a, aa, b) # list) | Some node \<Rightarrow> stack'' \<in> exec_node Gamma aa node ((a, aa, b) # list)))
 2. \<And>a aa b list. \<lbrakk>list \<noteq> []; \<And>st node. (stack' \<in> exec_node Gamma st node ((Ret, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((Ret, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (Ret, aa, b) # list; a = Ret\<rbrakk> \<Longrightarrow> (case list @ xs of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma aa node (tl (((a, aa, b) # list) @ xs)) | (_, ba) # xb \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case list of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)) | Some node \<Rightarrow> stack'' \<in> exec_node_return Gamma aa node (tl ((a, aa, b) # list)) | (_, ba) # xb \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list))))
 3. \<And>a aa b list. \<lbrakk>list \<noteq> []; \<And>st node. (stack' \<in> exec_node Gamma st node ((Err, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((Err, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (Err, aa, b) # list; a = Err\<rbrakk> \<Longrightarrow> (case list @ xs of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case list of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)))) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b list. \<lbrakk>list \<noteq> []; \<And>st node. (stack' \<in> exec_node Gamma st node ((Ret, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((Ret, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (Ret, aa, b) # list; a = Ret\<rbrakk> \<Longrightarrow> (case list @ xs of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma aa node (tl (((a, aa, b) # list) @ xs)) | (_, ba) # xb \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case list of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)) | Some node \<Rightarrow> stack'' \<in> exec_node_return Gamma aa node (tl ((a, aa, b) # list)) | (_, ba) # xb \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list))))
 2. \<And>a aa b list. \<lbrakk>list \<noteq> []; \<And>st node. (stack' \<in> exec_node Gamma st node ((Err, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((Err, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (Err, aa, b) # list; a = Err\<rbrakk> \<Longrightarrow> (case list @ xs of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case list of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)))) proof (prove)
goal (2 subgoals):
 1. \<And>aa b ac ba ys ad. \<lbrakk>\<And>st node. (stack' \<in> exec_node Gamma st node ((Ret, aa, b) # (ad, ac, ba) # ys @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((Ret, aa, b) # (ad, ac, ba) # ys)); \<And>st node. continuing ((ad, ac, ba) # ys) \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node ((ad, ac, ba) # ys @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node ((ad, ac, ba) # ys)); stack = (Ret, aa, b) # (ad, ac, ba) # ys\<rbrakk> \<Longrightarrow> (case ad of NextNode nn \<Rightarrow> case Gamma ba of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (((Ret, aa, b) # (ad, ac, ba) # ys) @ xs)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma aa node (tl (((Ret, aa, b) # (ad, ac, ba) # ys) @ xs)) | _ \<Rightarrow> stack' = upd_stack Err id (tl (((Ret, aa, b) # (ad, ac, ba) # ys) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case ad of NextNode nn \<Rightarrow> case Gamma ba of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack'' = upd_stack Err id (tl ((Ret, aa, b) # (ad, ac, ba) # ys)) | Some node \<Rightarrow> stack'' \<in> exec_node_return Gamma aa node (tl ((Ret, aa, b) # (ad, ac, ba) # ys)) | _ \<Rightarrow> stack'' = upd_stack Err id (tl ((Ret, aa, b) # (ad, ac, ba) # ys))))
 2. \<And>a aa b list. \<lbrakk>list \<noteq> []; \<And>st node. (stack' \<in> exec_node Gamma st node ((Err, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((Err, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (Err, aa, b) # list; a = Err\<rbrakk> \<Longrightarrow> (case list @ xs of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case list of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)))) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b list. \<lbrakk>list \<noteq> []; \<And>st node. (stack' \<in> exec_node Gamma st node ((Err, aa, b) # list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node Gamma st node ((Err, aa, b) # list)); \<And>st node. continuing list \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (list @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node list); stack = (Err, aa, b) # list; a = Err\<rbrakk> \<Longrightarrow> (case list @ xs of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack' = upd_stack Err id (tl (((a, aa, b) # list) @ xs))) = (\<exists>stack''. stack' = stack'' @ xs \<and> (case list of [] \<Rightarrow> False | ab # lista \<Rightarrow> stack'' = upd_stack Err id (tl ((a, aa, b) # list)))) proof (prove)
goal:
No subgoals!