theory GraphProof

lemma trace_end_trace_drop_n_Err:
  "option_map (fst o hd) (trace_end (trace_drop_n i j tr)) = Some Err
    \<Longrightarrow> tr \<in> exec_trace Gamma f
    \<Longrightarrow> trace_drop_n i j tr \<in> exec_trace Gamma f'
    \<Longrightarrow> option_map (fst o hd) (trace_end tr) = Some Err" apply clarsimp apply (drule(1) exec_trace_end_SomeD) apply (clarsimp simp: trace_drop_n_def[THEN fun_cong] if_x_None_eq_Some
                        drop_eq_Cons rev_swap) apply (frule(1) exec_trace_Err_propagate[OF _ _ order_refl]) apply (case_tac "tl (the (tr (n + i)))" rule: rev_cases) apply (frule_tac i="n + i" in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def trace_end_exec_SomeI) apply (simp add: rev_swap) apply (frule_tac i="n + i + length (the (tr (n + i))) - 2" in exec_trace_step_cases) apply (frule_tac i="n + i + length (the (tr (n + i))) - 1" in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def trace_end_exec_SomeI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_option (fst \<circ> hd) (trace_end (trace_drop_n i j tr)) = Some Err; tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'\<rbrakk> \<Longrightarrow> map_option (fst \<circ> hd) (trace_end tr) = Some Err proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'; trace_end (trace_drop_n i j tr) = Some z; fst (hd z) = Err\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'; fst (hd z) = Err; \<exists>n. trace_drop_n i j tr n = Some z \<and> trace_drop_n i j tr (Suc n) = None \<and> (\<exists>nn st g. z = [(nn, st, g)] \<and> nn \<in> {Ret, Err})\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (1 subgoal):
 1. \<And>n st g zs. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (length zs) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # rev zs); j = length zs\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (1 subgoal):
 1. \<And>n st g zs. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (length zs) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # rev zs); j = length zs; tr (n + i + length (rev zs)) = Some (upd_stack Err id (drop (length (rev zs)) ((Err, st, g) # rev zs)))\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (2 subgoals):
 1. \<And>n st g zs. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (length zs) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # rev zs); j = length zs; tr (n + i + length (rev zs)) = Some (upd_stack Err id (drop (length (rev zs)) ((Err, st, g) # rev zs))); tl (the (tr (n + i))) = []\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err
 2. \<And>n st g zs ys y. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (length zs) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # rev zs); j = length zs; tr (n + i + length (rev zs)) = Some (upd_stack Err id (drop (length (rev zs)) ((Err, st, g) # rev zs))); tl (the (tr (n + i))) = ys @ [y]\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (2 subgoals):
 1. \<And>n st g zs. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (length zs) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # rev zs); j = length zs; tr (n + i + length (rev zs)) = Some (upd_stack Err id (drop (length (rev zs)) ((Err, st, g) # rev zs))); tl (the (tr (n + i))) = []; tr (n + i) = None \<and> tr (Suc (n + i)) = None \<or> (\<exists>state. tr (n + i) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (n + i)) = None) \<or> tr (n + i) \<noteq> None \<and> tr (Suc (n + i)) \<noteq> None \<and> (the (tr (n + i)), the (tr (Suc (n + i)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err
 2. \<And>n st g zs ys y. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (length zs) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # rev zs); j = length zs; tr (n + i + length (rev zs)) = Some (upd_stack Err id (drop (length (rev zs)) ((Err, st, g) # rev zs))); tl (the (tr (n + i))) = ys @ [y]\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (1 subgoal):
 1. \<And>n st g zs ys y. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (length zs) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (length zs) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # rev zs); j = length zs; tr (n + i + length (rev zs)) = Some (upd_stack Err id (drop (length (rev zs)) ((Err, st, g) # rev zs))); tl (the (tr (n + i))) = ys @ [y]\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (1 subgoal):
 1. \<And>n st g zs ys y. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (Suc (length ys)) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (Suc (length ys)) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (Suc (length ys)) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # ys @ [y]); j = Suc (length ys); tr (Suc (n + i + length ys)) = Some [(Err, snd y)]; zs = y # rev ys\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (1 subgoal):
 1. \<And>n st g zs ys y. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (Suc (length ys)) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (Suc (length ys)) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (Suc (length ys)) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # ys @ [y]); j = Suc (length ys); tr (Suc (n + i + length ys)) = Some [(Err, snd y)]; zs = y # rev ys; tr (n + i + length (the (tr (n + i))) - 2) = None \<and> tr (Suc (n + i + length (the (tr (n + i))) - 2)) = None \<or> (\<exists>state. tr (n + i + length (the (tr (n + i))) - 2) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (n + i + length (the (tr (n + i))) - 2)) = None) \<or> tr (n + i + length (the (tr (n + i))) - 2) \<noteq> None \<and> tr (Suc (n + i + length (the (tr (n + i))) - 2)) \<noteq> None \<and> (the (tr (n + i + length (the (tr (n + i))) - 2)), the (tr (Suc (n + i + length (the (tr (n + i))) - 2)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal (1 subgoal):
 1. \<And>n st g zs ys y. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i (Suc (length ys)) tr \<in> exec_trace Gamma f'; \<forall>j<n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (Suc (length ys)) (rev (the (tr (i + j)))))); (if \<forall>j<Suc n. (\<exists>y. tr (i + j) = Some y) \<and> continuing (rev (drop (Suc (length ys)) (rev (the (tr (i + j)))))) then map_option (rev \<circ> drop (length zs) \<circ> rev) (tr (Suc n + i)) else None) = None; tr (n + i) = Some ((Err, st, g) # ys @ [y]); j = Suc (length ys); tr (Suc (n + i + length ys)) = Some [(Err, snd y)]; zs = y # rev ys; tr (n + i + length (the (tr (n + i))) - 2) = None \<and> tr (Suc (n + i + length (the (tr (n + i))) - 2)) = None \<or> (\<exists>state. tr (n + i + length (the (tr (n + i))) - 2) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (n + i + length (the (tr (n + i))) - 2)) = None) \<or> tr (n + i + length (the (tr (n + i))) - 2) \<noteq> None \<and> tr (Suc (n + i + length (the (tr (n + i))) - 2)) \<noteq> None \<and> (the (tr (n + i + length (the (tr (n + i))) - 2)), the (tr (Suc (n + i + length (the (tr (n + i))) - 2)))) \<in> exec_graph_step Gamma; tr (n + i + length (the (tr (n + i))) - 1) = None \<and> tr (Suc (n + i + length (the (tr (n + i))) - 1)) = None \<or> (\<exists>state. tr (n + i + length (the (tr (n + i))) - 1) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (n + i + length (the (tr (n + i))) - 1)) = None) \<or> tr (n + i + length (the (tr (n + i))) - 1) \<noteq> None \<and> tr (Suc (n + i + length (the (tr (n + i))) - 1)) \<noteq> None \<and> (the (tr (n + i + length (the (tr (n + i))) - 1)), the (tr (Suc (n + i + length (the (tr (n + i))) - 1)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err proof (prove)
goal:
No subgoals!