theory GraphProof

lemma exec_trace_Gamma_deterministic:
  "trace \<in> exec_trace Gamma f
    \<Longrightarrow> trace' \<in> exec_trace (adds ++ Gamma) f
    \<Longrightarrow> \<forall>gf \<in> ran Gamma. \<forall>nn fname inps outps.
        (Call nn fname inps outps) \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds
    \<Longrightarrow> trace 0 = trace' 0
    \<Longrightarrow> trace n = trace' n" apply (induct n) apply simp apply (clarsimp simp: exec_trace_def nat_trace_rel_def) apply (drule_tac x=n in spec)+ apply (case_tac "trace' n", clarsimp+) apply (case_tac "trace (Suc n)", simp_all) apply (auto dest: step_implies_continuing)[1] apply (clarsimp simp: step_implies_continuing) apply (metis exec_graph_step_Gamma_deterministic) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> exec_trace Gamma f; trace' \<in> exec_trace (adds ++ Gamma) f; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds; trace 0 = trace' 0\<rbrakk> \<Longrightarrow> trace n = trace' n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>trace \<in> exec_trace Gamma f; trace' \<in> exec_trace (adds ++ Gamma) f; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds; trace 0 = trace' 0\<rbrakk> \<Longrightarrow> trace 0 = trace' 0
 2. \<And>n. \<lbrakk>\<lbrakk>trace \<in> exec_trace Gamma f; trace' \<in> exec_trace (adds ++ Gamma) f; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds; trace 0 = trace' 0\<rbrakk> \<Longrightarrow> trace n = trace' n; trace \<in> exec_trace Gamma f; trace' \<in> exec_trace (adds ++ Gamma) f; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds; trace 0 = trace' 0\<rbrakk> \<Longrightarrow> trace (Suc n) = trace' (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>trace \<in> exec_trace Gamma f; trace' \<in> exec_trace (adds ++ Gamma) f; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds; trace 0 = trace' 0\<rbrakk> \<Longrightarrow> trace n = trace' n; trace \<in> exec_trace Gamma f; trace' \<in> exec_trace (adds ++ Gamma) f; \<forall>gf\<in>ran Gamma. \<forall>nn fname inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf) \<longrightarrow> fname \<notin> dom adds; trace 0 = trace' 0\<rbrakk> \<Longrightarrow> trace (Suc n) = trace' (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n gfa st. \<lbrakk>trace n = trace' n; \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; trace 0 = Some [(NextNode (entry_point gfa), st, f)]; Gamma f = Some gfa; \<forall>n. (trace n = None \<longrightarrow> trace (Suc n) = None) \<and> ((\<exists>y. trace (Suc n) = Some y) \<longrightarrow> (the (trace n), the (trace (Suc n))) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. trace n = Some y) \<and> continuing (the (trace n)) \<longrightarrow> (\<exists>y. trace (Suc n) = Some y)); \<forall>n. (trace' n = None \<longrightarrow> trace' (Suc n) = None) \<and> ((\<exists>y. trace' (Suc n) = Some y) \<longrightarrow> (the (trace' n), the (trace' (Suc n))) \<in> exec_graph_step (adds ++ Gamma)) \<and> ((\<exists>y. trace' n = Some y) \<and> continuing (the (trace' n)) \<longrightarrow> (\<exists>y. trace' (Suc n) = Some y)); trace' 0 = Some [(NextNode (entry_point gfa), st, f)]\<rbrakk> \<Longrightarrow> trace (Suc n) = trace' (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n gfa st. \<lbrakk>trace n = trace' n; \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; trace 0 = Some [(NextNode (entry_point gfa), st, f)]; Gamma f = Some gfa; trace' 0 = Some [(NextNode (entry_point gfa), st, f)]; (trace n = None \<longrightarrow> trace (Suc n) = None) \<and> ((\<exists>y. trace (Suc n) = Some y) \<longrightarrow> (the (trace n), the (trace (Suc n))) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. trace n = Some y) \<and> continuing (the (trace n)) \<longrightarrow> (\<exists>y. trace (Suc n) = Some y)); (trace' n = None \<longrightarrow> trace' (Suc n) = None) \<and> ((\<exists>y. trace' (Suc n) = Some y) \<longrightarrow> (the (trace' n), the (trace' (Suc n))) \<in> exec_graph_step (adds ++ Gamma)) \<and> ((\<exists>y. trace' n = Some y) \<and> continuing (the (trace' n)) \<longrightarrow> (\<exists>y. trace' (Suc n) = Some y))\<rbrakk> \<Longrightarrow> trace (Suc n) = trace' (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n gfa st a. \<lbrakk>trace n = Some a; \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; trace 0 = Some [(NextNode (entry_point gfa), st, f)]; Gamma f = Some gfa; trace' 0 = Some [(NextNode (entry_point gfa), st, f)]; trace' n = Some a; (\<exists>y. trace (Suc n) = Some y) \<longrightarrow> (a, the (trace (Suc n))) \<in> exec_graph_step Gamma; continuing a \<longrightarrow> (\<exists>y. trace (Suc n) = Some y); (\<exists>y. trace' (Suc n) = Some y) \<longrightarrow> (a, the (trace' (Suc n))) \<in> exec_graph_step (adds ++ Gamma); continuing a \<longrightarrow> (\<exists>y. trace' (Suc n) = Some y)\<rbrakk> \<Longrightarrow> trace (Suc n) = trace' (Suc n) proof (prove)
goal (2 subgoals):
 1. \<And>n gfa st a. \<lbrakk>trace n = Some a; \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; trace 0 = Some [(NextNode (entry_point gfa), st, f)]; Gamma f = Some gfa; trace' 0 = Some [(NextNode (entry_point gfa), st, f)]; trace' n = Some a; \<not> continuing a; (\<exists>y. trace' (Suc n) = Some y) \<longrightarrow> (a, the (trace' (Suc n))) \<in> exec_graph_step (adds ++ Gamma); trace (Suc n) = None\<rbrakk> \<Longrightarrow> None = trace' (Suc n)
 2. \<And>n gfa st a aa. \<lbrakk>trace n = Some a; \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; trace 0 = Some [(NextNode (entry_point gfa), st, f)]; Gamma f = Some gfa; trace' 0 = Some [(NextNode (entry_point gfa), st, f)]; trace' n = Some a; (a, aa) \<in> exec_graph_step Gamma; (\<exists>y. trace' (Suc n) = Some y) \<longrightarrow> (a, the (trace' (Suc n))) \<in> exec_graph_step (adds ++ Gamma); continuing a \<longrightarrow> (\<exists>y. trace' (Suc n) = Some y); trace (Suc n) = Some aa\<rbrakk> \<Longrightarrow> Some aa = trace' (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n gfa st a aa. \<lbrakk>trace n = Some a; \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; trace 0 = Some [(NextNode (entry_point gfa), st, f)]; Gamma f = Some gfa; trace' 0 = Some [(NextNode (entry_point gfa), st, f)]; trace' n = Some a; (a, aa) \<in> exec_graph_step Gamma; (\<exists>y. trace' (Suc n) = Some y) \<longrightarrow> (a, the (trace' (Suc n))) \<in> exec_graph_step (adds ++ Gamma); continuing a \<longrightarrow> (\<exists>y. trace' (Suc n) = Some y); trace (Suc n) = Some aa\<rbrakk> \<Longrightarrow> Some aa = trace' (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n gfa st a aa y. \<lbrakk>trace n = Some a; \<forall>gf\<in>ran Gamma. \<forall>nn fname. (\<exists>inps outps. node.Call nn fname inps outps \<in> ran (function_graph gf)) \<longrightarrow> fname \<notin> dom adds; trace 0 = Some [(NextNode (entry_point gfa), st, f)]; Gamma f = Some gfa; trace' 0 = Some [(NextNode (entry_point gfa), st, f)]; trace' n = Some a; (a, aa) \<in> exec_graph_step Gamma; (a, y) \<in> exec_graph_step (adds ++ Gamma); trace (Suc n) = Some aa; trace' (Suc n) = Some y\<rbrakk> \<Longrightarrow> aa = y proof (prove)
goal:
No subgoals!