theory GraphProof

lemma visit_merge:
  assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some f"
      and wf: "wf_graph_function f ilen olen"
      and ns: "nn \<noteq> NextNode (entry_point f)"
        "\<forall>n \<in> set ns. graph n = Some (Basic nn [])"
        "converse (reachable_step graph) `` {nn} \<subseteq> NextNode ` set ns"
     and geq: "function_graph f = graph"
     and cut: "\<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})"
              "\<forall>n \<in> set ns. (nn, NextNode n) \<notin> rtrancl
                      (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})"
  shows "visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n)
            (pred_restrs' n restrs)) ns) None" proof - note ns = ns[folded geq] note cut = cut[folded geq] have step_after:
    "\<And>n i. n \<in> set ns \<Longrightarrow> trace_bottom_addr tr i = Some (NextNode n)
        \<Longrightarrow> \<exists>st. tr i = Some [(NextNode n, st, fn)]
            \<and> tr (Suc i) = Some [(nn, st, fn)]
            \<and> trace_addr tr (Suc i) = Some nn
            \<and> restrs_condition tr restrs (Suc i)
                = restrs_condition tr (pred_restrs' n restrs) i" apply (drule exec_trace_non_Call[OF tr], (simp add: ns)+) apply (frule ns[rule_format], cut_tac tr(2)) apply (frule trace_addr_SomeD, clarsimp) apply (frule exec_trace_invariant[OF tr(1)]) apply (cut_tac i=i in exec_trace_step_cases[OF tr(1)]) apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons
                          upd_vars_def save_vals_def) apply (simp add: pred_restrs[OF tr(1)] trace_addr_SomeI trace_bottom_addr_def K_def) done have step_after_single:
    "\<And>n i. n \<in> set ns \<Longrightarrow> trace_bottom_addr tr i = Some (NextNode n)
        \<Longrightarrow> restrs_condition tr restrs (Suc i)
        \<Longrightarrow> (\<forall>n' j. n' \<in> set ns \<longrightarrow> trace_addr tr j = Some (NextNode n')
                \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i)" apply clarsimp apply (frule step_after, erule trace_addr_trace_bottom_addr_eq) apply (frule(1) step_after) apply clarsimp apply (drule(2) restrs_single_visit[OF tr wf _ _ _ _ cut(1)], simp_all) apply (rule not_trancl_converse_step, rule ns) apply (simp add: cut) done have visit_after:
    "\<And>n v. n \<in> set ns \<Longrightarrow> visit tr (NextNode n) (pred_restrs' n restrs) = Some v
        \<Longrightarrow> visit tr nn restrs \<noteq> None" apply (clarsimp simp: visit_eqs) apply (drule_tac i=i in step_after, simp add: trace_addr_trace_bottom_addr_eq) apply (rule_tac x="Suc i" in exI) apply clarsimp done show ?thesis apply (rule sym, cases "visit tr nn restrs", simp_all) apply (rule fold_merge_opt_Nones_eq) apply (rule ccontr, clarsimp simp: visit_after) apply (clarsimp simp: visit_eqs) apply (frule visit_immediate_pred[OF tr wf _ ns(1, 3)]) apply clarsimp apply (frule(1) step_after, clarsimp) apply (frule(2) step_after_single) apply (drule in_set_conv_decomp_last[THEN iffD1]) apply clarsimp apply (rule trans, rule fold_merge_opt_Nones_eq) apply (rule ccontr, clarsimp simp: visit_eqs pc_def ball_Un) apply (simp add: trace_addr_SomeI) apply (subst visit_known, assumption, simp_all) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (state)
goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (state)
this:
nn \<noteq> NextNode (entry_point f)
\<forall>n\<in>set ns. function_graph f n = Some (node.Basic nn [])
(reachable_step' f)\<inverse> `` {nn} \<subseteq> NextNode ` set ns

goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (state)
this:
\<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})
\<forall>n\<in>set ns. (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*

goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>st. tr i = Some [(NextNode n, st, fn)] \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n \<in> set ns; trace_addr tr i = Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>st. tr i = Some [(NextNode n, st, fn)] \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n \<in> set ns; trace_addr tr i = Some (NextNode n); function_graph f n = Some (node.Basic nn []); Gamma fn = Some f\<rbrakk> \<Longrightarrow> \<exists>st. tr i = Some [(NextNode n, st, fn)] \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i proof (prove)
goal (1 subgoal):
 1. \<And>n i st g. \<lbrakk>n \<in> set ns; trace_addr tr i = Some (NextNode n); function_graph f n = Some (node.Basic nn []); Gamma fn = Some f; tr i = Some [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> g = fn \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i proof (prove)
goal (1 subgoal):
 1. \<And>n i st g. \<lbrakk>n \<in> set ns; trace_addr tr i = Some (NextNode n); function_graph f n = Some (node.Basic nn []); Gamma fn = Some f; tr i = Some [(NextNode n, st, g)]; exec_graph_invariant Gamma fn [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> g = fn \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i proof (prove)
goal (1 subgoal):
 1. \<And>n i st g. \<lbrakk>n \<in> set ns; trace_addr tr i = Some (NextNode n); function_graph f n = Some (node.Basic nn []); Gamma fn = Some f; tr i = Some [(NextNode n, st, g)]; exec_graph_invariant Gamma fn [(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> g = fn \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i proof (prove)
goal (1 subgoal):
 1. \<And>n i st x1 x2 x3 x4. \<lbrakk>n \<in> set ns; trace_addr tr i = Some (NextNode n); x3 n = Some (node.Basic nn []); Gamma fn = Some (GraphFunction x1 x2 x3 x4); tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, st, fn)]; f = GraphFunction x1 x2 x3 x4\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?n \<in> set ns; trace_bottom_addr tr ?i = Some (NextNode ?n)\<rbrakk> \<Longrightarrow> \<exists>st. tr ?i = Some [(NextNode ?n, st, fn)] \<and> tr (Suc ?i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc ?i) = Some nn \<and> restrs_condition tr restrs (Suc ?i) = restrs_condition tr (pred_restrs' ?n restrs) ?i

goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n); restrs_condition tr restrs (Suc i)\<rbrakk> \<Longrightarrow> \<forall>n' j. n' \<in> set ns \<longrightarrow> trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i proof (prove)
goal (1 subgoal):
 1. \<And>n i n' j. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n); restrs_condition tr restrs (Suc i); n' \<in> set ns; trace_addr tr j = Some (NextNode n'); restrs_condition tr (pred_restrs' n' restrs) j\<rbrakk> \<Longrightarrow> j = i proof (prove)
goal (1 subgoal):
 1. \<And>n i n' j. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n); restrs_condition tr restrs (Suc i); n' \<in> set ns; trace_addr tr j = Some (NextNode n'); restrs_condition tr (pred_restrs' n' restrs) j; \<exists>st. tr j = Some [(NextNode n', st, fn)] \<and> tr (Suc j) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc j) = Some nn \<and> restrs_condition tr restrs (Suc j) = restrs_condition tr (pred_restrs' n' restrs) j\<rbrakk> \<Longrightarrow> j = i proof (prove)
goal (1 subgoal):
 1. \<And>n i n' j. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n); restrs_condition tr restrs (Suc i); n' \<in> set ns; trace_addr tr j = Some (NextNode n'); restrs_condition tr (pred_restrs' n' restrs) j; \<exists>st. tr j = Some [(NextNode n', st, fn)] \<and> tr (Suc j) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc j) = Some nn \<and> restrs_condition tr restrs (Suc j) = restrs_condition tr (pred_restrs' n' restrs) j; \<exists>st. tr i = Some [(NextNode n, st, fn)] \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> j = i proof (prove)
goal (1 subgoal):
 1. \<And>n i n' j st sta. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n); restrs_condition tr restrs (Suc i); n' \<in> set ns; trace_addr tr j = Some (NextNode n'); restrs_condition tr (pred_restrs' n' restrs) j; tr j = Some [(NextNode n', st, fn)]; tr i = Some [(NextNode n, sta, fn)]; tr (Suc j) = Some [(nn, st, fn)]; tr (Suc i) = Some [(nn, sta, fn)]; trace_addr tr (Suc j) = Some nn; restrs_condition tr restrs (Suc j); trace_addr tr (Suc i) = Some nn; restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> j = i proof (prove)
goal (1 subgoal):
 1. \<And>n i n' j st sta. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n); restrs_condition tr restrs (Suc i); n' \<in> set ns; trace_addr tr j = Some (NextNode n'); restrs_condition tr (pred_restrs' n' restrs) j; tr j = Some [(NextNode n', st, fn)]; tr i = Some [(NextNode n, sta, fn)]; tr (Suc j) = Some [(nn, st, fn)]; tr (Suc i) = Some [(nn, sta, fn)]; restrs_condition tr restrs (Suc j); trace_addr tr (Suc i) = Some nn; restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>n i n' j st sta. \<lbrakk>n \<in> set ns; trace_bottom_addr tr i = Some (NextNode n); restrs_condition tr restrs (Suc i); n' \<in> set ns; trace_addr tr j = Some (NextNode n'); restrs_condition tr (pred_restrs' n' restrs) j; tr j = Some [(NextNode n', st, fn)]; tr i = Some [(NextNode n, sta, fn)]; tr (Suc j) = Some [(nn, st, fn)]; tr (Suc i) = Some [(nn, sta, fn)]; restrs_condition tr restrs (Suc j); trace_addr tr (Suc i) = Some nn; restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> \<forall>z\<in>NextNode ` set ns. (nn, z) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>* proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?n \<in> set ns; trace_bottom_addr tr ?i = Some (NextNode ?n); restrs_condition tr restrs (Suc ?i)\<rbrakk> \<Longrightarrow> \<forall>n' j. n' \<in> set ns \<longrightarrow> trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = ?i

goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (prove)
goal (1 subgoal):
 1. \<And>n v. \<lbrakk>n \<in> set ns; visit tr (NextNode n) (pred_restrs' n restrs) = Some v\<rbrakk> \<Longrightarrow> visit tr nn restrs \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>n \<in> set ns; 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>i. trace_addr tr i = Some nn \<and> restrs_condition tr restrs i proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>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); \<exists>st. tr i = Some [(NextNode n, st, fn)] \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> \<exists>i. trace_addr tr i = Some nn \<and> restrs_condition tr restrs i proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>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); \<exists>st. tr i = Some [(NextNode n, st, fn)] \<and> tr (Suc i) = Some [(nn, st, fn)] \<and> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) = restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = Some nn \<and> restrs_condition tr restrs (Suc i) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?n \<in> set ns; visit tr (NextNode ?n) (pred_restrs' ?n restrs) = Some ?v\<rbrakk> \<Longrightarrow> visit tr nn restrs \<noteq> None

goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (prove)
goal (1 subgoal):
 1. visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None proof (prove)
goal (2 subgoals):
 1. visit tr nn restrs = None \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = None
 2. \<And>a. visit tr nn restrs = Some a \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some a proof (prove)
goal (2 subgoals):
 1. visit tr nn restrs = None \<Longrightarrow> \<forall>v\<in>set (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns). v = None
 2. \<And>a. visit tr nn restrs = Some a \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a. visit tr nn restrs = Some a \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some a proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>restrs_condition tr restrs i; trace_addr tr i = Some nn; \<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn\<rbrakk> \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some (fst (snd (hd (the (tr i))))) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>restrs_condition tr restrs i; trace_addr tr i = Some nn; \<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; \<exists>i' nn'. i = Suc i' \<and> nn' \<in> NextNode ` set ns \<and> trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some (fst (snd (hd (the (tr i))))) proof (prove)
goal (1 subgoal):
 1. \<And>i' nn'. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; nn' \<in> set ns; trace_bottom_addr tr i' = Some (NextNode nn')\<rbrakk> \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some (fst (snd (hd (the (tr (Suc i')))))) proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' st. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; nn' \<in> set ns; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'\<rbrakk> \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some st proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' st. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; nn' \<in> set ns; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n' j. n' \<in> set ns \<longrightarrow> trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i'\<rbrakk> \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some st proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' st. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n' j. n' \<in> set ns \<longrightarrow> trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i'; \<exists>ys zs. ns = ys @ nn' # zs \<and> nn' \<notin> set zs\<rbrakk> \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None = Some st proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' st ys zs. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n'. (n' = nn' \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode nn') \<longrightarrow> restrs_condition tr (pred_restrs' nn' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set ys \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set zs \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')); nn' \<notin> set zs; ns = ys @ nn' # zs\<rbrakk> \<Longrightarrow> fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) zs) (merge_opt (visit tr (NextNode nn') (pred_restrs' nn' restrs)) (fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ys) None)) = Some st proof (prove)
goal (2 subgoals):
 1. \<And>i' nn' st ys zs. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n'. (n' = nn' \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode nn') \<longrightarrow> restrs_condition tr (pred_restrs' nn' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set ys \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set zs \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')); nn' \<notin> set zs; ns = ys @ nn' # zs\<rbrakk> \<Longrightarrow> \<forall>v\<in>set (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) zs). v = None
 2. \<And>i' nn' st ys zs. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n'. (n' = nn' \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode nn') \<longrightarrow> restrs_condition tr (pred_restrs' nn' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set ys \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set zs \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')); nn' \<notin> set zs; ns = ys @ nn' # zs\<rbrakk> \<Longrightarrow> merge_opt (visit tr (NextNode nn') (pred_restrs' nn' restrs)) (fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ys) None) = Some st proof (prove)
goal (2 subgoals):
 1. \<And>i' nn' st ys zs v i. \<lbrakk>restrs_condition tr restrs (Suc i); trace_addr tr (Suc i) = Some nn; \<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i = Some (NextNode nn'); tr i = Some [(NextNode nn', st, fn)]; tr (Suc i) = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i; \<forall>n'. (n' = nn' \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode nn') \<longrightarrow> restrs_condition tr (pred_restrs' nn' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set ys \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set zs \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')); nn' \<notin> set zs; ns = ys @ nn' # zs; v \<in> set zs; trace_addr tr i = Some (NextNode v); restrs_condition tr (pred_restrs' v restrs) i\<rbrakk> \<Longrightarrow> False
 2. \<And>i' nn' st ys zs. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n'. (n' = nn' \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode nn') \<longrightarrow> restrs_condition tr (pred_restrs' nn' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set ys \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set zs \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')); nn' \<notin> set zs; ns = ys @ nn' # zs\<rbrakk> \<Longrightarrow> merge_opt (visit tr (NextNode nn') (pred_restrs' nn' restrs)) (fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ys) None) = Some st proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' st ys zs. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n'. (n' = nn' \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode nn') \<longrightarrow> restrs_condition tr (pred_restrs' nn' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set ys \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set zs \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')); nn' \<notin> set zs; ns = ys @ nn' # zs\<rbrakk> \<Longrightarrow> merge_opt (visit tr (NextNode nn') (pred_restrs' nn' restrs)) (fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ys) None) = Some st proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' st ys zs. \<lbrakk>restrs_condition tr restrs (Suc i'); trace_addr tr (Suc i') = Some nn; \<forall>j<Suc i'. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn; trace_bottom_addr tr i' = Some (NextNode nn'); tr i' = Some [(NextNode nn', st, fn)]; tr (Suc i') = Some [(nn, st, fn)]; restrs_condition tr (pred_restrs' nn' restrs) i'; \<forall>n'. (n' = nn' \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode nn') \<longrightarrow> restrs_condition tr (pred_restrs' nn' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set ys \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')) \<and> (n' \<in> set zs \<longrightarrow> (\<forall>j. trace_addr tr j = Some (NextNode n') \<longrightarrow> restrs_condition tr (pred_restrs' n' restrs) j \<longrightarrow> j = i')); nn' \<notin> set zs; ns = ys @ nn' # zs\<rbrakk> \<Longrightarrow> \<forall>j<i'. trace_addr tr j = Some (NextNode nn') \<longrightarrow> \<not> restrs_condition tr (pred_restrs' nn' restrs) j proof (prove)
goal:
No subgoals! proof (state)
this:
visit tr nn restrs = fold merge_opt (map (\<lambda>n. visit tr (NextNode n) (pred_restrs' n restrs)) ns) None

goal:
No subgoals!