theory GraphLangLemmas

lemma trace_end_trace_drop_n_Some:
  "trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', dontcare)]
    \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
    \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs)
    \<Longrightarrow> Gamma fname = Some f'
    \<Longrightarrow> tr i = Some [(NextNode n, st, fn')]
    \<Longrightarrow> \<exists>j. tr (Suc i + j) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)]
" apply (frule(4) exec_trace_drop_n) apply (drule trace_end_SomeD, fastforce simp add: exec_trace_def) apply clarsimp apply (frule(4) exec_trace_drop_n_rest, simp, drule spec, drule(1) mp) apply simp apply (frule(1) exec_trace_invariant[where stack="[a, b]" for a b]) apply (clarsimp simp: exec_graph_invariant_Cons get_state_function_call_def) apply (frule_tac i="Suc i + na" in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases) apply (metis add_Suc_right) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', dontcare)]; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc i + j) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', dontcare)]; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]; trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc i + j) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]; trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fname; \<exists>n. trace_drop_n (Suc i) (Suc 0) tr n = Some [(Ret, st', dontcare)] \<and> trace_drop_n (Suc i) (Suc 0) tr (Suc n) = None \<and> \<not> continuing [(Ret, st', dontcare)]\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc i + j) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', dontcare)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc (i + j)) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', dontcare)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some ([(Ret, st', dontcare)] @ [(NextNode n, st, fn')])\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc (i + j)) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', dontcare)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, st', dontcare), (NextNode n, st, fn')]\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc (i + j)) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', dontcare)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, st', dontcare), (NextNode n, st, fn')]; exec_graph_invariant Gamma fn [(Ret, st', dontcare), (NextNode n, st, fn')]\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc (i + j)) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn dontcare inputs outputs); Gamma dontcare = Some f'; tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma dontcare; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', dontcare)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, st', dontcare), (NextNode n, st, fn)]; fname = dontcare; fn' = fn\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc (i + j)) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn dontcare inputs outputs); Gamma dontcare = Some f'; tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma dontcare; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', dontcare)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, st', dontcare), (NextNode n, st, fn)]; fname = dontcare; fn' = fn; ([(Ret, st', dontcare), (NextNode n, st, fn)], y) \<in> exec_graph_step Gamma; tr (Suc (Suc (i + na))) = Some y\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc (i + j)) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); x3 n = Some (node.Call nn dontcare inputs outputs); Gamma dontcare = Some (GraphFunction x1a x2a x3a x4a); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma dontcare; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', dontcare)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, st', dontcare), (NextNode n, st, fn)]; fname = dontcare; fn' = fn; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs st' st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a\<rbrakk> \<Longrightarrow> \<exists>j. tr (Suc (i + j)) = Some [(nn, return_vars x2a outputs st' st, fn)] proof (prove)
goal:
No subgoals!