kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_Monad_Equations

lemma condition_apply_cong:
  "\<lbrakk> c s = c' s'; s = s'; \<And>s. c' s \<Longrightarrow> l s = l' s  ; \<And>s. \<not> c' s \<Longrightarrow> r s = r' s  \<rbrakk> \<Longrightarrow>  condition c l r s = condition c' l' r' s'" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c s = c' s'; s = s'; \<And>s. c' s \<Longrightarrow> l s = l' s; \<And>s. \<not> c' s \<Longrightarrow> r s = r' s\<rbrakk> \<Longrightarrow> condition c
  l
  r s = condition c'
  l'
  r' s'
theory Nondet_Monad_Equations

lemma condition_cong [cong, fundef_cong]:
  "\<lbrakk> c = c'; \<And>s. c' s \<Longrightarrow> l s = l' s; \<And>s. \<not> c' s \<Longrightarrow> r s = r' s \<rbrakk> \<Longrightarrow> condition c l r = condition c' l' r'" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = c'; \<And>s. c' s \<Longrightarrow> l s = l' s; \<And>s. \<not> c' s \<Longrightarrow> r s = r' s\<rbrakk> \<Longrightarrow> condition c
  l
  r = condition c'
  l'
  r'
theory Nondet_Monad_Equations

lemma lift_Inr [simp]: "(lift X (Inr r)) = (X r)" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift X (Inr r) = X r
theory Nondet_Monad_Equations

lemma lift_Inl [simp]: "lift C (Inl a) = throwError a" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift C (Inl a) = throwError a
theory Nondet_Monad_Equations

lemma returnOk_def2:  "returnOk a = return (Inr a)" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. returnOk a = return (Inr a)
theory Nondet_Monad_Equations

lemma liftE_fail[simp]: "liftE fail = fail" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE fail = fail
theory Nondet_Monad_Equations

lemma catch_bind_distrib:
  "do _ <- m <catch> h; f od = (doE m; liftE f odE <catch> (\<lambda>x. do h x; f od))" by (force simp: catch_def bindE_def bind_assoc liftE_def lift_def bind_def
                  split_def return_def throwError_def
            split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- m <catch> h;
f
od = (doE m;
liftE f
odE <catch> (\<lambda>x. do h x;
f
od))
theory Nondet_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 Nondet_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 Nondet_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> fst (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 Nondet_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 Nondet_Monad_Equations

lemma monad_eq_split:
  assumes "\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
          "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>r s. Q r s\<rbrace>"
          "P s"
  shows "(g >>= f) s = (g >>= f') s" proof - have pre: "\<And>rv s'. \<lbrakk>(rv, s') \<in> fst (g s)\<rbrakk> \<Longrightarrow> f rv s' = f' rv s'" using assms unfolding valid_def apply - by (erule allE[where x=s]) auto show ?thesis by (simp add: bind_def image_def case_prod_unfold pre) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (g >>= f) s = (g >>= f') s proof (state)
goal (1 subgoal):
 1. (g >>= f) s = (g >>= f') s proof (prove)
goal (1 subgoal):
 1. \<And>rv s'. (rv, s') \<in> fst (g s) \<Longrightarrow> f rv s' = f' rv s' proof (prove)
using this:
Q ?r ?s \<Longrightarrow> f ?r ?s = f' ?r ?s
\<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace>
P s

goal (1 subgoal):
 1. \<And>rv s'. (rv, s') \<in> fst (g s) \<Longrightarrow> f rv s' = f' rv s' proof (prove)
using this:
Q ?r ?s \<Longrightarrow> f ?r ?s = f' ?r ?s
\<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (g s). Q r s')
P s

goal (1 subgoal):
 1. \<And>rv s'. (rv, s') \<in> fst (g s) \<Longrightarrow> f rv s' = f' rv s' proof (prove)
goal (1 subgoal):
 1. \<And>rv s'. \<lbrakk>(rv, s') \<in> fst (g s); \<And>r s. Q r s \<Longrightarrow> f r s = f' r s; \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (g s). Q r s'); P s\<rbrakk> \<Longrightarrow> f rv s' = f' rv s' proof (state)
this:
(?rv, ?s') \<in> fst (g s) \<Longrightarrow> f ?rv ?s' = f' ?rv ?s'

goal (1 subgoal):
 1. (g >>= f) s = (g >>= f') s proof (prove)
goal (1 subgoal):
 1. (g >>= f) s = (g >>= f') s proof (state)
this:
(g >>= f) s = (g >>= f') s

goal:
No subgoals!
theory Nondet_Monad_Equations

lemma monad_eq_split2:
  assumes eq: " g' s = g s"
  assumes tail:"\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
  and hoare:   "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>r s. Q r s\<rbrace>" "P s"
  shows "(g >>= f) s = (g' >>= f') s" proof - have pre: "\<And>aa bb. \<lbrakk>(aa, bb) \<in> fst (g s)\<rbrakk> \<Longrightarrow> Q aa bb" using hoare by (auto simp: valid_def) show ?thesis by (simp add:bind_def eq image_def case_prod_unfold pre surjective_pairing tail) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (g >>= f) s = (g' >>= f') s proof (state)
goal (1 subgoal):
 1. (g >>= f) s = (g' >>= f') s proof (prove)
goal (1 subgoal):
 1. \<And>aa bb. (aa, bb) \<in> fst (g s) \<Longrightarrow> Q aa bb proof (prove)
using this:
\<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace>
P s

goal (1 subgoal):
 1. \<And>aa bb. (aa, bb) \<in> fst (g s) \<Longrightarrow> Q aa bb proof (state)
this:
(?aa, ?bb) \<in> fst (g s) \<Longrightarrow> Q ?aa ?bb

goal (1 subgoal):
 1. (g >>= f) s = (g' >>= f') s proof (prove)
goal (1 subgoal):
 1. (g >>= f) s = (g' >>= f') s proof (state)
this:
(g >>= f) s = (g' >>= f') s

goal:
No subgoals!
theory Nondet_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 Nondet_Monad_Equations

lemma double_gets_drop_regets:
  "(do x \<leftarrow> gets f;
       xa \<leftarrow> gets f;
       m xa x
    od) =
   (do xa \<leftarrow> gets f;
       m xa xa
    od)" by monad_eq

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

lemma bind_inv_inv_comm_weak:
  "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>_. (=) s\<rbrace>;
     empty_fail f; empty_fail g \<rbrakk> \<Longrightarrow>
   do x \<leftarrow> f; y \<leftarrow> g; n od = do y \<leftarrow> g; x \<leftarrow> f; n od" apply (rule ext) apply (fastforce simp: bind_def valid_def empty_fail_def split_def image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>_. (=) s\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> do x <- f;
y <- g;
n
od = do y <- g;
x <- f;
n
od proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>_. (=) s\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do x <- f;
y <- g;
n
od) x = (do y <- g;
x <- f;
n
od) x proof (prove)
goal:
No subgoals!
theory Nondet_Monad_Equations

lemma state_assert_false[simp]: "state_assert (\<lambda>_. False) = fail" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_assert (\<lambda>_. False) = fail
theory Nondet_Monad_Equations

lemma condition_fail_rhs: "condition C X fail = (state_assert C >>= (\<lambda>_. X))" by (monad_eq simp: Bex_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition C
  X
  fail = do _ <- state_assert C;
X
od
theory Nondet_Monad_Equations

lemma condition_swap: "condition C A B = condition (\<lambda>s. \<not> C s) B A" by monad_eq auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition C
  A
  B = condition (\<lambda>s. \<not> C s)
  B
  A
theory Nondet_Monad_Equations

lemma condition_fail_lhs: "condition C fail X = (state_assert (\<lambda>s. \<not> C s) >>= (\<lambda>_. X))" by (metis condition_fail_rhs condition_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition C
  fail
  X = do _ <- state_assert (\<lambda>s. \<not> C s);
X
od
theory Nondet_Monad_Equations

lemma condition_bind_fail[simp]:
    "(condition C A B >>= (\<lambda>_. fail)) = condition C (A >>= (\<lambda>_. fail)) (B >>= (\<lambda>_. fail))" by monad_eq blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- condition C
  A
  B;
fail
od = condition C
  (do _ <- A;
fail
od)
  (do _ <- B;
fail
od)
theory Nondet_Monad_Equations

lemma bind_fail_propagates:
  "empty_fail A \<Longrightarrow> A >>= (\<lambda>_. fail) = fail" by (monad_eq simp: empty_fail_def) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail A \<Longrightarrow> do _ <- A;
fail
od = fail
theory Nondet_Monad_Equations

lemma simple_bind_fail [simp]:
  "(state_assert X >>= (\<lambda>_. fail)) = fail"
  "(modify M >>= (\<lambda>_. fail)) = fail"
  "(return X >>= (\<lambda>_. fail)) = fail"
  "(gets X >>= (\<lambda>_. fail)) = fail" by (auto intro!: bind_fail_propagates)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (do _ <- state_assert X;
fail
od = fail &&& do _ <- modify M;
fail
od = fail) &&& do _ <- return X;
fail
od = fail &&& do _ <- gets X;
fail
od = fail
theory Nondet_Monad_Equations

lemma bind_known_operation_eq:
  "\<lbrakk> no_fail P f; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f \<rbrakk>
     \<Longrightarrow> (f >>= g) s = g x t" apply (drule(1) no_failD) apply (subgoal_tac "fst (f s) = {(x, t)}") apply (clarsimp simp: bind_def) apply (fastforce simp: valid_def empty_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f\<rbrakk> \<Longrightarrow> (f >>= g) s = g x t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f; \<not> snd (f s)\<rbrakk> \<Longrightarrow> (f >>= g) s = g x t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f; \<not> snd (f s); fst (f s) = {(x, t)}\<rbrakk> \<Longrightarrow> (f >>= g) s = g x t
 2. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f; \<not> snd (f s)\<rbrakk> \<Longrightarrow> fst (f s) = {(x, t)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f; \<not> snd (f s)\<rbrakk> \<Longrightarrow> fst (f s) = {(x, t)} proof (prove)
goal:
No subgoals!
theory Nondet_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 Nondet_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 Nondet_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 Nondet_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 Monad_Commute

lemma monad_eq:
  "a s = b s \<Longrightarrow> (a >>= g) s = (b >>= g) s" by (auto simp: bind_def)

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

lemma monad_commute_simple:
  "\<lbrakk> monad_commute P a b; P s \<rbrakk> \<Longrightarrow> (do x\<leftarrow>a;y\<leftarrow>b; g x y od) s = (do y\<leftarrow>b;x\<leftarrow>a; g x y od) s" apply (clarsimp simp: monad_commute_def) apply (drule spec) apply (erule(1) impE) apply (drule_tac g = "(\<lambda>t. g (fst t) (snd t))" in monad_eq) apply (simp add: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monad_commute P a b; P s\<rbrakk> \<Longrightarrow> (do x <- a;
b >>= g x
od) s = (do y <- b;
x <- a;
g x y
od) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (do x <- a;
y <- b;
return (x, y)
od) s = (do y <- b;
x <- a;
return (x, y)
od) s; P s\<rbrakk> \<Longrightarrow> (do x <- a;
b >>= g x
od) s = (do y <- b;
x <- a;
g x y
od) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; P ?s \<longrightarrow> (do x <- a;
y <- b;
return (x, y)
od) ?s = (do y <- b;
x <- a;
return (x, y)
od) ?s\<rbrakk> \<Longrightarrow> (do x <- a;
b >>= g x
od) s = (do y <- b;
x <- a;
g x y
od) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; (do x <- a;
y <- b;
return (x, y)
od) s = (do y <- b;
x <- a;
return (x, y)
od) s\<rbrakk> \<Longrightarrow> (do x <- a;
b >>= g x
od) s = (do y <- b;
x <- a;
g x y
od) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; (do t <- do x <- a;
y <- b;
return (x, y)
od;
g (fst t) (snd t)
od) s = (do t <- do y <- b;
x <- a;
return (x, y)
od;
g (fst t) (snd t)
od) s\<rbrakk> \<Longrightarrow> (do x <- a;
b >>= g x
od) s = (do y <- b;
x <- a;
g x y
od) s proof (prove)
goal:
No subgoals!
theory Monad_Commute

lemma monad_commute_simple':
  "monad_commute \<top> a b \<Longrightarrow> (do x \<leftarrow> a; y \<leftarrow> b; g x y od) = (do y \<leftarrow> b; x \<leftarrow> a; g x y od)" apply (clarsimp simp: monad_commute_def) apply (fastforce simp: bind_def' return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) a b \<Longrightarrow> do x <- a;
b >>= g x
od = do y <- b;
x <- a;
g x y
od proof (prove)
goal (1 subgoal):
 1. \<forall>s. (do x <- a;
y <- b;
return (x, y)
od) s = (do y <- b;
x <- a;
return (x, y)
od) s \<Longrightarrow> do x <- a;
b >>= g x
od = do y <- b;
x <- a;
g x y
od proof (prove)
goal:
No subgoals!
theory Monad_Commute

lemma commute_commute:
  "monad_commute P f h \<Longrightarrow> monad_commute P h f" apply (simp (no_asm) add: monad_commute_def) apply (clarsimp) apply (erule monad_commute_simple[symmetric]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute P f h \<Longrightarrow> monad_commute P h f proof (prove)
goal (1 subgoal):
 1. monad_commute P f h \<Longrightarrow> \<forall>s. P s \<longrightarrow> (do x <- h;
y <- f;
return (x, y)
od) s = (do y <- f;
x <- h;
return (x, y)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>monad_commute P f h; P s\<rbrakk> \<Longrightarrow> (do x <- h;
y <- f;
return (x, y)
od) s = (do y <- f;
x <- h;
return (x, y)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Monad_Commute

lemma assert_commute: "monad_commute (K G) (assert G) f" by (clarsimp simp: assert_def monad_commute_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (K G) (assert G) f
theory Monad_Commute

lemma cond_fail_commute: "monad_commute (K (\<not>G)) (when G fail) f" by (clarsimp simp: when_def fail_def monad_commute_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (K (\<not> G)) (when G fail) f
theory Monad_Commute

lemma return_commute: "monad_commute \<top> (return a) f" by (clarsimp simp: return_def bind_def monad_commute_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (return a) f