theory GraphProof

lemma exec_trace_step_reachable_induct:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> trace_bottom_addr tr (Suc i) = Some addr
    \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf))
        \<longrightarrow> trace_bottom_addr tr i \<noteq> None
        \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None
            \<or> trace_addr tr (Suc i) = Some addr
                \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf)" apply (frule_tac i=i in exec_trace_invariant') apply (frule_tac i=i in exec_trace_step_cases) apply (simp add: all_exec_graph_step_cases, safe dest!: trace_addr_SomeD,
         simp_all add: trace_bottom_addr_def del: last.simps) apply (auto simp: exec_graph_invariant_Cons reachable_step_def
                    get_state_function_call_def
             split: graph_function.split_asm,
         auto split: next_node.splits option.split node.splits if_split_asm
               simp: trace_addr_def neq_Nil_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_bottom_addr tr (Suc i) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_bottom_addr tr (Suc i) = Some addr; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_bottom_addr tr (Suc i) = Some addr; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack; tr i = None \<and> tr (Suc i) = None \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) \<or> tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf) proof (prove)
goal (40 subgoals):
 1. \<And>y ya aa b x22 x1 x1a x2a x3 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((Err, aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((Err, aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = None; ya = (Err, aa, b) # x22; trace_addr tr (Suc i) \<noteq> Some addr\<rbrakk> \<Longrightarrow> fst (last ((NextNode x1, aa, b) # x22)) = addr
 2. \<And>y ya aa b x22 x1 x1a x2a x3 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((Err, aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((Err, aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = None; ya = (Err, aa, b) # x22; trace_addr tr (Suc i) \<noteq> Some addr\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = None
 3. \<And>y ya aa b x22 x1 x1a x2a x3 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((Err, aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((Err, aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = None; ya = (Err, aa, b) # x22; (fst (last ((NextNode x1, aa, b) # x22)), addr) \<notin> reachable_step' gf\<rbrakk> \<Longrightarrow> fst (last ((NextNode x1, aa, b) # x22)) = addr
 4. \<And>y ya aa b x22 x1 x1a x2a x3 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((Err, aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((Err, aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = None; ya = (Err, aa, b) # x22; (fst (last ((NextNode x1, aa, b) # x22)), addr) \<notin> reachable_step' gf\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = None
 5. \<And>y ya aa b x22 x1 x1a x2a x3 x4 x11 x12. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((x11, upd_vars x12 aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((x11, upd_vars x12 aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Basic x11 x12); ya = (x11, upd_vars x12 aa, b) # x22; trace_addr tr (Suc i) \<noteq> Some addr\<rbrakk> \<Longrightarrow> fst (last ((NextNode x1, aa, b) # x22)) = addr
 6. \<And>y ya aa b x22 x1 x1a x2a x3 x4 x11 x12. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((x11, upd_vars x12 aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((x11, upd_vars x12 aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Basic x11 x12); ya = (x11, upd_vars x12 aa, b) # x22; trace_addr tr (Suc i) \<noteq> Some addr\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = None
 7. \<And>y ya aa b x22 x1 x1a x2a x3 x4 x11 x12. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((x11, upd_vars x12 aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((x11, upd_vars x12 aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Basic x11 x12); ya = (x11, upd_vars x12 aa, b) # x22; (fst (last ((NextNode x1, aa, b) # x22)), addr) \<notin> reachable_step' gf\<rbrakk> \<Longrightarrow> fst (last ((NextNode x1, aa, b) # x22)) = addr
 8. \<And>y ya aa b x22 x1 x1a x2a x3 x4 x11 x12. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((x11, upd_vars x12 aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((x11, upd_vars x12 aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Basic x11 x12); ya = (x11, upd_vars x12 aa, b) # x22; (fst (last ((NextNode x1, aa, b) # x22)), addr) \<notin> reachable_step' gf\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = None
 9. \<And>y ya aa b x22 x1 x1a x2a x3 x4 x21 x22a x23. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((if x23 aa then x21 else x22a, aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((if x23 aa then x21 else x22a, aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Cond x21 x22a x23); ya = (if x23 aa then x21 else x22a, aa, b) # x22; trace_addr tr (Suc i) \<noteq> Some addr\<rbrakk> \<Longrightarrow> fst (last ((NextNode x1, aa, b) # x22)) = addr
 10. \<And>y ya aa b x22 x1 x1a x2a x3 x4 x21 x22a x23. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; fst (last ((if x23 aa then x21 else x22a, aa, b) # x22)) = addr; exec_graph_invariant Gamma fn ((NextNode x1, aa, b) # x22); \<forall>n. fst (last ((NextNode x1, aa, b) # x22)) = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); tr i = Some ((NextNode x1, aa, b) # x22); tr (Suc i) = Some ((if x23 aa then x21 else x22a, aa, b) # x22); y = (NextNode x1, aa, b) # x22; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Cond x21 x22a x23); ya = (if x23 aa then x21 else x22a, aa, b) # x22; trace_addr tr (Suc i) \<noteq> Some addr\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = None
A total of 40 subgoals... proof (prove)
goal:
No subgoals!