theory SpecValid_R

lemma split_spec_bindE[wp_split]:
  assumes x: "\<And>rv s''. (Inr rv, s'') \<in> fst (f s') \<Longrightarrow> s'' \<turnstile> \<lbrace>B rv\<rbrace> g rv \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>"
  shows "s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>
   \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" apply (clarsimp simp: spec_validE_def validE_def valid_def bind_def bindE_def lift_def split_def) apply (case_tac a) apply (clarsimp simp add: throwError_def return_def) apply (erule(1) my_BallE, simp) apply clarsimp apply (erule(1) my_BallE, simp) apply (drule x) apply (clarsimp simp: spec_validE_def validE_def valid_def split_def) apply (erule(1) my_BallE, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>A s'; (a, b) \<in> fst (f s'); (aa, ba) \<in> fst ((case a of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) b); \<forall>x\<in>fst (f s'). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> B r (snd x)\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab. \<lbrakk>A s'; (a, b) \<in> fst (f s'); (aa, ba) \<in> fst ((case a of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) b); \<forall>x\<in>fst (f s'). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> B r (snd x); a = Inl ab\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba))
 2. \<And>a b aa ba bb. \<lbrakk>A s'; (a, b) \<in> fst (f s'); (aa, ba) \<in> fst ((case a of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) b); \<forall>x\<in>fst (f s'). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> B r (snd x); a = Inr bb\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal (2 subgoals):
 1. \<And>b ab. \<lbrakk>A s'; (Inl ab, b) \<in> fst (f s'); \<forall>x\<in>fst (f s'). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> B r (snd x)\<rbrakk> \<Longrightarrow> E ab b
 2. \<And>a b aa ba bb. \<lbrakk>A s'; (a, b) \<in> fst (f s'); (aa, ba) \<in> fst ((case a of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) b); \<forall>x\<in>fst (f s'). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> B r (snd x); a = Inr bb\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba bb. \<lbrakk>A s'; (a, b) \<in> fst (f s'); (aa, ba) \<in> fst ((case a of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) b); \<forall>x\<in>fst (f s'). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> B r (snd x); a = Inr bb\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba bb. \<lbrakk>A s'; (Inr bb, b) \<in> fst (f s'); (aa, ba) \<in> fst (g bb b); \<forall>x\<in>fst (f s'). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> B r (snd x)\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba bb. \<lbrakk>A s'; (Inr bb, b) \<in> fst (f s'); (aa, ba) \<in> fst (g bb b); B bb b\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba bb. \<lbrakk>A s'; (aa, ba) \<in> fst (g bb b); B bb b; b \<turnstile> \<lbrace>B bb\<rbrace> g bb \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba bb. \<lbrakk>A s'; (aa, ba) \<in> fst (g bb b); B bb b; \<forall>x\<in>fst (g bb b). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> C r (snd x)\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> E e (snd (aa, ba)) | Inr r \<Rightarrow> C r (snd (aa, ba)) proof (prove)
goal:
No subgoals!