kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_Empty_Fail

lemma empty_fail_guard[empty_fail_term]:
  "empty_fail (state_assert G)" by (clarsimp simp: state_assert_def empty_fail_cond empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (state_assert G)
theory Nondet_Empty_Fail

lemma empty_fail_spec[empty_fail_term]:
  "empty_fail (state_select F)" by (clarsimp simp: state_select_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (state_select F)
theory Nondet_Empty_Fail

lemma empty_fail_when[empty_fail_cond]:
  "(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)" unfolding when_def by (simp add: empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x) proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (if P then x else return ())
theory Nondet_Empty_Fail

lemma empty_fail_unless[empty_fail_cond]:
  "(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unless P f)" unfolding unless_def by (simp add: empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unless P f) proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (when (\<not> P) f)
theory Nondet_Empty_Fail

lemma empty_fail_liftM[empty_fail_cond]:
  "empty_fail m \<Longrightarrow> empty_fail (liftM f m)" unfolding liftM_def by (fastforce simp: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (liftM f m) proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (do x <- m;
return (f x)
od)
theory Nondet_Empty_Fail

lemma empty_fail_liftME[empty_fail_cond]:
  "empty_fail m \<Longrightarrow> empty_fail (liftME f m)" unfolding liftME_def by (simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (liftME f m) proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (doE x <- m;
returnOk (f x)
odE)
theory Nondet_Empty_Fail

lemma empty_fail_handleE[empty_fail_cond]:
  "\<lbrakk> empty_fail L; \<And>r. empty_fail (R r) \<rbrakk> \<Longrightarrow> empty_fail (L <handle> R)" by (clarsimp simp: handleE_def handleE'_def empty_fail_term empty_fail_cond split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail L; \<And>r. empty_fail (R r)\<rbrakk> \<Longrightarrow> empty_fail (L <handle> R)
theory Nondet_Empty_Fail

lemma empty_fail_handle'[empty_fail_cond]:
  "\<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (f <handle2> handler)" unfolding handleE'_def by (fastforce simp: empty_fail_term empty_fail_cond split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (f <handle2> handler) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (do v <- f;
case v of Inl e \<Rightarrow> handler e | Inr v' \<Rightarrow> return (Inr v')
od)
theory Nondet_Empty_Fail

lemma empty_fail_sequence[empty_fail_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence ms)" unfolding sequence_def by (induct ms; simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence ms) proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (let mcons = \<lambda>p q. do x <- p;
y <- q;
return (x # y)
od in foldr mcons ms (return []))
theory Nondet_Empty_Fail

lemma empty_fail_sequence_x[empty_fail_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence_x ms)" unfolding sequence_x_def by (induct ms; simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence_x ms) proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (foldr (\<lambda>x y. do _ <- x;
y
od) ms (return ()))
theory Nondet_Empty_Fail

lemma empty_fail_sequenceE[empty_fail_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE ms)" unfolding sequenceE_def by (induct ms; simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE ms) proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (let mcons = \<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE in foldr mcons ms (returnOk []))
theory Nondet_Empty_Fail

lemma empty_fail_sequenceE_x[empty_fail_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE_x ms)" unfolding sequenceE_x_def by (induct ms; simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE_x ms) proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (foldr (\<lambda>x y. doE _ <- x;
y
odE) ms (returnOk ()))
theory Nondet_Empty_Fail

lemma empty_fail_mapM_x[empty_fail_cond]:
  "(\<And>m. m \<in> f ` set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapM_x f ms)" unfolding mapM_x_def by (fastforce intro: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> f ` set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapM_x f ms) proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> f ` set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence_x (map f ms))
theory Nondet_Empty_Fail

lemma empty_fail_mapME[empty_fail_cond]:
  "(\<And>m. m \<in> f ` set xs \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapME f xs)" unfolding mapME_def by (fastforce intro: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> f ` set xs \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapME f xs) proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> f ` set xs \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE (map f xs))
theory Nondet_Empty_Fail

lemma empty_fail_filterM[empty_fail_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail (P m)) \<Longrightarrow> empty_fail (filterM P ms)" by (induct ms; simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> empty_fail (P m)) \<Longrightarrow> empty_fail (filterM P ms)
theory Nondet_Empty_Fail

lemma empty_fail_zipWithM_x[empty_fail_cond]:
  "(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM_x f xs ys)" unfolding zipWithM_x_def zipWith_def by (fastforce intro: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM_x f xs ys) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (sequence_x (map2 f xs ys))
theory Nondet_Empty_Fail

lemma empty_fail_zipWithM[empty_fail_cond]:
  "(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM f xs ys)" unfolding zipWithM_def zipWith_def by (fastforce intro: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM f xs ys) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (sequence (map2 f xs ys))
theory Nondet_Empty_Fail

lemma empty_fail_maybeM[empty_fail_cond]:
  "\<forall>x. empty_fail (f x) \<Longrightarrow> empty_fail (maybeM f t)" unfolding maybeM_def by (fastforce intro: empty_fail_term split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. empty_fail (f x) \<Longrightarrow> empty_fail (maybeM f t) proof (prove)
goal (1 subgoal):
 1. \<forall>x. empty_fail (f x) \<Longrightarrow> empty_fail (case t of None \<Rightarrow> return () | Some x \<Rightarrow> f x)
theory Nondet_Empty_Fail

lemma empty_fail_ifM[empty_fail_cond]:
  "\<lbrakk> empty_fail P; empty_fail a; empty_fail b \<rbrakk> \<Longrightarrow> empty_fail (ifM P a b)" by (simp add: ifM_def empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail P; empty_fail a; empty_fail b\<rbrakk> \<Longrightarrow> empty_fail (ifM P a b)
theory Nondet_Empty_Fail

lemma empty_fail_ifME[empty_fail_cond]:
  "\<lbrakk> empty_fail P; empty_fail a; empty_fail b \<rbrakk> \<Longrightarrow> empty_fail (ifME P a b)" by (simp add: ifME_def empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail P; empty_fail a; empty_fail b\<rbrakk> \<Longrightarrow> empty_fail (ifME P a b)
theory Nondet_Empty_Fail

lemma empty_fail_whenM[empty_fail_cond]:
  "\<lbrakk> empty_fail P; empty_fail f \<rbrakk> \<Longrightarrow> empty_fail (whenM P f)" by (simp add: whenM_def empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail P; empty_fail f\<rbrakk> \<Longrightarrow> empty_fail (whenM P f)
theory Nondet_Empty_Fail

lemma empty_fail_andM[empty_fail_cond]:
  "\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (andM A B)" by (simp add: andM_def empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail A; empty_fail B\<rbrakk> \<Longrightarrow> empty_fail (andM A B)
theory Nondet_Empty_Fail

lemma empty_fail_orM[empty_fail_cond]:
  "\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (orM A B)" by (simp add: orM_def empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail A; empty_fail B\<rbrakk> \<Longrightarrow> empty_fail (orM A B)
theory Nondet_Empty_Fail

lemma empty_fail_notM[empty_fail_cond]:
  "empty_fail A \<Longrightarrow> empty_fail (notM A)" by (simp add: notM_def empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail A \<Longrightarrow> empty_fail (notM A)
theory Nondet_Empty_Fail

lemma empty_fail_select_eq[simp]:
  "empty_fail (select V) = (V \<noteq> {})" by (clarsimp simp: select_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (select V) = (V \<noteq> {})
theory Nondet_Empty_Fail

lemma empty_fail_liftM_eq[simp]:
  "empty_fail (liftM f m) = empty_fail m" unfolding liftM_def by (fastforce dest: empty_fail_bindD1)

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

lemma empty_fail_liftE_eq[simp]:
  "empty_fail (liftE f) = empty_fail f" by (fastforce simp: liftE_def empty_fail_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (liftE f) = empty_fail f
theory Nondet_Empty_Fail

lemma liftME_empty_fail_eq[simp]:
  "empty_fail (liftME f m) = empty_fail m" unfolding liftME_def by (fastforce dest: empty_fail_bindD1 simp: bindE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (liftME f m) = empty_fail m proof (prove)
goal (1 subgoal):
 1. empty_fail (doE x <- m;
returnOk (f x)
odE) = empty_fail m
theory Nondet_Lemmas

lemma bind_cong[fundef_cong]:
  "\<lbrakk> f = f'; \<And>v s s'. (v, s') \<in> fst (f' s) \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" by (auto simp: bind_def split_def)

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

lemma bind_apply_cong [fundef_cong]:
  "\<lbrakk> f s = f' s'; \<And>rv st. (rv, st) \<in> fst (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
   \<Longrightarrow> (f >>= g) s = (f' >>= g') s'" by (auto simp: bind_def split_def)

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma nested_bind[simp]:
  "do x <- do y <- f; return (g y) od; h x od = do y <- f; h (g y) od" by (clarsimp simp: bind_def Let_def split_def return_def)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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