theory GraphLang

lemma exec_node_return_stack_extend:
  "continuing stack \<Longrightarrow>
    (stack' \<in> exec_node_return Gamma st node (stack @ xs))
        = (\<exists>stack''. stack' = stack'' @ xs
                \<and> stack'' \<in> exec_node_return Gamma st node stack)" apply (cases node, simp_all) apply (simp_all add: continuing_def
                split: list.split_asm prod.split_asm next_node.split_asm) apply (auto split: option.split graph_function.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. continuing stack \<Longrightarrow> (stack' \<in> exec_node_return Gamma st node (stack @ xs)) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> exec_node_return Gamma st node stack) proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34. \<lbrakk>continuing stack; node = node.Call x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (stack' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) (stack @ xs)})) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) stack})) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x21 x22 x1 x2 x1a x2a x1b. \<lbrakk>node = node.Call x31 x32 x33 x34; stack = [(NextNode x1b, x1a, x2a)]; x22 = []; x21 = (NextNode x1b, x1a, x2a); x2 = (x1a, x2a); x1 = NextNode x1b\<rbrakk> \<Longrightarrow> (stack' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) (stack @ xs)})) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) stack}))
 2. \<And>x31 x32 x33 x34 x21 x22 x21a x22a x21b x1 x2 x1a x2a x1b. \<lbrakk>node = node.Call x31 x32 x33 x34; stack = (NextNode x1b, x1a, x2a) # x21a # x22a; x21b = x21a; x22 = x21a # x22a; x21 = (NextNode x1b, x1a, x2a); x2 = (x1a, x2a); x1 = NextNode x1b\<rbrakk> \<Longrightarrow> (stack' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) (stack @ xs)})) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) stack}))
 3. \<And>x31 x32 x33 x34 x21 x22 x21a x22a x21b x1 x2 x1a x2a. \<lbrakk>node = node.Call x31 x32 x33 x34; stack = (Ret, x1a, x2a) # x21a # x22a; x21b = x21a; x22 = x21a # x22a; x21 = (Ret, x1a, x2a); x2 = (x1a, x2a); x1 = Ret\<rbrakk> \<Longrightarrow> (stack' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) (stack @ xs)})) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) stack}))
 4. \<And>x31 x32 x33 x34 x21 x22 x21a x22a x21b x1 x2 x1a x2a. \<lbrakk>node = node.Call x31 x32 x33 x34; stack = (Err, x1a, x2a) # x21a # x22a; x21b = x21a; x22 = x21a # x22a; x21 = (Err, x1a, x2a); x2 = (x1a, x2a); x1 = Err\<rbrakk> \<Longrightarrow> (stack' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) (stack @ xs)})) = (\<exists>stack''. stack' = stack'' @ xs \<and> stack'' \<in> (case Gamma x32 of None \<Rightarrow> {} | Some (GraphFunction inps outps graph ep) \<Rightarrow> {upd_stack x31 (return_vars outps x34 st) stack})) proof (prove)
goal:
No subgoals!