theory GraphProof

lemma exec_trace_Err_propagate:
  "tr \<in> exec_trace Gamma f
    \<Longrightarrow> tr i = Some ((Err, st, fname) # xs)
    \<Longrightarrow> j \<le> length xs \<Longrightarrow> tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs)))" apply (induct j arbitrary: xs) apply simp apply atomize apply clarsimp apply (cut_tac xs="drop j ((Err, st, fname) # xs)" in neq_Nil_conv) apply clarsimp apply (frule_tac i="i + j" in exec_trace_step_cases) apply (auto simp: exec_graph_step_def drop_eq_Cons Cons_eq_append_conv
                 split: list.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); j \<le> length xs\<rbrakk> \<Longrightarrow> tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs))) proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); 0 \<le> length xs\<rbrakk> \<Longrightarrow> tr (i + 0) = Some (upd_stack Err id (drop 0 ((Err, st, fname) # xs)))
 2. \<And>j xs. \<lbrakk>\<And>xs. \<lbrakk>tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); j \<le> length xs\<rbrakk> \<Longrightarrow> tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs))); tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); Suc j \<le> length xs\<rbrakk> \<Longrightarrow> tr (i + Suc j) = Some (upd_stack Err id (drop (Suc j) ((Err, st, fname) # xs))) proof (prove)
goal (1 subgoal):
 1. \<And>j xs. \<lbrakk>\<And>xs. \<lbrakk>tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); j \<le> length xs\<rbrakk> \<Longrightarrow> tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs))); tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); Suc j \<le> length xs\<rbrakk> \<Longrightarrow> tr (i + Suc j) = Some (upd_stack Err id (drop (Suc j) ((Err, st, fname) # xs))) proof (prove)
goal (1 subgoal):
 1. \<And>j xs. \<lbrakk>\<forall>xs. tr \<in> exec_trace Gamma f \<longrightarrow> tr i = Some ((Err, st, fname) # xs) \<longrightarrow> j \<le> length xs \<longrightarrow> tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs))); tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); Suc j \<le> length xs\<rbrakk> \<Longrightarrow> tr (i + Suc j) = Some (upd_stack Err id (drop (Suc j) ((Err, st, fname) # xs))) proof (prove)
goal (1 subgoal):
 1. \<And>j xs. \<lbrakk>tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs))); tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); Suc j \<le> length xs\<rbrakk> \<Longrightarrow> tr (Suc (i + j)) = Some (upd_stack Err id (drop j xs)) proof (prove)
goal (1 subgoal):
 1. \<And>j xs. \<lbrakk>tr (i + j) = Some (upd_stack Err id (drop j ((Err, st, fname) # xs))); tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); Suc j \<le> length xs; (drop j ((Err, st, fname) # xs) \<noteq> []) = (\<exists>y ys. drop j ((Err, st, fname) # xs) = y # ys)\<rbrakk> \<Longrightarrow> tr (Suc (i + j)) = Some (upd_stack Err id (drop j xs)) proof (prove)
goal (1 subgoal):
 1. \<And>j xs a aa b ys. \<lbrakk>tr (i + j) = Some ((Err, aa, b) # ys); tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); Suc j \<le> length xs; drop j ((Err, st, fname) # xs) = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> tr (Suc (i + j)) = Some (upd_stack Err id (drop j xs)) proof (prove)
goal (1 subgoal):
 1. \<And>j xs a aa b ys. \<lbrakk>tr (i + j) = Some ((Err, aa, b) # ys); tr \<in> exec_trace Gamma f; tr i = Some ((Err, st, fname) # xs); Suc j \<le> length xs; drop j ((Err, st, fname) # xs) = (a, aa, b) # ys; tr (i + j) = None \<and> tr (Suc (i + j)) = None \<or> (\<exists>state. tr (i + j) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (i + j)) = None) \<or> tr (i + j) \<noteq> None \<and> tr (Suc (i + j)) \<noteq> None \<and> (the (tr (i + j)), the (tr (Suc (i + j)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> tr (Suc (i + j)) = Some (upd_stack Err id (drop j xs)) proof (prove)
goal:
No subgoals!