theory GraphProof

lemma trace_end_visit_Ret:
  "tr n = Some [(Ret, st, g)] \<Longrightarrow> tr (Suc n) = None
    \<Longrightarrow> tr \<in> exec_trace Gamma gf
    \<Longrightarrow> restrs_eventually_condition tr rs
    \<Longrightarrow> visit tr Ret rs = Some st" apply (rule visit_known, assumption) apply (clarsimp simp: restrs_eventually_condition_def) apply (drule spec, erule mp) apply (clarsimp simp: exec_trace_def) apply (drule(1) trace_None_dom_subset) apply auto[1] apply (clarsimp dest!: trace_addr_SomeD) apply (frule_tac i=j in exec_trace_step_cases, simp add: all_exec_graph_step_cases) apply (clarsimp simp: exec_trace_def) apply (auto dest!: trace_None_dom_subset) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> visit tr Ret rs = Some st proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> restrs_condition tr rs n
 2. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> \<forall>j<n. trace_addr tr j = Some Ret \<longrightarrow> \<not> restrs_condition tr rs j proof (prove)
goal (2 subgoals):
 1. \<And>na y. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; \<forall>m\<ge>na. restrs_condition tr rs m; tr na = Some y\<rbrakk> \<Longrightarrow> restrs_condition tr rs n
 2. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> \<forall>j<n. trace_addr tr j = Some Ret \<longrightarrow> \<not> restrs_condition tr rs j proof (prove)
goal (2 subgoals):
 1. \<And>na y. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; tr na = Some y\<rbrakk> \<Longrightarrow> na \<le> n
 2. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> \<forall>j<n. trace_addr tr j = Some Ret \<longrightarrow> \<not> restrs_condition tr rs j proof (prove)
goal (2 subgoals):
 1. \<And>na y gfa sta. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr na = Some y; Gamma gf = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, gf)]\<rbrakk> \<Longrightarrow> na \<le> n
 2. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> \<forall>j<n. trace_addr tr j = Some Ret \<longrightarrow> \<not> restrs_condition tr rs j proof (prove)
goal (2 subgoals):
 1. \<And>na y gfa sta. \<lbrakk>tr n = Some [(Ret, st, g)]; tr na = Some y; Gamma gf = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, gf)]; dom tr \<subseteq> {..<Suc n}\<rbrakk> \<Longrightarrow> na \<le> n
 2. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> \<forall>j<n. trace_addr tr j = Some Ret \<longrightarrow> \<not> restrs_condition tr rs j proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs\<rbrakk> \<Longrightarrow> \<forall>j<n. trace_addr tr j = Some Ret \<longrightarrow> \<not> restrs_condition tr rs j proof (prove)
goal (1 subgoal):
 1. \<And>j sta ga. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs; j < n; tr j = Some [(Ret, sta, ga)]; restrs_condition tr rs j\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>j sta ga. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; tr \<in> exec_trace Gamma gf; restrs_eventually_condition tr rs; j < n; tr j = Some [(Ret, sta, ga)]; restrs_condition tr rs j; tr (Suc j) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>j sta ga gfa staa. \<lbrakk>tr n = Some [(Ret, st, g)]; tr (Suc n) = None; restrs_eventually_condition tr rs; j < n; tr j = Some [(Ret, sta, ga)]; restrs_condition tr rs j; tr (Suc j) = None; Gamma gf = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), staa, gf)]\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!