theory GraphLangLemmas

lemma trace_None_dom_eq:
  "tr n = None \<Longrightarrow> tr \<in> nat_trace_rel cont R
    \<Longrightarrow> (\<exists>n'. n' \<le> n \<and> dom tr = {..< n'})" apply (cases "\<forall>i. tr i = None") apply (rule_tac x=0 in exI) apply (simp add: fun_eq_iff) apply clarsimp apply (rule_tac x="Suc (Max (dom tr))" in exI) apply (drule(1) nat_trace_Max_dom_None[rotated, simplified, OF exI]) apply clarsimp apply (frule(1) trace_None_dom_subset) apply (rule conjI) apply auto[1] apply (rule equalityI) apply (auto simp: less_Suc_eq_le intro!: Max_ge elim: finite_subset)[1] apply (clarsimp, rule ccontr, clarsimp simp: less_Suc_eq_le) apply (drule(1) trace_None_dom_subset)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R\<rbrakk> \<Longrightarrow> \<exists>n'\<le>n. dom tr = {..<n'} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; \<forall>i. tr i = None\<rbrakk> \<Longrightarrow> \<exists>n'\<le>n. dom tr = {..<n'}
 2. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; \<not> (\<forall>i. tr i = None)\<rbrakk> \<Longrightarrow> \<exists>n'\<le>n. dom tr = {..<n'} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; \<forall>i. tr i = None\<rbrakk> \<Longrightarrow> 0 \<le> n \<and> dom tr = {..<0}
 2. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; \<not> (\<forall>i. tr i = None)\<rbrakk> \<Longrightarrow> \<exists>n'\<le>n. dom tr = {..<n'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; \<not> (\<forall>i. tr i = None)\<rbrakk> \<Longrightarrow> \<exists>n'\<le>n. dom tr = {..<n'} proof (prove)
goal (1 subgoal):
 1. \<And>i y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr i = Some y\<rbrakk> \<Longrightarrow> \<exists>n'\<le>n. dom tr = {..<n'} proof (prove)
goal (1 subgoal):
 1. \<And>i y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr i = Some y\<rbrakk> \<Longrightarrow> Suc (Max (dom tr)) \<le> n \<and> dom tr = {..<Suc (Max (dom tr))} proof (prove)
goal (1 subgoal):
 1. \<And>i y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; \<exists>y. tr (Max (dom tr)) = Some y\<rbrakk> \<Longrightarrow> Suc (Max (dom tr)) \<le> n \<and> dom tr = {..<Suc (Max (dom tr))} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y\<rbrakk> \<Longrightarrow> Suc (Max (dom tr)) \<le> n \<and> dom tr = {..<Suc (Max (dom tr))} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> Suc (Max (dom tr)) \<le> n \<and> dom tr = {..<Suc (Max (dom tr))} proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> Suc (Max (dom tr)) \<le> n
 2. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> dom tr = {..<Suc (Max (dom tr))} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> dom tr = {..<Suc (Max (dom tr))} proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> dom tr \<subseteq> {..<Suc (Max (dom tr))}
 2. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> {..<Suc (Max (dom tr))} \<subseteq> dom tr proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> {..<Suc (Max (dom tr))} \<subseteq> dom tr proof (prove)
goal (1 subgoal):
 1. \<And>y x. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}; x \<le> Max (dom tr); tr x = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y x. \<lbrakk>tr \<in> nat_trace_rel cont R; tr (Max (dom tr)) = Some y; dom tr \<subseteq> {..<n}; x \<le> Max (dom tr); dom tr \<subseteq> {..<n}; dom tr \<subseteq> {..<x}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!