theory GraphProof

lemma restrs_eventually_at_visit:
  "restrs_eventually_condition tr (restrs_list rs)
    \<Longrightarrow> trace_addr tr i = Some nn
    \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> distinct (map fst rs)
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> restrs_condition tr (restrs_list (restrs_visit rs nn gf)) i" apply (clarsimp simp: restrs_eventually_condition_def
                        restrs_condition_def restrs_visit_abstract) apply (case_tac "i \<ge> n") apply (drule spec, drule(1) mp) apply auto[1] apply (simp add: linorder_not_le) apply (drule spec, drule mp, rule order_refl) apply safe apply (fastforce intro: card_mono) apply (simp add: not_reachable_visits_same[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>restrs_eventually_condition tr (restrs_list rs); trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list (restrs_visit rs nn gf)) i proof (prove)
goal (1 subgoal):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; \<forall>m\<ge>n. \<forall>ma. card {i. i < m \<and> trace_addr tr i = Some (NextNode ma)} \<in> restrs_list rs ma; tr n = Some y\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m) proof (prove)
goal (2 subgoals):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; \<forall>m\<ge>n. \<forall>ma. card {i. i < m \<and> trace_addr tr i = Some (NextNode ma)} \<in> restrs_list rs ma; tr n = Some y; n \<le> i\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m)
 2. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; \<forall>m\<ge>n. \<forall>ma. card {i. i < m \<and> trace_addr tr i = Some (NextNode ma)} \<in> restrs_list rs ma; tr n = Some y; \<not> n \<le> i\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m) proof (prove)
goal (2 subgoals):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; tr n = Some y; n \<le> i; \<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m)
 2. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; \<forall>m\<ge>n. \<forall>ma. card {i. i < m \<and> trace_addr tr i = Some (NextNode ma)} \<in> restrs_list rs ma; tr n = Some y; \<not> n \<le> i\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m) proof (prove)
goal (1 subgoal):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; \<forall>m\<ge>n. \<forall>ma. card {i. i < m \<and> trace_addr tr i = Some (NextNode ma)} \<in> restrs_list rs ma; tr n = Some y; \<not> n \<le> i\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m) proof (prove)
goal (1 subgoal):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; \<forall>m\<ge>n. \<forall>ma. card {i. i < m \<and> trace_addr tr i = Some (NextNode ma)} \<in> restrs_list rs ma; tr n = Some y; i < n\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m) proof (prove)
goal (1 subgoal):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; tr n = Some y; i < n; \<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> restrs_list rs m\<rbrakk> \<Longrightarrow> ((nn, NextNode m) \<in> (reachable_step' gf)\<^sup>* \<longrightarrow> (\<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l)) \<and> ((nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>* \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m) proof (prove)
goal (2 subgoals):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; tr n = Some y; i < n; \<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> restrs_list rs m; (nn, NextNode m) \<in> (reachable_step' gf)\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>l. l \<in> restrs_list rs m \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<le> l
 2. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; tr n = Some y; i < n; \<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> restrs_list rs m; (nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>*\<rbrakk> \<Longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m proof (prove)
goal (1 subgoal):
 1. \<And>n m y. \<lbrakk>trace_addr tr i = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; distinct (map fst rs); wf_graph_function gf ilen olen; tr n = Some y; i < n; \<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> restrs_list rs m; (nn, NextNode m) \<notin> (reachable_step' gf)\<^sup>*\<rbrakk> \<Longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m proof (prove)
goal:
No subgoals!