theory GraphRefine

lemma nat_trace_rel_split:
  "tr n = Some v
    \<Longrightarrow> tr' (Suc n) = Some v'
    \<Longrightarrow> (v, v') \<in> R
    \<Longrightarrow> tr \<in> nat_trace_rel cont' R
    \<Longrightarrow> (\<lambda>i. tr' (Suc n + i)) \<in> nat_trace_rel cont R
    \<Longrightarrow> (\<lambda>i. if i \<le> n then tr i else tr' i) \<in> nat_trace_rel cont R" apply (frule(1) trace_Some_dom_superset) apply (clarsimp simp: nat_trace_rel_def, safe) apply (simp_all add: linorder_not_le less_Suc_eq_le subset_iff domIff) apply (drule_tac x="na - Suc n" in spec | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; tr \<in> nat_trace_rel cont' R; (\<lambda>i. tr' (Suc n + i)) \<in> nat_trace_rel cont R\<rbrakk> \<Longrightarrow> (\<lambda>i. if i \<le> n then tr i else tr' i) \<in> nat_trace_rel cont R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; tr \<in> nat_trace_rel cont' R; (\<lambda>i. tr' (Suc n + i)) \<in> nat_trace_rel cont R; {..n} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> (\<lambda>i. if i \<le> n then tr i else tr' i) \<in> nat_trace_rel cont R proof (prove)
goal (7 subgoals):
 1. \<And>na y. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); {..n} \<subseteq> dom tr; na \<le> n; Suc na \<le> n; cont (the (tr na)); tr na = Some y\<rbrakk> \<Longrightarrow> \<exists>y. tr (Suc na) = Some y
 2. \<And>na. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); {..n} \<subseteq> dom tr; na \<le> n; \<not> Suc na \<le> n; tr na = None\<rbrakk> \<Longrightarrow> tr' (Suc na) = None
 3. \<And>na y. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); {..n} \<subseteq> dom tr; na \<le> n; \<not> Suc na \<le> n; tr' (Suc na) = Some y\<rbrakk> \<Longrightarrow> (the (tr na), the (tr' (Suc na))) \<in> R
 4. \<And>na y. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); {..n} \<subseteq> dom tr; na \<le> n; \<not> Suc na \<le> n; cont (the (tr na)); tr na = Some y\<rbrakk> \<Longrightarrow> \<exists>y. tr' (Suc na) = Some y
 5. \<And>na. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); {..n} \<subseteq> dom tr; \<not> na \<le> n; tr' na = None\<rbrakk> \<Longrightarrow> tr' (Suc na) = None
 6. \<And>na y. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); {..n} \<subseteq> dom tr; \<not> na \<le> n; tr' (Suc na) = Some y\<rbrakk> \<Longrightarrow> (the (tr' na), the (tr' (Suc na))) \<in> R
 7. \<And>na y. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); {..n} \<subseteq> dom tr; \<not> na \<le> n; cont (the (tr' na)); tr' na = Some y\<rbrakk> \<Longrightarrow> \<exists>y. tr' (Suc na) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); \<forall>t\<le>n. \<exists>y. tr t = Some y; n < na; tr' na = None\<rbrakk> \<Longrightarrow> tr' (Suc na) = None
 2. \<And>na y. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); \<forall>t\<le>n. \<exists>y. tr t = Some y; n < na; tr' (Suc na) = Some y\<rbrakk> \<Longrightarrow> (the (tr' na), y) \<in> R
 3. \<And>na y. \<lbrakk>tr n = Some v; tr' (Suc n) = Some v'; (v, v') \<in> R; \<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> cont' (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); \<forall>na. (tr' (Suc (n + na)) = None \<longrightarrow> tr' (Suc (Suc (n + na))) = None) \<and> ((\<exists>y. tr' (Suc (Suc (n + na))) = Some y) \<longrightarrow> (the (tr' (Suc (n + na))), the (tr' (Suc (Suc (n + na))))) \<in> R) \<and> ((\<exists>y. tr' (Suc (n + na)) = Some y) \<and> cont (the (tr' (Suc (n + na)))) \<longrightarrow> (\<exists>y. tr' (Suc (Suc (n + na))) = Some y)); \<forall>t\<le>n. \<exists>y. tr t = Some y; n < na; cont y; tr' na = Some y\<rbrakk> \<Longrightarrow> \<exists>y. tr' (Suc na) = Some y proof (prove)
goal:
No subgoals!