theory GraphRefine

lemma exec_graph_trace_must_take_steps:
  "trace \<in> exec_trace \<Gamma> fn
    \<Longrightarrow> trace i = Some [(nn, st, fn)]
    \<Longrightarrow> (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}
    \<Longrightarrow> \<forall>k < j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k
        \<longrightarrow> continuing st'
    \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)]" apply (case_tac "trace (i + j)") apply (clarsimp simp add: exec_trace_def) apply (drule(1) trace_None_dom_eq) apply clarsimp apply (drule sym[where s="dom trace"]) apply (frule_tac x=i in eqset_imp_iff) apply (frule_tac x="n' - 1" in eqset_imp_iff) apply (frule_tac x="n'" in eqset_imp_iff) apply (simp(no_asm_use), clarsimp simp: domIff) apply (frule_tac i="n' - 1" in trace_end_eq_Some, simp+) apply (drule(1) trace_end_SomeD, clarsimp) apply (drule_tac x="n' - 1 - i" in spec, simp) apply (drule_tac i=i and j="n' - 1 - i" in nat_trace_rel_to_relpow, simp+) apply (clarsimp simp add: exec_trace_def) apply (drule_tac i=i and j=j in nat_trace_rel_to_relpow, simp+) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = None\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)]
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = None; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; \<exists>n'\<le>i + j. dom trace = {..<n'}\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n'. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; dom trace = {..<n'}\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n'. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n'. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace; (i \<in> {..<n'}) = (i \<in> dom trace)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n'. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace; (i \<in> {..<n'}) = (i \<in> dom trace); (n' - 1 \<in> {..<n'}) = (n' - 1 \<in> dom trace)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n'. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace; (i \<in> {..<n'}) = (i \<in> dom trace); (n' - 1 \<in> {..<n'}) = (n' - 1 \<in> dom trace); (n' \<in> {..<n'}) = (n' \<in> dom trace)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n' y. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace; i < n'; trace n' = None; trace (n' - Suc 0) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n' y. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace; i < n'; trace n' = None; trace (n' - Suc 0) = Some y; trace_end trace = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n' y n. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace; i < n'; trace n' = None; trace (n' - Suc 0) = Some y; trace n = Some y; trace (Suc n) = None; \<not> continuing y\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (2 subgoals):
 1. \<And>gf sta n' y n. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; n' \<le> i + j; {..<n'} = dom trace; i < n'; trace n' = None; trace (n' - Suc 0) = Some y; trace n = Some y; trace (Suc n) = None; \<not> continuing y; n' - Suc i < j \<longrightarrow> (\<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ (n' - Suc i) \<longrightarrow> continuing st')\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> trace (i + j) = Some [(nn', st', fn)] proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>trace \<in> exec_trace \<Gamma> fn; trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a\<rbrakk> \<Longrightarrow> a = [(nn', st', fn)] proof (prove)
goal (1 subgoal):
 1. \<And>a gf sta. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a; \<Gamma> fn = Some gf; trace \<in> nat_trace_rel continuing (exec_graph_step \<Gamma>); trace 0 = Some [(NextNode (entry_point gf), sta, fn)]\<rbrakk> \<Longrightarrow> a = [(nn', st', fn)] proof (prove)
goal (1 subgoal):
 1. \<And>a gf sta. \<lbrakk>trace i = Some [(nn, st, fn)]; (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}; \<forall>k<j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k \<longrightarrow> continuing st'; trace (i + j) = Some a; \<Gamma> fn = Some gf; trace 0 = Some [(NextNode (entry_point gf), sta, fn)]; ([(nn, st, fn)], a) \<in> exec_graph_step \<Gamma> ^^ j\<rbrakk> \<Longrightarrow> a = [(nn', st', fn)] proof (prove)
goal:
No subgoals!