kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_More_RG

lemma validIE_case_prod:
  "\<lbrakk> \<And>x y. validIE (P x y) R (f x y) G Q E \<rbrakk> \<Longrightarrow> validIE (case_prod P v) R (case_prod (\<lambda>x y. f x y) v) G Q E" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrace>P x y\<rbrace>, \<lbrace>R\<rbrace> f x y \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>case v of (x, xa) \<Rightarrow> P x xa\<rbrace>, \<lbrace>R\<rbrace> case v of (x, y) \<Rightarrow> f x y \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_More_RG

lemma rg_validIE_E_conjI:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<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 \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s0 s. E rv s0 s \<and> E' rv s0 s\<rbrace>" by (fastforce simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<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 \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv s0 s. E rv s0 s \<and> E' rv s0 s\<rbrace>
theory Trace_More_RG

lemma validIE_R_post_conjD2:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r s0 s. Q r s0 s \<and> Q' r s0 s\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>r s0 s. Q r s0 s \<and> Q' r s0 s\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_More_RG

lemma rg_name_pre_state2:
  "(\<And>s. \<lbrace>\<lambda>s0' s'. P s0' s' \<and> (s' = s)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (auto simp: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrace>\<lambda>s0' s'. P s0' s' \<and> s' = s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory StateMonad

lemma return_bind [simp]: "(return x >>= f) = f x" by (simp add: return_def bind_def runState_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. return x >>= f = f x
theory StateMonad

lemma bind_return [simp]: "(m >>= return) = m" unfolding bind_def return_def runState_def by (simp add: Let_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= return = m proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. let (v, s') = m s in (v, s')) = m
theory StateMonad

lemma bind_assoc:
  fixes m :: "('s,'a) state_monad"
  fixes f :: "'a \<Rightarrow> ('s,'b) state_monad"
  fixes g :: "'b \<Rightarrow> ('s,'c) state_monad"
  shows "(m >>= f) >>= g  =  m >>= (\<lambda>x. f x >>= g)" unfolding bind_def by (clarsimp simp add: Let_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= f >>= g = m >>= (\<lambda>x. f x >>= g) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. let (v, s') = let (x, y) = m s in f x y in g v s') = (\<lambda>s. let (v, s') = m s; (x, y) = f v s' in g x y)
theory StateMonad

lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x" unfolding bindE_def return_def returnOk_def by (clarsimp simp: lift_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. returnOk x >>=E f = f x proof (prove)
goal (1 subgoal):
 1. (Pair \<circ> Inr) x >>= lift f = f x
theory StateMonad

lemma lift_return [simp]:
  "lift (return \<circ> Inr) = return" by (auto simp: lift_def throwError_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift (return \<circ> Inr) = return
theory StateMonad

lemma bindE_assoc:
  shows "(m >>=E f) >>=E g  =  m >>=E (\<lambda>x. f x >>=E g)" by (auto simp: Let_def bindE_def bind_def lift_def split_def runState_def throwError_def return_def
           split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>=E f >>=E g = m >>=E (\<lambda>x. f x >>=E g)
theory StateMonad

lemma throwError_bindE [simp]:
  "throwError E >>=E f = throwError E" by (simp add: bindE_def bind_def throwError_def lift_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throwError E >>=E f = throwError E
theory StateMonad

lemma "do x \<leftarrow> return 1; return 2; return x od = return 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- return (1::'b);
return (2::'c);
   return x
od = return (1::'b)
theory StateMonad

lemma "doE x \<leftarrow> returnOk 1; returnOk 2; returnOk x odE = returnOk 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE x <- returnOk (1::'c);
returnOk (2::'d);
    returnOk x
odE = returnOk (1::'c)
theory StateMonad

lemma isSkip_bindI: "\<lbrakk> isSkip f; \<And>x. isSkip (g x) \<rbrakk> \<Longrightarrow> isSkip (f >>= g)" apply (clarsimp simp: isSkip_def bind_def Let_def) apply (erule_tac x=s in allE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isSkip f; \<And>x. isSkip (g x)\<rbrakk> \<Longrightarrow> isSkip (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. \<exists>r. f s = (r, s); \<And>x. \<forall>s. \<exists>r. g x s = (r, s)\<rbrakk> \<Longrightarrow> \<exists>r. (case f s of (x, xa) \<Rightarrow> g x xa) = (r, s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. \<forall>s. \<exists>r. g x s = (r, s); \<exists>r. f s = (r, s)\<rbrakk> \<Longrightarrow> \<exists>r. (case f s of (x, xa) \<Rightarrow> g x xa) = (r, s) proof (prove)
goal:
No subgoals!
theory StateMonad

lemma isSkip_gets [simp,intro!]:
  "isSkip (gets x)" by (simp add: isSkip_def gets_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isSkip (gets x)
theory StateMonad

lemma isSkip_liftE [iff]: "isSkip (liftE f) = isSkip f" apply (simp add: isSkip_def liftE_def Let_def split_def) apply rule apply clarsimp apply (case_tac "f s") apply (erule_tac x = s in allE) apply simp apply clarsimp apply (case_tac "f s") apply (erule_tac x = s in allE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isSkip (liftE f) = isSkip f proof (prove)
goal (1 subgoal):
 1. (\<forall>s. snd (f s) = s) = (\<forall>s. \<exists>r. f s = (r, s)) proof (prove)
goal (2 subgoals):
 1. \<forall>s. snd (f s) = s \<Longrightarrow> \<forall>s. \<exists>r. f s = (r, s)
 2. \<forall>s. \<exists>r. f s = (r, s) \<Longrightarrow> \<forall>s. snd (f s) = s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>s. snd (f s) = s \<Longrightarrow> \<exists>r. f s = (r, s)
 2. \<forall>s. \<exists>r. f s = (r, s) \<Longrightarrow> \<forall>s. snd (f s) = s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<forall>s. snd (f s) = s; f s = (a, b)\<rbrakk> \<Longrightarrow> \<exists>r. f s = (r, s)
 2. \<forall>s. \<exists>r. f s = (r, s) \<Longrightarrow> \<forall>s. snd (f s) = s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>f s = (a, b); snd (f s) = s\<rbrakk> \<Longrightarrow> \<exists>r. f s = (r, s)
 2. \<forall>s. \<exists>r. f s = (r, s) \<Longrightarrow> \<forall>s. snd (f s) = s proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<exists>r. f s = (r, s) \<Longrightarrow> \<forall>s. snd (f s) = s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>s. \<exists>r. f s = (r, s) \<Longrightarrow> snd (f s) = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. \<exists>r. f s = (r, s); f s = (a, b)\<rbrakk> \<Longrightarrow> snd (f s) = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>f s = (a, b); \<exists>r. f s = (r, s)\<rbrakk> \<Longrightarrow> snd (f s) = s proof (prove)
goal:
No subgoals!
theory StateMonad

lemma isSkip_liftI [simp, intro!]:
  "\<lbrakk> \<And>y. x = Inr y \<Longrightarrow> isSkip (f y) \<rbrakk> \<Longrightarrow> isSkip (lift f x)" by (simp add: lift_def throwError_def return_def isSkip_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y. x = Inr y \<Longrightarrow> isSkip (f y)) \<Longrightarrow> isSkip (lift f x)
theory StateMonad

lemma isSkip_Error [iff]:
  "isSkip (throwError x)" by (simp add: throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isSkip (throwError x)
theory StateMonad

lemma isSkip_throw_opt [iff]:
  "isSkip (throw_opt e x)" by (simp add: throw_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isSkip (throw_opt e x)
theory StateMonad

lemma nested_bind [simp]:
  "do x <- do y <- f; return (g y) od; h x od =
   do y <- f; h (g y) od" apply (clarsimp simp add: bind_def) apply (rule ext) apply (clarsimp simp add: Let_def split_def runState_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do y <- f;
   return (g y)
od >>= h = do y <- f;
   h (g y)
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. case case f s of (v, x) \<Rightarrow> return (g v) x of (x, xa) \<Rightarrow> h x xa) = (\<lambda>s. case f s of (v, x) \<Rightarrow> h (g v) x) proof (prove)
goal (1 subgoal):
 1. \<And>s. (case case f s of (v, x) \<Rightarrow> return (g v) x of (x, xa) \<Rightarrow> h x xa) = (case f s of (v, x) \<Rightarrow> h (g v) x) proof (prove)
goal:
No subgoals!
theory StateMonad

lemma skip_bind:
  "isSkip s \<Longrightarrow> do _ \<leftarrow> s; g od = g" apply (clarsimp simp add: bind_def) apply (rule ext) apply (clarsimp simp add: isSkip_def Let_def) apply (erule_tac x=sa in allE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isSkip s \<Longrightarrow> do _ <- s;
   g
od = g proof (prove)
goal (1 subgoal):
 1. isSkip s \<Longrightarrow> (\<lambda>sa. case s sa of (v, x) \<Rightarrow> g x) = g proof (prove)
goal (1 subgoal):
 1. \<And>sa. isSkip s \<Longrightarrow> (case s sa of (v, x) \<Rightarrow> g x) = g sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<forall>sa. \<exists>r. s sa = (r, sa) \<Longrightarrow> (case s sa of (v, x) \<Rightarrow> g x) = g sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<exists>r. s sa = (r, sa) \<Longrightarrow> (case s sa of (v, x) \<Rightarrow> g x) = g sa proof (prove)
goal:
No subgoals!
theory StateMonad

lemma bind_eqI:
  "\<lbrakk> f = f'; \<And>x. g x = g' x \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" by (simp add: bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = f'; \<And>x. g x = g' x\<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'
theory StateMonad

lemma bind_cong [fundef_cong]:
  "\<lbrakk> f = f'; \<And>v s s'. f' s = (v, s') \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" by (simp add: bind_def Let_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = f'; \<And>v s s'. f' s = (v, s') \<Longrightarrow> g v s' = g' v s'\<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'
theory StateMonad

lemma bind'_cong [fundef_cong]:
  "\<lbrakk> f = f'; \<And>v s s'. f' s = (v, s') \<Longrightarrow> g s' = g' s' \<rbrakk> \<Longrightarrow> bind' f g = bind' f' g'" by (auto intro: bind_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = f'; \<And>v s s'. f' s = (v, s') \<Longrightarrow> g s' = g' s'\<rbrakk> \<Longrightarrow> do f;
   g
od = do f';
   g'
od
theory StateMonad

lemma bindE_cong[fundef_cong]:
  "\<lbrakk> M = M' ; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'" apply (simp add: bindE_def) apply (rule bind_cong) apply (rule refl) apply (unfold lift_def) apply (case_tac v, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M = M'; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s'\<rbrakk> \<Longrightarrow> M >>=E N = M' >>=E N' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M = M'; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s'\<rbrakk> \<Longrightarrow> M' >>= lift N = M' >>= lift N' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>M = M'; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s'\<rbrakk> \<Longrightarrow> M' = M'
 2. \<And>v s s'. \<lbrakk>M = M'; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s'; M' s = (v, s')\<rbrakk> \<Longrightarrow> lift N v s' = lift N' v s' proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. \<lbrakk>M = M'; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s'; M' s = (v, s')\<rbrakk> \<Longrightarrow> lift N v s' = lift N' v s' proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. \<lbrakk>M = M'; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s'; M' s = (v, s')\<rbrakk> \<Longrightarrow> (case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> N v') s' = (case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> N' v') s' proof (prove)
goal:
No subgoals!
theory StateMonad

lemma bindE'_cong[fundef_cong]:
  "\<lbrakk> M = M' ; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N s' = N' s' \<rbrakk> \<Longrightarrow> bindE' M N = bindE' M' N'" by (auto intro: bindE_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M = M'; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N s' = N' s'\<rbrakk> \<Longrightarrow> doE M;
    N
odE = doE M';
    N'
odE
theory StateMonad

lemma validE_def2:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> \<equiv> \<lbrace>P\<rbrace> f \<lbrace> \<lambda>r s. case r of Inr b \<Rightarrow> Q b s | Inl a \<Rightarrow> R a s \<rbrace>" by (unfold valid_def validE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> \<equiv> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl a \<Rightarrow> R a s | Inr b \<Rightarrow> Q b s\<rbrace>
theory StateMonad

lemma pred_lift_taut[simp]: "\<guillemotleft>\<top>,\<top>\<guillemotright> = \<top>\<top>" by (simp add:pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>\<lambda>_. True,\<lambda>_. True\<guillemotright> = (\<lambda>_ _. True)
theory StateMonad

lemma pred_lift_cont_l[simp]: "\<guillemotleft>\<bottom>,x\<guillemotright> = \<bottom>\<bottom>" by (simp add:pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>\<lambda>_. False,x\<guillemotright> = (\<lambda>_ _. False)
theory StateMonad

lemma pred_liftI[intro!]: "\<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> \<guillemotleft>P,Q\<guillemotright> x y" by (simp add:pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> \<guillemotleft>P,Q\<guillemotright> x y
theory StateMonad

lemma pred_exact_split:
  "\<guillemotleft>P,Q\<guillemotright> = (\<guillemotleft>P,\<top>\<guillemotright> and \<guillemotleft>\<top>,Q\<guillemotright>)" by (simp add:pred_lift_exact_def pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>P,Q\<guillemotright> = (\<guillemotleft>P,\<lambda>_. True\<guillemotright> and \<guillemotleft>\<lambda>_. True,Q\<guillemotright>)
theory StateMonad

lemma pred_lift_add[simp]: "\<guillemotleft>P,Q\<guillemotright> x = ((\<lambda>s. P x) and Q)" by (simp add:pred_lift_exact_def pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>P,Q\<guillemotright> x = ((\<lambda>s. P x) and Q)
theory StateMonad

lemma seq':
  "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>;
     \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>;
     \<forall>x s. B x s \<longrightarrow> P x \<and> C s \<rbrakk> \<Longrightarrow>
   \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" apply (clarsimp simp: valid_def runState_def bind_def Let_def split_def) apply (case_tac "f s") apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<forall>x s. B x s \<longrightarrow> P x \<and> C s\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. A s \<longrightarrow> B (fst (f s)) (snd (f s)); \<forall>x. P x \<longrightarrow> (\<forall>s. C s \<longrightarrow> D (fst (g x s)) (snd (g x s))); \<forall>x s. B x s \<longrightarrow> P x \<and> C s; A s\<rbrakk> \<Longrightarrow> D (fst (g (fst (f s)) (snd (f s)))) (snd (g (fst (f s)) (snd (f s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. A s \<longrightarrow> B (fst (f s)) (snd (f s)); \<forall>x. P x \<longrightarrow> (\<forall>s. C s \<longrightarrow> D (fst (g x s)) (snd (g x s))); \<forall>x s. B x s \<longrightarrow> P x \<and> C s; A s; f s = (a, b)\<rbrakk> \<Longrightarrow> D (fst (g (fst (f s)) (snd (f s)))) (snd (g (fst (f s)) (snd (f s)))) proof (prove)
goal:
No subgoals!
theory StateMonad

lemma seq:
  assumes "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>"
  assumes "\<And>x. P x \<Longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>"
  assumes "\<And>x s. B x s \<Longrightarrow> P x \<and> C s"
  shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" using assms by (blast intro: seq')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace> proof (prove)
using this:
\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>
P ?x \<Longrightarrow> \<lbrace>C\<rbrace> g ?x \<lbrace>D\<rbrace>
B ?x ?s \<Longrightarrow> P ?x \<and> C ?s

goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace>
theory StateMonad

lemma seq_invar_nobind:
  assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>"
  assumes g_valid: "\<And>x. \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>"
  shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>" apply(rule_tac B="\<guillemotleft>\<top>,A\<guillemotright>" and C="A" and P="\<top>" in seq) apply(insert f_valid g_valid) apply(simp_all add:pred_lift_exact_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>
 2. \<And>x. True \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>
 3. \<And>x s. \<guillemotleft>\<lambda>_. True,A\<guillemotright> x s \<Longrightarrow> True \<and> A s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>; \<And>x. \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>
 2. \<And>x. \<lbrakk>True; \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>; \<And>x. \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>
 3. \<And>x s. \<lbrakk>\<guillemotleft>\<lambda>_. True,A\<guillemotright> x s; \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>; \<And>x. \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>\<rbrakk> \<Longrightarrow> True \<and> A s proof (prove)
goal:
No subgoals!
theory StateMonad

lemma seq_invar_bind:
  assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>B,A\<guillemotright>\<rbrace>"
  assumes g_valid: "\<And>x. P x \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>"
  assumes bind: "\<And>x. B x \<Longrightarrow> P x"
  shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>" apply(rule_tac B="\<guillemotleft>B,A\<guillemotright>" and C="A" and P="P" in seq) apply(insert f_valid g_valid bind) apply(simp_all add: pred_lift_exact_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>B,A\<guillemotright>\<rbrace>
 2. \<And>x. P x \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>
 3. \<And>x s. \<guillemotleft>B,A\<guillemotright> x s \<Longrightarrow> P x \<and> A s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>B,A\<guillemotright>\<rbrace>; \<And>x. P x \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>; \<And>x. B x \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>B,A\<guillemotright>\<rbrace>
 2. \<And>x. \<lbrakk>P x; \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>B,A\<guillemotright>\<rbrace>; \<And>x. P x \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>; \<And>x. B x \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>
 3. \<And>x s. \<lbrakk>\<guillemotleft>B,A\<guillemotright> x s; \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>B,A\<guillemotright>\<rbrace>; \<And>x. P x \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<lambda>_. True,A\<guillemotright>\<rbrace>; \<And>x. B x \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P x \<and> A s proof (prove)
goal:
No subgoals!
theory StateMonad

lemma seq_noimp:
  assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>C,B\<guillemotright>\<rbrace>"
  assumes g_valid: "\<And>x. C x \<Longrightarrow> \<lbrace>B\<rbrace> g x \<lbrace>D\<rbrace>"
  shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" apply(rule_tac B="\<guillemotleft>C,B\<guillemotright>" and C="B" and P="C" in seq) apply(insert f_valid g_valid, simp_all add:pred_lift_exact_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>C,B\<guillemotright>\<rbrace>
 2. \<And>x. C x \<Longrightarrow> \<lbrace>B\<rbrace> g x \<lbrace>D\<rbrace>
 3. \<And>x s. \<guillemotleft>C,B\<guillemotright> x s \<Longrightarrow> C x \<and> B s proof (prove)
goal:
No subgoals!
theory StateMonad

lemma seq_ext':
  "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" by (clarsimp simp: valid_def runState_def bind_def Let_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace>