theory Monad_Lists

lemma no_fail_mapM':
  assumes rl: "\<And>x. no_fail (\<lambda>_. P x) (f x)"
  shows "no_fail (\<lambda>_. \<forall>x \<in> set xs. P x) (mapM f xs)" proof (induct xs) case Nil thus ?case by (simp add: mapM_def sequence_def) next case (Cons x xs) have nf: "no_fail (\<lambda>_. P x) (f x)" by (rule rl) have ih: "no_fail (\<lambda>_. \<forall>x \<in> set xs. P x) (mapM f xs)" by (rule Cons) show ?case apply (simp add: mapM_Cons) apply (rule no_fail_pre) apply (wp nf ih) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) proof (state)
goal (2 subgoals):
 1. no_fail (\<lambda>_. \<forall>x\<in>set []. P x) (mapM f [])
 2. \<And>a xs. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) \<Longrightarrow> no_fail (\<lambda>_. \<forall>x\<in>set (a # xs). P x) (mapM f (a # xs)) proof (state)
this:


goal (2 subgoals):
 1. no_fail (\<lambda>_. \<forall>x\<in>set []. P x) (mapM f [])
 2. \<And>a xs. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) \<Longrightarrow> no_fail (\<lambda>_. \<forall>x\<in>set (a # xs). P x) (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. \<forall>x\<in>set []. P x) (mapM f []) proof (state)
this:
no_fail (\<lambda>_. \<forall>x\<in>set []. P x) (mapM f [])

goal (1 subgoal):
 1. \<And>a xs. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) \<Longrightarrow> no_fail (\<lambda>_. \<forall>x\<in>set (a # xs). P x) (mapM f (a # xs)) proof (state)
goal (1 subgoal):
 1. \<And>a xs. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) \<Longrightarrow> no_fail (\<lambda>_. \<forall>x\<in>set (a # xs). P x) (mapM f (a # xs)) proof (state)
this:
no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs)

goal (1 subgoal):
 1. \<And>a xs. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) \<Longrightarrow> no_fail (\<lambda>_. \<forall>x\<in>set (a # xs). P x) (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P x) (f x) proof (state)
this:
no_fail (\<lambda>_. P x) (f x)

goal (1 subgoal):
 1. \<And>a xs. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) \<Longrightarrow> no_fail (\<lambda>_. \<forall>x\<in>set (a # xs). P x) (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) proof (state)
this:
no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs)

goal (1 subgoal):
 1. \<And>a xs. no_fail (\<lambda>_. \<forall>x\<in>set xs. P x) (mapM f xs) \<Longrightarrow> no_fail (\<lambda>_. \<forall>x\<in>set (a # xs). P x) (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. \<forall>x\<in>set (x # xs). P x) (mapM f (x # xs)) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P x \<and> (\<forall>x\<in>set xs. P x)) (do y <- f x;
ys <- mapM f xs;
return (y # ys)
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P6 (do y <- f x;
ys <- mapM f xs;
return (y # ys)
od)
 2. \<And>s. P x \<and> (\<forall>x\<in>set xs. P x) \<Longrightarrow> ?P6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P x \<and> (\<forall>x\<in>set xs. P x) \<Longrightarrow> ((\<lambda>_. P x) and (\<lambda>s. (\<forall>x\<in>set xs. P x) \<and> True)) s proof (prove)
goal:
No subgoals! proof (state)
this:
no_fail (\<lambda>_. \<forall>x\<in>set (x # xs). P x) (mapM f (x # xs))

goal:
No subgoals!