theory SubMonadLib

lemma (in submonad) mapM_x_guard_preserved:
  "\<And>s s'. \<lbrakk> guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) xs s)\<rbrakk> \<Longrightarrow> guard s'" proof (induct xs) case Nil thus ?case by (simp add: mapM_x_def sequence_x_def return_def) next case (Cons x xs) thus ?case apply (clarsimp simp: o_def mapM_x_Cons return_def bind_def) apply (drule guard_preserved) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) xs s)\<rbrakk> \<Longrightarrow> guard s' proof (state)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) [] s)\<rbrakk> \<Longrightarrow> guard s'
 2. \<And>a xs s s'. \<lbrakk>\<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) xs s)\<rbrakk> \<Longrightarrow> guard s'; guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) (a # xs) s)\<rbrakk> \<Longrightarrow> guard s' proof (state)
this:
guard s
\<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) [] s)

goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) [] s)\<rbrakk> \<Longrightarrow> guard s'
 2. \<And>a xs s s'. \<lbrakk>\<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) xs s)\<rbrakk> \<Longrightarrow> guard s'; guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) (a # xs) s)\<rbrakk> \<Longrightarrow> guard s' proof (prove)
using this:
guard s
\<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) [] s)

goal (1 subgoal):
 1. guard s' proof (state)
this:
guard s'

goal (1 subgoal):
 1. \<And>a xs s s'. \<lbrakk>\<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) xs s)\<rbrakk> \<Longrightarrow> guard s'; guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) (a # xs) s)\<rbrakk> \<Longrightarrow> guard s' proof (state)
goal (1 subgoal):
 1. \<And>a xs s s'. \<lbrakk>\<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) xs s)\<rbrakk> \<Longrightarrow> guard s'; guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) (a # xs) s)\<rbrakk> \<Longrightarrow> guard s' proof (state)
this:
\<lbrakk>guard ?s; \<exists>rv. (rv, ?s') \<in> fst (mapM_x (fn \<circ> m) xs ?s)\<rbrakk> \<Longrightarrow> guard ?s'
guard s
\<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) (x # xs) s)

goal (1 subgoal):
 1. \<And>a xs s s'. \<lbrakk>\<And>s s'. \<lbrakk>guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) xs s)\<rbrakk> \<Longrightarrow> guard s'; guard s; \<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) (a # xs) s)\<rbrakk> \<Longrightarrow> guard s' proof (prove)
using this:
\<lbrakk>guard ?s; \<exists>rv. (rv, ?s') \<in> fst (mapM_x (fn \<circ> m) xs ?s)\<rbrakk> \<Longrightarrow> guard ?s'
guard s
\<exists>rv. (rv, s') \<in> fst (mapM_x (fn \<circ> m) (x # xs) s)

goal (1 subgoal):
 1. guard s' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>s s'. \<lbrakk>guard s; ((), s') \<in> fst (mapM_x (\<lambda>a. fn (m a)) xs s)\<rbrakk> \<Longrightarrow> guard s'; guard s; (a, b) \<in> fst (fn (m x) s); ((), s') \<in> fst (mapM_x (\<lambda>a. fn (m a)) xs b)\<rbrakk> \<Longrightarrow> guard s' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>s s'. \<lbrakk>guard s; ((), s') \<in> fst (mapM_x (\<lambda>a. fn (m a)) xs s)\<rbrakk> \<Longrightarrow> guard s'; guard s; ((), s') \<in> fst (mapM_x (\<lambda>a. fn (m a)) xs b); guard b\<rbrakk> \<Longrightarrow> guard s' proof (prove)
goal:
No subgoals! proof (state)
this:
guard s'

goal:
No subgoals!