theory GraphRefine

lemma extensible_traces_to_infinite_trace_choice:
  assumes step: "\<forall>x \<in> S. \<exists>y. (trace x, trace y) \<in> extend_rel
          \<and> y \<in> S \<and> m x < m y"
    and x: "x \<in> S"
  shows "\<exists>tr. \<forall>i :: nat. \<exists>y \<in> S. \<exists>j. m y > i \<and> fst (trace y) > i
    \<and> (trace y, (j, tr)) \<in> extend_rel" proof - let ?P = "\<lambda>i x. m x \<ge> i \<and> fst (trace x) \<ge> i \<and> x \<in> S" let ?Q = "\<lambda>x y. m y > m x \<and> (trace x, trace y) \<in> extend_rel" have induct:
    "\<And>x n. ?P n x \<Longrightarrow> \<exists>y. ?P (Suc n) y \<and> ?Q x y" apply clarsimp apply (frule step[THEN bspec]) apply clarsimp apply (rule_tac x=y in exI) apply simp done obtain f where f: "\<forall>n. ?P n (f n) \<and> ?Q (f n) (f (Suc n))" using x dependent_nat_choice[where P="?P" and Q="\<lambda>_. ?Q"] by (simp only: induct, auto) have f_induct: "\<And>i. m (f i) \<ge> i \<and> fst (trace (f i)) \<ge> i \<and> f i \<in> S" apply (cut_tac n=i in f[rule_format], simp) done have f_eq: "\<forall>i j k. i \<le> fst (trace (f j)) \<longrightarrow> j \<le> k
     \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f k)) \<and> snd (trace (f k)) i = snd (trace (f j)) i" apply (intro allI, induct_tac k) apply simp apply clarsimp apply (cut_tac i=n in f_induct[rule_format], clarsimp) apply (cut_tac n=n in f[rule_format], simp) apply (clarsimp simp: fun_eq_iff restrict_map_def linorder_not_le split_def
                   split: if_split_asm) apply (drule_tac x=i in spec) apply (auto simp: le_Suc_eq) done have f_norm:
    "\<forall>i j. j \<le> fst (trace (f i)) \<longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j" apply clarsimp apply (cut_tac i=j and j="min i j" and k="max i j" in f_eq[rule_format]) apply (simp add: min_def linorder_not_le f_induct) apply simp apply (simp add: min_def max_def split: if_split_asm) done show "?thesis" apply (rule_tac x="\<lambda>i. snd (trace (f i)) i" in exI) apply (clarsimp simp: split_def) apply (rule_tac x="f (Suc i)" in bexI) apply (cut_tac i="Suc i" in f_induct) apply (clarsimp simp: fun_eq_iff restrict_map_def f_norm
                 simp del: funpow.simps) apply (metis lessI) apply (simp add: f_induct del: funpow.simps) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (state)
goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (state)
goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (state)
goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<And>x n. n \<le> m x \<and> n \<le> fst (trace x) \<and> x \<in> S \<Longrightarrow> \<exists>y. (Suc n \<le> m y \<and> Suc n \<le> fst (trace y) \<and> y \<in> S) \<and> m x < m y \<and> (trace x, trace y) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>n \<le> m x; n \<le> fst (trace x); x \<in> S\<rbrakk> \<Longrightarrow> \<exists>y. Suc n \<le> m y \<and> Suc n \<le> fst (trace y) \<and> y \<in> S \<and> m x < m y \<and> (case trace x of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (trace y) proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>n \<le> m x; n \<le> fst (trace x); x \<in> S; \<exists>y. (trace x, trace y) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<and> y \<in> S \<and> m x < m y\<rbrakk> \<Longrightarrow> \<exists>y. Suc n \<le> m y \<and> Suc n \<le> fst (trace y) \<and> y \<in> S \<and> m x < m y \<and> (case trace x of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (trace y) proof (prove)
goal (1 subgoal):
 1. \<And>x n y xa ya xb yb. \<lbrakk>n \<le> m x; n \<le> xa; x \<in> S; trace x = (xa, ya); trace y = (xb, yb); y \<in> S; m x < m y; xa < xb; ya|\<^bsub>{..xa}\<^esub> = yb|\<^bsub>{..xa}\<^esub>\<rbrakk> \<Longrightarrow> \<exists>y. Suc n \<le> m y \<and> Suc n \<le> fst (trace y) \<and> y \<in> S \<and> m x < m y \<and> (case trace y of (j, tr') \<Rightarrow> xa < j \<and> yb|\<^bsub>{..xa}\<^esub> = tr'|\<^bsub>{..xa}\<^esub>) proof (prove)
goal (1 subgoal):
 1. \<And>x n y xa ya xb yb. \<lbrakk>n \<le> m x; n \<le> xa; x \<in> S; trace x = (xa, ya); trace y = (xb, yb); y \<in> S; m x < m y; xa < xb; ya|\<^bsub>{..xa}\<^esub> = yb|\<^bsub>{..xa}\<^esub>\<rbrakk> \<Longrightarrow> Suc n \<le> m y \<and> Suc n \<le> fst (trace y) \<and> y \<in> S \<and> m x < m y \<and> (case trace y of (j, tr') \<Rightarrow> xa < j \<and> yb|\<^bsub>{..xa}\<^esub> = tr'|\<^bsub>{..xa}\<^esub>) proof (prove)
goal:
No subgoals! proof (state)
this:
?n \<le> m ?x \<and> ?n \<le> fst (trace ?x) \<and> ?x \<in> S \<Longrightarrow> \<exists>y. (Suc ?n \<le> m y \<and> Suc ?n \<le> fst (trace y) \<and> y \<in> S) \<and> m ?x < m y \<and> (trace ?x, trace y) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}

goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<forall>n. (n \<le> m (f n) \<and> n \<le> fst (trace (f n)) \<and> f n \<in> S) \<and> m (f n) < m (f (Suc n)) \<and> (trace (f n), trace (f (Suc n))) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
x \<in> S
\<lbrakk>\<exists>x. 0 \<le> m x \<and> 0 \<le> fst (trace x) \<and> x \<in> S; \<And>x n. n \<le> m x \<and> n \<le> fst (trace x) \<and> x \<in> S \<Longrightarrow> \<exists>y. (Suc n \<le> m y \<and> Suc n \<le> fst (trace y) \<and> y \<in> S) \<and> m x < m y \<and> (trace x, trace y) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>n. (n \<le> m (f n) \<and> n \<le> fst (trace (f n)) \<and> f n \<in> S) \<and> m (f n) < m (f (Suc n)) \<and> (trace (f n), trace (f (Suc n))) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}

goal (1 subgoal):
 1. (\<And>f. \<forall>n. (n \<le> m (f n) \<and> n \<le> fst (trace (f n)) \<and> f n \<in> S) \<and> m (f n) < m (f (Suc n)) \<and> (trace (f n), trace (f (Suc n))) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
\<forall>n. (n \<le> m (f n) \<and> n \<le> fst (trace (f n)) \<and> f n \<in> S) \<and> m (f n) < m (f (Suc n)) \<and> (trace (f n), trace (f (Suc n))) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}

goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> m (f i) \<and> i \<le> fst (trace (f i)) \<and> f i \<in> S proof (prove)
goal:
No subgoals! proof (state)
this:
?i \<le> m (f ?i) \<and> ?i \<le> fst (trace (f ?i)) \<and> f ?i \<in> S

goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<forall>i j k. i \<le> fst (trace (f j)) \<longrightarrow> j \<le> k \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f k)) \<and> snd (trace (f k)) i = snd (trace (f j)) i proof (prove)
goal (2 subgoals):
 1. \<And>i j k. i \<le> fst (trace (f j)) \<longrightarrow> j \<le> 0 \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f 0)) \<and> snd (trace (f 0)) i = snd (trace (f j)) i
 2. \<And>i j k n. i \<le> fst (trace (f j)) \<longrightarrow> j \<le> n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f n)) \<and> snd (trace (f n)) i = snd (trace (f j)) i \<Longrightarrow> i \<le> fst (trace (f j)) \<longrightarrow> j \<le> Suc n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f (Suc n))) \<and> snd (trace (f (Suc n))) i = snd (trace (f j)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j k n. i \<le> fst (trace (f j)) \<longrightarrow> j \<le> n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f n)) \<and> snd (trace (f n)) i = snd (trace (f j)) i \<Longrightarrow> i \<le> fst (trace (f j)) \<longrightarrow> j \<le> Suc n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f (Suc n))) \<and> snd (trace (f (Suc n))) i = snd (trace (f j)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>i \<le> fst (trace (f j)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f n)) \<and> snd (trace (f n)) i = snd (trace (f j)) i\<rbrakk> \<Longrightarrow> fst (trace (f j)) \<le> fst (trace (f (Suc n))) \<and> snd (trace (f (Suc n))) i = snd (trace (f j)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>i \<le> fst (trace (f j)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f n)) \<and> snd (trace (f n)) i = snd (trace (f j)) i; n \<le> m (f n); n \<le> fst (trace (f n)); f n \<in> S\<rbrakk> \<Longrightarrow> fst (trace (f j)) \<le> fst (trace (f (Suc n))) \<and> snd (trace (f (Suc n))) i = snd (trace (f j)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>i \<le> fst (trace (f j)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f n)) \<and> snd (trace (f n)) i = snd (trace (f j)) i; n \<le> m (f n) \<and> n \<le> fst (trace (f n)) \<and> f n \<in> S \<and> m (f n) < m (f (Suc n)) \<and> (case trace (f n) of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (trace (f (Suc n)))\<rbrakk> \<Longrightarrow> fst (trace (f j)) \<le> fst (trace (f (Suc n))) \<and> snd (trace (f (Suc n))) i = snd (trace (f j)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>\<forall>x. fst (trace (f n)) < x \<or> snd (trace (f n)) x = snd (trace (f (Suc n))) x; i \<le> fst (trace (f j)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f n)) \<and> snd (trace (f n)) i = snd (trace (f j)) i; n \<le> m (f n); n \<le> fst (trace (f n)); f n \<in> S; m (f n) < m (f (Suc n)); fst (trace (f n)) < fst (trace (f (Suc n)))\<rbrakk> \<Longrightarrow> fst (trace (f j)) \<le> fst (trace (f (Suc n))) \<and> snd (trace (f (Suc n))) i = snd (trace (f j)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>i \<le> fst (trace (f j)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f n)) \<and> snd (trace (f n)) i = snd (trace (f j)) i; n \<le> m (f n); n \<le> fst (trace (f n)); f n \<in> S; m (f n) < m (f (Suc n)); fst (trace (f n)) < fst (trace (f (Suc n))); fst (trace (f n)) < i \<or> snd (trace (f n)) i = snd (trace (f (Suc n))) i\<rbrakk> \<Longrightarrow> fst (trace (f j)) \<le> fst (trace (f (Suc n))) \<and> snd (trace (f (Suc n))) i = snd (trace (f j)) i proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i j k. i \<le> fst (trace (f j)) \<longrightarrow> j \<le> k \<longrightarrow> fst (trace (f j)) \<le> fst (trace (f k)) \<and> snd (trace (f k)) i = snd (trace (f j)) i

goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<forall>i j. j \<le> fst (trace (f i)) \<longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j proof (prove)
goal (1 subgoal):
 1. \<And>i j. j \<le> fst (trace (f i)) \<Longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j proof (prove)
goal (3 subgoals):
 1. \<And>i j. j \<le> fst (trace (f i)) \<Longrightarrow> j \<le> fst (trace (f (min i j)))
 2. \<And>i j. j \<le> fst (trace (f i)) \<Longrightarrow> min i j \<le> max i j
 3. \<And>i j. \<lbrakk>j \<le> fst (trace (f i)); fst (trace (f (min i j))) \<le> fst (trace (f (max i j))) \<and> snd (trace (f (max i j))) j = snd (trace (f (min i j))) j\<rbrakk> \<Longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j proof (prove)
goal (2 subgoals):
 1. \<And>i j. j \<le> fst (trace (f i)) \<Longrightarrow> min i j \<le> max i j
 2. \<And>i j. \<lbrakk>j \<le> fst (trace (f i)); fst (trace (f (min i j))) \<le> fst (trace (f (max i j))) \<and> snd (trace (f (max i j))) j = snd (trace (f (min i j))) j\<rbrakk> \<Longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j \<le> fst (trace (f i)); fst (trace (f (min i j))) \<le> fst (trace (f (max i j))) \<and> snd (trace (f (max i j))) j = snd (trace (f (min i j))) j\<rbrakk> \<Longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i j. j \<le> fst (trace (f i)) \<longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j

goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, \<lambda>i. snd (trace (f i)) i) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} proof (prove)
goal (1 subgoal):
 1. \<And>i. \<exists>y\<in>S. i < m y \<and> i < fst (trace y) \<and> (\<exists>j. fst (trace y) < j) \<and> snd (trace y)|\<^bsub>{..fst (trace y)}\<^esub> = (\<lambda>i. snd (trace (f i)) i)|\<^bsub>{..fst (trace y)}\<^esub> proof (prove)
goal (2 subgoals):
 1. \<And>i. i < m (f (Suc i)) \<and> i < fst (trace (f (Suc i))) \<and> (\<exists>j. fst (trace (f (Suc i))) < j) \<and> snd (trace (f (Suc i)))|\<^bsub>{..fst (trace (f (Suc i)))}\<^esub> = (\<lambda>i. snd (trace (f i)) i)|\<^bsub>{..fst (trace (f (Suc i)))}\<^esub>
 2. \<And>i. f (Suc i) \<in> S proof (prove)
goal (2 subgoals):
 1. \<And>i. Suc i \<le> m (f (Suc i)) \<and> Suc i \<le> fst (trace (f (Suc i))) \<and> f (Suc i) \<in> S \<Longrightarrow> i < m (f (Suc i)) \<and> i < fst (trace (f (Suc i))) \<and> (\<exists>j. fst (trace (f (Suc i))) < j) \<and> snd (trace (f (Suc i)))|\<^bsub>{..fst (trace (f (Suc i)))}\<^esub> = (\<lambda>i. snd (trace (f i)) i)|\<^bsub>{..fst (trace (f (Suc i)))}\<^esub>
 2. \<And>i. f (Suc i) \<in> S proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>Suc i \<le> m (f (Suc i)); Suc i \<le> fst (trace (f (Suc i))); f (Suc i) \<in> S\<rbrakk> \<Longrightarrow> Ex ((<) (fst (trace (f (Suc i)))))
 2. \<And>i. f (Suc i) \<in> S proof (prove)
goal (1 subgoal):
 1. \<And>i. f (Suc i) \<in> S proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>tr. \<forall>i. \<exists>y\<in>S. \<exists>j. i < m y \<and> i < fst (trace y) \<and> (trace y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}

goal:
No subgoals!