theory GraphRefine

lemma c_trace_may_extend:
  "trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
    \<Longrightarrow> trace i = Some (com, Normal st)
    \<Longrightarrow> ((step \<Gamma>) ^^ j) (com, Normal st) (com', xst')
    \<Longrightarrow> (y, restrict_map trace {..i}) \<in> suffix_tuple_closure_inter Ss
    \<Longrightarrow> \<exists>trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
      \<and> trace' (i + j) = Some (com', xst')
      \<and> restrict_map trace' {.. i} = restrict_map trace {.. i}
      \<and> (y, restrict_map trace' {.. i + j}) \<in> suffix_tuple_closure_inter Ss" apply (cases "j = 0") apply fastforce apply (clarsimp simp: relpowp_fun_conv) apply (rule_tac x="\<lambda>k. if k \<le> i then trace k else
               if k \<le> i + j then Some (f (k - i))
               else None"
         in exI) apply (intro conjI) apply (erule nat_trace_rel_split, simp, simp_all) apply (drule_tac x=0 in spec, simp) apply (simp add: nat_trace_rel_def) apply (simp add: restrict_map_def cong: if_cong) apply (rule_tac k=i in suffix_tuple_closure_prefixI) apply (simp add: restrict_map_def cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (step \<Gamma> ^^ j) (com, Normal st) (com', xst'); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss\<rbrakk> \<Longrightarrow> \<exists>trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> trace' (i + j) = Some (com', xst') \<and> trace'|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, trace'|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (2 subgoals):
 1. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (step \<Gamma> ^^ j) (com, Normal st) (com', xst'); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; j = 0\<rbrakk> \<Longrightarrow> \<exists>trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> trace' (i + j) = Some (com', xst') \<and> trace'|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, trace'|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss
 2. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (step \<Gamma> ^^ j) (com, Normal st) (com', xst'); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; j \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> trace' (i + j) = Some (com', xst') \<and> trace'|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, trace'|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (step \<Gamma> ^^ j) (com, Normal st) (com', xst'); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; j \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> trace' (i + j) = Some (com', xst') \<and> trace'|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, trace'|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<exists>trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> trace' (i + j) = Some (com', xst') \<and> trace'|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, trace'|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None) \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> (if i + j \<le> i then trace (i + j) else if i + j \<le> i + j then Some (f (i + j - i)) else None) = Some (com', xst') \<and> (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (4 subgoals):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None) \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}
 2. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (if i + j \<le> i then trace (i + j) else if i + j \<le> i + j then Some (f (i + j - i)) else None) = Some (com', xst')
 3. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub>
 4. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (y, (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (4 subgoals):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (com, Normal st) \<rightarrow> f (Suc 0)
 2. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if Suc k \<le> j then Some (f (Suc i + k - i)) else None) \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}
 3. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub>
 4. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (y, (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if Suc k \<le> j then Some (f (Suc i + k - i)) else None) \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}
 2. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub>
 3. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (y, (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub>
 2. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (y, (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (y, (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; 0 < j; f 0 = (com, Normal st); f j = (com', xst'); \<forall>i<j. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (y, (\<lambda>k. if k \<le> i then trace k else if k \<le> i + j then Some (f (k - i)) else None)|\<^bsub>{..i + j}\<^esub>|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal:
No subgoals!