theory Trace_RG

lemma bindE_twp[wp_split]:
  "\<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>,\<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<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 >>=E (\<lambda>r. g r) \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (simp add: bindE_def validIE_def) apply (erule bind_twp[rotated]) apply (clarsimp simp: lift_def throwError_def split: sum.splits) apply (subst validI_valid_no_trace_eq) apply wpsimp+ 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>E\<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 >>=E g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q' r s0 s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f >>= lift g \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r. (\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s0 s. case r of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q' r s0 s\<rbrace>, \<lbrace>R\<rbrace> lift g r \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1. (\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace>) \<Longrightarrow> \<lbrace>E x1\<rbrace>, \<lbrace>R\<rbrace> return (Inl x1) \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. (\<forall>x1. v = Inl x1 \<longrightarrow> E x1 s0 s) \<and> (\<forall>x2. v = Inr x2 \<longrightarrow> Q x2 s0 s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. (\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace>) \<Longrightarrow> no_trace (return (Inl x1))
 2. \<And>x1. (\<And>r. \<lbrace>Q' r\<rbrace>, \<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace>) \<Longrightarrow> \<forall>s0. \<lbrace>E x1 s0\<rbrace> return (Inl x1) \<lbrace>\<lambda>v s. (\<forall>x1. v = Inl x1 \<longrightarrow> E x1 s0 s) \<and> (\<forall>x2. v = Inr x2 \<longrightarrow> Q x2 s0 s)\<rbrace> proof (prove)
goal:
No subgoals!