kings-crown/FVELER_Isabelle huggingface dataset:
theory Monad_Lists

lemma filterM_all:
  "\<lbrakk> \<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. \<forall>x \<in> set xs. P x s\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. P x s\<rbrace>" apply (rule_tac Q="\<lambda>rv s. set rv \<subseteq> set xs \<and> (\<forall>x \<in> set xs. P x s)"
              in hoare_strengthen_post) apply (wp filterM_subset hoare_vcg_const_Ball_lift filterM_preserved) apply simp+ apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. P x s\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. P x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. P x s\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. P x s)\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace>; set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. P x s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace>; x \<in> set xs; xa \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P x\<rbrace> m xa \<lbrace>\<lambda>rv. P x\<rbrace>
 2. \<And>s. \<lbrakk>\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace>; \<forall>x\<in>set xs. P x s\<rbrakk> \<Longrightarrow> True \<and> (\<forall>x\<in>set xs. P x s)
 3. \<And>rv s. \<lbrakk>\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace>; set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. P x s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace>; set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. P x s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma filterM_distinct:
  "\<lbrace>K (distinct xs)\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. distinct rv\<rbrace>" by (rule hoare_chain, rule filterM_distinct1[where P=True], simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (distinct xs)\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. distinct rv\<rbrace>
theory Monad_Lists

lemma mapM_wp:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
  shows      "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>" apply (induct xs) apply (simp add: mapM_def sequence_def) apply (simp add: mapM_Cons) apply wp apply (rule x, clarsimp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM f [] \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>; a \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- f a;
ys <- mapM f xs;
return (y # ys)
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>; a \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 a xs\<rbrace> f a \<lbrace>\<lambda>y. P\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>; a \<in> S \<and> set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> ?Q2 a xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>; a \<in> S \<and> set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_wp':
  assumes x: "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
  shows "\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>" apply (rule mapM_wp) apply (erule x) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> ?S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>
 2. set xs \<subseteq> ?S proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> set xs proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_set_inv:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>"
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>"
  assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>"
  shows "\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. P s \<and> (\<forall>x \<in> set xs. Q x s)\<rbrace>" apply (rule hoare_weaken_pre, rule hoare_vcg_conj_lift) apply (rule mapM_wp', erule assms) apply (rule mapM_set; rule assms; assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. P s \<and> (\<forall>x\<in>set xs. Q x s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P3\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<lbrace>?P'3\<rbrace> mapM f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. Q x s\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?P3 s \<and> ?P'3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'3\<rbrace> mapM f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. Q x s\<rbrace>
 2. \<And>s. P s \<Longrightarrow> P s \<and> ?P'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s \<and> P s proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_x_wp:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
  shows      "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. P\<rbrace>" by (subst mapM_x_mapM) (wp mapM_wp x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. P\<rbrace>
theory Monad_Lists

lemma det_mapM:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> det (f x)"
  shows      "set xs \<subseteq> S \<Longrightarrow> det (mapM f xs)" apply (induct xs) apply (simp add: mapM_def sequence_def) apply (simp add: mapM_Cons x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> det (mapM f xs) proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> S \<Longrightarrow> det (mapM f [])
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> det (mapM f xs); set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> det (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> det (mapM f xs); set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> det (mapM f (a # xs)) proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma det_zipWithM_x:
  assumes x: "\<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> det (f x y)"
  shows      "det (zipWithM_x f xs ys)" apply (simp add: zipWithM_x_mapM) apply (rule bind_detI) apply (rule det_mapM [where S="set (zip xs ys)"]) apply (clarsimp simp add: x) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (zipWithM_x f xs ys) proof (prove)
goal (1 subgoal):
 1. det (do _ <- mapM (\<lambda>(x, y). f x y) (zip xs ys);
return ()
od) proof (prove)
goal (2 subgoals):
 1. det (mapM (\<lambda>(x, y). f x y) (zip xs ys))
 2. \<forall>x. det (return ()) proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set (zip xs ys) \<Longrightarrow> det (case x of (x, xa) \<Rightarrow> f x xa)
 2. set (zip xs ys) \<subseteq> set (zip xs ys)
 3. \<forall>x. det (return ()) proof (prove)
goal (2 subgoals):
 1. set (zip xs ys) \<subseteq> set (zip xs ys)
 2. \<forall>x. det (return ()) proof (prove)
goal (1 subgoal):
 1. \<forall>x. det (return ()) proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma empty_fail_mapM_x [simp]:
  "(\<And>x. empty_fail (a x)) \<Longrightarrow> empty_fail (mapM_x a xs)" apply (induct_tac xs) apply (clarsimp simp: mapM_x_Nil) apply (clarsimp simp: mapM_x_Cons) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (a x)) \<Longrightarrow> empty_fail (mapM_x a xs) proof (prove)
goal (2 subgoals):
 1. (\<And>x. empty_fail (a x)) \<Longrightarrow> empty_fail (mapM_x a [])
 2. \<And>aa list. \<lbrakk>\<And>x. empty_fail (a x); empty_fail (mapM_x a list)\<rbrakk> \<Longrightarrow> empty_fail (mapM_x a (aa # list)) proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<And>x. empty_fail (a x); empty_fail (mapM_x a list)\<rbrakk> \<Longrightarrow> empty_fail (mapM_x a (aa # list)) proof (prove)
goal:
No subgoals!
theory Nondet_MonadEq

lemma monad_eq_simp[monad_eq]:
  "((A :: ('s, 'a) nondet_monad) = B) =
      ((\<forall>r t s. (r, t) \<in> fst (A s) \<longrightarrow> (r, t) \<in> fst (B s))
         \<and> (\<forall>r t s. (r, t) \<in> fst (B s) \<longrightarrow> (r, t) \<in> fst (A s))
         \<and> (\<forall>x. snd (A x) = snd (B x)))" by (auto intro!: set_eqI prod_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A = B) = ((\<forall>r t s. (r, t) \<in> fst (A s) \<longrightarrow> (r, t) \<in> fst (B s)) \<and> (\<forall>r t s. (r, t) \<in> fst (B s) \<longrightarrow> (r, t) \<in> fst (A s)) \<and> (\<forall>x. snd (A x) = snd (B x)))
theory Nondet_MonadEq_Lemmas

lemma snd_return[monad_eq]:
  "\<not> snd (return a b)" unfolding return_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd (return a b) proof (prove)
goal (1 subgoal):
 1. \<not> snd ({(a, b)}, False)
theory Nondet_MonadEq_Lemmas

lemma snd_throwError[monad_eq]:
  "\<not> snd (throwError e s)" unfolding throwError_def by (simp add: snd_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd (throwError e s) proof (prove)
goal (1 subgoal):
 1. \<not> snd ((return \<circ> Inl) e s)
theory Nondet_MonadEq_Lemmas

lemma snd_lift_Inr[monad_eq]:
  "snd (lift b (Inr r) t) = snd (b r t)" unfolding lift_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (lift b (Inr r) t) = snd (b r t) proof (prove)
goal (1 subgoal):
 1. snd ((case Inr r of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') t) = snd (b r t)
theory Nondet_MonadEq_Lemmas

lemma snd_lift_Inl[monad_eq]:
  "\<not> snd (lift b (Inl r) t)" unfolding lift_def by (simp add: snd_throwError)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd (lift b (Inl r) t) proof (prove)
goal (1 subgoal):
 1. \<not> snd ((case Inl r of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') t)
theory Nondet_MonadEq_Lemmas

lemma snd_fail[monad_eq]:
  "snd (fail s)" by (clarsimp simp: fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (fail s)
theory Nondet_MonadEq_Lemmas

lemma not_snd_bindD:
  "\<lbrakk> \<not> snd ((a >>= b) s); (rv, s') \<in> fst (a s) \<rbrakk> \<Longrightarrow> \<not> snd (a s) \<and> \<not> snd (b rv s')" by (fastforce simp: bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd ((a >>= b) s); (rv, s') \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<not> snd (a s) \<and> \<not> snd (b rv s')
theory Nondet_MonadEq_Lemmas

lemma not_snd_bindI1:
  "\<not> snd ((a >>= b) s) \<Longrightarrow> \<not> snd (a s)" by (fastforce simp: bind_def)

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

lemma not_snd_bindI2:
  "\<lbrakk> \<not> snd ((a >>= b) s); (rv, s') \<in> fst (a s) \<rbrakk> \<Longrightarrow> \<not> snd (b rv s')" by (fastforce simp: bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd ((a >>= b) s); (rv, s') \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<not> snd (b rv s')
theory Nondet_MonadEq_Lemmas

lemma in_returns[monad_eq]:
  "(r, s) \<in> fst (return r s)"
  "(Inr r, s) \<in> fst (returnOk r s)" by (simp add: in_monad)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s) \<in> fst (return r s) &&& (Inr r, s) \<in> fst (returnOk r s)
theory Nondet_MonadEq_Lemmas

lemma fst_return:
  "fst (return v s) = {(v, s)}" by (simp add: return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (return v s) = {(v, s)}
theory Nondet_MonadEq_Lemmas

lemma in_bind_split[monad_eq]:
  "(rv \<in> fst ((f >>= g) s)) = (\<exists>rv'. rv' \<in> fst (f s) \<and> rv \<in> fst (g (fst rv') (snd rv')))" by (cases rv) (fastforce simp: in_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv \<in> fst ((f >>= g) s)) = (\<exists>rv'. rv' \<in> fst (f s) \<and> rv \<in> fst (g (fst rv') (snd rv')))
theory Nondet_MonadEq_Lemmas

lemma Inr_in_liftE_simp[monad_eq]:
  "((Inr rv, x) \<in> fst (liftE fn s)) = ((rv, x) \<in> fst (fn s))" by (simp add: in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Inr rv, x) \<in> fst (liftE fn s)) = ((rv, x) \<in> fst (fn s))
theory Nondet_MonadEq_Lemmas

lemma gets_the_member:
  "(x, s') \<in> fst (gets_the f s) = (f s = Some x \<and> s' = s)" by (cases "f s"; simp add: gets_the_def simpler_gets_def bind_def in_assert_opt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, s') \<in> fst (gets_the f s)) = (f s = Some x \<and> s' = s)
theory Nondet_MonadEq_Lemmas

lemma fst_throwError_returnOk:
  "fst (throwError e s) = {(Inl e, s)}"
  "fst (returnOk v s) = {(Inr v, s)}" by (simp add: throwError_def returnOk_def return_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (throwError e s) = {(Inl e, s)} &&& fst (returnOk v s) = {(Inr v, s)}
theory Nondet_MonadEq_Lemmas

lemma not_snd_bindE_I1:
  "\<not> snd ((a >>=E b) s) \<Longrightarrow> \<not> snd (a s)" unfolding bindE_def by (erule not_snd_bindI1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd ((a >>=E b) s) \<Longrightarrow> \<not> snd (a s) proof (prove)
goal (1 subgoal):
 1. \<not> snd ((a >>= lift b) s) \<Longrightarrow> \<not> snd (a s)
theory Nondet_MonadEq_Lemmas

lemma snd_assert[monad_eq]:
  "snd (assert P s) = (\<not> P)" by (clarsimp simp: fail_def return_def assert_def)

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

lemma not_snd_assert :
  "(\<not> snd (assert P s)) = P" by (metis snd_assert)

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

lemma snd_assert_opt[monad_eq]:
  "snd (assert_opt f s) = (f = None)" by (monad_eq simp: assert_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (assert_opt f s) = (f = None)
theory Nondet_MonadEq_Lemmas

lemma not_snd_bindD':
  "\<lbrakk>\<not> snd ((a >>= b) s); \<not> snd (a s) \<Longrightarrow> (rv, s') \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<not> snd (a s) \<and> \<not> snd (b rv s')" by (metis not_snd_bindI1 not_snd_bindI2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd ((a >>= b) s); \<not> snd (a s) \<Longrightarrow> (rv, s') \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<not> snd (a s) \<and> \<not> snd (b rv s')
theory Nondet_MonadEq_Lemmas

lemma snd_bind[monad_eq]:
  "snd ((a >>= b) s) = (snd (a s) \<or> (\<exists>r s'. (r, s') \<in> fst (a s) \<and> snd (b r s')))" apply (clarsimp simp add: bind_def Bex_def image_def) apply (subst surjective_pairing, subst prod.inject, force) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd ((a >>= b) s) = (snd (a s) \<or> (\<exists>r s'. (r, s') \<in> fst (a s) \<and> snd (b r s'))) proof (prove)
goal (1 subgoal):
 1. ((\<exists>aa ab ba. (ab, ba) \<in> fst (a s) \<and> (aa, True) = b ab ba) \<or> snd (a s)) = (snd (a s) \<or> (\<exists>r s'. (r, s') \<in> fst (a s) \<and> snd (b r s'))) proof (prove)
goal:
No subgoals!
theory Nondet_MonadEq_Lemmas

lemma in_lift[monad_eq]:
  "(rv, s') \<in> fst (lift M v s) =
   (case v of Inl x \<Rightarrow> rv = Inl x \<and> s' = s
            | Inr x \<Rightarrow> (rv, s') \<in> fst (M x s))" by (clarsimp simp: lift_def throwError_def return_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> fst (lift M v s)) = (case v of Inl x \<Rightarrow> rv = Inl x \<and> s' = s | Inr x \<Rightarrow> (rv, s') \<in> fst (M x s))
theory Nondet_MonadEq_Lemmas

lemma snd_lift[monad_eq]:
  "snd (lift M a b) = (\<exists>x. a = Inr x \<and> snd (M x b))" by (clarsimp simp: lift_def throwError_def return_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (lift M a b) = (\<exists>x. a = Inr x \<and> snd (M x b))
theory Nondet_MonadEq_Lemmas

lemma snd_bindE[monad_eq]:
  "snd ((a >>=E b) s) = (snd (a s) \<or> (\<exists>r s'. (r, s') \<in> fst (a s) \<and> (\<exists>a. r = Inr a \<and> snd (b a s'))))" unfolding bindE_def by monad_eq

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

lemma snd_get[monad_eq]:
  "snd (get s) = False" by (simp add: get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (get s) = False
theory Nondet_MonadEq_Lemmas

lemma snd_gets[monad_eq]:
  "snd (gets f s) = False" by (simp add: gets_def snd_bind snd_get snd_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (gets f s) = False
theory Nondet_MonadEq_Lemmas

lemma in_handleE'[monad_eq]:
  "((rv, s') \<in> fst ((f <handle2> g) s)) =
    ((\<exists>ex. rv = Inr ex \<and> (Inr ex, s') \<in> fst (f s)) \<or>
     (\<exists>rv' s''. (rv, s') \<in> fst (g rv' s'') \<and> (Inl rv', s'') \<in> fst (f s)))" unfolding handleE'_def return_def by (simp add: in_bind_split) (fastforce split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> fst ((f <handle2> g) s)) = ((\<exists>ex. rv = Inr ex \<and> (Inr ex, s') \<in> fst (f s)) \<or> (\<exists>rv' s''. (rv, s') \<in> fst (g rv' s'') \<and> (Inl rv', s'') \<in> fst (f s))) proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> fst ((do v <- f;
case v of Inl e \<Rightarrow> g e | Inr v' \<Rightarrow> \<lambda>s. ({(Inr v', s)}, False)
od) s)) = ((\<exists>ex. rv = Inr ex \<and> (Inr ex, s') \<in> fst (f s)) \<or> (\<exists>rv' s''. (rv, s') \<in> fst (g rv' s'') \<and> (Inl rv', s'') \<in> fst (f s)))
theory Nondet_MonadEq_Lemmas

lemma in_handleE[monad_eq]:
  "(a, b) \<in> fst ((A <handle> B) s) =
    ((\<exists>x. a = Inr x \<and> (Inr x, b) \<in> fst (A s)) \<or>
     (\<exists>r t. (Inl r, t) \<in> fst (A s) \<and> (a, b) \<in> fst (B r t)))" unfolding handleE_def by (monad_eq split: sum.splits) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, b) \<in> fst ((A <handle> B) s)) = ((\<exists>x. a = Inr x \<and> (Inr x, b) \<in> fst (A s)) \<or> (\<exists>r t. (Inl r, t) \<in> fst (A s) \<and> (a, b) \<in> fst (B r t))) proof (prove)
goal (1 subgoal):
 1. ((a, b) \<in> fst ((A <handle2> B) s)) = ((\<exists>x. a = Inr x \<and> (Inr x, b) \<in> fst (A s)) \<or> (\<exists>r t. (Inl r, t) \<in> fst (A s) \<and> (a, b) \<in> fst (B r t)))
theory Nondet_MonadEq_Lemmas

lemma snd_handleE'[monad_eq]:
  "snd ((A <handle2> B) s) = (snd (A s) \<or> (\<exists>r s'. (r, s')\<in>fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s'))))" unfolding handleE'_def by (monad_eq simp: Bex_def split: sum.splits) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd ((A <handle2> B) s) = (snd (A s) \<or> (\<exists>r s'. (r, s') \<in> fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s')))) proof (prove)
goal (1 subgoal):
 1. snd ((do v <- A;
case v of Inl e \<Rightarrow> B e | Inr v' \<Rightarrow> return (Inr v')
od) s) = (snd (A s) \<or> (\<exists>r s'. (r, s') \<in> fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s'))))
theory Nondet_MonadEq_Lemmas

lemma snd_handleE[monad_eq]:
  "snd ((A <handle> B) s) = (snd (A s) \<or> (\<exists>r s'. (r, s')\<in>fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s'))))" unfolding handleE_def by (rule snd_handleE')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd ((A <handle> B) s) = (snd (A s) \<or> (\<exists>r s'. (r, s') \<in> fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s')))) proof (prove)
goal (1 subgoal):
 1. snd ((A <handle2> B) s) = (snd (A s) \<or> (\<exists>r s'. (r, s') \<in> fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s'))))
theory Nondet_MonadEq_Lemmas

lemma snd_liftM[monad_eq, simp]:
  "snd (liftM t f s) = snd (f s)" by (auto simp: liftM_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (liftM t f s) = snd (f s)
theory Nondet_MonadEq_Lemmas

lemma snd_liftE[monad_eq]:
  "snd ((liftE x) s) = snd (x s)" by (clarsimp simp: liftE_def snd_bind snd_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (liftE x s) = snd (x s)
theory Nondet_MonadEq_Lemmas

lemma snd_returnOk[monad_eq]:
  "\<not> snd (returnOk x s)" by (clarsimp simp: returnOk_def return_def)

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

lemma snd_when[monad_eq]:
  "snd (when P M s) = (P \<and> snd (M s))" by (clarsimp simp: when_def return_def)

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

lemma in_condition[monad_eq]:
  "(a, b) \<in> fst (condition C L R s) = ((C s \<longrightarrow> (a, b) \<in> fst (L s)) \<and> (\<not>C s \<longrightarrow> (a, b) \<in> fst (R s)))" by (rule condition_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, b) \<in> fst (condition C
  L
  R s)) = ((C s \<longrightarrow> (a, b) \<in> fst (L s)) \<and> (\<not> C s \<longrightarrow> (a, b) \<in> fst (R s)))
theory Nondet_MonadEq_Lemmas

lemma snd_condition[monad_eq]:
  "snd (condition C L R s) = ((C s \<longrightarrow> snd (L s)) \<and> (\<not>C s \<longrightarrow> snd (R s)))" by (rule condition_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (condition C
  L
  R s) = ((C s \<longrightarrow> snd (L s)) \<and> (\<not> C s \<longrightarrow> snd (R s)))