theory GraphProof

lemma restrs_eventually_init:
  "tr \<in> exec_trace Gamma fn
    \<Longrightarrow> Gamma fn = Some f
    \<Longrightarrow> converse (reachable_step' f) `` {NextNode (entry_point f)} \<subseteq> set []
    \<Longrightarrow> rs = (restrs_list [(entry_point f, [1])])
    \<Longrightarrow> restrs_eventually_condition tr rs" apply (clarsimp simp: restrs_eventually_condition_def) apply (rule_tac x=1 in exI) apply (rule conjI) apply (clarsimp simp: exec_trace_def nat_trace_rel_def) apply (clarsimp simp: restrs_condition_def restrs_list_def) apply (subst arg_cong[where f=card and y="{0}"], simp_all) apply (safe, simp_all) apply (case_tac x, simp_all) apply (drule(2) exec_trace_reachable_step, simp) apply auto[1] apply (clarsimp simp: exec_trace_def trace_addr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} \<subseteq> set []; rs = restrs_list [(entry_point f, [1])]\<rbrakk> \<Longrightarrow> restrs_eventually_condition tr rs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = restrs_list [(entry_point f, [Suc 0])]\<rbrakk> \<Longrightarrow> \<exists>n. (\<exists>y. tr n = Some y) \<and> (\<forall>m\<ge>n. restrs_condition tr (restrs_list [(entry_point f, [Suc 0])]) m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = restrs_list [(entry_point f, [Suc 0])]\<rbrakk> \<Longrightarrow> (\<exists>y. tr 1 = Some y) \<and> (\<forall>m\<ge>1. restrs_condition tr (restrs_list [(entry_point f, [Suc 0])]) m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = restrs_list [(entry_point f, [Suc 0])]\<rbrakk> \<Longrightarrow> \<exists>y. tr 1 = Some y
 2. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = restrs_list [(entry_point f, [Suc 0])]\<rbrakk> \<Longrightarrow> \<forall>m\<ge>1. restrs_condition tr (restrs_list [(entry_point f, [Suc 0])]) m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = restrs_list [(entry_point f, [Suc 0])]\<rbrakk> \<Longrightarrow> \<forall>m\<ge>1. restrs_condition tr (restrs_list [(entry_point f, [Suc 0])]) m proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc 0 \<le> m\<rbrakk> \<Longrightarrow> card {i. i < m \<and> trace_addr tr i = Some (NextNode (entry_point f))} = Suc 0 proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc 0 \<le> m\<rbrakk> \<Longrightarrow> {i. i < m \<and> trace_addr tr i = Some (NextNode (entry_point f))} = {0} proof (prove)
goal (2 subgoals):
 1. \<And>m x. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); x < m; trace_addr tr x = Some (NextNode (entry_point f))\<rbrakk> \<Longrightarrow> x = 0
 2. \<And>m. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc 0 \<le> m\<rbrakk> \<Longrightarrow> trace_addr tr 0 = Some (NextNode (entry_point f)) proof (prove)
goal (2 subgoals):
 1. \<And>m x nat. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc nat < m; trace_addr tr (Suc nat) = Some (NextNode (entry_point f)); x = Suc nat\<rbrakk> \<Longrightarrow> False
 2. \<And>m. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc 0 \<le> m\<rbrakk> \<Longrightarrow> trace_addr tr 0 = Some (NextNode (entry_point f)) proof (prove)
goal (2 subgoals):
 1. \<And>m x nat. \<lbrakk>Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc nat < m; trace_addr tr (Suc nat) = Some (NextNode (entry_point f)); x = Suc nat; \<exists>nn. (nn, NextNode (entry_point f)) \<in> reachable_step' f\<rbrakk> \<Longrightarrow> False
 2. \<And>m. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc 0 \<le> m\<rbrakk> \<Longrightarrow> trace_addr tr 0 = Some (NextNode (entry_point f)) proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (reachable_step' f)\<inverse> `` {NextNode (entry_point f)} = {}; rs = (\<lambda>i. if i = entry_point f then set [Suc 0] \<inter> UNIV else UNIV); Suc 0 \<le> m\<rbrakk> \<Longrightarrow> trace_addr tr 0 = Some (NextNode (entry_point f)) proof (prove)
goal:
No subgoals!