theory GraphProof

lemma visit_immediate_pred_step:
  "tr i = Some [(nn, st, fn')]
    \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> converse (reachable_step (function_graph gf)) `` {nn} \<subseteq> {NextNode n}
    \<Longrightarrow> nn \<noteq> NextNode (entry_point gf)
    \<Longrightarrow> (case (function_graph gf n) of None \<Rightarrow> False | Some (Call _ _ _ _) \<Rightarrow> False | _ \<Rightarrow> True)
    \<Longrightarrow> \<exists>i' st'. i = Suc i' \<and> fn' = fn \<and> tr i' = Some [(NextNode n, st', fn)]
      \<and> (([(NextNode n, st', fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma)" apply (frule(2) visit_immediate_pred[where i=i], simp_all) apply (simp add: trace_addr_def) apply (clarsimp split: option.split_asm) apply (frule(4) exec_trace_non_Call) apply (clarsimp dest!: trace_addr_SomeD) apply (frule_tac i=i' in exec_trace_step_cases, clarsimp) apply (frule_tac i=i' in exec_trace_invariant') apply (frule_tac i=i in exec_trace_invariant') apply (clarsimp simp: exec_graph_invariant_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); case function_graph gf n of None \<Rightarrow> False | Some (node.Call x xa xb xc) \<Rightarrow> False | Some _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> \<exists>i' st'. i = Suc i' \<and> fn' = fn \<and> tr i' = Some [(NextNode n, st', fn)] \<and> ([(NextNode n, st', fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr i = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); case function_graph gf n of None \<Rightarrow> False | Some (node.Call x xa xb xc) \<Rightarrow> False | Some _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> trace_addr tr i = Some nn
 2. \<lbrakk>tr i = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); case function_graph gf n of None \<Rightarrow> False | Some (node.Call x xa xb xc) \<Rightarrow> False | Some _ \<Rightarrow> True; \<exists>i'. i = Suc i' \<and> (\<exists>nn'. nn' \<in> {NextNode n} \<and> trace_bottom_addr tr i' = Some nn')\<rbrakk> \<Longrightarrow> \<exists>i'. i = Suc i' \<and> fn' = fn \<and> (\<exists>st'. tr i' = Some [(NextNode n, st', fn)] \<and> ([(NextNode n, st', fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); case function_graph gf n of None \<Rightarrow> False | Some (node.Call x xa xb xc) \<Rightarrow> False | Some _ \<Rightarrow> True; \<exists>i'. i = Suc i' \<and> (\<exists>nn'. nn' \<in> {NextNode n} \<and> trace_bottom_addr tr i' = Some nn')\<rbrakk> \<Longrightarrow> \<exists>i'. i = Suc i' \<and> fn' = fn \<and> (\<exists>st'. tr i' = Some [(NextNode n, st', fn)] \<and> ([(NextNode n, st', fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma) proof (prove)
goal (1 subgoal):
 1. \<And>x2 i'. \<lbrakk>tr (Suc i') = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); function_graph gf n = Some x2; i = Suc i'; trace_bottom_addr tr i' = Some (NextNode n); case x2 of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> fn' = fn \<and> (\<exists>st'. tr i' = Some [(NextNode n, st', fn)] \<and> ([(NextNode n, st', fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma) proof (prove)
goal (1 subgoal):
 1. \<And>x2 i'. \<lbrakk>tr (Suc i') = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); function_graph gf n = Some x2; i = Suc i'; trace_bottom_addr tr i' = Some (NextNode n); case x2 of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; trace_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> fn' = fn \<and> (\<exists>st'. tr i' = Some [(NextNode n, st', fn)] \<and> ([(NextNode n, st', fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma) proof (prove)
goal (1 subgoal):
 1. \<And>x2 i' sta g. \<lbrakk>tr (Suc i') = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); function_graph gf n = Some x2; i = Suc i'; trace_bottom_addr tr i' = Some (NextNode n); case x2 of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr i' = Some [(NextNode n, sta, g)]\<rbrakk> \<Longrightarrow> fn' = fn \<and> g = fn \<and> ([(NextNode n, sta, fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma proof (prove)
goal (1 subgoal):
 1. \<And>x2 i' sta g. \<lbrakk>tr (Suc i') = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); function_graph gf n = Some x2; i = Suc i'; trace_bottom_addr tr i' = Some (NextNode n); case x2 of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr i' = Some [(NextNode n, sta, g)]; ([(NextNode n, sta, g)], [(nn, st, fn')]) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> fn' = fn \<and> g = fn \<and> ([(NextNode n, sta, fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma proof (prove)
goal (1 subgoal):
 1. \<And>x2 i' sta g. \<lbrakk>tr (Suc i') = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); function_graph gf n = Some x2; i = Suc i'; trace_bottom_addr tr i' = Some (NextNode n); case x2 of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr i' = Some [(NextNode n, sta, g)]; ([(NextNode n, sta, g)], [(nn, st, fn')]) \<in> exec_graph_step Gamma; \<forall>stack. tr i' = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack\<rbrakk> \<Longrightarrow> fn' = fn \<and> g = fn \<and> ([(NextNode n, sta, fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma proof (prove)
goal (1 subgoal):
 1. \<And>x2 i' sta g. \<lbrakk>tr (Suc i') = Some [(nn, st, fn')]; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); function_graph gf n = Some x2; i = Suc i'; trace_bottom_addr tr i' = Some (NextNode n); case x2 of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr i' = Some [(NextNode n, sta, g)]; ([(NextNode n, sta, g)], [(nn, st, fn')]) \<in> exec_graph_step Gamma; \<forall>stack. tr i' = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack\<rbrakk> \<Longrightarrow> fn' = fn \<and> g = fn \<and> ([(NextNode n, sta, fn)], [(nn, st, fn)]) \<in> exec_graph_step Gamma proof (prove)
goal:
No subgoals!