theory GraphProof

lemma visit_Basic:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> function_graph gf = graph
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> graph n = Some (Basic nn upds)
    \<Longrightarrow> converse (reachable_step graph) `` {nn} \<subseteq> {NextNode n}
    \<Longrightarrow> nn \<noteq> NextNode (entry_point gf)
    \<Longrightarrow> visit tr nn restrs = option_map (upd_vars upds)
        (visit tr (NextNode n) (pred_restrs' n restrs))" apply (cases "visit tr (NextNode n) (pred_restrs' n restrs)", simp_all) apply (clarsimp simp: visit_eqs) apply (frule(5) visit_immediate_pred) apply (clarsimp simp: pred_restrs) apply (frule(3) exec_trace_non_Call, simp) apply simp apply (clarsimp simp: visit_eqs) apply (frule trace_addr_SomeD, clarsimp) apply (frule_tac i=i in exec_trace_step_cases) apply (frule(1) exec_trace_invariant) apply (rule_tac x="Suc i" in exI) apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons K_def) apply (simp add: pred_restrs[unfolded trace_bottom_addr_def] trace_addr_SomeI) apply clarsimp apply (frule(2) visit_immediate_pred, simp+) apply clarsimp apply (frule(2) exec_trace_non_Call, simp+) apply (clarsimp simp: pred_restrs split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf)\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (upd_vars upds) (visit tr (NextNode n) (pred_restrs' n restrs)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); visit tr (NextNode n) (pred_restrs' n restrs) = None\<rbrakk> \<Longrightarrow> visit tr nn restrs = None
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> visit tr nn restrs = Some (upd_vars upds a) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; trace_addr tr i = Some nn; restrs_condition tr restrs i\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> visit tr nn restrs = Some (upd_vars upds a) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; trace_addr tr i = Some nn; restrs_condition tr restrs i; \<exists>i' nn'. i = Suc i' \<and> nn' \<in> {NextNode n} \<and> trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> visit tr nn restrs = Some (upd_vars upds a) proof (prove)
goal (2 subgoals):
 1. \<And>i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; trace_addr tr (Suc i') = Some nn; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> visit tr nn restrs = Some (upd_vars upds a) proof (prove)
goal (2 subgoals):
 1. \<And>i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; trace_addr tr (Suc i') = Some nn; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> visit tr nn restrs = Some (upd_vars upds a) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> visit tr nn restrs = Some (upd_vars upds a) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); graph = function_graph gf; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>ia. restrs_condition tr restrs ia \<and> trace_addr tr ia = Some nn \<and> upd_vars upds (fst (snd (hd (the (tr i))))) = fst (snd (hd (the (tr ia)))) \<and> (\<forall>j<ia. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); graph = function_graph gf; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> upd_vars upds st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); graph = function_graph gf; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, g)]; 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> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> upd_vars upds st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); graph = function_graph gf; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, g)]; 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; exec_graph_invariant Gamma fn [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> upd_vars upds st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Basic nn upds); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); graph = function_graph gf; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, g)]; 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; exec_graph_invariant Gamma fn [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc i) \<and> trace_addr tr (Suc i) = Some nn \<and> upd_vars upds st = fst (snd (hd (the (tr (Suc i))))) \<and> (\<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn) proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, upd_vars upds st, fn)]; gf = GraphFunction x1 x2 graph x4\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc i) \<and> trace_addr tr (Suc i) = Some nn \<and> (\<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn) proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, upd_vars upds st, fn)]; gf = GraphFunction x1 x2 graph x4\<rbrakk> \<Longrightarrow> \<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 j. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, upd_vars upds st, fn)]; gf = GraphFunction x1 x2 graph x4; j < Suc i; restrs_condition tr restrs j; trace_addr tr j = Some nn\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 j. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, upd_vars upds st, fn)]; gf = GraphFunction x1 x2 graph x4; j < Suc i; restrs_condition tr restrs j; trace_addr tr j = Some nn; \<exists>i'. j = Suc i' \<and> trace_bottom_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, upd_vars upds st, fn)]; gf = GraphFunction x1 x2 graph x4; restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; trace_bottom_addr tr i' = Some (NextNode n); i' < i\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Basic nn upds); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, upd_vars upds st, fn)]; gf = GraphFunction x1 x2 graph x4; restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; trace_bottom_addr tr i' = Some (NextNode n); i' < i; trace_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!