kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_Monad_Equations

lemma mapM_x_split:
  "(\<forall>x \<in> set xs. \<forall>y \<in> set xs. do z \<leftarrow> g y; f x od = do (z :: unit) \<leftarrow> f x; g y od)
   \<Longrightarrow> mapM_x (\<lambda>x. do z \<leftarrow> f x; g x od) xs = do y \<leftarrow> mapM_x f xs; mapM_x g xs od" apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons bind_assoc) apply (subst bind_assoc[symmetric], subst mapM_x_comm[where f=f and g="g x" for x]) apply simp apply (simp add: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. \<forall>y\<in>set xs. do z <- g y;
f x
od = do z <- f x;
g y
od \<Longrightarrow> mapM_x (\<lambda>x. do z <- f x;
g x
od) xs = do y <- mapM_x f xs;
mapM_x g xs
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>mapM_x (\<lambda>x. do z <- f x;
g x
od) xs = do y <- mapM_x f xs;
mapM_x g xs
od; do z <- g a;
f a
od = do z <- f a;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f a
od = do z <- f a;
g y
od) \<and> (\<forall>x\<in>set xs. do z <- g a;
f x
od = do z <- f x;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f x
od = do z <- f x;
g y
od))\<rbrakk> \<Longrightarrow> do x <- f a;
y <- g a;
y <- mapM_x f xs;
mapM_x g xs
od = do x <- f a;
y <- mapM_x f xs;
y <- g a;
mapM_x g xs
od proof (prove)
goal (2 subgoals):
 1. \<And>a xs x. \<lbrakk>mapM_x (\<lambda>x. do z <- f x;
g x
od) xs = do y <- mapM_x f xs;
mapM_x g xs
od; do z <- g a;
f a
od = do z <- f a;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f a
od = do z <- f a;
g y
od) \<and> (\<forall>x\<in>set xs. do z <- g a;
f x
od = do z <- f x;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f x
od = do z <- f x;
g y
od))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. do y <- g a;
f x
od = do y <- f x;
g a
od
 2. \<And>a xs. \<lbrakk>mapM_x (\<lambda>x. do z <- f x;
g x
od) xs = do y <- mapM_x f xs;
mapM_x g xs
od; do z <- g a;
f a
od = do z <- f a;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f a
od = do z <- f a;
g y
od) \<and> (\<forall>x\<in>set xs. do z <- g a;
f x
od = do z <- f x;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f x
od = do z <- f x;
g y
od))\<rbrakk> \<Longrightarrow> do x <- f a;
y <- do y <- mapM_x f xs;
g a
od;
mapM_x g xs
od = do x <- f a;
y <- mapM_x f xs;
y <- g a;
mapM_x g xs
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>mapM_x (\<lambda>x. do z <- f x;
g x
od) xs = do y <- mapM_x f xs;
mapM_x g xs
od; do z <- g a;
f a
od = do z <- f a;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f a
od = do z <- f a;
g y
od) \<and> (\<forall>x\<in>set xs. do z <- g a;
f x
od = do z <- f x;
g a
od \<and> (\<forall>y\<in>set xs. do z <- g y;
f x
od = do z <- f x;
g y
od))\<rbrakk> \<Longrightarrow> do x <- f a;
y <- do y <- mapM_x f xs;
g a
od;
mapM_x g xs
od = do x <- f a;
y <- mapM_x f xs;
y <- g a;
mapM_x g xs
od proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma mapM_x_put:
  "mapM_x put xs = unless (xs = []) (put (last xs))" apply (induct xs rule: rev_induct) apply (simp add: mapM_x_Nil unless_def when_def) apply (simp add: mapM_x_append mapM_x_Cons mapM_x_Nil) apply (simp add: bind_def unless_def when_def put_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x put xs = unless (xs = []) (put (last xs)) proof (prove)
goal (2 subgoals):
 1. mapM_x put [] = unless ([] = []) (put (last []))
 2. \<And>x xs. mapM_x put xs = unless (xs = []) (put (last xs)) \<Longrightarrow> mapM_x put (xs @ [x]) = unless (xs @ [x] = []) (put (last (xs @ [x]))) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. mapM_x put xs = unless (xs = []) (put (last xs)) \<Longrightarrow> mapM_x put (xs @ [x]) = unless (xs @ [x] = []) (put (last (xs @ [x]))) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. mapM_x put xs = unless (xs = []) (put (last xs)) \<Longrightarrow> do xa <- unless (xs = []) (put (last xs));
put x
od = put x proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma put_trace_mapM_x:
  "put_trace xs = mapM_x put_trace_elem (rev xs)" by (induct xs; simp add: mapM_x_Nil mapM_x_append mapM_x_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. put_trace xs = mapM_x put_trace_elem (rev xs)
theory Trace_Monad_Equations

lemma rev_surj:
  "surj rev" by (rule surjI[where f=rev], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. surj rev
theory Trace_Monad_Equations

lemma select_image:
  "select (f ` S) = do x \<leftarrow> select S; return (f x) od" by (auto simp add: bind_def select_def return_def Sigma_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select (f ` S) = do x <- select S;
return (f x)
od
theory Trace_Monad_Equations

lemma env_steps_repeat:
  "env_steps = repeat env_step" apply (simp add: env_step_def repeat_choice env_steps_def
                   select_early) apply (simp add: put_trace_elem_put_comm) apply (simp add: mapM_x_split put_trace_elem_put_comm put_trace_put_comm
                   mapM_x_put) apply (simp add: put_trace_mapM_x rev_map mapM_x_map o_def) apply (subst rev_surj[symmetric], simp add: select_image bind_assoc) apply (rule arg_cong2[where f=bind, OF refl ext]) apply (simp add: bind_def get_def put_def unless_def when_def return_def) apply (simp add: last_st_tr_def hd_map hd_rev) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. env_steps = repeat env_step proof (prove)
goal (1 subgoal):
 1. do xs <- select UNIV;
s <- get;
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od = select UNIV >>= mapM_x (\<lambda>s'. do y <- put_trace_elem (Env, s');
put s'
od) proof (prove)
goal (1 subgoal):
 1. do xs <- select UNIV;
s <- get;
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od = select UNIV >>= mapM_x (\<lambda>s'. do y <- put s';
put_trace_elem (Env, s')
od) proof (prove)
goal (1 subgoal):
 1. do xs <- select UNIV;
s <- get;
y <- put (last_st_tr (map (Pair Env) xs) s);
put_trace (map (Pair Env) xs)
od = do xs <- select UNIV;
y <- unless (xs = []) (put (last xs));
mapM_x (\<lambda>s'. put_trace_elem (Env, s')) xs
od proof (prove)
goal (1 subgoal):
 1. do xs <- select UNIV;
s <- get;
y <- put (last_st_tr (map (Pair Env) xs) s);
mapM_x (\<lambda>x. put_trace_elem (Env, x)) (rev xs)
od = do xs <- select UNIV;
y <- unless (xs = []) (put (last xs));
mapM_x (\<lambda>s'. put_trace_elem (Env, s')) xs
od proof (prove)
goal (1 subgoal):
 1. do x <- select UNIV;
s <- get;
y <- put (last_st_tr (map (Pair Env) (rev x)) s);
mapM_x (\<lambda>x. put_trace_elem (Env, x)) x
od = do xs <- select UNIV;
y <- unless (xs = []) (put (last xs));
mapM_x (\<lambda>s'. put_trace_elem (Env, s')) xs
od proof (prove)
goal (1 subgoal):
 1. \<And>x. do s <- get;
y <- put (last_st_tr (map (Pair Env) (rev x)) s);
mapM_x (\<lambda>x. put_trace_elem (Env, x)) x
od = do y <- unless (x = []) (put (last x));
mapM_x (\<lambda>s'. put_trace_elem (Env, s')) x
od proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<noteq> [] \<longrightarrow> (\<lambda>s. mapM_x (\<lambda>x. put_trace_elem (Env, x)) x (last_st_tr (map (Pair Env) (rev x)) s)) = (\<lambda>s. mapM_x (\<lambda>s'. put_trace_elem (Env, s')) x (last x)) proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma repeat_n_plus:
  "repeat_n (n + m) f = do repeat_n n f; repeat_n m f od" by (induct n; simp add: bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. repeat_n (n + m) f = do repeat_n n f;
repeat_n m f
od
theory Trace_No_Trace

lemma no_trace_emp:
  "\<lbrakk>no_trace f; (tr, r) \<in> f s\<rbrakk> \<Longrightarrow> tr = []" by (simp add: no_traceD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; (tr, r) \<in> f s\<rbrakk> \<Longrightarrow> tr = []
theory Trace_No_Trace

lemma no_trace_Incomplete_mem:
  "no_trace f \<Longrightarrow> (tr, Incomplete) \<notin> f s" by (auto dest: no_traceD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace f \<Longrightarrow> (tr, Incomplete) \<notin> f s
theory Trace_No_Trace

lemma no_trace_Incomplete_eq:
  "\<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> res \<noteq> Incomplete" by (auto dest: no_traceD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> res \<noteq> Incomplete
theory Trace_No_Trace

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

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

lemma no_trace_bind[wp_split]:
  "\<lbrakk>no_trace f; \<forall>rv. no_trace (g rv)\<rbrakk>
   \<Longrightarrow> no_trace (do rv \<leftarrow> f; g rv od)" apply (subst no_trace_def) apply (clarsimp simp: bind_def split: tmres.split_asm;
         fastforce dest: no_traceD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; \<forall>rv. no_trace (g rv)\<rbrakk> \<Longrightarrow> no_trace (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; \<forall>rv. no_trace (g rv)\<rbrakk> \<Longrightarrow> \<forall>tr res s. (tr, res) \<in> (f >>= g) s \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete proof (prove)
goal:
No subgoals!
theory Trace_No_Trace

lemma no_trace_get[no_trace_terminal]:
  "no_trace get" by (simp add: no_trace_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace get
theory Trace_No_Trace

lemma no_trace_put[no_trace_terminal]:
  "no_trace (put s)" by (simp add: no_trace_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (put s)
theory Trace_No_Trace

lemma no_trace_modify[no_trace_terminal]:
  "no_trace (modify f)" by (wpsimp simp: modify_def wp: no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (modify f)
theory Trace_No_Trace

lemma no_trace_return[no_trace_terminal]:
  "no_trace (return v)" by (simp add: no_trace_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (return v)
theory Trace_No_Trace

lemma no_trace_fail[no_trace_terminal]:
  "no_trace fail" by (simp add: no_trace_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace fail
theory Trace_No_Trace

lemma no_trace_returnOk[no_trace_terminal]:
  "no_trace (returnOk v)" by (simp add: returnOk_def no_trace_terminal)

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

lemma no_trace_gets[no_trace_terminal]:
  "no_trace (gets f)" by (wpsimp simp: gets_def wp: no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (gets f)
theory Trace_No_Trace

lemma no_trace_assert[no_trace_terminal]:
  "no_trace (assert P)" by (simp add: assert_def no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (assert P)
theory Trace_No_Trace

lemma no_trace_case_option[no_trace_cond]:
  assumes f: "no_trace f"
  assumes g: "\<And>x. no_trace (g x)"
  shows "no_trace (case_option f g x)" by (clarsimp simp: f g split: option.split)

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

lemma no_trace_assert_opt[no_trace_terminal]:
  "no_trace (assert_opt Q)" by (simp add: assert_opt_def no_trace_terminal no_trace_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (assert_opt Q)
theory Trace_No_Trace

lemma no_trace_alt[no_trace_cond]:
  "\<lbrakk> no_trace f; no_trace g \<rbrakk> \<Longrightarrow> no_trace (f \<sqinter> g)" apply (subst no_trace_def) apply (clarsimp simp add: alternative_def;
         fastforce dest: no_traceD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; no_trace g\<rbrakk> \<Longrightarrow> no_trace (f \<sqinter> g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; no_trace g\<rbrakk> \<Longrightarrow> \<forall>tr res s. (tr, res) \<in> (f \<sqinter> g) s \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete proof (prove)
goal:
No subgoals!
theory Trace_No_Trace

lemma no_trace_when[no_trace_cond]:
  "\<lbrakk>P \<Longrightarrow> no_trace f\<rbrakk> \<Longrightarrow> no_trace (when P f)" by (simp add: when_def no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> no_trace f) \<Longrightarrow> no_trace (when P f)
theory Trace_No_Trace

lemma no_trace_unless[no_trace_cond]:
  "\<lbrakk>\<not>P \<Longrightarrow> no_trace f\<rbrakk> \<Longrightarrow> no_trace (unless P f)" by (simp add: unless_def when_def no_trace_terminal)

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

lemma no_trace_if[no_trace_cond]:
  "\<lbrakk> P \<Longrightarrow> no_trace f; \<not>P \<Longrightarrow> no_trace g \<rbrakk> \<Longrightarrow> no_trace (if P then f else g)" by simp

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

lemma no_trace_apply[no_trace_cond]:
  "no_trace (f (g x)) \<Longrightarrow> no_trace (f $ g x)" by simp

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

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

lemma no_trace_liftM[no_trace_cond]:
  "no_trace m \<Longrightarrow> no_trace (liftM f m)" by simp

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

lemma no_trace_assertE[no_trace_terminal]:
  "no_trace (assertE P)" by (simp add: assertE_def no_trace_terminal)

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

lemma no_trace_whenE[no_trace_cond]:
  "\<lbrakk> G \<Longrightarrow> no_trace f \<rbrakk> \<Longrightarrow> no_trace (whenE G f)" by (simp add: whenE_def no_trace_terminal)

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

lemma no_trace_unlessE[no_trace_cond]:
  "\<lbrakk> \<not> G \<Longrightarrow> no_trace f \<rbrakk> \<Longrightarrow> no_trace (unlessE G f)" by (simp add: unlessE_def no_trace_terminal)

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

lemma no_trace_throwError[no_trace_terminal]:
  "no_trace (throwError e)" by (simp add: throwError_def no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (throwError e)
theory Trace_No_Trace

lemma no_trace_liftE[no_trace_cond]:
  "no_trace f \<Longrightarrow> no_trace (liftE f)" unfolding liftE_def by (wpsimp wp: no_trace_terminal)

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

lemma no_trace_gets_the[no_trace_terminal]:
  "no_trace (gets_the f)" unfolding gets_the_def by (wpsimp wp: no_trace_terminal)

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

lemma no_trace_lift[no_trace_cond]:
  "\<lbrakk>\<And>y. x = Inr y \<Longrightarrow> no_trace (f y)\<rbrakk> \<Longrightarrow> no_trace (lift f x)" unfolding lift_def by (wpsimp wp: no_trace_terminal split: sum.splits)

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

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

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

lemma no_trace_gets_map[no_trace_terminal]:
  "no_trace (gets_map f p)" unfolding gets_map_def by (wpsimp wp: no_trace_terminal)

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

lemma no_trace_state_assert[no_trace_terminal]:
  "no_trace (state_assert P)" unfolding state_assert_def by (wpsimp wp: no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (state_assert P) proof (prove)
goal (1 subgoal):
 1. no_trace (do s <- get;
assert (P s)
od)
theory Trace_No_Trace

lemma no_trace_condition[no_trace_cond]:
  "\<lbrakk>no_trace A; no_trace B\<rbrakk> \<Longrightarrow> no_trace (condition C A B)" unfolding condition_def no_trace_def apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace A; no_trace B\<rbrakk> \<Longrightarrow> no_trace condition C
  A
  B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>tr res s. (tr, res) \<in> A s \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; \<forall>tr res s. (tr, res) \<in> B s \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> \<forall>tr res s. (tr, res) \<in> (if C s then A s else B s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete proof (prove)
goal (1 subgoal):
 1. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> A s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; \<forall>tr res. (\<exists>s. (tr, res) \<in> B s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; C s \<longrightarrow> (tr, res) \<in> A s; \<not> C s \<longrightarrow> (tr, res) \<in> B s\<rbrakk> \<Longrightarrow> tr = [] \<and> res \<noteq> Incomplete proof (prove)
goal:
No subgoals!
theory Trace_No_Trace

lemma no_trace_catch[no_trace_cond]:
  "\<lbrakk> no_trace f; \<And>x. no_trace (g x) \<rbrakk> \<Longrightarrow> no_trace (catch f g)" unfolding catch_def by (wpsimp wp: no_trace_terminal split: sum.split)

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

lemma no_trace_state_select[no_trace_terminal]:
  "no_trace (state_select F)" unfolding state_select_def2 by (wpsimp wp: no_trace_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (state_select F) proof (prove)
goal (1 subgoal):
 1. no_trace (do s <- get;
S <- return {s'. (s, s') \<in> F};
assert (S \<noteq> {});
select S >>= put
od)
theory Trace_No_Trace

lemma no_trace_liftME[no_trace_cond]:
  "no_trace m \<Longrightarrow> no_trace (liftME f m)" unfolding liftME_def by (wpsimp wp: no_trace_terminal)

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

lemma no_trace_handle'[no_trace_cond]:
  "\<lbrakk>no_trace f; \<And>e. no_trace (handler e)\<rbrakk> \<Longrightarrow> no_trace (f <handle2> handler)" unfolding handleE'_def by (wpsimp wp: no_trace_terminal split: sum.split)

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

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

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

lemma no_trace_handle_elseE[no_trace_cond]:
  "\<lbrakk> no_trace f; \<And>r. no_trace (g r); \<And>r. no_trace (h r) \<rbrakk> \<Longrightarrow> no_trace (f <handle> g <else> h)" unfolding handle_elseE_def by (wpsimp wp: no_trace_terminal split: sum.split)

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

lemma no_trace_sequence[no_trace_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> no_trace m) \<Longrightarrow> no_trace (sequence ms)" unfolding sequence_def by (induct ms; wpsimp wp: no_trace_terminal)

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

lemma no_trace_sequence_x[no_trace_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> no_trace m) \<Longrightarrow> no_trace (sequence_x ms)" unfolding sequence_x_def by (induct ms; wpsimp wp: no_trace_terminal)

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

lemma no_trace_sequenceE[no_trace_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> no_trace m) \<Longrightarrow> no_trace (sequenceE ms)" unfolding sequenceE_def by (induct ms; wpsimp wp: no_trace_terminal)

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

lemma no_trace_sequenceE_x[no_trace_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> no_trace m) \<Longrightarrow> no_trace (sequenceE_x ms)" unfolding sequenceE_x_def by (induct ms; wpsimp wp: no_trace_terminal)

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