theory GraphProof

lemma restrs_eventually_upt:
  "\<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> tr m \<noteq> None
    \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j
    \<Longrightarrow> restrs_eventually_condition tr ((\<lambda>_. UNIV) (n := {i ..< j}))" apply (clarsimp simp: restrs_eventually_condition_def restrs_condition_def) apply (rule exI, rule conjI, erule exI) apply (clarsimp simp: Suc_le_eq) apply (intro conjI impI allI) apply (rule card_mono) apply simp apply clarsimp apply (frule neq_counting_le, simp_all) apply (clarsimp simp: Collect_less_Suc) apply (drule_tac x=0 in spec, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> tr m \<noteq> None; \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j\<rbrakk> \<Longrightarrow> restrs_eventually_condition tr ((\<lambda>_. UNIV)(n := {i..<j})) proof (prove)
goal (1 subgoal):
 1. \<And>m y. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y\<rbrakk> \<Longrightarrow> \<exists>na. (\<exists>y. tr na = Some y) \<and> (\<forall>ma\<ge>na. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<le> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} \<and> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} < j) proof (prove)
goal (1 subgoal):
 1. \<And>m y. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y\<rbrakk> \<Longrightarrow> \<forall>ma\<ge>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<le> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} \<and> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} < j proof (prove)
goal (1 subgoal):
 1. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<le> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} \<and> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} < j proof (prove)
goal (2 subgoals):
 1. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<le> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)}
 2. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} < j proof (prove)
goal (3 subgoals):
 1. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> finite {i. i < ma \<and> trace_addr tr i = Some (NextNode n)}
 2. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<subseteq> {i. i < ma \<and> trace_addr tr i = Some (NextNode n)}
 3. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} < j proof (prove)
goal (2 subgoals):
 1. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<subseteq> {i. i < ma \<and> trace_addr tr i = Some (NextNode n)}
 2. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} < j proof (prove)
goal (1 subgoal):
 1. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> card {i. i < ma \<and> trace_addr tr i = Some (NextNode n)} < j proof (prove)
goal (2 subgoals):
 1. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> \<forall>i. card {ia. ia < Suc i \<and> trace_addr tr ia = Some (NextNode n)} \<le> Suc (card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode n)})
 2. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> 0 < j proof (prove)
goal (1 subgoal):
 1. \<And>m y ma. \<lbrakk>\<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j; i = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; tr m = Some y; m \<le> ma\<rbrakk> \<Longrightarrow> 0 < j proof (prove)
goal:
No subgoals!