theory Trace_RG

lemma catch_twp:
  "\<lbrakk> \<And>x. \<lbrace>E x\<rbrace>,\<lbrace>R\<rbrace> handler x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> catch f handler \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding validI_def validIE_def apply (rule conjI, clarsimp) unfolding catch_def return_def rely_def bind_def apply (fastforce simp: rely_cond_append guar_cond_append
                 split: sum.splits tmres.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>E x\<rbrace>, \<lbrace>R\<rbrace> handler x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f <catch> handler \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. prefix_closed (handler x) \<and> (\<forall>s0 s tr res. E x s0 s \<and> (tr, res) \<in> rely (handler x) 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')); prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q r (last_st_tr tr s0) s')))\<rbrakk> \<Longrightarrow> prefix_closed (f <catch> handler) \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely (f <catch> handler) 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>x. prefix_closed (handler x) \<and> (\<forall>s0 s tr res. E x s0 s \<and> (tr, res) \<in> rely (handler x) 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')); prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q r (last_st_tr tr s0) s')))\<rbrakk> \<Longrightarrow> \<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely (f <catch> handler) 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>x. prefix_closed (handler x) \<and> (\<forall>s0 s tr res. E x s0 s \<and> (tr, res) \<in> handler x s \<inter> Collect (rely_cond R s0) \<times> UNIV \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')); prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> f s \<inter> Collect (rely_cond R s0) \<times> UNIV \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q r (last_st_tr tr s0) s')))\<rbrakk> \<Longrightarrow> \<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> (\<Union>(xs, y)\<in>f s. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` (case rv of Inl x \<Rightarrow> handler x | Inr b \<Rightarrow> \<lambda>s. {([], Result (b, s))}) s) y) \<inter> Collect (rely_cond R s0) \<times> UNIV \<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:
No subgoals!