theory GraphLang

lemma relpow_nat_trace:
  "((s, s') \<in> r ^^ n) = (\<exists>tr \<in> nat_trace_rel (\<lambda>x. False) r. tr 0 = Some s
    \<and> tr n = Some s' \<and> tr (Suc n) = None)" apply (simp add: relpow_fun_conv, safe) apply (rule_tac x="\<lambda>x. if x < Suc n then Some (f x) else None" in bexI) apply simp apply (simp add: nat_trace_rel_def) apply (rule_tac x="the o tr" in exI) apply (frule(1) nat_trace_rel_Some_range[where n=n]) apply (clarsimp simp: nat_trace_rel_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((s, s') \<in> r ^^ n) = (\<exists>tr\<in>nat_trace_rel (\<lambda>x. False) r. tr 0 = Some s \<and> tr n = Some s' \<and> tr (Suc n) = None) proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>s = f 0; \<forall>i<n. (f i, f (Suc i)) \<in> r; s' = f n\<rbrakk> \<Longrightarrow> \<exists>tr\<in>nat_trace_rel (\<lambda>x. False) r. tr 0 = Some (f 0) \<and> tr n = Some (f n) \<and> tr (Suc n) = None
 2. \<And>tr. \<lbrakk>tr \<in> nat_trace_rel (\<lambda>x. False) r; tr 0 = Some s; tr n = Some s'; tr (Suc n) = None\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = s \<and> f n = s' \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> r) proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrakk>s = f 0; \<forall>i<n. (f i, f (Suc i)) \<in> r; s' = f n\<rbrakk> \<Longrightarrow> (if 0 < Suc n then Some (f 0) else None) = Some (f 0) \<and> (if n < Suc n then Some (f n) else None) = Some (f n) \<and> (if Suc n < Suc n then Some (f (Suc n)) else None) = None
 2. \<And>f. \<lbrakk>s = f 0; \<forall>i<n. (f i, f (Suc i)) \<in> r; s' = f n\<rbrakk> \<Longrightarrow> (\<lambda>x. if x < Suc n then Some (f x) else None) \<in> nat_trace_rel (\<lambda>x. False) r
 3. \<And>tr. \<lbrakk>tr \<in> nat_trace_rel (\<lambda>x. False) r; tr 0 = Some s; tr n = Some s'; tr (Suc n) = None\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = s \<and> f n = s' \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> r) proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>s = f 0; \<forall>i<n. (f i, f (Suc i)) \<in> r; s' = f n\<rbrakk> \<Longrightarrow> (\<lambda>x. if x < Suc n then Some (f x) else None) \<in> nat_trace_rel (\<lambda>x. False) r
 2. \<And>tr. \<lbrakk>tr \<in> nat_trace_rel (\<lambda>x. False) r; tr 0 = Some s; tr n = Some s'; tr (Suc n) = None\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = s \<and> f n = s' \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> r) proof (prove)
goal (1 subgoal):
 1. \<And>tr. \<lbrakk>tr \<in> nat_trace_rel (\<lambda>x. False) r; tr 0 = Some s; tr n = Some s'; tr (Suc n) = None\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = s \<and> f n = s' \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> r) proof (prove)
goal (1 subgoal):
 1. \<And>tr. \<lbrakk>tr \<in> nat_trace_rel (\<lambda>x. False) r; tr 0 = Some s; tr n = Some s'; tr (Suc n) = None\<rbrakk> \<Longrightarrow> (the \<circ> tr) 0 = s \<and> (the \<circ> tr) n = s' \<and> (\<forall>i<n. ((the \<circ> tr) i, (the \<circ> tr) (Suc i)) \<in> r) proof (prove)
goal (1 subgoal):
 1. \<And>tr. \<lbrakk>tr \<in> nat_trace_rel (\<lambda>x. False) r; tr 0 = Some s; tr n = Some s'; tr (Suc n) = None; \<forall>i\<le>n. \<exists>v'. tr i = Some v'\<rbrakk> \<Longrightarrow> (the \<circ> tr) 0 = s \<and> (the \<circ> tr) n = s' \<and> (\<forall>i<n. ((the \<circ> tr) i, (the \<circ> tr) (Suc i)) \<in> r) proof (prove)
goal:
No subgoals!