theory GraphProof

lemma exec_trace_non_Call:
  "\<lbrakk> tr \<in> exec_trace Gamma fn; Gamma fn = Some f;
        trace_bottom_addr tr i = Some (NextNode n);
        function_graph f n = Some node;
        case node of Call _ _ _ _ \<Rightarrow> False | _ \<Rightarrow> True
    \<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n)" apply (clarsimp simp: trace_bottom_addr_def split: option.split_asm) apply (frule(1) exec_trace_invariant) apply (clarsimp simp: exec_graph_invariant_def neq_Nil_conv) apply (case_tac "tl (the (tr i))" rule: rev_cases) apply (clarsimp simp: trace_addr_SomeI) apply (clarsimp simp: get_state_function_call_def split: node.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; trace_bottom_addr tr i = Some (NextNode n); function_graph f n = Some node; case node of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>function_graph f n = Some node; case node of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr i = Some x2; (case x2 of [] \<Rightarrow> None | a # list \<Rightarrow> Some (fst (last (a # list)))) = Some (NextNode n)\<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>function_graph f n = Some node; case node of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr i = Some x2; (case x2 of [] \<Rightarrow> None | a # list \<Rightarrow> Some (fst (last (a # list)))) = Some (NextNode n); exec_graph_invariant Gamma fn x2\<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ys. \<lbrakk>function_graph f n = Some node; case node of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr i = Some ((a, aa, b) # ys); fst (if ys = [] then (a, aa, b) else last ys) = NextNode n; \<forall>frame\<in>set ys. \<exists>y. get_state_function_call Gamma frame = Some y; Some b # map (Some \<circ> snd \<circ> snd) ys = map (get_state_function_call Gamma) ys @ [Some fn]\<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ys. \<lbrakk>function_graph f n = Some node; case node of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr i = Some ((a, aa, b) # ys); fst (if ys = [] then (a, aa, b) else last ys) = NextNode n; \<forall>frame\<in>set ys. \<exists>y. get_state_function_call Gamma frame = Some y; Some b # map (Some \<circ> snd \<circ> snd) ys = map (get_state_function_call Gamma) ys @ [Some fn]; tl (the (tr i)) = []\<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n)
 2. \<And>a aa b ys ysa y. \<lbrakk>function_graph f n = Some node; case node of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr i = Some ((a, aa, b) # ys); fst (if ys = [] then (a, aa, b) else last ys) = NextNode n; \<forall>frame\<in>set ys. \<exists>y. get_state_function_call Gamma frame = Some y; Some b # map (Some \<circ> snd \<circ> snd) ys = map (get_state_function_call Gamma) ys @ [Some fn]; tl (the (tr i)) = ysa @ [y]\<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ys ysa y. \<lbrakk>function_graph f n = Some node; case node of node.Call x xa xb xc \<Rightarrow> False | _ \<Rightarrow> True; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr i = Some ((a, aa, b) # ys); fst (if ys = [] then (a, aa, b) else last ys) = NextNode n; \<forall>frame\<in>set ys. \<exists>y. get_state_function_call Gamma frame = Some y; Some b # map (Some \<circ> snd \<circ> snd) ys = map (get_state_function_call Gamma) ys @ [Some fn]; tl (the (tr i)) = ysa @ [y]\<rbrakk> \<Longrightarrow> trace_addr tr i = Some (NextNode n) proof (prove)
goal:
No subgoals!