theory Arch_AC

lemma mapM_set'':
  assumes ip: "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>I x and I y and Q\<rbrace> f x \<lbrace>\<lambda>_. I y and Q\<rbrace>"
  and rl: "\<And>s. (\<forall>x \<in> set xs. I x s) \<and> Q s \<Longrightarrow> P s"
  shows "\<lbrace>\<lambda>s. (\<forall>x \<in> set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>" apply (rule hoare_post_imp[OF rl]) apply assumption apply (cases "xs = []") apply (simp add: mapM_Nil) apply (rule hoare_pre) apply (rule mapM_set'[where I = "\<lambda>x s. I x s \<and> Q s"]) apply (rule hoare_pre) apply (rule ip[simplified pred_conj_def]) apply (auto simp: neq_Nil_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>uu_ s. ?Q uu_ s \<Longrightarrow> (\<forall>x\<in>set xs. I x s) \<and> Q s
 2. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>?Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace>
 2. xs \<noteq> [] \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. xs \<noteq> [] \<Longrightarrow> \<lbrace>?Q6\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrace>
 2. \<And>s. \<lbrakk>xs \<noteq> []; (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>xs \<noteq> []; x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. I x s \<and> Q s) and (\<lambda>s. I y s \<and> Q s)\<rbrace> f x \<lbrace>\<lambda>_ s. I y s \<and> Q s\<rbrace>
 2. \<And>s. \<lbrakk>xs \<noteq> []; \<forall>x\<in>set xs. I x s \<and> Q s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. I x s) \<and> Q s
 3. \<And>s. \<lbrakk>xs \<noteq> []; (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. I x s \<and> Q s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>xs \<noteq> []; x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 x y\<rbrace> f x \<lbrace>\<lambda>_ s. I y s \<and> Q s\<rbrace>
 2. \<And>x y s. \<lbrakk>xs \<noteq> []; x \<in> set xs; y \<in> set xs; ((\<lambda>s. I x s \<and> Q s) and (\<lambda>s. I y s \<and> Q s)) s\<rbrakk> \<Longrightarrow> ?Q12 x y s
 3. \<And>s. \<lbrakk>xs \<noteq> []; \<forall>x\<in>set xs. I x s \<and> Q s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. I x s) \<and> Q s
 4. \<And>s. \<lbrakk>xs \<noteq> []; (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. I x s \<and> Q s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>xs \<noteq> []; x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> x \<in> set xs
 2. \<And>x y. \<lbrakk>xs \<noteq> []; x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> y \<in> set xs
 3. \<And>x y s. \<lbrakk>xs \<noteq> []; x \<in> set xs; y \<in> set xs; ((\<lambda>s. I x s \<and> Q s) and (\<lambda>s. I y s \<and> Q s)) s\<rbrakk> \<Longrightarrow> (I x s \<and> I y s) \<and> Q s
 4. \<And>s. \<lbrakk>xs \<noteq> []; \<forall>x\<in>set xs. I x s \<and> Q s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. I x s) \<and> Q s
 5. \<And>s. \<lbrakk>xs \<noteq> []; (\<forall>x\<in>set xs. I x s) \<and> Q s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. I x s \<and> Q s proof (prove)
goal:
No subgoals!