theory Nondet_Empty_Fail

lemma empty_fail_mapM[empty_fail_cond]:
  assumes m: "\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)"
  shows "empty_fail (mapM m xs)" using m proof (induct xs) case Nil thus ?case by (simp add: mapM_def sequence_def empty_fail_term) next case Cons have P: "\<And>m x xs. 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) from Cons show ?case by (simp add: P m empty_fail_cond empty_fail_term) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (mapM m xs) proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> empty_fail (m ?x)

goal (1 subgoal):
 1. empty_fail (mapM m xs) proof (state)
goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m [])
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> empty_fail (m x)\<rbrakk> \<Longrightarrow> empty_fail (mapM m (a # xs)) proof (state)
this:
?x \<in> set [] \<Longrightarrow> empty_fail (m ?x)

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m [])
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> empty_fail (m x)\<rbrakk> \<Longrightarrow> empty_fail (mapM m (a # xs)) proof (prove)
using this:
?x \<in> set [] \<Longrightarrow> empty_fail (m ?x)

goal (1 subgoal):
 1. empty_fail (mapM m []) proof (state)
this:
empty_fail (mapM m [])

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> empty_fail (m x)\<rbrakk> \<Longrightarrow> empty_fail (mapM m (a # xs)) proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> empty_fail (m x)\<rbrakk> \<Longrightarrow> empty_fail (mapM m (a # xs)) proof (state)
this:
(\<And>x. x \<in> set xs_ \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs_)
?x \<in> set (a_ # xs_) \<Longrightarrow> empty_fail (m ?x)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> empty_fail (m x)\<rbrakk> \<Longrightarrow> empty_fail (mapM m (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>m x xs. mapM m (x # xs) = do y <- m x;
ys <- mapM m xs;
return (y # ys)
od proof (state)
this:
mapM ?m (?x # ?xs) = do y <- ?m ?x;
ys <- mapM ?m ?xs;
return (y # ys)
od

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> empty_fail (m x)\<rbrakk> \<Longrightarrow> empty_fail (mapM m (a # xs)) proof (chain)
picking this:
(\<And>x. x \<in> set xs_ \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs_)
?x \<in> set (a_ # xs_) \<Longrightarrow> empty_fail (m ?x) proof (prove)
using this:
(\<And>x. x \<in> set xs_ \<Longrightarrow> empty_fail (m x)) \<Longrightarrow> empty_fail (mapM m xs_)
?x \<in> set (a_ # xs_) \<Longrightarrow> empty_fail (m ?x)

goal (1 subgoal):
 1. empty_fail (mapM m (a_ # xs_)) proof (state)
this:
empty_fail (mapM m (a_ # xs_))

goal:
No subgoals!