theory GraphRefine

lemma extensible_traces_to_infinite_trace:
  assumes step: "\<forall>x \<in> S. (trace x, trace (f x)) \<in> extend_rel
          \<and> f x \<in> S \<and> m x < m (f x)"
    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 ?f = "\<lambda>i. (f ^^ i) x" have f_induct: "\<And>i. m (?f i) \<ge> i \<and> fst (trace (?f i)) \<ge> i \<and> ?f i \<in> S" apply (induct_tac i) apply (simp add: x) apply (auto dest: step[rule_format]) 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 (frule_tac step[rule_format]) 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 (prove)
goal (1 subgoal):
 1. \<And>i. i \<le> m ((f ^^ i) x) \<and> i \<le> fst (trace ((f ^^ i) x)) \<and> (f ^^ i) x \<in> S proof (prove)
goal (2 subgoals):
 1. \<And>i. 0 \<le> m ((f ^^ 0) x) \<and> 0 \<le> fst (trace ((f ^^ 0) x)) \<and> (f ^^ 0) x \<in> S
 2. \<And>i n. n \<le> m ((f ^^ n) x) \<and> n \<le> fst (trace ((f ^^ n) x)) \<and> (f ^^ n) x \<in> S \<Longrightarrow> Suc n \<le> m ((f ^^ Suc n) x) \<and> Suc n \<le> fst (trace ((f ^^ Suc n) x)) \<and> (f ^^ Suc n) x \<in> S proof (prove)
goal (1 subgoal):
 1. \<And>i n. n \<le> m ((f ^^ n) x) \<and> n \<le> fst (trace ((f ^^ n) x)) \<and> (f ^^ n) x \<in> S \<Longrightarrow> Suc n \<le> m ((f ^^ Suc n) x) \<and> Suc n \<le> fst (trace ((f ^^ Suc n) x)) \<and> (f ^^ Suc n) x \<in> S proof (prove)
goal:
No subgoals! proof (state)
this:
?i \<le> m ((f ^^ ?i) x) \<and> ?i \<le> fst (trace ((f ^^ ?i) x)) \<and> (f ^^ ?i) x \<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) x)) \<longrightarrow> j \<le> k \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ k) x)) \<and> snd (trace ((f ^^ k) x)) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal (2 subgoals):
 1. \<And>i j k. i \<le> fst (trace ((f ^^ j) x)) \<longrightarrow> j \<le> 0 \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ 0) x)) \<and> snd (trace ((f ^^ 0) x)) i = snd (trace ((f ^^ j) x)) i
 2. \<And>i j k n. i \<le> fst (trace ((f ^^ j) x)) \<longrightarrow> j \<le> n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ n) x)) \<and> snd (trace ((f ^^ n) x)) i = snd (trace ((f ^^ j) x)) i \<Longrightarrow> i \<le> fst (trace ((f ^^ j) x)) \<longrightarrow> j \<le> Suc n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ Suc n) x)) \<and> snd (trace ((f ^^ Suc n) x)) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j k n. i \<le> fst (trace ((f ^^ j) x)) \<longrightarrow> j \<le> n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ n) x)) \<and> snd (trace ((f ^^ n) x)) i = snd (trace ((f ^^ j) x)) i \<Longrightarrow> i \<le> fst (trace ((f ^^ j) x)) \<longrightarrow> j \<le> Suc n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ Suc n) x)) \<and> snd (trace ((f ^^ Suc n) x)) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>i \<le> fst (trace ((f ^^ j) x)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ n) x)) \<and> snd (trace ((f ^^ n) x)) i = snd (trace ((f ^^ j) x)) i\<rbrakk> \<Longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace (f ((f ^^ n) x))) \<and> snd (trace (f ((f ^^ n) x))) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>i \<le> fst (trace ((f ^^ j) x)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ n) x)) \<and> snd (trace ((f ^^ n) x)) i = snd (trace ((f ^^ j) x)) i; n \<le> m ((f ^^ n) x); n \<le> fst (trace ((f ^^ n) x)); (f ^^ n) x \<in> S\<rbrakk> \<Longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace (f ((f ^^ n) x))) \<and> snd (trace (f ((f ^^ n) x))) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>i \<le> fst (trace ((f ^^ j) x)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ n) x)) \<and> snd (trace ((f ^^ n) x)) i = snd (trace ((f ^^ j) x)) i; n \<le> m ((f ^^ n) x); n \<le> fst (trace ((f ^^ n) x)); (f ^^ n) x \<in> S; (trace ((f ^^ n) x), trace (f ((f ^^ n) x))) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<and> f ((f ^^ n) x) \<in> S \<and> m ((f ^^ n) x) < m (f ((f ^^ n) x))\<rbrakk> \<Longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace (f ((f ^^ n) x))) \<and> snd (trace (f ((f ^^ n) x))) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>\<forall>xa. fst (trace ((f ^^ n) x)) < xa \<or> snd (trace ((f ^^ n) x)) xa = snd (trace (f ((f ^^ n) x))) xa; f ((f ^^ n) x) \<in> S; m ((f ^^ n) x) < m (f ((f ^^ n) x)); i \<le> fst (trace ((f ^^ j) x)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ n) x)) \<and> snd (trace ((f ^^ n) x)) i = snd (trace ((f ^^ j) x)) i; n \<le> m ((f ^^ n) x); n \<le> fst (trace ((f ^^ n) x)); (f ^^ n) x \<in> S; fst (trace ((f ^^ n) x)) < fst (trace (f ((f ^^ n) x)))\<rbrakk> \<Longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace (f ((f ^^ n) x))) \<and> snd (trace (f ((f ^^ n) x))) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal (1 subgoal):
 1. \<And>i j n. \<lbrakk>f ((f ^^ n) x) \<in> S; m ((f ^^ n) x) < m (f ((f ^^ n) x)); i \<le> fst (trace ((f ^^ j) x)); j \<le> Suc n; j \<le> n \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ n) x)) \<and> snd (trace ((f ^^ n) x)) i = snd (trace ((f ^^ j) x)) i; n \<le> m ((f ^^ n) x); n \<le> fst (trace ((f ^^ n) x)); (f ^^ n) x \<in> S; fst (trace ((f ^^ n) x)) < fst (trace (f ((f ^^ n) x))); fst (trace ((f ^^ n) x)) < i \<or> snd (trace ((f ^^ n) x)) i = snd (trace (f ((f ^^ n) x))) i\<rbrakk> \<Longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace (f ((f ^^ n) x))) \<and> snd (trace (f ((f ^^ n) x))) i = snd (trace ((f ^^ j) x)) i proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i j k. i \<le> fst (trace ((f ^^ j) x)) \<longrightarrow> j \<le> k \<longrightarrow> fst (trace ((f ^^ j) x)) \<le> fst (trace ((f ^^ k) x)) \<and> snd (trace ((f ^^ k) x)) i = snd (trace ((f ^^ j) x)) 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) x)) \<longrightarrow> snd (trace ((f ^^ i) x)) j = snd (trace ((f ^^ j) x)) j proof (prove)
goal (1 subgoal):
 1. \<And>i j. j \<le> fst (trace ((f ^^ i) x)) \<Longrightarrow> snd (trace ((f ^^ i) x)) j = snd (trace ((f ^^ j) x)) j proof (prove)
goal (3 subgoals):
 1. \<And>i j. j \<le> fst (trace ((f ^^ i) x)) \<Longrightarrow> j \<le> fst (trace ((f ^^ min i j) x))
 2. \<And>i j. j \<le> fst (trace ((f ^^ i) x)) \<Longrightarrow> min i j \<le> max i j
 3. \<And>i j. \<lbrakk>j \<le> fst (trace ((f ^^ i) x)); fst (trace ((f ^^ min i j) x)) \<le> fst (trace ((f ^^ max i j) x)) \<and> snd (trace ((f ^^ max i j) x)) j = snd (trace ((f ^^ min i j) x)) j\<rbrakk> \<Longrightarrow> snd (trace ((f ^^ i) x)) j = snd (trace ((f ^^ j) x)) j proof (prove)
goal (2 subgoals):
 1. \<And>i j. j \<le> fst (trace ((f ^^ i) x)) \<Longrightarrow> min i j \<le> max i j
 2. \<And>i j. \<lbrakk>j \<le> fst (trace ((f ^^ i) x)); fst (trace ((f ^^ min i j) x)) \<le> fst (trace ((f ^^ max i j) x)) \<and> snd (trace ((f ^^ max i j) x)) j = snd (trace ((f ^^ min i j) x)) j\<rbrakk> \<Longrightarrow> snd (trace ((f ^^ i) x)) j = snd (trace ((f ^^ j) x)) j proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j \<le> fst (trace ((f ^^ i) x)); fst (trace ((f ^^ min i j) x)) \<le> fst (trace ((f ^^ max i j) x)) \<and> snd (trace ((f ^^ max i j) x)) j = snd (trace ((f ^^ min i j) x)) j\<rbrakk> \<Longrightarrow> snd (trace ((f ^^ i) x)) j = snd (trace ((f ^^ j) x)) j proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i j. j \<le> fst (trace ((f ^^ i) x)) \<longrightarrow> snd (trace ((f ^^ i) x)) j = snd (trace ((f ^^ j) x)) 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) x)) 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) x)) i)|\<^bsub>{..fst (trace y)}\<^esub> proof (prove)
goal (2 subgoals):
 1. \<And>i. i < m ((f ^^ Suc i) x) \<and> i < fst (trace ((f ^^ Suc i) x)) \<and> (\<exists>j. fst (trace ((f ^^ Suc i) x)) < j) \<and> snd (trace ((f ^^ Suc i) x))|\<^bsub>{..fst (trace ((f ^^ Suc i) x))}\<^esub> = (\<lambda>i. snd (trace ((f ^^ i) x)) i)|\<^bsub>{..fst (trace ((f ^^ Suc i) x))}\<^esub>
 2. \<And>i. (f ^^ Suc i) x \<in> S proof (prove)
goal (2 subgoals):
 1. \<And>i. Suc i \<le> m ((f ^^ Suc i) x) \<and> Suc i \<le> fst (trace ((f ^^ Suc i) x)) \<and> (f ^^ Suc i) x \<in> S \<Longrightarrow> i < m ((f ^^ Suc i) x) \<and> i < fst (trace ((f ^^ Suc i) x)) \<and> (\<exists>j. fst (trace ((f ^^ Suc i) x)) < j) \<and> snd (trace ((f ^^ Suc i) x))|\<^bsub>{..fst (trace ((f ^^ Suc i) x))}\<^esub> = (\<lambda>i. snd (trace ((f ^^ i) x)) i)|\<^bsub>{..fst (trace ((f ^^ Suc i) x))}\<^esub>
 2. \<And>i. (f ^^ Suc i) x \<in> S proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>Suc i \<le> m ((f ^^ Suc i) x); Suc i \<le> fst (trace ((f ^^ Suc i) x)); (f ^^ Suc i) x \<in> S\<rbrakk> \<Longrightarrow> Ex ((<) (fst (trace ((f ^^ Suc i) x))))
 2. \<And>i. (f ^^ Suc i) x \<in> S proof (prove)
goal (1 subgoal):
 1. \<And>i. (f ^^ Suc i) x \<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!