kings-crown/FVELER_Isabelle huggingface dataset:
theory MonadicRewrite

lemma monadic_rewrite_transverse:
  "\<lbrakk> monadic_rewrite False True Q c b; monadic_rewrite F E P a b \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and Q) a c" by (auto simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite False True Q c b; monadic_rewrite F E P a b\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and Q) a c
theory MonadicRewrite

lemma monadic_rewrite_weaken_failure:
  "\<lbrakk> monadic_rewrite True True P f f'; no_fail P' f; no_fail Q' f' \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and P' and Q') f f'" by (clarsimp simp: monadic_rewrite_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite True True P f f'; no_fail P' f; no_fail Q' f'\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and P' and Q') f f'
theory MonadicRewrite

lemma monadic_rewrite_corres_l_generic:
  "\<lbrakk> monadic_rewrite F E Q a a';
     corres_underlying R nf nf' r P P' a' c;
     F \<longrightarrow> nf \<rbrakk>
   \<Longrightarrow> corres_underlying R nf nf' r (P and Q) P' a c" by (fastforce simp add: corres_underlying_def monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E Q a a'; corres_underlying R nf nf' r P P' a' c; F \<longrightarrow> nf\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r (P and Q) P' a c
theory MonadicRewrite

lemma monadic_rewrite_corres_l:
  "\<lbrakk> monadic_rewrite False E Q a a';
     corres_underlying R nf nf' r P P' a' c \<rbrakk>
   \<Longrightarrow> corres_underlying R nf nf' r (P and Q) P' a c" by (rule monadic_rewrite_corres_l_generic, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite False E Q a a'; corres_underlying R nf nf' r P P' a' c\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r (P and Q) P' a c
theory MonadicRewrite

lemma monadic_rewrite_corres_r_generic:
  "\<lbrakk> monadic_rewrite F E Q c' c;
     corres_underlying R nf nf'' r P P' a c';
     F \<longrightarrow> nf''; nf' \<longrightarrow> nf'' \<rbrakk>
   \<Longrightarrow> corres_underlying R nf nf' r P (P' and Q) a c" by (fastforce simp: corres_underlying_def monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E Q c' c; corres_underlying R nf nf'' r P P' a c'; F \<longrightarrow> nf''; nf' \<longrightarrow> nf''\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P (P' and Q) a c
theory MonadicRewrite

lemma monadic_rewrite_corres_r_generic_ex_abs:
  "\<lbrakk> monadic_rewrite F E (\<lambda>s'. Q s' \<and> ex_abs_underlying sr P s') c' c;
     corres_underlying sr nf nf'' r P P' a c';
     F \<longrightarrow> nf''; nf' \<longrightarrow> nf'' \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r P (P' and Q) a c" by (fastforce simp: corres_underlying_def monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E (\<lambda>s'. Q s' \<and> ex_abs_underlying sr P s') c' c; corres_underlying sr nf nf'' r P P' a c'; F \<longrightarrow> nf''; nf' \<longrightarrow> nf''\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (P' and Q) a c
theory MonadicRewrite

lemma monadic_rewrite_corres_r:
  "\<lbrakk> monadic_rewrite False True Q c c';
     corres_underlying R nf nf' r P P' a c' \<rbrakk>
   \<Longrightarrow> corres_underlying R nf nf' r P (P' and Q) a c" by (erule (1) monadic_rewrite_corres_r_generic[OF monadic_rewrite_sym], simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite False True Q c c'; corres_underlying R nf nf' r P P' a c'\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P (P' and Q) a c
theory MonadicRewrite

lemma oblivious_monadic_rewrite:
  "oblivious f m \<Longrightarrow> monadic_rewrite F E \<top> (do modify f; m od) (do m; modify f od)" by (clarsimp simp: monadic_rewrite_def oblivious_modify_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f m \<Longrightarrow> monadic_rewrite F E (\<lambda>_. True) (do modify f;
m
od) (do m;
modify f
od)
theory MonadicRewrite

lemma wpc_helper_monadic_rewrite:
  "monadic_rewrite F E Q m m'
   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (monadic_rewrite F E P m m')" by (auto simp: wpc_helper_def elim!: monadic_rewrite_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E Q m m' \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (monadic_rewrite F E P m m')
theory BCorres_UL

lemma wpc_helper_bcorres:
  "bcorres_underlying t f g \<Longrightarrow>  wpc_helper P Q (bcorres_underlying t f g)" by (simp add: wpc_helper_def split: prod.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t f g \<Longrightarrow> wpc_helper P Q (bcorres_underlying t f g)
theory BCorres_UL

lemma s_bcorres_underlying_split[wp_split]:
  "(\<And>r s'. (r,s') \<in> fst (f s) \<Longrightarrow>  (s_bcorres_underlying t (g r) (g' r) s')) \<Longrightarrow>
   s_bcorres_underlying t f f' s \<Longrightarrow>
   s_bcorres_underlying t (f >>= g) (f' >>= g') s" by (clarsimp simp: s_bcorres_underlying_def bind_def) force

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

lemma bcorres_underlying_split[wp_split]:
  "(\<And>r. (bcorres_underlying t (g r) (g' r))) \<Longrightarrow>
   bcorres_underlying t f f' \<Longrightarrow>
   bcorres_underlying t (f >>= g) (f' >>= g')" by (simp add: bcorres_underlying_def s_bcorres_underlying_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. bcorres_underlying t (g r) (g' r); bcorres_underlying t f f'\<rbrakk> \<Longrightarrow> bcorres_underlying t (f >>= g) (f' >>= g')
theory BCorres_UL

lemma get_s_bcorres_underlying[wp]:
  "s_bcorres_underlying t (f s) (f' (t s)) s \<Longrightarrow> s_bcorres_underlying t (get >>= f) (get >>= f') s" by (simp add: gets_def s_bcorres_underlying_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres_underlying t (f s) (f' (t s)) s \<Longrightarrow> s_bcorres_underlying t (get >>= f) (get >>= f') s
theory BCorres_UL

lemma gets_s_bcorres_underlying[wp]:
  "x' (t s) = x s \<Longrightarrow>  s_bcorres_underlying t (gets x) (gets x') s" by (simp add: s_bcorres_underlying_def gets_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x' (t s) = x s \<Longrightarrow> s_bcorres_underlying t (gets x) (gets x') s
theory BCorres_UL

lemma gets_bcorres_underlying[wp]:
  "(\<And>s. x' (t s) = x s) \<Longrightarrow> bcorres_underlying t (gets x) (gets x')" by (simp add: bcorres_underlying_def gets_s_bcorres_underlying)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. x' (t s) = x s) \<Longrightarrow> bcorres_underlying t (gets x) (gets x')
theory BCorres_UL

lemma gets_map_bcorres_underlying[wp]:
  "(\<And>s. f' (t s) p = f s p) \<Longrightarrow> bcorres_underlying t (gets_map f p) (gets_map f' p)" by (simp add: gets_map_def bcorres_underlying_def s_bcorres_underlying_def simpler_gets_def
                bind_def assert_opt_def fail_def return_def
        split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. f' (t s) p = f s p) \<Longrightarrow> bcorres_underlying t (gets_map f p) (gets_map f' p)
theory BCorres_UL

lemma gets_bcorres_underlying':
  "(\<And>xa. bcorres_underlying t (f (x xa)) (f' (x' (t xa)))) \<Longrightarrow>
  bcorres_underlying t (gets x >>= f) (gets x' >>= f')" by (wpsimp simp: gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>xa. bcorres_underlying t (f (x xa)) (f' (x' (t xa)))) \<Longrightarrow> bcorres_underlying t (gets x >>= f) (gets x' >>= f')
theory BCorres_UL

lemma assert_bcorres_underlying[wp]:
  "f = f' \<Longrightarrow> bcorres_underlying t (assert f) (assert f')" by (simp add: assert_def bcorres_underlying_def return_def s_bcorres_underlying_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f = f' \<Longrightarrow> bcorres_underlying t (assert f) (assert f')
theory BCorres_UL

lemma return_bcorres[wp]:
  "bcorres_underlying t (return x) (return x)" by (simp add:return_def bcorres_underlying_def s_bcorres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t (return x) (return x)
theory BCorres_UL

lemma drop_sbcorres_underlying:
  "bcorres_underlying t f g \<Longrightarrow> s_bcorres_underlying t f g s" by (simp add: bcorres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t f g \<Longrightarrow> s_bcorres_underlying t f g s
theory BCorres_UL

lemma use_sbcorres_underlying:
  "(\<And>s. s_bcorres_underlying t f g s) \<Longrightarrow> bcorres_underlying t f g" by (simp add: bcorres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s_bcorres_underlying t f g s) \<Longrightarrow> bcorres_underlying t f g
theory BCorres_UL

lemma s_bcorres_underlying_splitE[wp_split]:
  "(\<And>r s'. (Inr r,s') \<in> fst (f s) \<Longrightarrow> s_bcorres_underlying t (g r) (g' r) s') \<Longrightarrow>
   s_bcorres_underlying t f f' s \<Longrightarrow>
   s_bcorres_underlying t (f >>=E g) (f' >>=E g') s" by (wpsimp simp: bindE_def lift_def split: sum.splits | rule conjI drop_sbcorres_underlying)+

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

lemma get_s_bcorres_underlyingE[wp]:
  "s_bcorres_underlying t (f s) (f' (t s)) s \<Longrightarrow>
   s_bcorres_underlying t (liftE get >>=E f) (liftE get >>=E f') s" by (simp add: gets_def s_bcorres_underlying_def get_def bindE_def bind_def return_def liftE_def lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres_underlying t (f s) (f' (t s)) s \<Longrightarrow> s_bcorres_underlying t (liftE get >>=E f) (liftE get >>=E f') s
theory BCorres_UL

lemma bcorres_underlying_splitE[wp_split]:
  "(\<And>r. bcorres_underlying t (g r) (g' r)) \<Longrightarrow>
   bcorres_underlying t f f' \<Longrightarrow>
   bcorres_underlying t (f >>=E g) (f' >>=E g')" by (simp add: bcorres_underlying_def s_bcorres_underlying_splitE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. bcorres_underlying t (g r) (g' r); bcorres_underlying t f f'\<rbrakk> \<Longrightarrow> bcorres_underlying t (f >>=E g) (f' >>=E g')
theory BCorres_UL

lemma liftE_s_bcorres_underlying[wp]:
  "s_bcorres_underlying t f f' s \<Longrightarrow> s_bcorres_underlying t (liftE f) (liftE f') s" by (wpsimp simp: liftE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres_underlying t f f' s \<Longrightarrow> s_bcorres_underlying t (liftE f) (liftE f') s
theory BCorres_UL

lemma liftE_bcorres_underlying[wp]:
  "bcorres_underlying t f f' \<Longrightarrow>  bcorres_underlying t (liftE f) (liftE f')" by (simp add: bcorres_underlying_def liftE_s_bcorres_underlying)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (liftE f) (liftE f')
theory BCorres_UL

lemma returnOk_bcorres_underlying[wp]:
  "bcorres_underlying t (returnOk x) (returnOk x)" by (wpsimp simp: returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t (returnOk x) (returnOk x)
theory BCorres_UL

lemma whenE_s_bcorres_underlying[wp]:
  "\<lbrakk> \<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> s_bcorres_underlying t f f' s; P = P' \<rbrakk> \<Longrightarrow>
   s_bcorres_underlying t (whenE P f) (whenE P' f') s" by (wpsimp simp: whenE_def|rule drop_sbcorres_underlying)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> s_bcorres_underlying t f f' s; P = P'\<rbrakk> \<Longrightarrow> s_bcorres_underlying t (whenE P f) (whenE P' f') s
theory BCorres_UL

lemma select_s_bcorres_underlying[wp]:
  "A \<subseteq> B \<Longrightarrow> s_bcorres_underlying t (select A) (select B) s" by (simp add: s_bcorres_underlying_def select_def image_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> s_bcorres_underlying t (select A) (select B) s
theory BCorres_UL

lemma fail_s_bcorres_underlying[wp]:
  "s_bcorres_underlying t fail fail s" by (simp add: s_bcorres_underlying_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres_underlying t fail fail s
theory BCorres_UL

lemma fail_bcorres_underlying[wp]:
  "bcorres_underlying t fail fail" by (simp add: bcorres_underlying_def fail_s_bcorres_underlying)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t fail fail
theory BCorres_UL

lemma assertE_bcorres_underlying[wp]:
  "bcorres_underlying t (assertE P) (assertE P)" by (wpsimp simp: assertE_def returnOk_def|rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t (assertE P) (assertE P)
theory BCorres_UL

lemma when_s_bcorres_underlying[wp]:
  "(P \<Longrightarrow> s_bcorres_underlying t f f' s) \<Longrightarrow> s_bcorres_underlying t (when P f) (when P f') s" by (simp add: return_s_bcorres_underlying when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> s_bcorres_underlying t f f' s) \<Longrightarrow> s_bcorres_underlying t (when P f) (when P f') s
theory BCorres_UL

lemma when_bcorres_underlying[wp]:
  "(P \<Longrightarrow> bcorres_underlying t f f') \<Longrightarrow> bcorres_underlying t (when P f) (when P f')" by (simp add: bcorres_underlying_def when_s_bcorres_underlying)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> bcorres_underlying t f f') \<Longrightarrow> bcorres_underlying t (when P f) (when P f')
theory BCorres_UL

lemma put_bcorres_underlying[wp]:
  "t f = f' \<Longrightarrow> bcorres_underlying t (put f) (put f')" by (simp add: bcorres_underlying_def s_bcorres_underlying_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t f = f' \<Longrightarrow> bcorres_underlying t (put f) (put f')
theory BCorres_UL

lemma modify_bcorres_underlying[wp]:
  "(\<And>x. t (f x) = f' (t x)) \<Longrightarrow> bcorres_underlying t (modify f) (modify f')" by (wpsimp simp: modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. t (f x) = f' (t x)) \<Longrightarrow> bcorres_underlying t (modify f) (modify f')
theory BCorres_UL

lemma sequence_x_bcorres_underlying[wp]:
  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow>
   bcorres_underlying t (sequence_x (map f xs)) (sequence_x (map f' xs))" by (induct xs; wpsimp simp: sequence_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (sequence_x (map f xs)) (sequence_x (map f' xs))
theory BCorres_UL

lemma sequence_bcorres_underlying[wp]:
  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow>
   bcorres_underlying t (sequence (map f xs)) (sequence (map f' xs))" by (induct xs; wpsimp simp: sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (sequence (map f xs)) (sequence (map f' xs))
theory BCorres_UL

lemma mapM_x_bcorres_underlying[wp]:
  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapM_x f xs) (mapM_x f' xs)" by (wpsimp simp: mapM_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapM_x f xs) (mapM_x f' xs)
theory BCorres_UL

lemma mapM_bcorres_underlying[wp]:
  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapM f xs) (mapM f' xs)" by (simp add: mapM_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapM f xs) (mapM f' xs)
theory BCorres_UL

lemma gets_s_bcorres_underlyingE':
  "s_bcorres_underlying t (f (x s)) (f' (x' (t s))) s \<Longrightarrow>
   s_bcorres_underlying t (liftE (gets x) >>=E f) (liftE (gets x') >>=E f') s" by (simp add: gets_def liftE_def lift_def bindE_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres_underlying t (f (x s)) (f' (x' (t s))) s \<Longrightarrow> s_bcorres_underlying t (liftE (gets x) >>=E f) (liftE (gets x') >>=E f') s
theory BCorres_UL

lemma bcorres_underlying_filterM[wp]:
  "(\<And>x. bcorres_underlying t (a x) (a' x)) \<Longrightarrow> bcorres_underlying t (filterM a b) (filterM a' b)" by (induct b; wpsimp simp: filterM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. bcorres_underlying t (a x) (a' x)) \<Longrightarrow> bcorres_underlying t (filterM a b) (filterM a' b)
theory BCorres_UL

lemma option_rec_bcorres_underlying[wp_split]:
  "(\<And>x y. bcorres_underlying t (g x y) (g' x y)) \<Longrightarrow>
   (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow>
   bcorres_underlying t (rec_option f g a b) (rec_option f' g' a b)" by (cases a, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. bcorres_underlying t (g x y) (g' x y); \<And>x. bcorres_underlying t (f x) (f' x)\<rbrakk> \<Longrightarrow> bcorres_underlying t (rec_option f g a b) (rec_option f' g' a b)
theory BCorres_UL

lemma bcorres_underlying_mapME[wp]:
  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapME f r) (mapME f' r)" by (induct r; wpsimp simp: mapME_def sequenceE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapME f r) (mapME f' r)
theory BCorres_UL

lemma handle2_bcorres_underlying[wp]:
  "bcorres_underlying t f f' \<Longrightarrow>
   (\<And>x. bcorres_underlying t (g x) (g' x)) \<Longrightarrow>
   bcorres_underlying t (f <handle2> g) (f' <handle2> g')" by (wpsimp simp: handleE'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcorres_underlying t f f'; \<And>x. bcorres_underlying t (g x) (g' x)\<rbrakk> \<Longrightarrow> bcorres_underlying t (f <handle2> g) (f' <handle2> g')
theory BCorres_UL

lemma liftME_bcorres_underlying[wp]:
  "bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (liftME a f) (liftME a f')" by (wpsimp simp: liftME_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (liftME a f) (liftME a f')
theory BCorres_UL

lemma zipWithM_x_bcorres[wp]:
  "(\<And>x y. bcorres_underlying t (f x y) (f' x y) ) \<Longrightarrow>
   bcorres_underlying t (zipWithM_x f xs ys) (zipWithM_x f' xs ys)" by (wpsimp simp: zipWithM_x_def zipWith_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. bcorres_underlying t (f x y) (f' x y)) \<Longrightarrow> bcorres_underlying t (zipWithM_x f xs ys) (zipWithM_x f' xs ys)
theory BCorres_UL

lemma mapME_x_bcorres_underlying[wp]:
  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapME_x f xs) (mapME_x f' xs)" by (induct xs; wpsimp simp: mapME_x_def sequenceE_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapME_x f xs) (mapME_x f' xs)
theory BCorres_UL

lemma liftE_bind_bcorres[wp]:
  "bcorres_underlying t (f >>= g) (f' >>= g') \<Longrightarrow>
   bcorres_underlying t (liftE f >>=E g) (liftE f' >>=E g')" by (simp add: gets_def bcorres_underlying_def s_bcorres_underlying_def get_def bind_def return_def
                split_def liftE_def bindE_def lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t (f >>= g) (f' >>= g') \<Longrightarrow> bcorres_underlying t (liftE f >>=E g) (liftE f' >>=E g')
theory BCorres_UL

lemma select_f_bcorres[wp]: "bcorres_underlying t (select_f f) (select_f f)" by (fastforce simp: select_f_def bcorres_underlying_def s_bcorres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t (select_f f) (select_f f)
theory BCorres_UL

lemma bcorres_underlying_if[wp]:
  "(b \<Longrightarrow> bcorres_underlying t f f') \<Longrightarrow>
   (\<not>b \<Longrightarrow> bcorres_underlying t g g') \<Longrightarrow>
   bcorres_underlying t (if b then f else g) (if b then f' else g')" by (case_tac b; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<Longrightarrow> bcorres_underlying t f f'; \<not> b \<Longrightarrow> bcorres_underlying t g g'\<rbrakk> \<Longrightarrow> bcorres_underlying t (if b then f else g) (if b then f' else g')
theory BCorres_UL

lemma unlessb_corres_underlying[wp]:
  "bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (unless a f) (unless a f')" by (wpsimp simp: unless_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (unless a f) (unless a f')
theory BCorres_UL

lemma select_bcorres_underlying[wp]:
  "A \<subseteq> B \<Longrightarrow> bcorres_underlying t (select A) (select B)" by (fastforce simp: bcorres_underlying_def select_def s_bcorres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> bcorres_underlying t (select A) (select B)
theory BCorres_UL

lemma catch_bcorres[wp]:
  "bcorres_underlying t f f' \<Longrightarrow>
   (\<And>x. bcorres_underlying t (g x) (g' x)) \<Longrightarrow>
   bcorres_underlying t (f <catch> g) (f' <catch> g')" unfolding catch_def by wpsimp

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

lemma whenE_bcorres_underlying[wp]:
  "\<lbrakk> \<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> bcorres_underlying t f f'; P = P' \<rbrakk> \<Longrightarrow>
  bcorres_underlying t (whenE P f) (whenE P' f')" unfolding whenE_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> bcorres_underlying t f f'; P = P'\<rbrakk> \<Longrightarrow> bcorres_underlying t (whenE P f) (whenE P' f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> bcorres_underlying t f f'; P = P'\<rbrakk> \<Longrightarrow> bcorres_underlying t (if P then f else returnOk ()) (if P' then f' else returnOk ())
theory BCorres_UL

lemma unlessE_bcorres[wp]:
  "bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (unlessE P f) (unlessE P f')" by (wpsimp simp: unlessE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (unlessE P f) (unlessE P f')
theory BCorres_UL

lemma alternative_bcorres[wp]:
  "\<lbrakk> bcorres_underlying t f f';  bcorres_underlying t g g' \<rbrakk> \<Longrightarrow>
  bcorres_underlying t (f \<sqinter> g) (f' \<sqinter> g')" by (fastforce simp: alternative_def bcorres_underlying_def s_bcorres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcorres_underlying t f f'; bcorres_underlying t g g'\<rbrakk> \<Longrightarrow> bcorres_underlying t (f \<sqinter> g) (f' \<sqinter> g')