[STATEMENT]
lemma fold_M_pure_I : "(\<And>d x. pure (f d x) h) \<Longrightarrow> (\<And>d. pure (fold_M f d xs) h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d x. pure (f d x) h) \<Longrightarrow> (\<And>d. pure (fold_M f d xs) h)
[PROOF STEP]
apply(induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>d. (\<And>d x. pure (f d x) h) \<Longrightarrow> pure (fold_M f d []) h
 2. \<And>a xs d. \<lbrakk>\<And>d. (\<And>d x. pure (f d x) h) \<Longrightarrow> pure (fold_M f d xs) h; \<And>d x. pure (f d x) h\<rbrakk> \<Longrightarrow> pure (fold_M f d (a # xs)) h
[PROOF STEP]
by(auto intro: bind_pure_I)