kings-crown/FVELER_Isabelle huggingface dataset:
theory SubMonadLib

lemma (in submonad) fn_stateAssert:
  "fn m >>= (\<lambda>x. stateAssert guard [] >>= (\<lambda>u. n x)) = (fn m >>= n)" apply (simp add: fn_is_sm submonad_fn_def bind_assoc split_def) apply (rule ext) apply (rule bind_apply_cong [OF refl])+ apply (clarsimp simp: stateAssert_def bind_assoc in_monad select_f_def) apply (drule iffD2 [OF replace_preserves_guard]) apply (fastforce simp: bind_def assert_def get_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- fn m;
u <- stateAssert guard [];
n x
od = fn m >>= n proof (prove)
goal (1 subgoal):
 1. do x <- stateAssert guard [];
x <- gets fetch;
x <- select_f (m x);
y <- modify (replace (snd x));
u <- stateAssert guard [];
n (fst x)
od = do x <- stateAssert guard [];
x <- gets fetch;
x <- select_f (m x);
y <- modify (replace (snd x));
n (fst x)
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- stateAssert guard [];
x <- gets fetch;
x <- select_f (m x);
y <- modify (replace (snd x));
u <- stateAssert guard [];
n (fst x)
od) x = (do x <- stateAssert guard [];
x <- gets fetch;
x <- select_f (m x);
y <- modify (replace (snd x));
n (fst x)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb rvc stc. \<lbrakk>(rv, st) \<in> fst (stateAssert guard [] x); (rva, sta) \<in> fst (gets fetch st); (rvb, stb) \<in> fst (select_f (m rva) sta); (rvc, stc) \<in> fst (modify (replace (snd rvb)) stb)\<rbrakk> \<Longrightarrow> (do u <- stateAssert guard [];
n (fst rvb)
od) stc = n (fst rvb) stc proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>guard x; (a, b) \<in> fst (m (fetch x))\<rbrakk> \<Longrightarrow> (do x <- get;
u <- assert (guard x);
n a
od) (replace b x) = n a (replace b x) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>(a, b) \<in> fst (m (fetch x)); guard (replace (?x17 x a b) x)\<rbrakk> \<Longrightarrow> (do x <- get;
u <- assert (guard x);
n a
od) (replace b x) = n a (replace b x) proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma corres_select:
  "(\<forall>s' \<in> S'. \<exists>s \<in> S. rvr s s') \<Longrightarrow> corres_underlying sr nf nf' rvr \<top> \<top> (select S) (select S')" by (clarsimp simp: select_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'\<in>S'. \<exists>s\<in>S. rvr s s' \<Longrightarrow> corres_underlying sr nf nf' rvr (\<lambda>_. True) (\<lambda>_. True) (select S) (select S')
theory SubMonadLib

lemma corres_select_f:
  "\<lbrakk> \<forall>s' \<in> fst S'. \<exists>s \<in> fst S. rvr s s'; nf' \<Longrightarrow> \<not> snd S' \<rbrakk>
      \<Longrightarrow> corres_underlying sr nf nf' rvr \<top> \<top> (select_f S) (select_f S')" by (clarsimp simp: select_f_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s'\<in>fst S'. \<exists>s\<in>fst S. rvr s s'; nf' \<Longrightarrow> \<not> snd S'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' rvr (\<lambda>_. True) (\<lambda>_. True) (select_f S) (select_f S')
theory SubMonadLib

lemma corres_modify':
  "\<lbrakk> (\<forall>s s'. (s, s') \<in> sr \<longrightarrow> (f s, f' s') \<in> sr); r () () \<rbrakk>
      \<Longrightarrow> corres_underlying sr nf nf' r \<top> \<top> (modify f) (modify f')" by (clarsimp simp: modify_def corres_underlying_def bind_def get_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s s'. (s, s') \<in> sr \<longrightarrow> (f s, f' s') \<in> sr; r () ()\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (modify f) (modify f')
theory SubMonadLib

lemma corres_select_f_stronger:
  "\<lbrakk> \<forall>s' \<in> fst S'. \<exists>s \<in> fst S. rvr s s'; nf' \<Longrightarrow> \<not> snd S' \<rbrakk>
      \<Longrightarrow> corres_underlying sr nf nf' rvr \<top> \<top> (select_f S) (select_f S')" by (clarsimp simp: select_f_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s'\<in>fst S'. \<exists>s\<in>fst S. rvr s s'; nf' \<Longrightarrow> \<not> snd S'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' rvr (\<lambda>_. True) (\<lambda>_. True) (select_f S) (select_f S')
theory SubMonadLib

lemma stateAssert_sp:
  "\<lbrace>P\<rbrace> stateAssert Q l \<lbrace>\<lambda>_. P and Q\<rbrace>" by (clarsimp simp: valid_def stateAssert_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> stateAssert Q l \<lbrace>\<lambda>_. P and Q\<rbrace>
theory SubMonadLib

lemma stateAssert_A_top [simp]:
  "stateAssert \<top> l = return ()" by (simp add: stateAssert_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. stateAssert (\<lambda>_. True) l = return ()
theory SubMonadLib

lemma gets_modify_comm:
  "\<And> s. \<lbrakk> g (f s) = g s \<rbrakk> \<Longrightarrow>
   (do x \<leftarrow> modify f; y \<leftarrow> gets g; m x y od) s =
   (do y \<leftarrow> gets g; x \<leftarrow> modify f; m x y od) s" by (simp add: modify_def gets_def get_def bind_def put_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. g (f s) = g s \<Longrightarrow> (do x <- modify f;
gets g >>= m x
od) s = (do y <- gets g;
x <- modify f;
m x y
od) s
theory SubMonadLib

lemma bind_subst_lhs_inv:
  "\<And>s. \<lbrakk> \<And>x s'. P s' \<Longrightarrow> (f x >>= g x) s' = h x s'; \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>; P s \<rbrakk> \<Longrightarrow>
   (do x \<leftarrow> a; y \<leftarrow> f x; g x y od) s = (a >>= h) s" apply (rule bind_apply_cong [OF refl]) apply (drule(2) use_valid) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x s'. P s' \<Longrightarrow> (f x >>= g x) s' = h x s'; \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>; P s\<rbrakk> \<Longrightarrow> (do x <- a;
f x >>= g x
od) s = (a >>= h) s proof (prove)
goal (1 subgoal):
 1. \<And>s rv st. \<lbrakk>\<And>x s'. P s' \<Longrightarrow> (f x >>= g x) s' = h x s'; \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>; P s; (rv, st) \<in> fst (a s)\<rbrakk> \<Longrightarrow> (f rv >>= g rv) st = h rv st proof (prove)
goal (1 subgoal):
 1. \<And>s rv st. \<lbrakk>\<And>x s'. P s' \<Longrightarrow> (f x >>= g x) s' = h x s'; \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>; P s; P st\<rbrakk> \<Longrightarrow> (f rv >>= g rv) st = h rv st proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma gets_comm:
  "do x \<leftarrow> gets f; y \<leftarrow> gets g; m x y od = do y \<leftarrow> gets g; x \<leftarrow> gets f; m x y od" by (simp add: gets_def get_def return_def bind_def)

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

lemma submonad_comm2:
  assumes x1: "submonad_args f r g" and x2: "m = submonad_fn f r g im"
  assumes y: "submonad f' r' g' m'"
  assumes z: "\<And>s x x'. r x (r' x' s) = r' x' (r x s)"
  assumes gp: "\<And>s x. g (r' x s) = g s" and gp': "\<And>s x. g' (r x s) = g' s"
  assumes efim: "empty_fail im" and efim': "empty_fail im'"
  shows      "do x \<leftarrow> m; y \<leftarrow> m' im'; n x y od = do y \<leftarrow> m' im'; x \<leftarrow> m; n x y od" apply (rule submonad_comm[where f'=f' and r'=r', OF x1 _ x2 _ z]) apply (insert y) apply (fastforce simp add: submonad_def) apply (fastforce dest: submonad.fn_is_sm) apply (simp add: efim efim' gp gp')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- m;
m' im' >>= n x
od = do y <- m' im';
x <- m;
n x y
od proof (prove)
goal (6 subgoals):
 1. submonad_args f' r' ?g'
 2. m' im' = submonad_fn f' r' ?g' ?im'
 3. \<And>s x. g (r' x s) = g s
 4. \<And>s x. ?g' (r x s) = ?g' s
 5. empty_fail im
 6. empty_fail ?im' proof (prove)
goal (6 subgoals):
 1. submonad f' r' g' m' \<Longrightarrow> submonad_args f' r' ?g'
 2. submonad f' r' g' m' \<Longrightarrow> m' im' = submonad_fn f' r' ?g' ?im'
 3. \<And>s x. submonad f' r' g' m' \<Longrightarrow> g (r' x s) = g s
 4. \<And>s x. submonad f' r' g' m' \<Longrightarrow> ?g' (r x s) = ?g' s
 5. submonad f' r' g' m' \<Longrightarrow> empty_fail im
 6. submonad f' r' g' m' \<Longrightarrow> empty_fail ?im' proof (prove)
goal (5 subgoals):
 1. submonad f' r' g' m' \<Longrightarrow> m' im' = submonad_fn f' r' g' ?im'
 2. \<And>s x. submonad f' r' g' m' \<Longrightarrow> g (r' x s) = g s
 3. \<And>s x. submonad f' r' g' m' \<Longrightarrow> g' (r x s) = g' s
 4. submonad f' r' g' m' \<Longrightarrow> empty_fail im
 5. submonad f' r' g' m' \<Longrightarrow> empty_fail ?im' proof (prove)
goal (4 subgoals):
 1. \<And>s x. submonad f' r' g' m' \<Longrightarrow> g (r' x s) = g s
 2. \<And>s x. submonad f' r' g' m' \<Longrightarrow> g' (r x s) = g' s
 3. submonad f' r' g' m' \<Longrightarrow> empty_fail im
 4. submonad f' r' g' m' \<Longrightarrow> empty_fail im' proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma submonad_bind_alt:
  assumes x: "submonad_args f r g"
  assumes y: "a = submonad_fn f r g a'" "\<And>rv. b rv = submonad_fn f r g (b' rv)"
  assumes efa: "empty_fail a'" and efb: "\<And>x. empty_fail (b' x)"
  shows      "(a >>= b) = submonad_fn f r g (a' >>= b')" proof - have P: "submonad f r g (submonad_fn f r g)" by (simp add: x submonad_def submonad_axioms_def) have Q: "b = (\<lambda>rv. submonad_fn f r g (b' rv))" by (rule ext) fact+ show ?thesis by (simp add: y Q submonad_bind [OF P P P efa efb]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a >>= b = submonad_fn f r g (a' >>= b') proof (state)
goal (1 subgoal):
 1. a >>= b = submonad_fn f r g (a' >>= b') proof (prove)
goal (1 subgoal):
 1. submonad f r g (submonad_fn f r g) proof (state)
this:
submonad f r g (submonad_fn f r g)

goal (1 subgoal):
 1. a >>= b = submonad_fn f r g (a' >>= b') proof (prove)
goal (1 subgoal):
 1. b = (\<lambda>rv. submonad_fn f r g (b' rv)) proof (state)
this:
b = (\<lambda>rv. submonad_fn f r g (b' rv))

goal (1 subgoal):
 1. a >>= b = submonad_fn f r g (a' >>= b') proof (prove)
goal (1 subgoal):
 1. a >>= b = submonad_fn f r g (a' >>= b') proof (state)
this:
a >>= b = submonad_fn f r g (a' >>= b')

goal:
No subgoals!
theory SubMonadLib

lemma submonad_singleton:
  "submonad_fn fetch replace \<top> (\<lambda>s. ({(rv s, s' s)}, False))
     = (\<lambda>s. ({(rv (fetch s), replace (s' (fetch s)) s)}, False))" apply (rule ext) apply (simp add: submonad_fn_def bind_def gets_def
                put_def get_def modify_def return_def
                select_f_def UNION_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad_fn fetch replace (\<lambda>_. True) (\<lambda>s. ({(rv s, s' s)}, False)) = (\<lambda>s. ({(rv (fetch s), replace (s' (fetch s)) s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s. submonad_fn fetch replace (\<lambda>_. True) (\<lambda>s. ({(rv s, s' s)}, False)) s = ({(rv (fetch s), replace (s' (fetch s)) s)}, False) proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma modify_submonad:
  "\<lbrakk> \<And>s. f s = replace (K_record (f' (fetch s))) s; m = modify f' \<rbrakk>
     \<Longrightarrow> modify f = submonad_fn fetch (replace o K_record) \<top> m" by (simp add: simpler_modify_def submonad_singleton)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. f s = replace (K_record (f' (fetch s))) s; m = modify f'\<rbrakk> \<Longrightarrow> modify f = submonad_fn fetch (replace \<circ> K_record) (\<lambda>_. True) m
theory SubMonadLib

lemma fail_submonad:
  "fail = submonad_fn fetch replace \<top> fail" by (simp add: submonad_fn_def simpler_gets_def return_def
                simpler_modify_def select_f_def bind_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fail = submonad_fn fetch replace (\<lambda>_. True) fail
theory SubMonadLib

lemma return_submonad:
  "submonad_args fetch replace guard \<Longrightarrow>
   return v = submonad_fn fetch replace \<top> (return v)" by (simp add: return_def submonad_singleton submonad_args.args)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad_args fetch replace guard \<Longrightarrow> return v = submonad_fn fetch replace (\<lambda>_. True) (return v)
theory SubMonadLib

lemma assert_opt_submonad:
  "submonad_args fetch replace \<top> \<Longrightarrow>
   assert_opt v = submonad_fn fetch replace \<top> (assert_opt v)" apply (case_tac v, simp_all add: assert_opt_def) apply (rule fail_submonad) apply (rule return_submonad) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad_args fetch replace (\<lambda>_. True) \<Longrightarrow> assert_opt v = submonad_fn fetch replace (\<lambda>_. True) (assert_opt v) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>submonad_args fetch replace (\<lambda>_. True); v = None\<rbrakk> \<Longrightarrow> fail = submonad_fn fetch replace (\<lambda>_. True) fail
 2. \<And>a. \<lbrakk>submonad_args fetch replace (\<lambda>_. True); v = Some a\<rbrakk> \<Longrightarrow> return a = submonad_fn fetch replace (\<lambda>_. True) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>submonad_args fetch replace (\<lambda>_. True); v = Some a\<rbrakk> \<Longrightarrow> return a = submonad_fn fetch replace (\<lambda>_. True) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>submonad_args fetch replace (\<lambda>_. True); v = Some a\<rbrakk> \<Longrightarrow> submonad_args fetch replace (?guard3 a) proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma is_modify:
  "\<And>s. \<lbrakk> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) (replace s)\<rbrace>; empty_fail f;
          no_fail guard f; guard s \<rbrakk>
    \<Longrightarrow> f s = modify replace s" apply (clarsimp simp: bind_def empty_fail_def valid_def no_fail_def
                        stateAssert_def assert_def modify_def get_def put_def
                        return_def fail_def image_def split_def) apply (case_tac "f s") apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) (replace s)\<rbrace>; empty_fail f; no_fail guard f; guard s\<rbrakk> \<Longrightarrow> f s = modify replace s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>x\<in>fst (f s). replace s = snd x; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); guard s\<rbrakk> \<Longrightarrow> f s = ({((), replace s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>x\<in>fst (f s). replace s = snd x; \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>s. guard s \<longrightarrow> \<not> snd (f s); guard s; f s = (a, b)\<rbrakk> \<Longrightarrow> f s = ({((), replace s)}, False) proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma submonad_comm':
  assumes sm1: "submonad f r g m" and sm2: "submonad f' r' g' m'"
  assumes z: "\<And>s x x'. r x (r' x' s) = r' x' (r x s)"
  assumes gp: "\<And>s x. g (r' x s) = g s" and gp': "\<And>s x. g' (r x s) = g' s"
  assumes efim: "empty_fail im" and efim': "empty_fail im'"
  shows      "(do x \<leftarrow> m im; y \<leftarrow> m' im'; n x y od) =
              (do y \<leftarrow> m' im'; x \<leftarrow> m im; n x y od)" apply (rule submonad_comm [where f'=f' and r'=r', OF _ _ _ _ z]) apply (insert sm1 sm2) apply (fastforce dest: submonad.fn_is_sm simp: submonad_def)+ apply (simp add: efim efim' gp gp')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- m im;
m' im' >>= n x
od = do y <- m' im';
x <- m im;
n x y
od proof (prove)
goal (8 subgoals):
 1. submonad_args ?f (\<lambda>a b. r (?x3 a b) b) ?g
 2. submonad_args f' r' ?g'
 3. m im = submonad_fn ?f (\<lambda>a b. r (?x3 a b) b) ?g ?im
 4. m' im' = submonad_fn f' r' ?g' ?im'
 5. \<And>s x. ?g (r' x s) = ?g s
 6. \<And>s x. ?g' (r (?x3 x s) s) = ?g' s
 7. empty_fail ?im
 8. empty_fail ?im'
flex-flex pairs:
\<lambda>s x x'. ?x3 x s \<equiv>\<^sup>? \<lambda>s x x'. ?x3 x (r' x' s) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> submonad_args ?f (\<lambda>a b. r (?x3 a b) b) ?g
 2. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> submonad_args f' r' ?g'
 3. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> m im = submonad_fn ?f (\<lambda>a b. r (?x3 a b) b) ?g ?im
 4. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> m' im' = submonad_fn f' r' ?g' ?im'
 5. \<And>s x. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> ?g (r' x s) = ?g s
 6. \<And>s x. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> ?g' (r (?x3 x s) s) = ?g' s
 7. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> empty_fail ?im
 8. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> empty_fail ?im'
flex-flex pairs:
\<lambda>s x x'. ?x3 x s \<equiv>\<^sup>? \<lambda>s x x'. ?x3 x (r' x' s) proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> g (r' x s) = g s
 2. \<And>s x. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> g' (r x s) = g' s
 3. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> empty_fail im
 4. \<lbrakk>submonad f r g m; submonad f' r' g' m'\<rbrakk> \<Longrightarrow> empty_fail im' proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma hoare_spec_gen_asm:
  "\<lbrakk> F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f \<lbrace>Q\<rbrace>"
  "\<lbrakk> F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding spec_valid_def spec_validE_def validE_def apply (clarsimp simp only: pred_conj_def conj_assoc[symmetric]
               intro!: hoare_gen_asm[unfolded pred_conj_def])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f \<lbrace>Q\<rbrace>) &&& ((F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f' \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f' \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) proof (prove)
goal (1 subgoal):
 1. ((F \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> (P and K F) sa\<rbrace> f \<lbrace>Q\<rbrace>) &&& ((F \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa\<rbrace> f' \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> (P and K F) sa\<rbrace> f' \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>) proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma spec_validE_fail:
  "s \<turnstile> \<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by wp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory LemmaBucket

lemma mresults_fail: "mresults fail = {}" by (simp add: mresults_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mresults fail = {}
theory LemmaBucket

lemma gets_symb_exec_l:
  "corres_underlying sr nf nf' dc P P' (gets f) (return x)" by (simp add: corres_underlying_def return_def simpler_gets_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc P P' (gets f) (return x)
theory LemmaBucket

lemma mapM_wp_inv:
  "(\<And>x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>" apply (rule  valid_return_unit) apply (fold mapM_x_mapM) apply (erule mapM_x_wp_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> do _ <- mapM f xs;
return ()
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma corres_underlying_similar:
  "\<lbrakk> a = a'; b = b'; nf' \<Longrightarrow> no_fail \<top> (f a b) \<rbrakk>
         \<Longrightarrow> corres_underlying Id nf nf' dc \<top> \<top> (f a b) (f a' b')" by (simp add: corres_underlying_def no_fail_def, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = a'; b = b'; nf' \<Longrightarrow> no_fail (\<lambda>_. True) (f a b)\<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' dc (\<lambda>_. True) (\<lambda>_. True) (f a b) (f a' b')
theory LemmaBucket

lemma corres_underlying_gets_pre_lhs:
  "(\<And>x. corres_underlying S nf nf' r (P x) P' (g x) g') \<Longrightarrow>
  corres_underlying S nf nf' r (\<lambda>s. P (f s) s) P' (gets f >>= (\<lambda>x. g x)) g'" apply (simp add: simpler_gets_def bind_def split_def corres_underlying_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. corres_underlying S nf nf' r (P x) P' (g x) g') \<Longrightarrow> corres_underlying S nf nf' r (\<lambda>s. P (f s) s) P' (gets f >>= g) g' proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<forall>xa\<in>S. P x (fst xa) \<and> P' (snd xa) \<longrightarrow> (nf \<longrightarrow> \<not> snd (g x (fst xa))) \<longrightarrow> (\<forall>xb\<in>fst (g' (snd xa)). \<exists>x\<in>fst (g x (fst xa)). (snd x, snd xb) \<in> S \<and> r (fst x) (fst xb)) \<and> (nf' \<longrightarrow> \<not> snd (g' (snd xa)))) \<Longrightarrow> \<forall>x\<in>S. P (f (fst x)) (fst x) \<and> P' (snd x) \<longrightarrow> (nf \<longrightarrow> \<not> snd (g (f (fst x)) (fst x))) \<longrightarrow> nf' \<longrightarrow> \<not> snd (g' (snd x)) proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma mapM_x_inv_wp:
  assumes x: "\<And>s. I s \<Longrightarrow> Q s"
  assumes y: "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>rv. I\<rbrace>"
  assumes z: "\<And>s. I s \<Longrightarrow> P s"
  shows      "\<lbrace>I\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace>" apply (rule hoare_post_imp) apply (erule x) apply (rule mapM_x_wp) apply (rule hoare_pre_imp [OF _ y]) apply (erule z) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> Q s
 2. \<lbrace>I\<rbrace> mapM_x m xs \<lbrace>?Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. I\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> ?S4 \<Longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>rv. I\<rbrace>
 2. set xs \<subseteq> ?S4 proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> ?S4; I s\<rbrakk> \<Longrightarrow> P s
 2. \<And>x. x \<in> ?S4 \<Longrightarrow> x \<in> set xs
 3. set xs \<subseteq> ?S4 proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> ?S4 \<Longrightarrow> x \<in> set xs
 2. set xs \<subseteq> ?S4 proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> set xs proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma isRight_rel_sum_comb2:
  "\<lbrakk> (f \<oplus> r) v v'; isRight v' \<rbrakk>
       \<Longrightarrow> isRight v \<and> r (theRight v) (theRight v')" by (cases v; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f \<oplus> r) v v'; isRight v'\<rbrakk> \<Longrightarrow> isRight v \<and> r (theRight v) (theRight v')