kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_MonadEq_Lemmas

lemma in_catch[monad_eq]:
  "(r, t) \<in> fst ((M <catch> E) s)
     = ((Inr r, t) \<in> fst (M s) \<or> (\<exists>r' s'. ((Inl r', s') \<in> fst (M s)) \<and> (r, t) \<in> fst (E r' s')))" apply (rule iffI; clarsimp simp: catch_def in_bind in_return split: sum.splits) apply (metis sumE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, t) \<in> fst ((M <catch> E) s)) = ((Inr r, t) \<in> fst (M s) \<or> (\<exists>r' s'. (Inl r', s') \<in> fst (M s) \<and> (r, t) \<in> fst (E r' s'))) proof (prove)
goal (2 subgoals):
 1. \<And>s'' x. \<lbrakk>\<forall>x1. x = Inl x1 \<longrightarrow> (Inl x1, s'') \<in> fst (M s) \<and> (r, t) \<in> fst (E x1 s''); \<forall>x2. x = Inr x2 \<longrightarrow> r = x2 \<and> (Inr x2, s'') \<in> fst (M s) \<and> t = s''; \<forall>r' s'. (Inl r', s') \<in> fst (M s) \<longrightarrow> (r, t) \<notin> fst (E r' s')\<rbrakk> \<Longrightarrow> (Inr r, t) \<in> fst (M s)
 2. (Inr r, t) \<in> fst (M s) \<or> (\<exists>r' s'. (Inl r', s') \<in> fst (M s) \<and> (r, t) \<in> fst (E r' s')) \<Longrightarrow> \<exists>s'' x. (\<forall>x1. x = Inl x1 \<longrightarrow> (Inl x1, s'') \<in> fst (M s) \<and> (r, t) \<in> fst (E x1 s'')) \<and> (\<forall>x2. x = Inr x2 \<longrightarrow> (Inr x2, s'') \<in> fst (M s) \<and> r = x2 \<and> t = s'') proof (prove)
goal (1 subgoal):
 1. (Inr r, t) \<in> fst (M s) \<or> (\<exists>r' s'. (Inl r', s') \<in> fst (M s) \<and> (r, t) \<in> fst (E r' s')) \<Longrightarrow> \<exists>s'' x. (\<forall>x1. x = Inl x1 \<longrightarrow> (Inl x1, s'') \<in> fst (M s) \<and> (r, t) \<in> fst (E x1 s'')) \<and> (\<forall>x2. x = Inr x2 \<longrightarrow> (Inr x2, s'') \<in> fst (M s) \<and> r = x2 \<and> t = s'') proof (prove)
goal:
No subgoals!
theory Nondet_MonadEq_Lemmas

lemma snd_catch[monad_eq]:
  "snd ((M <catch> E) s)
     = (snd (M s) \<or> (\<exists>r' s'. ((Inl r', s') \<in> fst (M s)) \<and> snd (E r' s')))" by (force simp: catch_def snd_bind snd_return split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd ((M <catch> E) s) = (snd (M s) \<or> (\<exists>r' s'. (Inl r', s') \<in> fst (M s) \<and> snd (E r' s')))
theory Nondet_MonadEq_Lemmas

lemma returnOk_cong:
  "\<lbrakk> \<And>s. B a s = B' a s \<rbrakk> \<Longrightarrow> ((returnOk a) >>=E B) = ((returnOk a) >>=E B')" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. B a s = B' a s) \<Longrightarrow> returnOk a >>=E B = returnOk a >>=E B'
theory Nondet_MonadEq_Lemmas

lemma in_state_assert [monad_eq, simp]:
  "(rv, s') \<in> fst (state_assert P s) = (rv = () \<and> s' = s \<and> P s)" by (monad_eq simp: state_assert_def)
     metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> fst (state_assert P s)) = (rv = () \<and> s' = s \<and> P s)
theory Nondet_MonadEq_Lemmas

lemma snd_state_assert[monad_eq]:
  "snd (state_assert P s) = (\<not> P s)" by (monad_eq simp: state_assert_def Bex_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (state_assert P s) = (\<not> P s)
theory Nondet_MonadEq_Lemmas

lemma in_select[monad_eq]:
  "(rv, s') \<in> fst (select S s) = (s' = s \<and> rv \<in> S)" by (fastforce simp: select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> fst (select S s)) = (s' = s \<and> rv \<in> S)
theory Nondet_MonadEq_Lemmas

lemma snd_select[monad_eq]:
  "\<not> snd (select S s)" by (clarsimp simp: select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd (select S s)
theory Nondet_MonadEq_Lemmas

lemma snd_put[monad_eq]:
  "\<not> snd (put t s)" by (clarsimp simp: put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd (put t s)
theory Nondet_MonadEq_Lemmas

lemma snd_modify[monad_eq]:
  "\<not> snd (modify t s)" by (clarsimp simp: modify_def put_def get_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd (modify t s)
theory Nondet_MonadEq_Lemmas

lemma snd_gets_the[monad_eq]:
  "snd (gets_the X s) = (X s = None)" by (monad_eq simp: gets_the_def gets_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (gets_the X s) = (X s = None)
theory Nondet_Monad_Equations

lemma assert_def2:
  "assert v = assert_opt (if v then Some () else None)" by (cases v; simp add: assert_def assert_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert v = assert_opt (if v then Some () else None)
theory Nondet_Monad_Equations

lemma return_returnOk:
  "return (Inr x) = returnOk x" unfolding returnOk_def by simp

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

lemma exec_modify:
  "(modify f >>= g) s = g () (f s)" by (simp add: bind_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (modify f >>= g) s = g () (f s)
theory Nondet_Monad_Equations

lemma bind_return_eq:
  "(a >>= return) = (b >>= return) \<Longrightarrow> a = b" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a >>= return = b >>= return \<Longrightarrow> a = b
theory Nondet_Monad_Equations

lemma bindE_bind_linearise:
  "((f >>=E g) >>= h) =
   (f >>= case_sum (h o Inl) (\<lambda>rv. g rv >>= h))" apply (simp add: bindE_def bind_assoc) apply (rule ext, rule bind_apply_cong, rule refl) apply (simp add: lift_def throwError_def split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f >>=E g >>= h = f >>= case_sum (h \<circ> Inl) (\<lambda>rv. g rv >>= h) proof (prove)
goal (1 subgoal):
 1. do x <- f;
lift g x >>= h
od = f >>= case_sum (h \<circ> Inl) (\<lambda>rv. g rv >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>x rv st. (rv, st) \<in> fst (f x) \<Longrightarrow> (lift g rv >>= h) st = (case rv of Inl x \<Rightarrow> (h \<circ> Inl) x | Inr rv \<Rightarrow> g rv >>= h) st proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma throwError_bind:
  "(throwError e >>= f) = (f (Inl e))" by (simp add: throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throwError e >>= f = f (Inl e)
theory Nondet_Monad_Equations

lemma bind_bindE_assoc:
  "((f >>= g) >>=E h)
   = f >>= (\<lambda>rv. g rv >>=E h)" by (simp add: bindE_def bind_assoc)

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

lemma liftE_bind:
  "(liftE m >>= m') = (m >>= (\<lambda>rv. m' (Inr rv)))" by (simp add: liftE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE m >>= m' = do rv <- m;
m' (Inr rv)
od
theory Nondet_Monad_Equations

lemma catch_throwError: "catch (throwError ft) g = g ft" by (simp add: catch_def throwError_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (throwError ft <catch> g) = g ft
theory Nondet_Monad_Equations

lemma cart_singleton_image:
  "S \<times> {s} = (\<lambda>v. (v, s)) ` S" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<times> {s} = (\<lambda>v. (v, s)) ` S
theory Nondet_Monad_Equations

lemma select_bind_eq2:
  "\<lbrakk> v = v'; \<And>x. x \<in> fst v \<Longrightarrow> f x s = g x s' \<rbrakk> \<Longrightarrow>
    (select_f v >>= f) s = (select_f v' >>= g) s'" by (simp add: select_f_def bind_def split_def
                cart_singleton_image image_image
          cong: image_cong)

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

lemma select_f_singleton_return:
  "select_f ({v}, False) = return v" by (simp add: select_f_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f ({v}, False) = return v
theory Nondet_Monad_Equations

lemma select_f_returns:
  "select_f (return v s) = return (v, s)"
  "select_f (get s) = return (s, s)"
  "select_f (gets f s) = return (f s, s)"
  "select_f (modify g s) = return ((), g s)" by (simp add: select_f_def return_def get_def
                simpler_gets_def simpler_modify_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (select_f (return v s) = return (v, s) &&& select_f (get s) = return (s, s)) &&& select_f (gets f s) = return (f s, s) &&& select_f (modify g s) = return ((), g s)
theory Nondet_Monad_Equations

lemma select_eq_select_f:
  "select S = select_f (S, False)" by (simp add: select_def select_f_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select S = select_f (S, False)
theory Nondet_Monad_Equations

lemma select_f_select_f:
  "select_f (select_f v s) = liftM (swp Pair s) (select_f v)" apply (rule ext) apply (simp add: select_f_def liftM_def swp_def
                   bind_def return_def split_def
                   image_image image_constant_conv) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f (select_f v s) = liftM (swp Pair s) (select_f v) proof (prove)
goal (1 subgoal):
 1. \<And>x. select_f (select_f v s) x = liftM (swp Pair s) (select_f v) x proof (prove)
goal (1 subgoal):
 1. \<And>x. fst v \<noteq> {} \<longrightarrow> (fst v \<times> {s}) \<times> {x} = (\<Union>x\<in>fst v \<times> {x}. {((fst x, s), snd x)}) proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma select_f_select:
  "select_f (select S s) = liftM (swp Pair s) (select S)" unfolding select_eq_select_f by (rule select_f_select_f)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f (select S s) = liftM (swp Pair s) (select S) proof (prove)
goal (1 subgoal):
 1. select_f (select_f (S, False) s) = liftM (swp Pair s) (select_f (S, False))
theory Nondet_Monad_Equations

lemma select_f_asserts:
  "select_f (fail s) = fail"
  "select_f (assert P s) = do assert P; return ((), s) od"
  "select_f (assert_opt v s) = do v' \<leftarrow> assert_opt v; return (v', s) od" by (simp add: select_f_def fail_def assert_def return_def bind_def
                assert_opt_def split: if_split option.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f (fail s) = fail &&& select_f (assert P s) = do assert P;
return ((), s)
od &&& select_f (assert_opt v s) = do v' <- assert_opt v;
return (v', s)
od
theory Nondet_Monad_Equations

lemma liftE_bindE_handle:
  "((liftE f >>=E (\<lambda>x. g x)) <handle> h)
   = f >>= (\<lambda>x. g x <handle> h)" by (simp add: liftE_bindE handleE_def handleE'_def
                bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE f >>=E g <handle> h) = do x <- f;
g x <handle> h
od
theory Nondet_Monad_Equations

lemma catch_liftE_bindE:
  "catch (liftE g >>=E (\<lambda>x. f x)) h = g >>= (\<lambda>x. catch (f x) h)" by (simp add: liftE_bindE catch_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE g >>=E f <catch> h) = do x <- g;
f x <catch> h
od
theory Nondet_Monad_Equations

lemma returnOk_catch_bind:
  "catch (returnOk v) h >>= g = g v" by (simp add: returnOk_liftE catch_liftE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (returnOk v <catch> h) >>= g = g v
theory Nondet_Monad_Equations

lemma liftE_bindE_assoc:
  "(liftE f >>=E g) >>= h = f >>= (\<lambda>x. g x >>= h)" by (simp add: liftE_bindE bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE f >>=E g >>= h = do x <- f;
g x >>= h
od
theory Nondet_Monad_Equations

lemma unlessE_throw_catch_If:
  "catch (unlessE P (throwError e) >>=E f) g
   = (if P then catch (f ()) g else g e)" by (simp add: unlessE_def catch_throwError split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (unlessE P (throwError e) >>=E f <catch> g) = (if P then f () <catch> g else g e)
theory Nondet_Monad_Equations

lemma whenE_bindE_throwError_to_if:
  "whenE P (throwError e) >>=E (\<lambda>_. b) = (if P then (throwError e) else b)" unfolding whenE_def bindE_def by (auto simp: lift_def throwError_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE _ <- whenE P (throwError e);
b
odE = (if P then throwError e else b) proof (prove)
goal (1 subgoal):
 1. (if P then throwError e else returnOk ()) >>= lift (\<lambda>_. b) = (if P then throwError e else b)
theory Nondet_Monad_Equations

lemma alternative_liftE_returnOk:
  "(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)" by (simp add: liftE_def alternative_def returnOk_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)
theory Nondet_Monad_Equations

lemma alternative_left_readonly_bind:
  "\<lbrakk> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {} \<rbrakk>
   \<Longrightarrow> alternative (f >>= (\<lambda>x. g x)) h s
       = (f >>= (\<lambda>x. alternative (g x) h)) s" apply (subgoal_tac "\<forall>x \<in> fst (f s). snd x = s") apply (clarsimp simp: alternative_def bind_def split_def) apply fastforce apply clarsimp apply (drule(1) use_valid, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {}\<rbrakk> \<Longrightarrow> (f >>= g \<sqinter> h) s = (do x <- f;
g x \<sqinter> h
od) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {}; \<forall>x\<in>fst (f s). snd x = s\<rbrakk> \<Longrightarrow> (f >>= g \<sqinter> h) s = (do x <- f;
g x \<sqinter> h
od) s
 2. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). snd x = s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {}; \<forall>x\<in>fst (f s). snd x = s\<rbrakk> \<Longrightarrow> ((\<exists>x\<in>fst (f s). snd (g (fst x) s)) \<or> snd (f s) \<or> snd (h s)) = ((\<exists>x\<in>fst (f s). snd (g (fst x) s) \<or> snd (h s)) \<or> snd (f s))
 2. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). snd x = s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). snd x = s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {}; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> b = s proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma gets_the_return:
  "(return x = gets_the f) = (\<forall>s. f s = Some x)" apply (subst fun_eq_iff) apply (simp add: return_def gets_the_def exec_gets
                   assert_opt_def fail_def
            split: option.split) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (return x = gets_the f) = (\<forall>s. f s = Some x) proof (prove)
goal (1 subgoal):
 1. (\<forall>xa. return x xa = gets_the f xa) = (\<forall>s. f s = Some x) proof (prove)
goal (1 subgoal):
 1. (\<forall>xa. (\<exists>y. f xa = Some y) \<and> (\<forall>x2. f xa = Some x2 \<longrightarrow> x = x2)) = (\<forall>s. f s = Some x) proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma gets_the_returns:
  "(return x = gets_the f) = (\<forall>s. f s = Some x)"
  "(returnOk x = gets_the g) = (\<forall>s. g s = Some (Inr x))"
  "(throwError x = gets_the h) = (\<forall>s. h s = Some (Inl x))" by (simp_all add: returnOk_def throwError_def
                    gets_the_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (return x = gets_the f) = (\<forall>s. f s = Some x) &&& (returnOk x = gets_the g) = (\<forall>s. g s = Some (Inr x)) &&& (throwError x = gets_the h) = (\<forall>s. h s = Some (Inl x))
theory Nondet_Monad_Equations

lemma gets_the_eq_bind:
  "\<lbrakk> f = gets_the (fn_f o fn'); \<And>rv. g rv = gets_the (fn_g rv o fn') \<rbrakk>
   \<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')" apply clarsimp apply (rule exI[where x="\<lambda>s. case (fn_f s) of None \<Rightarrow> None | Some v \<Rightarrow> fn_g v s"]) apply (simp add: gets_the_def bind_assoc exec_gets
                   assert_opt_def fun_eq_iff
            split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = gets_the (fn_f \<circ> fn'); \<And>rv. g rv = gets_the (fn_g rv \<circ> fn')\<rbrakk> \<Longrightarrow> \<exists>fn. f >>= g = gets_the (fn \<circ> fn') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = gets_the (fn_f \<circ> fn'); \<And>rv. g rv = gets_the (fn_g rv \<circ> fn')\<rbrakk> \<Longrightarrow> \<exists>fn. gets_the (fn_f \<circ> fn') >>= g = gets_the (fn \<circ> fn') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = gets_the (fn_f \<circ> fn'); \<And>rv. g rv = gets_the (fn_g rv \<circ> fn')\<rbrakk> \<Longrightarrow> gets_the (fn_f \<circ> fn') >>= g = gets_the ((\<lambda>s. case fn_f s of None \<Rightarrow> None | Some v \<Rightarrow> fn_g v s) \<circ> fn') proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma gets_the_eq_bindE:
  "\<lbrakk> f = gets_the (fn_f o fn'); \<And>rv. g rv = gets_the (fn_g rv o fn') \<rbrakk>
   \<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')" unfolding bindE_def apply (erule gets_the_eq_bind[where fn_g="\<lambda>rv s. case rv of Inl e \<Rightarrow> Some (Inl e) | Inr v \<Rightarrow> fn_g v s"]) apply (simp add: lift_def gets_the_returns split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = gets_the (fn_f \<circ> fn'); \<And>rv. g rv = gets_the (fn_g rv \<circ> fn')\<rbrakk> \<Longrightarrow> \<exists>fn. f >>=E g = gets_the (fn \<circ> fn') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = gets_the (fn_f \<circ> fn'); \<And>rv. g rv = gets_the (fn_g rv \<circ> fn')\<rbrakk> \<Longrightarrow> \<exists>fn. f >>= lift g = gets_the (fn \<circ> fn') proof (prove)
goal (1 subgoal):
 1. \<And>rv. (\<And>rv. g rv = gets_the (fn_g rv \<circ> fn')) \<Longrightarrow> lift g rv = gets_the ((\<lambda>s. case rv of Inl e \<Rightarrow> Some (Inl e) | Inr v \<Rightarrow> fn_g v s) \<circ> fn') proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma gets_the_fail:
  "(fail = gets_the f) = (\<forall>s. f s = None)" by (simp add: gets_the_def exec_gets assert_opt_def
                fail_def return_def fun_eq_iff
         split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fail = gets_the f) = (\<forall>s. f s = None)
theory Nondet_Monad_Equations

lemma gets_the_asserts:
  "(fail = gets_the f) = (\<forall>s. f s = None)"
  "(assert P = gets_the g) = (\<forall>s. g s = (if P then Some () else None))"
  "(assertE P = gets_the h) = (\<forall>s. h s = (if P then Some (Inr ()) else None))" by (simp add: assert_def assertE_def gets_the_fail gets_the_returns
         split: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fail = gets_the f) = (\<forall>s. f s = None) &&& (assert P = gets_the g) = (\<forall>s. g s = (if P then Some () else None)) &&& (assertE P = gets_the h) = (\<forall>s. h s = (if P then Some (Inr ()) else None))
theory Nondet_Monad_Equations

lemma ex_const_function:
  "\<exists>f. \<forall>s. f (f' s) = v" by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>f. \<forall>s. f (f' s) = v
theory Nondet_Monad_Equations

lemma gets_the_condsE:
  "(\<exists>fn. whenE P f = gets_the (fn o fn'))
   = (P \<longrightarrow> (\<exists>fn. f = gets_the (fn o fn')))"
  "(\<exists>fn. unlessE P g = gets_the (fn o fn'))
   = (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn o fn')))" by (simp add: whenE_def unlessE_def gets_the_returns ex_const_function
         split: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>fn. whenE P f = gets_the (fn \<circ> fn')) = (P \<longrightarrow> (\<exists>fn. f = gets_the (fn \<circ> fn'))) &&& (\<exists>fn. unlessE P g = gets_the (fn \<circ> fn')) = (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn \<circ> fn')))
theory Nondet_Monad_Equations

lemma let_into_return:
  "(let f = x in m f) = (do f \<leftarrow> return x; m f od)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Let x m = return x >>= m
theory Nondet_Monad_Equations

lemma liftME_return:
  "liftME f (returnOk v) = returnOk (f v)" by (simp add: liftME_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftME f (returnOk v) = returnOk (f v)
theory Nondet_Monad_Equations

lemma fold_bindE_into_list_case:
  "(doE v \<leftarrow> f; case_list (g v) (h v) x odE)
   = (case_list (doE v \<leftarrow> f; g v odE) (\<lambda>x xs. doE v \<leftarrow> f; h v x xs odE) x)" by (simp split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE v <- f;
case x of [] \<Rightarrow> g v | x # xa \<Rightarrow> h v x xa
odE = (case x of [] \<Rightarrow> f >>=E g | x # xs \<Rightarrow> doE v <- f;
h v x xs
odE)
theory Nondet_Monad_Equations

lemma whenE_liftE:
  "whenE P (liftE f) = liftE (when P f)" by (simp add: whenE_def when_def returnOk_liftE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whenE P (liftE f) = liftE (when P f)
theory Nondet_Monad_Equations

lemma whenE_whenE_body:
  "whenE P (throwError f) >>=E (\<lambda>_. whenE Q (throwError f) >>=E r) = whenE (P \<or> Q) (throwError f) >>=E r" apply (cases P) apply (simp add: whenE_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE _ <- whenE P (throwError f);
whenE Q (throwError f) >>=E r
odE = whenE (P \<or> Q) (throwError f) >>=E r proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> doE _ <- whenE P (throwError f);
whenE Q (throwError f) >>=E r
odE = whenE (P \<or> Q) (throwError f) >>=E r
 2. \<not> P \<Longrightarrow> doE _ <- whenE P (throwError f);
whenE Q (throwError f) >>=E r
odE = whenE (P \<or> Q) (throwError f) >>=E r proof (prove)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> doE _ <- whenE P (throwError f);
whenE Q (throwError f) >>=E r
odE = whenE (P \<or> Q) (throwError f) >>=E r proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma exec_select_f_singleton:
  "(select_f ({v},False) >>= f) = f v" by (simp add: select_f_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f ({v}, False) >>= f = f v
theory Nondet_Monad_Equations

lemma maybe_fail_bind_fail:
  "unless P fail >>= (\<lambda>_. fail) = fail"
  "when P fail >>= (\<lambda>_. fail) = fail" by (clarsimp simp: bind_def fail_def return_def
                     unless_def when_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- unless P fail;
fail
od = fail &&& do _ <- when P fail;
fail
od = fail
theory Nondet_Monad_Equations

lemma select_singleton[simp]:
  "select {x} = return x" by (simp add: select_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select {x} = return x
theory Nondet_Monad_Equations

lemma return_modify:
  "return () = modify id" by (simp add: return_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. return () = modify id
theory Nondet_Monad_Equations

lemma liftE_liftM_liftME:
  "liftE (liftM f m) = liftME f (liftE m)" by (simp add: liftE_liftM liftME_liftM liftM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (liftM f m) = liftME f (liftE m)
theory Nondet_Monad_Equations

lemma bind_return_unit:
  "f = (f >>= (\<lambda>x. return ()))" by simp

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

lemma modify_id_return:
 "modify id = return ()" by (simp add: simpler_modify_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify id = return ()