kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_Monad

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

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

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 Trace_Monad

lemma bindE_returnOk[simp]:
  "(m >>=E returnOk) = m" by (simp add: bindE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>=E returnOk = m
theory Trace_Monad

lemma bindE_assoc:
  "(m >>=E f) >>=E g = m >>=E (\<lambda>x. f x >>=E g)" unfolding bindE_def by (fastforce simp: bind_assoc lift_def throwError_def
                split: sum.splits
                intro: arg_cong[where f="\<lambda>x. m >>= x"])

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

lemma returnOk_liftE:
  "returnOk x = liftE (return x)" by (simp add: liftE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. returnOk x = liftE (return x)
theory Trace_Monad

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 Trace_Monad

lemma "do x \<leftarrow> return 1;
          return (2::nat);
          return x
       od =
       return 1 >>=
       (\<lambda>x. return (2::nat) >>=
            K_bind (return x))" by (rule refl)

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

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 Trace_Monad

lemma "doE x \<leftarrow> returnOk 1;
           returnOk (2::nat);
           returnOk x
       odE =
       returnOk 1 >>=E
       (\<lambda>x. returnOk (2::nat) >>=E
            K_bind (returnOk x))" by (rule refl)

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

lemma last_st_tr_simps[simp]:
  "last_st_tr [] s = s"
  "last_st_tr (x # xs) s = snd x"
  "last_st_tr (tr @ tr') s = last_st_tr tr (last_st_tr tr' s)" by (simp add: last_st_tr_def hd_append)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. last_st_tr [] s = s &&& last_st_tr (x # xs) s = snd x &&& last_st_tr (tr @ tr') s = last_st_tr tr (last_st_tr tr' s)
theory Trace_Monad

lemma state_select_def2:
  "state_select r \<equiv> (do
    s \<leftarrow> get;
    S \<leftarrow> return {s'. (s, s') \<in> r};
    assert (S \<noteq> {});
    s' \<leftarrow> select S;
    put s'
  od)" apply (clarsimp simp add: state_select_def get_def return_def assert_def fail_def select_def
                            put_def bind_def fun_eq_iff default_elem_def
                    intro!: eq_reflection) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_select r \<equiv> do s <- get;
S <- return {s'. (s, s') \<in> r};
assert (S \<noteq> {});
select S >>= put
od proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (x, xa) \<in> r \<Longrightarrow> Pair [] ` Result ` Pair () ` {s'. (x, s') \<in> r} = (\<Union>x\<in>{s'. (x, s') \<in> r} \<times> {x}. case x of (rv, s) \<Rightarrow> {([], Result ((), rv))}) proof (prove)
goal:
No subgoals!
theory Trace_Monad

lemma parallel_def3:
  "parallel f g = (\<lambda>s. (\<lambda>(ys, zs, rv). (map parallel_mrg (zip ys zs), rv))
    ` {(ys, zs, rv). (ys, rv) \<in> f s \<and> (zs, rv) \<in> g s
    \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs})" by (simp add: parallel_def2, rule ext, auto simp: image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. parallel f g = (\<lambda>s. (\<lambda>(ys, zs, rv). (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs, rv)) ` {(ys, zs, rv). (ys, rv) \<in> f s \<and> (zs, rv) \<in> g s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs})
theory Trace_Lemmas

lemma in_mres:
  "(tr, Result (rv, s)) \<in> S \<Longrightarrow> (rv, s) \<in> mres S" by (fastforce simp: mres_def intro: image_eqI[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tr, Result (rv, s)) \<in> S \<Longrightarrow> (rv, s) \<in> mres S
theory Trace_Lemmas

lemma bind_apply_cong':
  "\<lbrakk>f s = f' s'; (\<forall>rv st. (rv, st) \<in> mres (f s) \<longrightarrow> g rv st = g' rv st)\<rbrakk>
   \<Longrightarrow> bind f g s = bind f' g' s'" apply (simp add: bind_def) apply (rule SUP_cong; simp?) apply (clarsimp split: tmres.split) apply (drule spec2, drule mp, erule in_mres) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f s = f' s'; \<forall>rv st. (rv, st) \<in> mres (f s) \<longrightarrow> g rv st = g' rv st\<rbrakk> \<Longrightarrow> (f >>= g) s = (f' >>= g') s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f s = f' s'; \<forall>rv st. (rv, st) \<in> mres (f' s') \<longrightarrow> g rv st = g' rv st\<rbrakk> \<Longrightarrow> (\<Union>x\<in>f' s'. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s) = (\<Union>x\<in>f' s'. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g' rv s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f s = f' s'; \<forall>rv st. (rv, st) \<in> mres (f' s') \<longrightarrow> g rv st = g' rv st; x \<in> f' s'\<rbrakk> \<Longrightarrow> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s) = (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g' rv s) proof (prove)
goal (1 subgoal):
 1. \<And>a aa ba. \<lbrakk>f s = f' s'; \<forall>rv st. (rv, st) \<in> mres (f' s') \<longrightarrow> g rv st = g' rv st; (a, Result (aa, ba)) \<in> f' s'\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (aa, x) \<Rightarrow> (aa @ a, x)) ` g aa ba = (\<lambda>x. case x of (aa, x) \<Rightarrow> (aa @ a, x)) ` g' aa ba proof (prove)
goal (1 subgoal):
 1. \<And>a aa ba. \<lbrakk>f s = f' s'; (a, Result (aa, ba)) \<in> f' s'; g aa ba = g' aa ba\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (aa, x) \<Rightarrow> (aa @ a, x)) ` g aa ba = (\<lambda>x. case x of (aa, x) \<Rightarrow> (aa @ a, x)) ` g' aa ba proof (prove)
goal:
No subgoals!
theory Trace_Lemmas

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

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

lemma bindE_cong[fundef_cong]:
  "\<lbrakk> M = M' ; \<And>v s s'. (Inr v, s') \<in> mres (M' s) \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'" by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_cong)

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

lemma bindE_apply_cong[fundef_cong]:
  "\<lbrakk> f s = f' s'; \<And>rv st. (Inr rv, st) \<in> mres (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
  \<Longrightarrow> (f >>=E g) s = (f' >>=E g') s'" by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_apply_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f s = f' s'; \<And>rv st. (Inr rv, st) \<in> mres (f' s') \<Longrightarrow> g rv st = g' rv st\<rbrakk> \<Longrightarrow> (f >>=E g) s = (f' >>=E g') s'
theory Trace_Lemmas

lemma K_bind_apply_cong[fundef_cong]:
  "\<lbrakk> f st = f' st' \<rbrakk> \<Longrightarrow> K_bind f arg st = K_bind f' arg' st'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f st = f' st' \<Longrightarrow> K_bind f arg st = K_bind f' arg' st'
theory Trace_Lemmas

lemma when_apply_cong[fundef_cong]:
  "\<lbrakk> C = C'; s = s'; C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> when C m s = when C' m' s'" by (simp add: when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C = C'; s = s'; C' \<Longrightarrow> m s' = m' s'\<rbrakk> \<Longrightarrow> when C m s = when C' m' s'
theory Trace_Lemmas

lemma unless_apply_cong[fundef_cong]:
  "\<lbrakk> C = C'; s = s'; \<not> C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> unless C m s = unless C' m' s'" by (simp add: when_def unless_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C = C'; s = s'; \<not> C' \<Longrightarrow> m s' = m' s'\<rbrakk> \<Longrightarrow> unless C m s = unless C' m' s'
theory Trace_Lemmas

lemma whenE_apply_cong[fundef_cong]:
  "\<lbrakk> C = C'; s = s'; C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> whenE C m s = whenE C' m' s'" by (simp add: whenE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C = C'; s = s'; C' \<Longrightarrow> m s' = m' s'\<rbrakk> \<Longrightarrow> whenE C m s = whenE C' m' s'
theory Trace_Lemmas

lemma nested_bind[simp]:
  "do x <- do y <- f; return (g y) od; h x od = do y <- f; h (g y) od" by (fastforce simp: bind_def return_def split: tmres.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do y <- f;
return (g y)
od >>= h = do y <- f;
h (g y)
od
theory Trace_Lemmas

lemma bind_dummy_ret_val:
  "do y \<leftarrow> a; b od = do a; b od" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do y <- a;
b
od = do a;
b
od
theory Trace_Lemmas

lemma fail_update[iff]:
  "fail (f s) = fail s" by (simp add: fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fail (f s) = fail s
theory Trace_Lemmas

lemma fail_bind[simp]:
  "fail >>= f = fail" by (simp add: bind_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fail >>= f = fail
theory Trace_Lemmas

lemma fail_bindE[simp]:
  "fail >>=E f = fail" by (simp add: bindE_def bind_def fail_def)

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

lemma assert_A_False[simp]:
  "assert False = fail" by (simp add: assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert False = fail
theory Trace_Lemmas

lemma assert_A_True[simp]:
  "assert True = return ()" by (simp add: assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert True = return ()
theory Trace_Lemmas

lemma assert_False[simp]:
  "assert False >>= f = fail" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert False >>= f = fail
theory Trace_Lemmas

lemma assertE_False[simp]:
  "assertE False >>=E f = fail" by (simp add: assertE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assertE False >>=E f = fail
theory Trace_Lemmas

lemma assertE_True[simp]:
  "assertE True >>=E f = f ()" by (simp add: assertE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assertE True >>=E f = f ()
theory Trace_Lemmas

lemma when_False_bind[simp]:
  "when False g >>= f = f ()" by (rule ext) (simp add: when_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. when False g >>= f = f ()
theory Trace_Lemmas

lemma when_True_bind[simp]:
  "when True g >>= f = g >>= f" by (simp add: when_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. when True g >>= f = g >>= f
theory Trace_Lemmas

lemma whenE_False_bind[simp]:
  "whenE False g >>=E f = f ()" by (simp add: whenE_def bindE_def returnOk_def lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whenE False g >>=E f = f ()
theory Trace_Lemmas

lemma whenE_True_bind[simp]:
  "whenE True g >>=E f = g >>=E f" by (simp add: whenE_def bindE_def returnOk_def lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whenE True g >>=E f = g >>=E f
theory Trace_Lemmas

lemma when_True[simp]:
  "when True X = X" by (clarsimp simp: when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. when True X = X
theory Trace_Lemmas

lemma when_False[simp]:
  "when False X = return ()" by (clarsimp simp: when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. when False X = return ()
theory Trace_Lemmas

lemma unless_False[simp]:
  "unless False X = X" by (clarsimp simp: unless_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unless False X = X
theory Trace_Lemmas

lemma unlessE_False[simp]:
  "unlessE False f = f" unfolding unlessE_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unlessE False f = f proof (prove)
goal (1 subgoal):
 1. (if False then returnOk () else f) = f
theory Trace_Lemmas

lemma unless_True[simp]:
  "unless True X = return ()" by (clarsimp simp: unless_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unless True X = return ()
theory Trace_Lemmas

lemma unlessE_True[simp]:
  "unlessE True f = returnOk ()" unfolding unlessE_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unlessE True f = returnOk () proof (prove)
goal (1 subgoal):
 1. (if True then returnOk () else f) = returnOk ()
theory Trace_Lemmas

lemma unlessE_whenE:
  "unlessE P = whenE (\<not>P)" by (rule ext) (simp add: unlessE_def whenE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unlessE P = whenE (\<not> P)
theory Trace_Lemmas

lemma unless_when:
  "unless P = when (\<not>P)" by (rule ext) (simp add: unless_def when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unless P = when (\<not> P)
theory Trace_Lemmas

lemma assert_opt_Some:
  "assert_opt (Some x) = return x" by (simp add: assert_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert_opt (Some x) = return x
theory Trace_Lemmas

lemma assertE_liftE:
  "assertE P = liftE (assert P)" by (simp add: assertE_def assert_def liftE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assertE P = liftE (assert P)
theory Trace_Lemmas

lemma liftE_handleE'[simp]:
  "(liftE a <handle2> b) = liftE a" by (clarsimp simp: liftE_def handleE'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE a <handle2> b) = liftE a
theory Trace_Lemmas

lemma liftE_handleE[simp]:
  "(liftE a <handle> b) = liftE a" unfolding handleE_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE a <handle> b) = liftE a proof (prove)
goal (1 subgoal):
 1. (liftE a <handle2> b) = liftE a
theory Trace_Lemmas

lemma alternative_bind:
  "((a \<sqinter> b) >>= c) = ((a >>= c) \<sqinter> (b >>= c))" by (fastforce simp add: alternative_def bind_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<sqinter> b) >>= c = (a >>= c \<sqinter> b >>= c)
theory Trace_Lemmas

lemma alternative_refl:
  "(a \<sqinter> a) = a" by (simp add: alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<sqinter> a) = a
theory Trace_Lemmas

lemma alternative_com:
  "(f \<sqinter> g) = (g \<sqinter> f)" by (auto simp: alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> g) = (g \<sqinter> f)
theory Trace_Lemmas

lemma liftE_alternative:
  "liftE (a \<sqinter> b) = (liftE a \<sqinter> liftE b)" by (simp add: liftE_def alternative_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (a \<sqinter> b) = (liftE a \<sqinter> liftE b)
theory Trace_Lemmas

lemma liftE_liftM:
  "liftE = liftM Inr" by (auto simp: liftE_def liftM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE = liftM Inr
theory Trace_Lemmas

lemma liftME_liftM:
  "liftME f = liftM (case_sum Inl (Inr \<circ> f))" unfolding liftME_def liftM_def bindE_def returnOk_def lift_def apply (rule ext) apply (rule arg_cong[where f="bind m" for m]) apply (fastforce simp: throwError_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftME f = liftM (case_sum Inl (Inr \<circ> f)) proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. m >>= case_sum throwError (\<lambda>x. (return \<circ> Inr) (f x))) = (\<lambda>m. do x <- m;
return (case x of Inl x \<Rightarrow> Inl x | Inr x \<Rightarrow> (Inr \<circ> f) x)
od) proof (prove)
goal (1 subgoal):
 1. \<And>m. m >>= case_sum throwError (\<lambda>x. (return \<circ> Inr) (f x)) = do x <- m;
return (case x of Inl x \<Rightarrow> Inl x | Inr x \<Rightarrow> (Inr \<circ> f) x)
od proof (prove)
goal (1 subgoal):
 1. \<And>m. case_sum throwError (\<lambda>x. (return \<circ> Inr) (f x)) = (\<lambda>x. return (case x of Inl x \<Rightarrow> Inl x | Inr x \<Rightarrow> (Inr \<circ> f) x)) proof (prove)
goal:
No subgoals!
theory Trace_Lemmas

lemma liftE_bindE:
  "liftE a >>=E b = a >>= b" by (simp add: liftE_def bindE_def lift_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE a >>=E b = a >>= b
theory Trace_Lemmas

lemma liftM_id[simp]:
  "liftM id = id" by (auto simp: liftM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftM id = id
theory Trace_Lemmas

lemma gets_bind_ign:
  "gets f >>= (\<lambda>x. m) = m" by (simp add: bind_def simpler_gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- gets f;
m
od = m
theory Trace_Lemmas

lemma exec_get:
  "(get >>= f) x = f x x" by (simp add: get_def bind_def)

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

lemma exec_gets:
  "(gets f >>= m) s = m (f s) s" by (simp add: simpler_gets_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (gets f >>= m) s = m (f s) s
theory Trace_Lemmas

lemma bind_eqI:
  "\<lbrakk> f = f'; \<And>x. g x = g' x \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" by (auto simp: bind_def split_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 Trace_Lemmas

lemma condition_split:
  "P (condition C a b s) \<longleftrightarrow> (C s \<longrightarrow> P (a s)) \<and> (\<not>C s \<longrightarrow> P (b s))" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (condition C
  a
  b s) = ((C s \<longrightarrow> P (a s)) \<and> (\<not> C s \<longrightarrow> P (b s)))
theory Trace_Lemmas

lemma condition_split_asm:
  "P (condition C a b s) \<longleftrightarrow> (\<not>(C s \<and> \<not> P (a s) \<or> \<not>C s \<and> \<not>P (b s)))" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (condition C
  a
  b s) = (\<not> (C s \<and> \<not> P (a s) \<or> \<not> C s \<and> \<not> P (b s)))
theory Trace_Lemmas

lemma condition_true_triv[simp]:
  "condition (\<lambda>_. True) A B = A" by (fastforce split: condition_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition (\<lambda>_. True)
  A
  B = A
theory Trace_Lemmas

lemma condition_false_triv[simp]:
  "condition (\<lambda>_. False) A B = B" by (fastforce split: condition_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition (\<lambda>_. False)
  A
  B = B
theory Trace_Lemmas

lemma condition_true:
  "P s \<Longrightarrow> condition P A B s = A s" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> condition P
  A
  B s = A s
theory Trace_Lemmas

lemma condition_false:
  "\<not> P s \<Longrightarrow> condition P A B s = B s" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> P s \<Longrightarrow> condition P
  A
  B s = B s
theory Trace_In_Monad

lemma in_throwError:
  "((v, s') \<in> mres (throwError e s)) = (v = Inl e \<and> s' = s)" by (simp add: throwError_def return_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> mres (throwError e s)) = (v = Inl e \<and> s' = s)
theory Trace_In_Monad

lemma in_bind:
  "((r,s') \<in> mres ((do x \<leftarrow> f; g x od) s)) =
   (\<exists>s'' x. (x, s'') \<in> mres (f s) \<and> (r, s') \<in> mres (g x s''))" by (force simp: bind_def split_def mres_def split: tmres.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres ((f >>= g) s)) = (\<exists>s'' x. (x, s'') \<in> mres (f s) \<and> (r, s') \<in> mres (g x s''))
theory Trace_In_Monad

lemma in_bindE_L:
  "((Inl r, s') \<in> mres ((doE x \<leftarrow> f; g x odE) s)) \<Longrightarrow>
   (\<exists>s'' x. (Inr x, s'') \<in> mres (f s) \<and> (Inl r, s') \<in> mres (g x s'')) \<or> ((Inl r, s') \<in> mres (f s))" by (simp add: bindE_def in_bind)
     (force simp: return_def throwError_def lift_def split_def mres_def split: sum.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Inl r, s') \<in> mres ((f >>=E g) s) \<Longrightarrow> (\<exists>s'' x. (Inr x, s'') \<in> mres (f s) \<and> (Inl r, s') \<in> mres (g x s'')) \<or> (Inl r, s') \<in> mres (f s)
theory Trace_In_Monad

lemma in_return:
  "(r, s') \<in> mres (return v s) = (r = v \<and> s' = s)" by (simp add: return_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (return v s)) = (r = v \<and> s' = s)
theory Trace_In_Monad

lemma in_liftE:
  "((v, s') \<in> mres (liftE f s)) = (\<exists>v'. v = Inr v' \<and> (v', s') \<in> mres (f s))" by (force simp: liftE_def in_bind in_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> mres (liftE f s)) = (\<exists>v'. v = Inr v' \<and> (v', s') \<in> mres (f s))
theory Trace_In_Monad

lemma in_whenE:
  "((v, s') \<in> mres (whenE P f s)) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (\<not>P \<longrightarrow> v = Inr () \<and> s' = s))" by (simp add: whenE_def in_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> mres (whenE P f s)) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (\<not> P \<longrightarrow> v = Inr () \<and> s' = s))
theory Trace_In_Monad

lemma inr_in_unlessE_throwError[termination_simp]:
  "(Inr (), s') \<in> mres (unlessE P (throwError E) s) = (P \<and> s'=s)" by (simp add: unlessE_def returnOk_def throwError_def in_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Inr (), s') \<in> mres (unlessE P (throwError E) s)) = (P \<and> s' = s)
theory Trace_In_Monad

lemma in_fail:
  "r \<in> mres (fail s) = False" by (simp add: fail_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r \<in> mres (fail s)) = False
theory Trace_In_Monad

lemma in_assert:
  "(r, s') \<in> mres (assert P s) = (P \<and> s' = s)" by (simp add: assert_def return_def fail_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (assert P s)) = (P \<and> s' = s)