theory Trace_RG

lemma bind_twp[wp_split]:
  "\<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>,\<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= (\<lambda>rv. g rv) \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (subst validI_def, rule conjI) apply (blast intro: prefix_closed_bind validI_prefix_closed) apply (clarsimp simp: bind_def rely_def) apply (drule(2) validI_D) apply (clarsimp simp: rely_cond_append split: tmres.split_asm) apply (clarsimp split: tmres.split_asm) apply (drule meta_spec, frule(2) validI_D) apply (clarsimp simp: rely_cond_append split: if_split_asm) apply (clarsimp simp: guar_cond_append) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f >>= g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> prefix_closed (f >>= g)
 2. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely (f >>= g) R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely (f >>= g) R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res a b. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>; P s0 s; rely_cond R s0 tr; (a, b) \<in> f s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(aa, y). (aa @ a, y)) ` g rv s)\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr res a b. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; rely_cond R s0 tr; (a, b) \<in> f s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(aa, y). (aa @ a, y)) ` g rv s)\<rbrakk> \<Longrightarrow> rely_cond R s0 a
 2. \<And>s0 s tr res a b. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; rely_cond R s0 tr; (a, b) \<in> f s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(aa, y). (aa @ a, y)) ` g rv s); guar_cond G s0 a \<and> (\<forall>rv s'. b = Result (rv, s') \<longrightarrow> Q' rv (last_st_tr a s0) s')\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res a b. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; rely_cond R s0 tr; (a, b) \<in> f s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(aa, y). (aa @ a, y)) ` g rv s); guar_cond G s0 a \<and> (\<forall>rv s'. b = Result (rv, s') \<longrightarrow> Q' rv (last_st_tr a s0) s')\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s a aa ba ab bb. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; rely_cond R s0 (ab @ a); (a, Result (aa, ba)) \<in> f s; guar_cond G s0 a; Q' aa (last_st_tr a s0) ba; (ab, bb) \<in> g aa ba\<rbrakk> \<Longrightarrow> guar_cond G s0 (ab @ a) \<and> (\<forall>rv s'. bb = Result (rv, s') \<longrightarrow> Q rv (last_st_tr ab (last_st_tr a s0)) s') proof (prove)
goal (2 subgoals):
 1. \<And>s0 s a aa ba ab bb. \<lbrakk>P s0 s; rely_cond R s0 (ab @ a); (a, Result (aa, ba)) \<in> f s; guar_cond G s0 a; Q' aa (last_st_tr a s0) ba; (ab, bb) \<in> g aa ba; \<lbrace>Q' aa\<rbrace>, \<lbrace>R\<rbrace> g aa \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> rely_cond R (last_st_tr a s0) ab
 2. \<And>s0 s a aa ba ab bb. \<lbrakk>P s0 s; rely_cond R s0 (ab @ a); (a, Result (aa, ba)) \<in> f s; guar_cond G s0 a; Q' aa (last_st_tr a s0) ba; (ab, bb) \<in> g aa ba; \<lbrace>Q' aa\<rbrace>, \<lbrace>R\<rbrace> g aa \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; guar_cond G (last_st_tr a s0) ab \<and> (\<forall>rv s'. bb = Result (rv, s') \<longrightarrow> Q rv (last_st_tr ab (last_st_tr a s0)) s')\<rbrakk> \<Longrightarrow> guar_cond G s0 (ab @ a) \<and> (\<forall>rv s'. bb = Result (rv, s') \<longrightarrow> Q rv (last_st_tr ab (last_st_tr a s0)) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s a aa ba ab bb. \<lbrakk>P s0 s; rely_cond R s0 (ab @ a); (a, Result (aa, ba)) \<in> f s; guar_cond G s0 a; Q' aa (last_st_tr a s0) ba; (ab, bb) \<in> g aa ba; \<lbrace>Q' aa\<rbrace>, \<lbrace>R\<rbrace> g aa \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; guar_cond G (last_st_tr a s0) ab \<and> (\<forall>rv s'. bb = Result (rv, s') \<longrightarrow> Q rv (last_st_tr ab (last_st_tr a s0)) s')\<rbrakk> \<Longrightarrow> guar_cond G s0 (ab @ a) \<and> (\<forall>rv s'. bb = Result (rv, s') \<longrightarrow> Q rv (last_st_tr ab (last_st_tr a s0)) s') proof (prove)
goal:
No subgoals!