kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_Empty_Fail

lemma empty_fail_bind[empty_fail_cond]:
  "\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)" unfolding empty_fail_def apply clarsimp apply (drule mres_bind_empty) apply (erule context_disjE) apply (fastforce intro: bind_failedI1) apply (fastforce intro!: bind_failedI2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail a; \<And>x. empty_fail (b x)\<rbrakk> \<Longrightarrow> empty_fail (a >>= b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. mres (a s) = {} \<longrightarrow> failed (a s); \<And>x. \<forall>s. mres (b x s) = {} \<longrightarrow> failed (b x s)\<rbrakk> \<Longrightarrow> \<forall>s. mres ((a >>= b) s) = {} \<longrightarrow> failed ((a >>= b) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. mres (a s) = {} \<longrightarrow> failed (a s); \<And>x. \<forall>s. mres (b x s) = {} \<longrightarrow> failed (b x s); mres ((a >>= b) s) = {}\<rbrakk> \<Longrightarrow> failed ((a >>= b) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. mres (a s) = {} \<longrightarrow> failed (a s); \<And>x. \<forall>s. mres (b x s) = {} \<longrightarrow> failed (b x s); mres (a s) = {} \<or> (\<forall>res\<in>mres (a s). mres (b (fst res) (snd res)) = {})\<rbrakk> \<Longrightarrow> failed ((a >>= b) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. mres (a s) = {} \<longrightarrow> failed (a s); \<And>x. \<forall>s. mres (b x s) = {} \<longrightarrow> failed (b x s); mres (a s) = {}\<rbrakk> \<Longrightarrow> failed ((a >>= b) s)
 2. \<And>s. \<lbrakk>\<forall>s. mres (a s) = {} \<longrightarrow> failed (a s); \<And>x. \<forall>s. mres (b x s) = {} \<longrightarrow> failed (b x s); mres (a s) \<noteq> {}; \<forall>res\<in>mres (a s). mres (b (fst res) (snd res)) = {}\<rbrakk> \<Longrightarrow> failed ((a >>= b) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. mres (a s) = {} \<longrightarrow> failed (a s); \<And>x. \<forall>s. mres (b x s) = {} \<longrightarrow> failed (b x s); mres (a s) \<noteq> {}; \<forall>res\<in>mres (a s). mres (b (fst res) (snd res)) = {}\<rbrakk> \<Longrightarrow> failed ((a >>= b) s) proof (prove)
goal:
No subgoals!
theory Trace_Empty_Fail

lemma empty_fail_return[empty_fail_term]:
  "empty_fail (return x)" by (simp add: empty_fail_def return_def mres_def vimage_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (return x)
theory Trace_Empty_Fail

lemma empty_fail_returnOk[empty_fail_term]:
  "empty_fail (returnOk v)" by (fastforce simp: returnOk_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (returnOk v)
theory Trace_Empty_Fail

lemma empty_fail_throwError[empty_fail_term]:
  "empty_fail (throwError v)" by (fastforce simp: throwError_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (throwError v)
theory Trace_Empty_Fail

lemma empty_fail_lift[empty_fail_cond]:
  "\<lbrakk> \<And>x. empty_fail (f x) \<rbrakk> \<Longrightarrow> empty_fail (lift f x)" unfolding lift_def by (auto simp: empty_fail_term split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> empty_fail (lift f x) proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> empty_fail (case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> f v')
theory Trace_Empty_Fail

lemma empty_fail_bindE[empty_fail_cond]:
  "\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)" by (simp add: bindE_def empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<And>rv. empty_fail (g rv)\<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)
theory Trace_Empty_Fail

lemma empty_fail_assert[empty_fail_term]:
  "empty_fail (assert P)" unfolding assert_def by (simp add: empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (assert P) proof (prove)
goal (1 subgoal):
 1. empty_fail (if P then return () else fail)
theory Trace_Empty_Fail

lemma empty_fail_assert_opt[empty_fail_term]:
  "empty_fail (assert_opt x)" by (simp add: assert_opt_def empty_fail_term split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (assert_opt x)
theory Trace_Empty_Fail

lemma empty_fail_mk_ef[empty_fail_term]:
  "empty_fail (mk_ef o m)" by (simp add: empty_fail_def mk_ef_def failed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (mk_ef \<circ> m)
theory Trace_Empty_Fail

lemma empty_fail_gets_the[empty_fail_term]:
  "empty_fail (gets_the f)" unfolding gets_the_def by (simp add: empty_fail_cond empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (gets_the f) proof (prove)
goal (1 subgoal):
 1. empty_fail (gets f >>= assert_opt)
theory Trace_Empty_Fail

lemma empty_fail_gets_map[empty_fail_term]:
  "empty_fail (gets_map f p)" unfolding gets_map_def by (simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (gets_map f p) proof (prove)
goal (1 subgoal):
 1. empty_fail (do m <- gets f;
assert_opt (m p)
od)
theory Trace_Empty_Fail

lemma empty_fail_whenEs[empty_fail_cond]:
  "(P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (whenE P f)"
  "(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unlessE P f)" by (auto simp add: whenE_def unlessE_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (whenE P f)) &&& ((\<not> P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unlessE P f))
theory Trace_Empty_Fail

lemma empty_fail_assertE[empty_fail_term]:
  "empty_fail (assertE P)" by (simp add: assertE_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (assertE P)
theory Trace_Empty_Fail

lemma empty_fail_get[empty_fail_term]:
  "empty_fail get" by (simp add: empty_fail_def get_def mres_def vimage_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail get
theory Trace_Empty_Fail

lemma empty_fail_catch[empty_fail_cond]:
  "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)" by (simp add: catch_def empty_fail_cond empty_fail_term split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<And>x. empty_fail (g x)\<rbrakk> \<Longrightarrow> empty_fail (f <catch> g)
theory Trace_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 Trace_Empty_Fail

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (state_select F)
theory Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_Empty_Fail

lemma empty_fail_put_trace_elem[empty_fail_term]:
  "empty_fail (put_trace_elem x)" by (clarsimp simp: put_trace_elem_def empty_fail_def mres_def vimage_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (put_trace_elem x)
theory Trace_Empty_Fail

lemma empty_fail_put_trace[empty_fail_term]:
  "empty_fail (put_trace xs)" apply (induct xs) apply (clarsimp simp: empty_fail_term) apply (clarsimp simp: empty_fail_term empty_fail_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (put_trace xs) proof (prove)
goal (2 subgoals):
 1. empty_fail (put_trace [])
 2. \<And>a xs. empty_fail (put_trace xs) \<Longrightarrow> empty_fail (put_trace (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. empty_fail (put_trace xs) \<Longrightarrow> empty_fail (put_trace (a # xs)) proof (prove)
goal:
No subgoals!
theory Trace_Empty_Fail

lemma empty_fail_interference[empty_fail_term]:
  "empty_fail interference" by (simp add: interference_def commit_step_def empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail interference
theory Trace_Empty_Fail

lemma last_st_tr_not_empty:
  "P s \<Longrightarrow> \<exists>xs. P (last_st_tr (map (Pair Env) xs) s')" apply (rule exI[where x="[s]"]) apply (auto simp: last_st_tr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> \<exists>xs. P (last_st_tr (map (Pair Env) xs) s') proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> P (last_st_tr (map (Pair Env) [s]) s') proof (prove)
goal:
No subgoals!
theory Trace_Empty_Fail

lemma empty_fail_Await[empty_fail_term]:
  "\<exists>s. c s \<Longrightarrow> empty_fail (Await c)" by (clarsimp simp: Await_def last_st_tr_not_empty empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>s. c s \<Longrightarrow> empty_fail (Await c)
theory Trace_Empty_Fail

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (select V) = (V \<noteq> {})
theory Trace_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 Trace_Empty_Fail

lemma empty_fail_liftE_eq[simp]:
  "empty_fail (liftE f) = empty_fail f" by (auto simp: liftE_def empty_fail_bindD1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (liftE f) = empty_fail f
theory Trace_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 Trace_Total

lemma validNF_alt_def:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! = (\<forall>s. P s \<longrightarrow> ((\<forall>(r', s') \<in> mres (f s). Q r' s') \<and> \<not> failed (f s)))" by (auto simp: validNF_def valid_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! = (\<forall>s. P s \<longrightarrow> (\<forall>(r', s')\<in>mres (f s). Q r' s') \<and> \<not> failed (f s))
theory Trace_Total

lemma validE_NF_alt_def:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>!" by (clarsimp simp: validE_NF_def validE_def validNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>!
theory Trace_Total

lemma wpc_helper_validNF:
  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!" unfolding wpc_helper_def by clarsimp (metis hoare_vcg_precond_imp no_fail_pre validNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> (case (P, P', P'') of (P, P', P'') \<Rightarrow> \<lambda>(Q, Q', Q''). (\<longrightarrow>) ((\<forall>s. P s \<longrightarrow> Q s) \<and> (\<forall>s. P' s \<longrightarrow> Q' s) \<and> P'' \<subseteq> Q'')) (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!
theory Trace_Total

lemma validNF_make_schematic_post:
  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>!) \<Longrightarrow>
   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>!" by (fastforce simp: valid_def validNF_def no_fail_def mres_def image_def
               split: prod.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>Q s0\<rbrace>! \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')\<rbrace> f \<lbrace>Q'\<rbrace>!