kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 ()
theory Trace_Monad_Equations

lemma liftE_bind_return_bindE_returnOk:
  "liftE (v >>= (\<lambda>rv. return (f rv)))
   = (liftE v >>=E (\<lambda>rv. returnOk (f rv)))" by (simp add: liftE_bindE, simp add: liftE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (do rv <- v;
return (f rv)
od) = doE rv <- liftE v;
returnOk (f rv)
odE
theory Trace_Monad_Equations

lemma bind_eqI:
  "g = g' \<Longrightarrow> f >>= g = f >>= g'" by simp

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

lemma unlessE_throwError_returnOk:
  "(if P then returnOk v else throwError x)
   = (unlessE P (throwError x) >>=E (\<lambda>_. returnOk v))" by (cases P, simp_all add: unlessE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then returnOk v else throwError x) = doE _ <- unlessE P (throwError x);
returnOk v
odE
theory Trace_Monad_Equations

lemma gets_the_bind_eq:
  "\<lbrakk> f s = Some x; g x s = h s \<rbrakk>
   \<Longrightarrow> (gets_the f >>= g) s = h s" by (simp add: gets_the_def bind_assoc exec_gets assert_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f s = Some x; g x s = h s\<rbrakk> \<Longrightarrow> (gets_the f >>= g) s = h s
theory Trace_Monad_Equations

lemma zipWithM_x_modify:
  "zipWithM_x (\<lambda>a b. modify (f a b)) as bs
   = modify (\<lambda>s. foldl (\<lambda>s (a, b). f a b s) s (zip as bs))" apply (simp add: zipWithM_x_def zipWith_def sequence_x_def) apply (induct ("zip as bs")) apply (simp add: simpler_modify_def return_def) apply (rule ext) apply (simp add: simpler_modify_def bind_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x (\<lambda>a b. modify (f a b)) as bs = modify (\<lambda>s. foldl (\<lambda>s (a, b). f a b s) s (zip as bs)) proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. do _ <- x;
y
od) (map2 (\<lambda>a b. modify (f a b)) as bs) (return ()) = modify (\<lambda>s. foldl (\<lambda>s (a, b). f a b s) s (zip as bs)) proof (prove)
goal (2 subgoals):
 1. foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>a. case a of (a, b) \<Rightarrow> modify (f a b)) []) (return ()) = modify (\<lambda>s. foldl (\<lambda>s a. case a of (a, b) \<Rightarrow> f a b s) s [])
 2. \<And>a list. foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>a. case a of (a, b) \<Rightarrow> modify (f a b)) list) (return ()) = modify (\<lambda>s. foldl (\<lambda>s a. case a of (a, b) \<Rightarrow> f a b s) s list) \<Longrightarrow> foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>a. case a of (a, b) \<Rightarrow> modify (f a b)) (a # list)) (return ()) = modify (\<lambda>s. foldl (\<lambda>s a. case a of (a, b) \<Rightarrow> f a b s) s (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>a. case a of (a, b) \<Rightarrow> modify (f a b)) list) (return ()) = modify (\<lambda>s. foldl (\<lambda>s a. case a of (a, b) \<Rightarrow> f a b s) s list) \<Longrightarrow> foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>a. case a of (a, b) \<Rightarrow> modify (f a b)) (a # list)) (return ()) = modify (\<lambda>s. foldl (\<lambda>s a. case a of (a, b) \<Rightarrow> f a b s) s (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list x. foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>a. case a of (a, b) \<Rightarrow> modify (f a b)) list) (return ()) = modify (\<lambda>s. foldl (\<lambda>s a. case a of (a, b) \<Rightarrow> f a b s) s list) \<Longrightarrow> foldr (\<lambda>x y. do _ <- x;
y
od) (map (\<lambda>a. case a of (a, b) \<Rightarrow> modify (f a b)) (a # list)) (return ()) x = modify (\<lambda>s. foldl (\<lambda>s a. case a of (a, b) \<Rightarrow> f a b s) s (a # list)) x proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma assert2:
  "(do v1 \<leftarrow> assert P; v2 \<leftarrow> assert Q; c od)
   = (do v \<leftarrow> assert (P \<and> Q); c od)" by (simp add: assert_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do v1 <- assert P;
v2 <- assert Q;
c
od = do v <- assert (P \<and> Q);
c
od
theory Trace_Monad_Equations

lemma assert_opt_def2:
  "assert_opt v = (do assert (v \<noteq> None); return (the v) od)" by (simp add: assert_opt_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert_opt v = do assert (v \<noteq> None);
return (the v)
od
theory Trace_Monad_Equations

lemma gets_assert:
  "(do v1 \<leftarrow> assert v; v2 \<leftarrow> gets f; c v1 v2 od)
   = (do v2 \<leftarrow> gets f; v1 \<leftarrow> assert v; c v1 v2 od)" by (simp add: simpler_gets_def return_def assert_def fail_def bind_def
         split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do v1 <- assert v;
gets f >>= c v1
od = do v2 <- gets f;
v1 <- assert v;
c v1 v2
od
theory Trace_Monad_Equations

lemma gets_prod_comp:
  "gets (case x of (a, b) \<Rightarrow> f a b) = (case x of (a, b) \<Rightarrow> gets (f a b))" by (auto simp: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets (case x of (a, b) \<Rightarrow> f a b) = (case x of (a, b) \<Rightarrow> gets (f a b))
theory Trace_Monad_Equations

lemma bind_assoc2:
  "(do x \<leftarrow> a; _ \<leftarrow> b; c x od) = (do x \<leftarrow> (do x' \<leftarrow> a; _ \<leftarrow> b; return x' od); c x od)" by (simp add: bind_assoc)

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

lemma bind_assoc_return_reverse:
  "do x \<leftarrow> f;
      _ \<leftarrow> g x;
      h x
   od =
   do x \<leftarrow> do x \<leftarrow> f;
              _ \<leftarrow> g x;
              return x
           od;
      h x
   od" by (simp only: bind_assoc return_bind)

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

lemma if_bind:
  "(if P then (a >>= (\<lambda>_. b)) else return ()) =
   (if P then a else return ()) >>= (\<lambda>_. if P then b else return ())" by (cases P; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then do _ <- a;
b
od else return ()) = do _ <- if P then a else return ();
if P then b else return ()
od
theory Trace_Monad_Equations

lemma bind_liftE_distrib: "(liftE (A >>= (\<lambda>x. B x))) = (liftE A >>=E (\<lambda>x. liftE (\<lambda>s. B x s)))" by (clarsimp simp: liftE_def bindE_def lift_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (A >>= B) = doE x <- liftE A;
liftE (B x)
odE
theory Trace_Monad_Equations

lemma if_catch_distrib:
  "((if P then f else g) <catch> h) = (if P then f <catch> h else g <catch> h)" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then f else g) <catch> h) = (if P then f <catch> h else g <catch> h)
theory Trace_Monad_Equations

lemma will_throw_and_catch:
  "f = throwError e \<Longrightarrow> (f <catch> (\<lambda>_. g)) = g" by (simp add: catch_def throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f = throwError e \<Longrightarrow> (f <catch> (\<lambda>_. g)) = g
theory Trace_Monad_Equations

lemma catch_is_if:
  "(doE x <- f; g x odE <catch> h) =
   do
     rv <- f;
     if sum.isl rv then h (projl rv) else g (projr rv) <catch> h
   od" apply (simp add: bindE_def catch_def bind_assoc cong: if_cong) apply (rule bind_cong, rule refl) apply (clarsimp simp: lift_def throwError_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f >>=E g <catch> h) = do rv <- f;
if isl rv then h (projl rv) else g (projr rv) <catch> h
od proof (prove)
goal (1 subgoal):
 1. do x <- f;
lift g x >>= case_sum h return
od = do rv <- f;
if isl rv then h (projl rv) else do x <- g (projr rv);
case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b
od
od proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> mres (f s) \<Longrightarrow> (lift g v >>= case_sum h return) s' = (if isl v then h (projl v) else do x <- g (projr v);
case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b
od) s' proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma liftE_K_bind: "liftE ((K_bind (\<lambda>s. A s)) x) = K_bind (liftE (\<lambda>s. A s)) x" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (K_bind A x) = K_bind (liftE A) x
theory Trace_Monad_Equations

lemma monad_eq_split_tail:
  "\<lbrakk>f = g; a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = ((b >>= g) s)" by (simp add:bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = g; a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = (b >>= g) s
theory Trace_Monad_Equations

lemma assert_opt_If:
  "assert_opt v = If (v = None) fail (return (the v))" by (simp add: assert_opt_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert_opt v = (if v = None then fail else return (the v))
theory Trace_Monad_Equations

lemma if_to_top_of_bind:
  "(bind (If P x y) z) = If P (bind x z) (bind y z)" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then x else y) >>= z = (if P then x >>= z else y >>= z)
theory Trace_Monad_Equations

lemma if_to_top_of_bindE:
  "(bindE (If P x y) z) = If P (bindE x z) (bindE y z)" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then x else y) >>=E z = (if P then x >>=E z else y >>=E z)
theory Trace_Monad_Equations

lemma modify_modify:
  "(do x \<leftarrow> modify f; modify (g x) od) = modify (g () o f)" by (simp add: bind_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- modify f;
modify (g x)
od = modify (g () \<circ> f)
theory Trace_Monad_Equations

lemma mapM_Cons:
  "mapM f (x # xs) = do
     y \<leftarrow> f x;
     ys \<leftarrow> mapM f xs;
     return (y # ys)
   od"
  and mapM_Nil:
  "mapM f [] = return []" by (simp_all add: mapM_def sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM f (x # xs) = do y <- f x;
ys <- mapM f xs;
return (y # ys)
od &&& mapM f [] = return []
theory Trace_Monad_Equations

lemma mapM_append:
  "mapM f (xs @ ys) = (do
     fxs \<leftarrow> mapM f xs;
     fys \<leftarrow> mapM f ys;
     return (fxs @ fys)
   od)" by (induct xs, simp_all add: mapM_Cons mapM_Nil bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM f (xs @ ys) = do fxs <- mapM f xs;
fys <- mapM f ys;
return (fxs @ fys)
od
theory Trace_Monad_Equations

lemma mapM_x_append:
  "mapM_x f (xs @ ys) = (do
     x \<leftarrow> mapM_x f xs;
     mapM_x f ys
   od)" by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f (xs @ ys) = do x <- mapM_x f xs;
mapM_x f ys
od
theory Trace_Monad_Equations

lemma mapM_x_map:
  "mapM_x f (map g xs) = mapM_x (f o g) xs" by (induct xs; simp add: mapM_x_Nil mapM_x_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f (map g xs) = mapM_x (f \<circ> g) xs
theory Trace_Monad_Equations

lemma repeat_n_mapM_x:
  "repeat_n n f = mapM_x (\<lambda>_. f) (replicate n ())" by (induct n, simp_all add: mapM_x_Cons mapM_x_Nil)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. repeat_n n f = mapM_x (\<lambda>_. f) (replicate n ())
theory Trace_Monad_Equations

lemma elem_select_bind:
  "(tr, res) \<in> (do x \<leftarrow> select S; f x od) s
   = (\<exists>x \<in> S. (tr, res) \<in> f x s)" by (simp add: bind_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((tr, res) \<in> (select S >>= f) s) = (\<exists>x\<in>S. (tr, res) \<in> f x s)
theory Trace_Monad_Equations

lemma select_bind_UN:
  "(do x \<leftarrow> select S; f x od) = (\<lambda>s. \<Union>x \<in> S. f x s)" by (rule ext, auto simp: elem_select_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select S >>= f = (\<lambda>s. \<Union>x\<in>S. f x s)
theory Trace_Monad_Equations

lemma select_early:
  "S \<noteq> {}
   \<Longrightarrow> do x \<leftarrow> f; y \<leftarrow> select S; g x y od
       = do y \<leftarrow> select S; x \<leftarrow> f; g x y od" apply (simp add: bind_def select_def Sigma_def) apply (rule ext) apply (fastforce elim: rev_bexI image_eqI[rotated] split: tmres.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> do x <- f;
select S >>= g x
od = do y <- select S;
x <- f;
g x y
od proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> (\<lambda>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>(a, b). (a @ xs, b)) ` (\<Union>x\<in>S. g rv x s)) = (\<lambda>s. \<Union>x\<in>S. \<Union>(xs, y)\<in>f s. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` g rv x s) y) proof (prove)
goal (1 subgoal):
 1. \<And>s. S \<noteq> {} \<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>(a, b). (a @ xs, b)) ` (\<Union>x\<in>S. g rv x s)) = (\<Union>x\<in>S. \<Union>(xs, y)\<in>f s. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` g rv x s) y) proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma repeat_choice:
  "S \<noteq> {}
   \<Longrightarrow> repeat (do x \<leftarrow> select S; f x od)
       = (do xs \<leftarrow> select {xs. set xs \<subseteq> S}; mapM_x f xs od)" apply (simp add: repeat_def repeat_n_choice) apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> repeat (select S >>= f) = select {xs. set xs \<subseteq> S} >>= mapM_x f proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> do n <- select UNIV;
select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f
od = select {xs. set xs \<subseteq> S} >>= mapM_x f proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma put_trace_append:
  "put_trace (xs @ ys) = do put_trace ys; put_trace xs od" by (induct xs; simp add: bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. put_trace (xs @ ys) = do put_trace ys;
put_trace xs
od
theory Trace_Monad_Equations

lemma put_trace_elem_put_comm:
  "do y \<leftarrow> put_trace_elem x; put s od
   = do y \<leftarrow> put s; put_trace_elem x od" by (simp add: put_def put_trace_elem_def bind_def insert_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do y <- put_trace_elem x;
put s
od = do y <- put s;
put_trace_elem x
od
theory Trace_Monad_Equations

lemma mapM_x_comm:
  "(\<forall>x \<in> set xs. do y \<leftarrow> g; f x od = do y \<leftarrow> f x; g od)
   \<Longrightarrow> do y \<leftarrow> g; mapM_x f xs od = do y \<leftarrow> mapM_x f xs; g od" apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons) apply (simp add: bind_assoc[symmetric], simp add: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. do y <- g;
f x
od = do y <- f x;
g
od \<Longrightarrow> do y <- g;
mapM_x f xs
od = do y <- mapM_x f xs;
g
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>do y <- g;
mapM_x f xs
od = do y <- mapM_x f xs;
g
od; do y <- g;
f a
od = do y <- f a;
g
od \<and> (\<forall>x\<in>set xs. do y <- g;
f x
od = do y <- f x;
g
od)\<rbrakk> \<Longrightarrow> do y <- g;
y <- f a;
mapM_x f xs
od = do y <- do y <- f a;
mapM_x f xs
od;
g
od proof (prove)
goal:
No subgoals!