theory GraphRefine

lemma trace_prefixes_to_trace:
  assumes i: "\<forall>i. \<exists>j tr k. j \<ge> i \<and> tr j \<noteq> None
        \<and> ((j, tr), (k, tr')) \<in> extend_rel \<and> tr \<in> nat_trace_rel c R"
  shows "trace_end tr' = None \<and> tr' \<in> nat_trace_rel c' R" proof (intro conjI) have weak: "tr' \<in> nat_trace_rel (\<lambda>x. False) R" apply (clarsimp simp: nat_trace_rel_def) apply (cut_tac i="Suc n" in i[rule_format]) apply (clarsimp simp: nat_trace_rel_def) apply (drule_tac x=n in spec, clarsimp) apply (clarsimp simp: restrict_map_prefix_eq) done have inf: "\<forall>i. tr' i \<noteq> None" apply (intro allI notI) apply (cut_tac i=i in i[rule_format]) apply (clarsimp simp: restrict_map_prefix_eq) apply (drule trace_None_dom_subset[OF _ weak]) apply auto done thus "trace_end tr' = None" by (simp only: trace_end_def, simp) show "tr' \<in> nat_trace_rel c' R" using weak by (simp only: nat_trace_rel_def inf mem_Collect_eq, simp) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trace_end tr' = None \<and> tr' \<in> nat_trace_rel c' R proof (state)
goal (2 subgoals):
 1. trace_end tr' = None
 2. tr' \<in> nat_trace_rel c' R proof (prove)
goal (1 subgoal):
 1. tr' \<in> nat_trace_rel (\<lambda>x. False) R proof (prove)
goal (1 subgoal):
 1. \<And>n. (tr' n = None \<longrightarrow> tr' (Suc n) = None) \<and> ((\<exists>y. tr' (Suc n) = Some y) \<longrightarrow> (the (tr' n), the (tr' (Suc n))) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<exists>j tr k. Suc n \<le> j \<and> tr j \<noteq> None \<and> ((j, tr), k, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<and> tr \<in> nat_trace_rel c R \<Longrightarrow> (tr' n = None \<longrightarrow> tr' (Suc n) = None) \<and> ((\<exists>y. tr' (Suc n) = Some y) \<longrightarrow> (the (tr' n), the (tr' (Suc n))) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>n j tr y x. \<lbrakk>Suc n \<le> j; tr j = Some y; j < x; tr|\<^bsub>{..j}\<^esub> = tr'|\<^bsub>{..j}\<^esub>; \<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>y. tr (Suc n) = Some y) \<longrightarrow> (the (tr n), the (tr (Suc n))) \<in> R) \<and> ((\<exists>y. tr n = Some y) \<and> c (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y))\<rbrakk> \<Longrightarrow> (tr' n = None \<longrightarrow> tr' (Suc n) = None) \<and> ((\<exists>y. tr' (Suc n) = Some y) \<longrightarrow> (the (tr' n), the (tr' (Suc n))) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>n j tr y x. \<lbrakk>Suc n \<le> j; tr j = Some y; j < x; tr|\<^bsub>{..j}\<^esub> = tr'|\<^bsub>{..j}\<^esub>; tr n = None \<longrightarrow> tr (Suc n) = None; (\<exists>y. tr (Suc n) = Some y) \<longrightarrow> (the (tr n), the (tr (Suc n))) \<in> R; (\<exists>y. tr n = Some y) \<and> c (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)\<rbrakk> \<Longrightarrow> (tr' n = None \<longrightarrow> tr' (Suc n) = None) \<and> ((\<exists>y. tr' (Suc n) = Some y) \<longrightarrow> (the (tr' n), the (tr' (Suc n))) \<in> R) proof (prove)
goal:
No subgoals! proof (state)
this:
tr' \<in> nat_trace_rel (\<lambda>x. False) R

goal (2 subgoals):
 1. trace_end tr' = None
 2. tr' \<in> nat_trace_rel c' R proof (prove)
goal (1 subgoal):
 1. \<forall>i. tr' i \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>i. tr' i = None \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr' i = None; \<exists>j tr k. i \<le> j \<and> tr j \<noteq> None \<and> ((j, tr), k, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<and> tr \<in> nat_trace_rel c R\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i j tr y x. \<lbrakk>tr' i = None; i \<le> j; tr' j = Some y; j < x; \<forall>i\<le>j. tr i = tr' i; tr \<in> nat_trace_rel c R\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i j tr y x. \<lbrakk>i \<le> j; tr' j = Some y; j < x; \<forall>i\<le>j. tr i = tr' i; tr \<in> nat_trace_rel c R; dom tr' \<subseteq> {..<i}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i. tr' i \<noteq> None

goal (2 subgoals):
 1. trace_end tr' = None
 2. tr' \<in> nat_trace_rel c' R proof (prove)
using this:
\<forall>i. tr' i \<noteq> None

goal (1 subgoal):
 1. trace_end tr' = None proof (state)
this:
trace_end tr' = None

goal (1 subgoal):
 1. tr' \<in> nat_trace_rel c' R proof (prove)
goal (1 subgoal):
 1. tr' \<in> nat_trace_rel c' R proof (prove)
using this:
tr' \<in> nat_trace_rel (\<lambda>x. False) R

goal (1 subgoal):
 1. tr' \<in> nat_trace_rel c' R proof (state)
this:
tr' \<in> nat_trace_rel c' R

goal:
No subgoals!