kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_No_Trace

lemma no_trace_mapM_x[no_trace_cond]:
  "(\<And>m. m \<in> f ` set ms \<Longrightarrow> no_trace m) \<Longrightarrow> no_trace (mapM_x f ms)" unfolding mapM_x_def by (fastforce intro: no_trace_sequence_x)

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

lemma no_trace_mapME[no_trace_cond]:
  "(\<And>m. m \<in> f ` set xs \<Longrightarrow> no_trace m) \<Longrightarrow> no_trace (mapME f xs)" unfolding mapME_def by (fastforce intro: no_trace_sequenceE)

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

lemma no_trace_mapME_x[no_trace_cond]:
  "(\<And>m'. m' \<in> f ` set xs \<Longrightarrow> no_trace m') \<Longrightarrow> no_trace (mapME_x f xs)" unfolding mapME_x_def by (fastforce intro: no_trace_sequenceE_x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m'. m' \<in> f ` set xs \<Longrightarrow> no_trace m') \<Longrightarrow> no_trace (mapME_x f xs) proof (prove)
goal (1 subgoal):
 1. (\<And>m'. m' \<in> f ` set xs \<Longrightarrow> no_trace m') \<Longrightarrow> no_trace (sequenceE_x (map f xs))
theory Trace_No_Trace

lemma no_trace_filterM[no_trace_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> no_trace (P m)) \<Longrightarrow> no_trace (filterM P ms)" by (induct ms; wpsimp wp: no_trace_terminal split_del: if_split)

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

lemma no_trace_zipWithM_x[no_trace_cond]:
  "(\<And>x y. no_trace (f x y)) \<Longrightarrow> no_trace (zipWithM_x f xs ys)" unfolding zipWithM_x_def zipWith_def by (fastforce intro: no_trace_sequence_x)

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

lemma no_trace_zipWithM[no_trace_cond]:
  "(\<And>x y. no_trace (f x y)) \<Longrightarrow> no_trace (zipWithM f xs ys)" unfolding zipWithM_def zipWith_def by (fastforce intro: no_trace_sequence)

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

lemma no_trace_foldM[no_trace_cond]:
  "(\<And>x y. no_trace (m x y)) \<Longrightarrow> no_trace (foldM m xs a)" unfolding foldM_def by (induct xs; wpsimp wp: no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. no_trace (m x y)) \<Longrightarrow> no_trace (foldM m xs a) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. no_trace (m x y)) \<Longrightarrow> no_trace (foldr (\<lambda>p q. q >>= m p) xs (return a))
theory Trace_No_Trace

lemma no_trace_foldME[no_trace_cond]:
  "(\<And>x y. no_trace (m x y)) \<Longrightarrow> no_trace (foldME m a xs)" unfolding foldME_def by (induct xs; wpsimp wp: no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. no_trace (m x y)) \<Longrightarrow> no_trace (foldME m a xs) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. no_trace (m x y)) \<Longrightarrow> no_trace (foldr (\<lambda>p q. q >>=E swp m p) xs (returnOk a))
theory Trace_No_Trace

lemma no_trace_maybeM[no_trace_cond]:
  "\<forall>x. no_trace (f x) \<Longrightarrow> no_trace (maybeM f t)" unfolding maybeM_def by (fastforce intro: no_trace_terminal split: option.splits)

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

lemma no_trace_notM[no_trace_cond]:
  "no_trace A \<Longrightarrow> no_trace (notM A)" unfolding notM_def by (wpsimp wp: no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace A \<Longrightarrow> no_trace (notM A) proof (prove)
goal (1 subgoal):
 1. no_trace A \<Longrightarrow> no_trace (do c <- A;
return (\<not> c)
od)
theory Trace_No_Trace

lemma no_trace_ifM[no_trace_cond]:
  "\<lbrakk> no_trace P; no_trace a; no_trace b \<rbrakk> \<Longrightarrow> no_trace (ifM P a b)" unfolding ifM_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace P; no_trace a; no_trace b\<rbrakk> \<Longrightarrow> no_trace (ifM P a b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace P; no_trace a; no_trace b\<rbrakk> \<Longrightarrow> no_trace (do c <- P;
if c then a else b
od)
theory Trace_No_Trace

lemma no_trace_ifME[no_trace_cond]:
  "\<lbrakk> no_trace P; no_trace a; no_trace b \<rbrakk> \<Longrightarrow> no_trace (ifME P a b)" unfolding ifME_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace P; no_trace a; no_trace b\<rbrakk> \<Longrightarrow> no_trace (ifME P a b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace P; no_trace a; no_trace b\<rbrakk> \<Longrightarrow> no_trace (doE c <- P;
if c then a else b
odE)
theory Trace_No_Trace

lemma no_trace_whenM[no_trace_cond]:
  "\<lbrakk> no_trace P; no_trace f \<rbrakk> \<Longrightarrow> no_trace (whenM P f)" unfolding whenM_def by (wpsimp wp: no_trace_terminal no_trace_cond)

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

lemma no_trace_orM[no_trace_cond]:
  "\<lbrakk> no_trace A; no_trace B \<rbrakk> \<Longrightarrow> no_trace (orM A B)" unfolding orM_def by (wpsimp wp: no_trace_terminal no_trace_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace A; no_trace B\<rbrakk> \<Longrightarrow> no_trace (orM A B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace A; no_trace B\<rbrakk> \<Longrightarrow> no_trace (ifM A (return True) B)
theory Trace_No_Trace

lemma no_trace_andM[no_trace_cond]:
  "\<lbrakk> no_trace A; no_trace B \<rbrakk> \<Longrightarrow> no_trace (andM A B)" unfolding andM_def by (wpsimp wp: no_trace_terminal no_trace_cond)

\<comment> \<open>While the parallel composition of traceless functions doesn't make much sense, this
   still might be useful to handle trivial goals as part of a proof by contradiction.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace A; no_trace B\<rbrakk> \<Longrightarrow> no_trace (andM A B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace A; no_trace B\<rbrakk> \<Longrightarrow> no_trace (ifM A B (return False))
theory Trace_No_Trace

lemma no_trace_parallel[no_trace_cond]:
  "\<lbrakk> no_trace f; no_trace g \<rbrakk> \<Longrightarrow> no_trace (parallel f g)" by (fastforce simp: parallel_def2 no_trace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; no_trace g\<rbrakk> \<Longrightarrow> no_trace (parallel f g)
theory Trace_Prefix_Closed

lemma in_fst_snd_image_eq:
  "x \<in> fst ` S = (\<exists>y. (x, y) \<in> S)"
  "y \<in> snd ` S = (\<exists>x. (x, y) \<in> S)" by (auto elim: image_eqI[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> fst ` S) = (\<exists>y. (x, y) \<in> S) &&& (y \<in> snd ` S) = (\<exists>x. (x, y) \<in> S)
theory Trace_Prefix_Closed

lemma in_fst_snd_image:
  "(x, y) \<in> S \<Longrightarrow> x \<in> fst ` S"
  "(x, y) \<in> S \<Longrightarrow> y \<in> snd ` S" by (auto simp: in_fst_snd_image_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> S \<Longrightarrow> x \<in> fst ` S) &&& ((x, y) \<in> S \<Longrightarrow> y \<in> snd ` S)
theory Trace_Prefix_Closed

lemma prefix_closed_is_triple[wp_trip]:
  "prefix_closed f = triple_judgement \<top> f (\<lambda>() f. id prefix_closed f)" by (simp add: triple_judgement_def split: unit.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f = triple_judgement (\<lambda>_. True) f (\<lambda>(). id prefix_closed)
theory Trace_Prefix_Closed

lemma prefix_closed_bind[wp_split]:
  "\<lbrakk>prefix_closed f; \<And>x. prefix_closed (g x)\<rbrakk> \<Longrightarrow> prefix_closed (f >>= g)" apply (subst prefix_closed_def, clarsimp simp: bind_def) apply (auto 4 4 simp: Cons_eq_append_conv split: tmres.split_asm
                 dest!: prefix_closedD[rotated] elim: rev_bexI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<And>x. prefix_closed (g x)\<rbrakk> \<Longrightarrow> prefix_closed (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ba ab bb. \<lbrakk>prefix_closed f; \<And>x. prefix_closed (g x); (ab, bb) \<in> f s; ((a, b) # xs, ba) \<in> (case bb of Failed \<Rightarrow> {(ab, Failed)} | Incomplete \<Rightarrow> {(ab, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ ab, y)) ` g rv s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (xs, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s) proof (prove)
goal:
No subgoals!
theory Trace_Prefix_Closed

lemma prefix_closed_case_option[prefix_closed_cond]:
  assumes f: "prefix_closed f"
  assumes g: "\<And>x. prefix_closed (g x)"
  shows "prefix_closed (case_option f g x)" by (clarsimp simp: f g split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (case x of None \<Rightarrow> f | Some x \<Rightarrow> g x)
theory Trace_Prefix_Closed

lemma prefix_closed_alt[prefix_closed_cond]:
  "\<lbrakk> prefix_closed f; prefix_closed g \<rbrakk> \<Longrightarrow> prefix_closed (f \<sqinter> g)" apply (subst prefix_closed_def) apply (clarsimp simp add: alternative_def;
         fastforce dest: prefix_closedD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; prefix_closed g\<rbrakk> \<Longrightarrow> prefix_closed (f \<sqinter> g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; prefix_closed g\<rbrakk> \<Longrightarrow> \<forall>s x xs. x # xs \<in> fst ` (f \<sqinter> g) s \<longrightarrow> (xs, Incomplete) \<in> (f \<sqinter> g) s proof (prove)
goal:
No subgoals!
theory Trace_Prefix_Closed

lemma prefix_closed_unless[prefix_closed_cond]:
  "\<lbrakk>\<not>P \<Longrightarrow> prefix_closed f\<rbrakk> \<Longrightarrow> prefix_closed (unless P f)" by (simp add: unless_def when_def prefix_closed_terminal)

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

lemma prefix_closed_if[prefix_closed_cond]:
  "\<lbrakk> P \<Longrightarrow> prefix_closed f; \<not>P \<Longrightarrow> prefix_closed g \<rbrakk> \<Longrightarrow> prefix_closed (if P then f else g)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> prefix_closed f; \<not> P \<Longrightarrow> prefix_closed g\<rbrakk> \<Longrightarrow> prefix_closed (if P then f else g)
theory Trace_Prefix_Closed

lemma prefix_closed_apply[prefix_closed_cond]:
  "prefix_closed (f (g x)) \<Longrightarrow> prefix_closed (f $ g x)" by simp

\<comment> \<open>FIXME: make proof nicer\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (f (g x)) \<Longrightarrow> prefix_closed (f $ g x)
theory Trace_Prefix_Closed

lemma prefix_closed_liftM[prefix_closed_cond]:
  "prefix_closed m \<Longrightarrow> prefix_closed (liftM f m)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed m \<Longrightarrow> prefix_closed (liftM f m)
theory Trace_Prefix_Closed

lemma prefix_closed_whenE[prefix_closed_cond]:
  "\<lbrakk> G \<Longrightarrow> prefix_closed f \<rbrakk> \<Longrightarrow> prefix_closed (whenE G f)" by (simp add: whenE_def prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (G \<Longrightarrow> prefix_closed f) \<Longrightarrow> prefix_closed (whenE G f)
theory Trace_Prefix_Closed

lemma prefix_closed_unlessE[prefix_closed_cond]:
  "\<lbrakk> \<not> G \<Longrightarrow> prefix_closed f \<rbrakk> \<Longrightarrow> prefix_closed (unlessE G f)" by (simp add: unlessE_def prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> G \<Longrightarrow> prefix_closed f) \<Longrightarrow> prefix_closed (unlessE G f)
theory Trace_Prefix_Closed

lemma prefix_closed_liftE[prefix_closed_cond]:
  "prefix_closed f \<Longrightarrow> prefix_closed (liftE f)" unfolding liftE_def by (wpsimp wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> prefix_closed (liftE f) proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> prefix_closed (do r <- f;
return (Inr r)
od)
theory Trace_Prefix_Closed

lemma prefix_closed_lift[prefix_closed_cond]:
  "\<lbrakk>\<And>y. x = Inr y \<Longrightarrow> prefix_closed (f y)\<rbrakk> \<Longrightarrow> prefix_closed (lift f x)" unfolding lift_def by (wpsimp wp: prefix_closed_terminal split: sum.splits)

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

lemma prefix_closed_bindE[wp_split]:
  "\<lbrakk> prefix_closed f; \<And>rv. prefix_closed (g rv)\<rbrakk> \<Longrightarrow> prefix_closed (f >>=E g)" unfolding bindE_def by (wpsimp wp: prefix_closed_cond)

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

lemma prefix_closed_condition[prefix_closed_cond]:
  "\<lbrakk>prefix_closed A; prefix_closed B\<rbrakk> \<Longrightarrow> prefix_closed (condition C A B)" unfolding condition_def prefix_closed_def apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed A; prefix_closed B\<rbrakk> \<Longrightarrow> prefix_closed condition C
  A
  B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s x xs. x # xs \<in> fst ` A s \<longrightarrow> (xs, Incomplete) \<in> A s; \<forall>s x xs. x # xs \<in> fst ` B s \<longrightarrow> (xs, Incomplete) \<in> B s\<rbrakk> \<Longrightarrow> \<forall>s x xs. x # xs \<in> fst ` (if C s then A s else B s) \<longrightarrow> (xs, Incomplete) \<in> (if C s then A s else B s) proof (prove)
goal:
No subgoals!
theory Trace_Prefix_Closed

lemma prefix_closed_mapM[prefix_closed_cond]:
  "\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> prefix_closed (f x)\<rbrakk> \<Longrightarrow> prefix_closed (mapM f xs)" apply (induct xs) apply (simp add: mapM_def sequence_def prefix_closed_terminal) apply (clarsimp simp: mapM_Cons) apply (wpsimp wp: prefix_closed_terminal) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> set xs \<Longrightarrow> prefix_closed (f x)) \<Longrightarrow> prefix_closed (mapM f xs) proof (prove)
goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> prefix_closed (f x)) \<Longrightarrow> prefix_closed (mapM f [])
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> prefix_closed (f x)) \<Longrightarrow> prefix_closed (mapM f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> prefix_closed (f x)\<rbrakk> \<Longrightarrow> prefix_closed (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> prefix_closed (f x)) \<Longrightarrow> prefix_closed (mapM f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> prefix_closed (f x)\<rbrakk> \<Longrightarrow> prefix_closed (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>prefix_closed (mapM f xs); \<And>x. x = a \<or> x \<in> set xs \<Longrightarrow> prefix_closed (f x)\<rbrakk> \<Longrightarrow> prefix_closed (do y <- f a;
ys <- mapM f xs;
return (y # ys)
od) proof (prove)
goal:
No subgoals!
theory Trace_Prefix_Closed

lemma prefix_closed_catch[prefix_closed_cond]:
  "\<lbrakk> prefix_closed f; \<And>x. prefix_closed (g x) \<rbrakk> \<Longrightarrow> prefix_closed (catch f g)" unfolding catch_def by (wpsimp wp: prefix_closed_terminal split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<And>x. prefix_closed (g x)\<rbrakk> \<Longrightarrow> prefix_closed (f <catch> g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<And>x. prefix_closed (g x)\<rbrakk> \<Longrightarrow> prefix_closed (do x <- f;
case x of Inl e \<Rightarrow> g e | Inr b \<Rightarrow> return b
od)
theory Trace_Prefix_Closed

lemma prefix_closed_liftME[prefix_closed_cond]:
  "prefix_closed m \<Longrightarrow> prefix_closed (liftME f m)" unfolding liftME_def by (wpsimp wp: prefix_closed_terminal)

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

lemma prefix_closed_handle'[prefix_closed_cond]:
  "\<lbrakk>prefix_closed f; \<And>e. prefix_closed (handler e)\<rbrakk> \<Longrightarrow> prefix_closed (f <handle2> handler)" unfolding handleE'_def by (wpsimp wp: prefix_closed_terminal split: sum.split)

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

lemma prefix_closed_handleE[prefix_closed_cond]:
  "\<lbrakk> prefix_closed L; \<And>r. prefix_closed (R r) \<rbrakk> \<Longrightarrow> prefix_closed (L <handle> R)" unfolding handleE_def by (simp add: prefix_closed_cond)

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

lemma prefix_closed_handle_elseE[prefix_closed_cond]:
  "\<lbrakk> prefix_closed f; \<And>r. prefix_closed (g r); \<And>r. prefix_closed (h r) \<rbrakk> \<Longrightarrow> prefix_closed (f <handle> g <else> h)" unfolding handle_elseE_def by (wpsimp wp: prefix_closed_terminal split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<And>r. prefix_closed (g r); \<And>r. prefix_closed (h r)\<rbrakk> \<Longrightarrow> prefix_closed (f <handle> g <else> h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<And>r. prefix_closed (g r); \<And>r. prefix_closed (h r)\<rbrakk> \<Longrightarrow> prefix_closed (do v <- f;
case v of Inl e \<Rightarrow> g e | Inr v' \<Rightarrow> h v'
od)
theory Trace_Prefix_Closed

lemma prefix_closed_sequence[prefix_closed_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> prefix_closed m) \<Longrightarrow> prefix_closed (sequence ms)" unfolding sequence_def by (induct ms; wpsimp wp: prefix_closed_terminal)

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

lemma prefix_closed_sequence_x[prefix_closed_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> prefix_closed m) \<Longrightarrow> prefix_closed (sequence_x ms)" unfolding sequence_x_def by (induct ms; wpsimp wp: prefix_closed_terminal)

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

lemma prefix_closed_sequenceE[prefix_closed_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> prefix_closed m) \<Longrightarrow> prefix_closed (sequenceE ms)" unfolding sequenceE_def by (induct ms; wpsimp wp: prefix_closed_terminal)

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

lemma prefix_closed_sequenceE_x[prefix_closed_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> prefix_closed m) \<Longrightarrow> prefix_closed (sequenceE_x ms)" unfolding sequenceE_x_def by (induct ms; wpsimp wp: prefix_closed_terminal)

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

lemma prefix_closed_mapM_x[prefix_closed_cond]:
  "(\<And>m. m \<in> f ` set ms \<Longrightarrow> prefix_closed m) \<Longrightarrow> prefix_closed (mapM_x f ms)" unfolding mapM_x_def by (fastforce intro: prefix_closed_sequence_x)

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

lemma prefix_closed_mapME_x[prefix_closed_cond]:
  "(\<And>m'. m' \<in> f ` set xs \<Longrightarrow> prefix_closed m') \<Longrightarrow> prefix_closed (mapME_x f xs)" unfolding mapME_x_def by (fastforce intro: prefix_closed_sequenceE_x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m'. m' \<in> f ` set xs \<Longrightarrow> prefix_closed m') \<Longrightarrow> prefix_closed (mapME_x f xs) proof (prove)
goal (1 subgoal):
 1. (\<And>m'. m' \<in> f ` set xs \<Longrightarrow> prefix_closed m') \<Longrightarrow> prefix_closed (sequenceE_x (map f xs))