theory GraphProof

lemma num_visits_equals_j_first:
  "card {i. i < m \<and> trace_addr tr i = Some n} = j
    \<Longrightarrow> j \<noteq> 0
    \<Longrightarrow> \<exists>m'. trace_addr tr m' = Some n \<and> card {i. i < m' \<and> trace_addr tr i = Some n} = j - 1" apply (frule_tac P="\<lambda>m. card {i. i < m \<and> trace_addr tr i = Some n} = j" in ex_least_nat_le) apply simp apply clarify apply (rule_tac x="k - 1" in exI) apply (case_tac k) apply (simp del: Collect_empty_eq) apply (simp add: Collect_less_Suc split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>card {i. i < m \<and> trace_addr tr i = Some n} = j; j \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>m'. trace_addr tr m' = Some n \<and> card {i. i < m' \<and> trace_addr tr i = Some n} = j - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>card {i. i < m \<and> trace_addr tr i = Some n} = j; j \<noteq> 0\<rbrakk> \<Longrightarrow> card {i. i < 0 \<and> trace_addr tr i = Some n} \<noteq> j
 2. \<lbrakk>card {i. i < m \<and> trace_addr tr i = Some n} = j; j \<noteq> 0; \<exists>k\<le>m. (\<forall>i<k. card {ia. ia < i \<and> trace_addr tr ia = Some n} \<noteq> j) \<and> card {i. i < k \<and> trace_addr tr i = Some n} = j\<rbrakk> \<Longrightarrow> \<exists>m'. trace_addr tr m' = Some n \<and> card {i. i < m' \<and> trace_addr tr i = Some n} = j - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>card {i. i < m \<and> trace_addr tr i = Some n} = j; j \<noteq> 0; \<exists>k\<le>m. (\<forall>i<k. card {ia. ia < i \<and> trace_addr tr ia = Some n} \<noteq> j) \<and> card {i. i < k \<and> trace_addr tr i = Some n} = j\<rbrakk> \<Longrightarrow> \<exists>m'. trace_addr tr m' = Some n \<and> card {i. i < m' \<and> trace_addr tr i = Some n} = j - 1 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>j = card {i. i < m \<and> trace_addr tr i = Some n}; 0 < card {i. i < m \<and> trace_addr tr i = Some n}; k \<le> m; \<forall>i<k. card {ia. ia < i \<and> trace_addr tr ia = Some n} \<noteq> card {i. i < m \<and> trace_addr tr i = Some n}; card {i. i < k \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n}\<rbrakk> \<Longrightarrow> \<exists>m'. trace_addr tr m' = Some n \<and> card {i. i < m' \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n} - 1 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>j = card {i. i < m \<and> trace_addr tr i = Some n}; 0 < card {i. i < m \<and> trace_addr tr i = Some n}; k \<le> m; \<forall>i<k. card {ia. ia < i \<and> trace_addr tr ia = Some n} \<noteq> card {i. i < m \<and> trace_addr tr i = Some n}; card {i. i < k \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n}\<rbrakk> \<Longrightarrow> trace_addr tr (k - 1) = Some n \<and> card {i. i < k - 1 \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n} - 1 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>j = card {i. i < m \<and> trace_addr tr i = Some n}; 0 < card {i. i < m \<and> trace_addr tr i = Some n}; k \<le> m; \<forall>i<k. card {ia. ia < i \<and> trace_addr tr ia = Some n} \<noteq> card {i. i < m \<and> trace_addr tr i = Some n}; card {i. i < k \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n}; k = 0\<rbrakk> \<Longrightarrow> trace_addr tr (k - 1) = Some n \<and> card {i. i < k - 1 \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n} - 1
 2. \<And>k nat. \<lbrakk>j = card {i. i < m \<and> trace_addr tr i = Some n}; 0 < card {i. i < m \<and> trace_addr tr i = Some n}; k \<le> m; \<forall>i<k. card {ia. ia < i \<and> trace_addr tr ia = Some n} \<noteq> card {i. i < m \<and> trace_addr tr i = Some n}; card {i. i < k \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n}; k = Suc nat\<rbrakk> \<Longrightarrow> trace_addr tr (k - 1) = Some n \<and> card {i. i < k - 1 \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n} - 1 proof (prove)
goal (1 subgoal):
 1. \<And>k nat. \<lbrakk>j = card {i. i < m \<and> trace_addr tr i = Some n}; 0 < card {i. i < m \<and> trace_addr tr i = Some n}; k \<le> m; \<forall>i<k. card {ia. ia < i \<and> trace_addr tr ia = Some n} \<noteq> card {i. i < m \<and> trace_addr tr i = Some n}; card {i. i < k \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n}; k = Suc nat\<rbrakk> \<Longrightarrow> trace_addr tr (k - 1) = Some n \<and> card {i. i < k - 1 \<and> trace_addr tr i = Some n} = card {i. i < m \<and> trace_addr tr i = Some n} - 1 proof (prove)
goal:
No subgoals!