theory GraphProof

lemma visit_immediate_pred:
  "\<lbrakk> tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen;
        trace_addr tr i = Some nn; nn \<noteq> NextNode (entry_point f);
        converse (reachable_step' f) `` {nn} \<subseteq> S \<rbrakk>
    \<Longrightarrow> \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn'" apply (case_tac i) apply (clarsimp dest!: exec_trace_init trace_addr_SomeD) apply (rename_tac i') apply (frule trace_addr_SomeD, clarsimp) apply (frule(1) exec_trace_invariant) apply (frule_tac i=i' in exec_trace_step_reachable_induct2, assumption+) apply (simp add: trace_bottom_addr_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = 0\<rbrakk> \<Longrightarrow> \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn'
 2. \<And>nat. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc nat\<rbrakk> \<Longrightarrow> \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc nat\<rbrakk> \<Longrightarrow> \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal (1 subgoal):
 1. \<And>i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc i'\<rbrakk> \<Longrightarrow> \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal (1 subgoal):
 1. \<And>i' st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr (Suc i') = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc i'; tr (Suc i') = Some [(nn, st, g)]\<rbrakk> \<Longrightarrow> \<exists>nn'. nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal (1 subgoal):
 1. \<And>i' st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr (Suc i') = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc i'; tr (Suc i') = Some [(nn, st, g)]; exec_graph_invariant Gamma fn [(nn, st, g)]\<rbrakk> \<Longrightarrow> \<exists>nn'. nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal (2 subgoals):
 1. \<And>i' st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr (Suc i') = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc i'; tr (Suc i') = Some [(nn, st, g)]; exec_graph_invariant Gamma fn [(nn, st, g)]\<rbrakk> \<Longrightarrow> trace_bottom_addr tr (Suc i') = Some (?addr17 i' st g)
 2. \<And>i' st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr (Suc i') = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc i'; tr (Suc i') = Some [(nn, st, g)]; exec_graph_invariant Gamma fn [(nn, st, g)]; (\<forall>n. trace_bottom_addr tr i' = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph f)) \<and> trace_bottom_addr tr i' \<noteq> None \<and> (trace_bottom_addr tr i' = Some (?addr17 i' st g) \<and> trace_addr tr (Suc i') = None \<or> trace_addr tr (Suc i') = Some (?addr17 i' st g) \<and> (the (trace_bottom_addr tr i'), ?addr17 i' st g) \<in> reachable_step' f)\<rbrakk> \<Longrightarrow> \<exists>nn'. nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal (1 subgoal):
 1. \<And>i' st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; trace_addr tr (Suc i') = Some nn; nn \<noteq> NextNode (entry_point f); (reachable_step' f)\<inverse> `` {nn} \<subseteq> S; i = Suc i'; tr (Suc i') = Some [(nn, st, g)]; exec_graph_invariant Gamma fn [(nn, st, g)]; (\<forall>n. trace_bottom_addr tr i' = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph f)) \<and> trace_bottom_addr tr i' \<noteq> None \<and> (trace_bottom_addr tr i' = Some nn \<and> trace_addr tr (Suc i') = None \<or> trace_addr tr (Suc i') = Some nn \<and> (the (trace_bottom_addr tr i'), nn) \<in> reachable_step' f)\<rbrakk> \<Longrightarrow> \<exists>nn'. nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn' proof (prove)
goal:
No subgoals!