theory Prefix_Refinement

lemma validI_drop_next_G:
  "\<lbrakk> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; (tr, res) \<in> f s;
        rely_cond R s0 (drop (n - m) tr); n = length tr; m < length tr \<rbrakk>
    \<Longrightarrow> fst (rev tr ! m) \<noteq> Env
        \<longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m))" apply clarify apply (drule(2) validI_GD_drop[where n="n - Suc m"]) apply (simp add: drop_sub_Suc_is_Cons) apply (rule rely_cond_Cons; simp) apply (subst(asm) guar_cond_append_split[where n=1]) apply (simp add: take_Suc Suc_diff_Suc) apply (simp add: guar_cond_def take_rev hd_drop_conv_nth
                   eq_Me_neq_Env rev_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (n - m) tr); n = length tr; m < length tr\<rbrakk> \<Longrightarrow> fst (rev tr ! m) \<noteq> Env \<longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env\<rbrakk> \<Longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env\<rbrakk> \<Longrightarrow> rely_cond R s0 (drop (n - Suc m) tr)
 2. \<lbrakk>P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env; guar_cond G s0 (drop (n - Suc m) tr)\<rbrakk> \<Longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env\<rbrakk> \<Longrightarrow> rely_cond R s0 (rev tr ! m # drop (length tr - m) tr)
 2. \<lbrakk>P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env; guar_cond G s0 (drop (n - Suc m) tr)\<rbrakk> \<Longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env; guar_cond G s0 (drop (n - Suc m) tr)\<rbrakk> \<Longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env; guar_cond G s0 (drop 1 (drop (n - Suc m) tr)) \<and> guar_cond G (last_st_tr (drop 1 (drop (n - Suc m) tr)) s0) (take 1 (drop (n - Suc m) tr))\<rbrakk> \<Longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop (length tr - m) tr); m < length tr; n = length tr; fst (rev tr ! m) \<noteq> Env; guar_cond G s0 (drop (length tr - m) tr) \<and> guar_cond G (last_st_tr (drop (length tr - m) tr) s0) [hd (drop (length tr - Suc m) tr)]\<rbrakk> \<Longrightarrow> G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m)) proof (prove)
goal:
No subgoals!