theory GraphLangLemmas

lemma exec_trace_step_cases:
  assumes exec: "tr \<in> exec_trace Gamma gf"
  shows "((tr i = None \<and> tr (Suc i) = None))
        \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None)
        \<or> (tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma)" using exec exec_trace_Nil[OF exec] apply (clarsimp simp: exec_trace_def nat_trace_rel_def continuing_def Ball_def) apply (drule_tac x=i in spec)+ apply (auto split: list.split_asm option.split_asm prod.split_asm next_node.split_asm)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tr i = None \<and> tr (Suc i) = None \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) \<or> tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma proof (prove)
using this:
tr \<in> exec_trace Gamma gf
tr ?i \<noteq> Some []

goal (1 subgoal):
 1. tr i = None \<and> tr (Suc i) = None \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) \<or> tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma proof (prove)
goal (1 subgoal):
 1. \<And>gfa st. \<lbrakk>\<And>i. tr i \<noteq> Some []; Gamma gf = Some gfa; \<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> exec_graph_step Gamma) \<and> ((\<exists>y. tr n = Some y) \<and> (case the (tr n) of [] \<Rightarrow> False | [(NextNode x, xa, xb)] \<Rightarrow> True | (NextNode x, xa, xb) # _ \<Rightarrow> True | [(_, b)] \<Rightarrow> False | (_, b) # a # lista \<Rightarrow> True) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); tr 0 = Some [(NextNode (entry_point gfa), st, gf)]; (\<exists>y. tr i = Some y) \<or> (\<exists>y. tr (Suc i) = Some y); tr i = None \<or> tr (Suc i) = None \<or> (the (tr i), the (tr (Suc i))) \<notin> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>aa b. tr i = Some [(a, aa, b)]) \<and> (a = Ret \<or> a = Err) \<and> tr (Suc i) = None proof (prove)
goal (1 subgoal):
 1. \<And>gfa st. \<lbrakk>\<And>i. tr i \<noteq> Some []; Gamma gf = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), st, gf)]; (\<exists>y. tr i = Some y) \<or> (\<exists>y. tr (Suc i) = Some y); tr i = None \<or> tr (Suc i) = None \<or> (the (tr i), the (tr (Suc i))) \<notin> exec_graph_step Gamma; (tr i = None \<longrightarrow> tr (Suc i) = None) \<and> ((\<exists>y. tr (Suc i) = Some y) \<longrightarrow> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. tr i = Some y) \<and> (case the (tr i) of [] \<Rightarrow> False | [(NextNode x, xa, xb)] \<Rightarrow> True | (NextNode x, xa, xb) # _ \<Rightarrow> True | [(_, b)] \<Rightarrow> False | (_, b) # a # lista \<Rightarrow> True) \<longrightarrow> (\<exists>y. tr (Suc i) = Some y))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>aa b. tr i = Some [(a, aa, b)]) \<and> (a = Ret \<or> a = Err) \<and> tr (Suc i) = None proof (prove)
goal:
No subgoals!