kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_More_VCG

lemma validE_case_prod:
  "\<lbrakk> \<And>x y. validE (P x y) (f x y) Q E \<rbrakk> \<Longrightarrow> validE (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q E" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrace>P x y\<rbrace> f x y \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>case v of (x, xa) \<Rightarrow> P x xa\<rbrace> case v of (x, y) \<Rightarrow> f x y \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_More_VCG

lemma valid_pre_satisfies_post:
  "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>" by (clarsimp simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s r' s'. P s \<Longrightarrow> Q r' s') \<Longrightarrow> \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>
theory Nondet_More_VCG

lemma validE_pre_satisfies_post:
  "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s'; \<And>s r' s'. P s \<Longrightarrow> R r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace>" by (clarsimp simp: validE_def2 split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s r' s'. P s \<Longrightarrow> Q r' s'; \<And>s r' s'. P s \<Longrightarrow> R r' s'\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>
theory Nondet_More_VCG

lemma hoare_validE_R_conjI:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - ; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, - \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, -" by (clarsimp simp: Ball_def validE_R_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, -
theory Nondet_More_VCG

lemma hoare_validE_E_conjI:
  "\<lbrakk> \<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace> ; \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace> \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" by (clarsimp simp: Ball_def validE_E_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>
theory Nondet_More_VCG

lemma validE_R_post_conjD1:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Nondet_More_VCG

lemma throw_opt_wp[wp]:
  "\<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding throw_opt_def by wpsimp auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if v = None then E ex else Q (the v)\<rbrace> case v of None \<Rightarrow> throwError ex | Some v \<Rightarrow> returnOk v \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_More_VCG

lemma hoare_name_pre_state2:
  "(\<And>s. \<lbrace>P and ((=) s)\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (auto simp: valid_def intro: hoare_name_pre_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrace>P and (=) s\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
theory Nondet_More_VCG

lemma returnOk_E': "\<lbrace>P\<rbrace> returnOk r -,\<lbrace>E\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk r -, \<lbrace>E\<rbrace>
theory Nondet_More_VCG

lemma throwError_R': "\<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>,-" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>, -
theory Nondet_Det

lemma return_det[iff]:
  "det (return x)" by (simp add: det_def return_def)

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

lemma put_det[iff]:
  "det (put s)" by (simp add: det_def put_def)

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

lemma get_det[iff]:
  "det get" by (simp add: det_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det get
theory Nondet_Det

lemma det_gets[iff]:
  "det (gets f)" by (auto simp add: gets_def det_def get_def return_def bind_def)

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

lemma det_UN:
  "det f \<Longrightarrow> (\<Union>x \<in> fst (f s). g x) = (g (THE x. x \<in> fst (f s)))" unfolding det_def by (smt (verit) SUP_eq_const emptyE fst_conv singletonD singletonI the1_equality)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> \<Union> (g ` fst (f s)) = g (THE x. x \<in> fst (f s)) proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<exists>r. f s = ({r}, False) \<Longrightarrow> \<Union> (g ` fst (f s)) = g (THE x. x \<in> fst (f s))
theory Nondet_Det

lemma bind_detI[simp, intro!]:
  "\<lbrakk> det f; \<forall>x. det (g x) \<rbrakk> \<Longrightarrow> det (f >>= g)" unfolding bind_def det_def apply (erule all_reg[rotated]) apply clarsimp by (metis fst_conv snd_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det f; \<forall>x. det (g x)\<rbrakk> \<Longrightarrow> det (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. \<exists>r. f s = ({r}, False); \<forall>x s. \<exists>r. g x s = ({r}, False)\<rbrakk> \<Longrightarrow> \<forall>s. \<exists>r. (\<Union> (fst ` (\<lambda>(x, y). g x y) ` fst (f s)), True \<in> snd ` (\<lambda>(x, y). g x y) ` fst (f s) \<or> snd (f s)) = ({r}, False) proof (prove)
goal (1 subgoal):
 1. \<forall>x s. \<exists>r. g x s = ({r}, False) \<Longrightarrow> \<forall>x. (\<exists>r. f x = ({r}, False)) \<longrightarrow> (\<exists>r. (\<Union> (fst ` (\<lambda>(x, y). g x y) ` fst (f x)), True \<in> snd ` (\<lambda>(x, y). g x y) ` fst (f x) \<or> snd (f x)) = ({r}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>\<forall>x s. \<exists>a b. g x s = ({(a, b)}, False); f x = ({(a, b)}, False)\<rbrakk> \<Longrightarrow> (\<exists>aa ba. fst (g a b) = {(aa, ba)}) \<and> \<not> snd (g a b)
theory Nondet_Det

lemma det_modify[iff]:
  "det (modify f)" by (simp add: modify_def)

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

lemma the_run_state_det:
  "\<lbrakk> s' \<in> fst (M s); det M \<rbrakk> \<Longrightarrow> the_run_state M s = s'" by (simp add: the_run_stateI det_set_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> fst (M s); det M\<rbrakk> \<Longrightarrow> the_run_state M s = s'
theory Monad_Lists

lemma mapME_Cons:
  "mapME m (x # xs) = (doE y \<leftarrow> m x; ys \<leftarrow> (mapME m xs); returnOk (y # ys) odE)" by (simp add: mapME_def sequenceE_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME m (x # xs) = doE y <- m x;
ys <- mapME m xs;
returnOk (y # ys)
odE
theory Monad_Lists

lemma mapME_Nil : "mapME f [] = returnOk []" unfolding mapME_def by (simp add: sequenceE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME f [] = returnOk [] proof (prove)
goal (1 subgoal):
 1. sequenceE (map f []) = returnOk []
theory Monad_Lists

lemma zipWithM_x_inv:
  assumes x: "\<And>x y. m x y \<lbrace>P\<rbrace>"
  shows      "length xs = length ys \<Longrightarrow> zipWithM_x m xs ys \<lbrace>P\<rbrace>" by (rule zipWithM_x_inv', rule x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> \<lbrace>P\<rbrace> zipWithM_x m xs ys \<lbrace>\<lambda>_. P\<rbrace>
theory Monad_Lists

lemma sequence_x_Cons: "\<And>x xs. sequence_x (x # xs) = (x >>= (\<lambda>_. sequence_x xs))" by (simp add: sequence_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. sequence_x (x # xs) = do _ <- x;
sequence_x xs
od
theory Monad_Lists

lemma mapM_Cons: "mapM m (x # xs) = (do y \<leftarrow> m x; ys \<leftarrow> (mapM m xs); return (y # ys) od)" by (simp add: mapM_def sequence_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM m (x # xs) = do y <- m x;
ys <- mapM m xs;
return (y # ys)
od
theory Monad_Lists

lemma mapM_Nil:
  "mapM m [] = return []" by (simp add: mapM_def sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM m [] = return []
theory Monad_Lists

lemma zipWithM_x_mapM:
 "zipWithM_x f as bs = (mapM (case_prod f) (zip as bs) >>= (\<lambda>_. return ()))" apply (simp add: zipWithM_x_def zipWith_def) apply (induct ("zip as bs")) apply (simp add: sequence_x_def mapM_def sequence_def) apply (simp add: sequence_x_Cons mapM_Cons bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x f as bs = do _ <- mapM (\<lambda>(x, y). f x y) (zip as bs);
return ()
od proof (prove)
goal (1 subgoal):
 1. sequence_x (map2 f as bs) = do _ <- mapM (\<lambda>(x, y). f x y) (zip as bs);
return ()
od proof (prove)
goal (2 subgoals):
 1. sequence_x (map (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) []) = do _ <- mapM (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) [];
return ()
od
 2. \<And>a list. sequence_x (map (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) list) = do _ <- mapM (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) list;
return ()
od \<Longrightarrow> sequence_x (map (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) (a # list)) = do _ <- mapM (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) (a # list);
return ()
od proof (prove)
goal (1 subgoal):
 1. \<And>a list. sequence_x (map (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) list) = do _ <- mapM (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) list;
return ()
od \<Longrightarrow> sequence_x (map (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) (a # list)) = do _ <- mapM (\<lambda>a. case a of (a, b) \<Rightarrow> f a b) (a # list);
return ()
od proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_x_mapM:
  "mapM_x m l = (mapM m l >>= (\<lambda>x. return ()))" apply (simp add: mapM_x_def sequence_x_def mapM_def sequence_def) apply (induct l, simp_all add: Let_def bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x m l = do x <- mapM m l;
return ()
od proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. do _ <- x;
y
od) (map m l) (return ()) = do x <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map m l) (return []);
return ()
od proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_x_Nil:
  "mapM_x f [] = return ()" unfolding mapM_x_def sequence_x_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f [] = return () proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. do _ <- x;
y
od) (map f []) (return ()) = return ()
theory Monad_Lists

lemma sequence_xappend1:
  "sequence_x (xs @ [x]) = (sequence_x xs >>= (\<lambda>_. x))" by (induct xs) (simp add: sequence_x_def, simp add: sequence_x_Cons bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sequence_x (xs @ [x]) = do _ <- sequence_x xs;
x
od
theory Monad_Lists

lemma mapM_append_single:
  "mapM_x f (xs @ [y]) = (mapM_x f xs >>= (\<lambda>_. f y))" unfolding mapM_x_def by (simp add: sequence_xappend1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f (xs @ [y]) = do _ <- mapM_x f xs;
f y
od proof (prove)
goal (1 subgoal):
 1. sequence_x (map f (xs @ [y])) = do _ <- sequence_x (map f xs);
f y
od
theory Monad_Lists

lemma mapM_x_Cons:
  "mapM_x m (x # xs) = (do m x; mapM_x m xs od)" by (simp add: mapM_x_def sequence_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x m (x # xs) = do m x;
mapM_x m xs
od
theory Monad_Lists

lemma zipWithM_x_mapM_x:
  "zipWithM_x f as bs = mapM_x (\<lambda>(x, y). f x y) (zip as bs)" apply (subst zipWithM_x_mapM) apply (subst mapM_x_mapM) apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x f as bs = mapM_x (\<lambda>(x, y). f x y) (zip as bs) proof (prove)
goal (1 subgoal):
 1. do _ <- mapM (\<lambda>(x, y). f x y) (zip as bs);
return ()
od = mapM_x (\<lambda>(x, y). f x y) (zip as bs) proof (prove)
goal (1 subgoal):
 1. do _ <- mapM (\<lambda>(x, y). f x y) (zip as bs);
return ()
od = do x <- mapM (\<lambda>(x, y). f x y) (zip as bs);
return ()
od proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma zipWithM_x_append1:
  fixes f :: "'b \<Rightarrow> 'c \<Rightarrow> ('a, unit) nondet_monad"
  assumes ls: "length xs = length ys"
  shows "(zipWithM_x f (xs @ [x]) (ys @ [y])) = (zipWithM_x f xs ys >>= (\<lambda>_. f x y))" unfolding zipWithM_x_def zipWith_def by (subst zip_append [OF ls], simp, rule sequence_xappend1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x f (xs @ [x]) (ys @ [y]) = do _ <- zipWithM_x f xs ys;
f x y
od proof (prove)
goal (1 subgoal):
 1. sequence_x (map2 f (xs @ [x]) (ys @ [y])) = do _ <- sequence_x (map2 f xs ys);
f x y
od
theory Monad_Lists

lemma zipWithM_x_Cons:
  assumes ls: "length xs = length ys"
  shows "(zipWithM_x f (x # xs) (y # ys)) = (f x y >>=  (\<lambda>_. zipWithM_x f xs ys))" unfolding zipWithM_x_def zipWith_def by (simp, rule sequence_x_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x f (x # xs) (y # ys) = do _ <- f x y;
zipWithM_x f xs ys
od proof (prove)
goal (1 subgoal):
 1. sequence_x (map2 f (x # xs) (y # ys)) = do _ <- f x y;
sequence_x (map2 f xs ys)
od
theory Monad_Lists

lemma mapME_x_map_simp:
  "mapME_x m (map f xs) = mapME_x (m o f) xs" by (simp add: mapME_x_def sequenceE_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x m (map f xs) = mapME_x (m \<circ> f) xs
theory Monad_Lists

lemma mapM_return:
  "mapM (\<lambda>x. return (f x)) xs = return (map f xs)" apply (induct xs) apply (simp add: mapM_def sequence_def) apply (simp add: mapM_Cons) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM (\<lambda>x. return (f x)) xs = return (map f xs) proof (prove)
goal (2 subgoals):
 1. mapM (\<lambda>x. return (f x)) [] = return (map f [])
 2. \<And>a xs. mapM (\<lambda>x. return (f x)) xs = return (map f xs) \<Longrightarrow> mapM (\<lambda>x. return (f x)) (a # xs) = return (map f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. mapM (\<lambda>x. return (f x)) xs = return (map f xs) \<Longrightarrow> mapM (\<lambda>x. return (f x)) (a # xs) = return (map f (a # xs)) proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma liftM_return [simp]:
  "liftM f (return x) = return (f x)" by (simp add: liftM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftM f (return x) = return (f x)
theory Monad_Lists

lemma mapM_x_return :
  "mapM_x (\<lambda>_. return v) xs = return v" by (induct xs) (auto simp: mapM_x_Nil mapM_x_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x (\<lambda>_. return v) xs = return v
theory Monad_Lists

lemma bind_comm_mapM_comm:
  assumes bind_comm:
    "\<And>n z. do x \<leftarrow> a; y \<leftarrow> b z; (n x y :: ('a, 's) nondet_monad) od =
            do y \<leftarrow> b z; x \<leftarrow> a; n x y od"
  shows "\<And>n'. do x \<leftarrow> a; ys \<leftarrow> mapM b zs; (n' x ys :: ('a, 's) nondet_monad) od =
         do ys \<leftarrow> mapM b zs; x \<leftarrow> a; n' x ys od" proof (induct zs) case Nil thus ?case by (simp add: mapM_def sequence_def) next case (Cons z zs') thus ?case by (clarsimp simp: mapM_Cons bind_assoc bind_comm intro!: bind_cong [OF refl]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>n'. do x <- a;
mapM b zs >>= n' x
od = do ys <- mapM b zs;
x <- a;
n' x ys
od proof (state)
goal (2 subgoals):
 1. \<And>n'. do x <- a;
mapM b [] >>= n' x
od = do ys <- mapM b [];
x <- a;
n' x ys
od
 2. \<And>aa zs n'. (\<And>n'. do x <- a;
mapM b zs >>= n' x
od = do ys <- mapM b zs;
x <- a;
n' x ys
od) \<Longrightarrow> do x <- a;
mapM b (aa # zs) >>= n' x
od = do ys <- mapM b (aa # zs);
x <- a;
n' x ys
od proof (state)
this:


goal (2 subgoals):
 1. \<And>n'. do x <- a;
mapM b [] >>= n' x
od = do ys <- mapM b [];
x <- a;
n' x ys
od
 2. \<And>aa zs n'. (\<And>n'. do x <- a;
mapM b zs >>= n' x
od = do ys <- mapM b zs;
x <- a;
n' x ys
od) \<Longrightarrow> do x <- a;
mapM b (aa # zs) >>= n' x
od = do ys <- mapM b (aa # zs);
x <- a;
n' x ys
od proof (prove)
goal (1 subgoal):
 1. do x <- a;
mapM b [] >>= n' x
od = do ys <- mapM b [];
x <- a;
n' x ys
od proof (state)
this:
do x <- a;
mapM b [] >>= n' x
od = do ys <- mapM b [];
x <- a;
n' x ys
od

goal (1 subgoal):
 1. \<And>aa zs n'. (\<And>n'. do x <- a;
mapM b zs >>= n' x
od = do ys <- mapM b zs;
x <- a;
n' x ys
od) \<Longrightarrow> do x <- a;
mapM b (aa # zs) >>= n' x
od = do ys <- mapM b (aa # zs);
x <- a;
n' x ys
od proof (state)
goal (1 subgoal):
 1. \<And>aa zs n'. (\<And>n'. do x <- a;
mapM b zs >>= n' x
od = do ys <- mapM b zs;
x <- a;
n' x ys
od) \<Longrightarrow> do x <- a;
mapM b (aa # zs) >>= n' x
od = do ys <- mapM b (aa # zs);
x <- a;
n' x ys
od proof (state)
this:
do x <- a;
mapM b zs' >>= ?n' x
od = do ys <- mapM b zs';
x <- a;
?n' x ys
od

goal (1 subgoal):
 1. \<And>aa zs n'. (\<And>n'. do x <- a;
mapM b zs >>= n' x
od = do ys <- mapM b zs;
x <- a;
n' x ys
od) \<Longrightarrow> do x <- a;
mapM b (aa # zs) >>= n' x
od = do ys <- mapM b (aa # zs);
x <- a;
n' x ys
od proof (prove)
using this:
do x <- a;
mapM b zs' >>= ?n' x
od = do ys <- mapM b zs';
x <- a;
?n' x ys
od

goal (1 subgoal):
 1. do x <- a;
mapM b (z # zs') >>= n' x
od = do ys <- mapM b (z # zs');
x <- a;
n' x ys
od proof (state)
this:
do x <- a;
mapM b (z # zs') >>= n' x
od = do ys <- mapM b (z # zs');
x <- a;
n' x ys
od

goal:
No subgoals!
theory Monad_Lists

lemma liftE_handle :
  "(liftE f <handle> g) = liftE f" by (simp add: handleE_def handleE'_def liftE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE f <handle> g) = liftE f
theory Monad_Lists

lemma mapM_empty:
  "mapM f [] = return []" unfolding mapM_def by (simp add: sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM f [] = return [] proof (prove)
goal (1 subgoal):
 1. sequence (map f []) = return []
theory Monad_Lists

lemma mapM_append:
  "mapM f (xs @ ys) =
  (do x \<leftarrow> mapM f xs;
      y \<leftarrow> mapM f ys;
      return (x @ y)
   od)" proof (induct xs) case Nil thus ?case by (simp add: mapM_empty) next case (Cons x xs) show ?case by (simp add: mapM_Cons bind_assoc Cons.hyps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM f (xs @ ys) = do x <- mapM f xs;
y <- mapM f ys;
return (x @ y)
od proof (state)
goal (2 subgoals):
 1. mapM f ([] @ ys) = do x <- mapM f [];
y <- mapM f ys;
return (x @ y)
od
 2. \<And>a xs. mapM f (xs @ ys) = do x <- mapM f xs;
y <- mapM f ys;
return (x @ y)
od \<Longrightarrow> mapM f ((a # xs) @ ys) = do x <- mapM f (a # xs);
y <- mapM f ys;
return (x @ y)
od proof (state)
this:


goal (2 subgoals):
 1. mapM f ([] @ ys) = do x <- mapM f [];
y <- mapM f ys;
return (x @ y)
od
 2. \<And>a xs. mapM f (xs @ ys) = do x <- mapM f xs;
y <- mapM f ys;
return (x @ y)
od \<Longrightarrow> mapM f ((a # xs) @ ys) = do x <- mapM f (a # xs);
y <- mapM f ys;
return (x @ y)
od proof (prove)
goal (1 subgoal):
 1. mapM f ([] @ ys) = do x <- mapM f [];
y <- mapM f ys;
return (x @ y)
od proof (state)
this:
mapM f ([] @ ys) = do x <- mapM f [];
y <- mapM f ys;
return (x @ y)
od

goal (1 subgoal):
 1. \<And>a xs. mapM f (xs @ ys) = do x <- mapM f xs;
y <- mapM f ys;
return (x @ y)
od \<Longrightarrow> mapM f ((a # xs) @ ys) = do x <- mapM f (a # xs);
y <- mapM f ys;
return (x @ y)
od proof (state)
goal (1 subgoal):
 1. \<And>a xs. mapM f (xs @ ys) = do x <- mapM f xs;
y <- mapM f ys;
return (x @ y)
od \<Longrightarrow> mapM f ((a # xs) @ ys) = do x <- mapM f (a # xs);
y <- mapM f ys;
return (x @ y)
od proof (state)
this:
mapM f (xs @ ys) = do x <- mapM f xs;
y <- mapM f ys;
return (x @ y)
od

goal (1 subgoal):
 1. \<And>a xs. mapM f (xs @ ys) = do x <- mapM f xs;
y <- mapM f ys;
return (x @ y)
od \<Longrightarrow> mapM f ((a # xs) @ ys) = do x <- mapM f (a # xs);
y <- mapM f ys;
return (x @ y)
od proof (prove)
goal (1 subgoal):
 1. mapM f ((x # xs) @ ys) = do x <- mapM f (x # xs);
y <- mapM f ys;
return (x @ y)
od proof (state)
this:
mapM f ((x # xs) @ ys) = do x <- mapM f (x # xs);
y <- mapM f ys;
return (x @ y)
od

goal:
No subgoals!
theory Monad_Lists

lemma mapM_x_append2:
  "mapM_x f (xs @ ys) = do mapM_x f xs; mapM_x f ys od" apply (simp add: mapM_x_def sequence_x_def) apply (induct xs) apply simp apply (simp add: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f (xs @ ys) = do mapM_x f xs;
mapM_x f ys
od proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())) = do y <- foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ());
foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())
od proof (prove)
goal (2 subgoals):
 1. foldr (\<lambda>x y. do _ <- x;
y
od) (map f []) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())) = do y <- foldr (\<lambda>x y. do _ <- x;
y
od) (map f []) (return ());
foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())
od
 2. \<And>a xs. foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())) = do y <- foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ());
foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())
od \<Longrightarrow> foldr (\<lambda>x y. do _ <- x;
y
od) (map f (a # xs)) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())) = do y <- foldr (\<lambda>x y. do _ <- x;
y
od) (map f (a # xs)) (return ());
foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())) = do y <- foldr (\<lambda>x y. do _ <- x;
y
od) (map f xs) (return ());
foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())
od \<Longrightarrow> foldr (\<lambda>x y. do _ <- x;
y
od) (map f (a # xs)) (foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())) = do y <- foldr (\<lambda>x y. do _ <- x;
y
od) (map f (a # xs)) (return ());
foldr (\<lambda>x y. do _ <- x;
y
od) (map f ys) (return ())
od proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_singleton:
  "mapM f [x] = do r \<leftarrow> f x; return [r] od" by (simp add: mapM_def sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM f [x] = do r <- f x;
return [r]
od
theory Monad_Lists

lemma mapM_x_singleton:
  "mapM_x f [x] = f x" by (simp add: mapM_x_mapM mapM_singleton)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f [x] = f x