theory GraphLang

lemma trace_end_SomeD:
  "trace_end tr = Some v \<Longrightarrow> tr \<in> nat_trace_rel cont r
    \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> \<not> cont v" apply (clarsimp simp: trace_end_def split: if_split_asm) apply (rule exI, rule conjI, assumption) apply (case_tac "tr (Suc (Max (dom tr)))") apply (simp add: nat_trace_rel_def) apply (metis option.sel option.simps(3)) apply (cut_tac x="Suc y" for y in Max_ge[OF finite_subset domI]) apply (erule(1) trace_None_dom_subset[rotated]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end tr = Some v; tr \<in> nat_trace_rel cont r\<rbrakk> \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> \<not> cont v proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v\<rbrakk> \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> \<not> cont v proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v\<rbrakk> \<Longrightarrow> tr (Suc (Max (dom tr))) = None \<and> \<not> cont v proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = None\<rbrakk> \<Longrightarrow> tr (Suc (Max (dom tr))) = None \<and> \<not> cont v
 2. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> tr (Suc (Max (dom tr))) = None \<and> \<not> cont v proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<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)); tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = None\<rbrakk> \<Longrightarrow> \<not> cont v
 2. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> tr (Suc (Max (dom tr))) = None \<and> \<not> cont v proof (prove)
goal (1 subgoal):
 1. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> tr (Suc (Max (dom tr))) = None \<and> \<not> cont v proof (prove)
goal (4 subgoals):
 1. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> dom (?m22 n a) \<subseteq> ?B23 n a
 2. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> finite (?B23 n a)
 3. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> ?m22 n a (Suc (?y27 n a)) = Some (?b22 n a)
 4. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a; Suc (?y27 n a) \<le> Max (dom (?m22 n a))\<rbrakk> \<Longrightarrow> tr (Suc (Max (dom tr))) = None \<and> \<not> cont v proof (prove)
goal (3 subgoals):
 1. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> finite {..<n}
 2. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a\<rbrakk> \<Longrightarrow> tr (Suc (?y27 n a)) = Some (?b22 n a)
 3. \<And>n a. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = None; tr (Max (dom tr)) = Some v; tr (Suc (Max (dom tr))) = Some a; Suc (?y27 n a) \<le> Max (dom tr)\<rbrakk> \<Longrightarrow> tr (Suc (Max (dom tr))) = None \<and> \<not> cont v proof (prove)
goal:
No subgoals!