theory Trace_No_Trace

lemma no_trace_mapM[no_trace_cond]:
  assumes m: "\<And>x. x \<in> set xs \<Longrightarrow> no_trace (m x)"
  shows "no_trace (mapM m xs)" using m proof (induct xs) case Nil thus ?case by (simp add: mapM_def sequence_def no_trace_terminal) 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 apply (simp add: P) apply (wpsimp wp: no_trace_terminal) done qed

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

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

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

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

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

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

goal (1 subgoal):
 1. no_trace (mapM m (a_ # xs_)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace (mapM m xs_); \<And>x. x = a_ \<or> x \<in> set xs_ \<Longrightarrow> no_trace (m x)\<rbrakk> \<Longrightarrow> no_trace (do y <- m a_;
ys <- mapM m xs_;
return (y # ys)
od) proof (prove)
goal:
No subgoals! proof (state)
this:
no_trace (mapM m (a_ # xs_))

goal:
No subgoals!