theory GraphRefine

lemma nontermination_to_c_trace:
  "tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma> \<turnstile> cfg \<rightarrow> cfg'}
    \<Longrightarrow> tr i = Some (add_cont com con, st)
    \<Longrightarrow> \<not> terminates \<Gamma> com st
    \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace \<Gamma> \<and> restrict_map tr' {..i} = restrict_map tr {..i}
      \<and> trace_end tr' = None" apply (clarsimp simp: terminates_iff_no_infinite_computation inf_def) apply (rule_tac x="\<lambda>j. if j \<le> i then tr j else case f (j - i) of
      (com', st') \<Rightarrow> Some (add_cont com' con, st')" in exI) apply (rule conjI) apply (simp add: c_trace_def) apply (rule nat_trace_rel_split, assumption, simp_all) apply (simp add: split_def) apply (rule add_cont_step) apply (drule spec[where x=0]) apply simp apply (clarsimp simp: nat_trace_rel_def split_def) apply (rule add_cont_step, simp) apply (frule(1) trace_Some_dom_superset) apply (rule conjI) apply (simp add: restrict_map_def fun_eq_iff) apply (simp only: trace_end_def) apply (rule if_not_P) apply (simp add: trace_end_def split_def subset_iff domIff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); \<not> \<Gamma>\<turnstile>com \<down> st\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace \<Gamma> \<and> tr'|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end tr' = None proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace \<Gamma> \<and> tr'|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end tr' = None proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> c_trace \<Gamma> \<and> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> c_trace \<Gamma>
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (4 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (case f (Suc 0) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = Some (?v'7 f)
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (add_cont com con, st) \<rightarrow> ?v'7 f
 3. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. case f (Suc j) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}
 4. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (add_cont com con, st) \<rightarrow> (add_cont (fst (f (Suc 0))) con, snd (f (Suc 0)))
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. case f (Suc j) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}
 3. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (com, st) \<rightarrow> (fst (f (Suc 0)), snd (f (Suc 0)))
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. case f (Suc j) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}
 3. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (com, st) \<rightarrow> (fst (f (Suc 0)), snd (f (Suc 0)))
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. case f (Suc j) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}
 3. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. case f (Suc j) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (2 subgoals):
 1. \<And>f n. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> \<Gamma>\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> F (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (add_cont (fst (f (Suc n))) con, snd (f (Suc n))) \<rightarrow> (add_cont (fst (f (Suc (Suc n)))) con, snd (f (Suc (Suc n))))
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub> \<and> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))|\<^bsub>{..i}\<^esub> = tr|\<^bsub>{..i}\<^esub>
 2. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> trace_end (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> (if \<exists>n. (if n \<le> i then tr n else case f (n - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None then if Max (dom (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))) \<le> i then tr (Max (dom (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')))) else case f (Max (dom (\<lambda>j. if j \<le> i then tr j else case f (j - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st'))) - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st') else None) = None proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>tr \<in> nat_trace_rel F {(cfg, cfg'). \<Gamma>\<turnstile> cfg \<rightarrow> cfg'}; tr i = Some (add_cont com con, st); f 0 = (com, st); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> \<nexists>n. (if n \<le> i then tr n else case f (n - i) of (com', st') \<Rightarrow> Some (add_cont com' con, st')) = None proof (prove)
goal:
No subgoals!