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\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace>"
  and rl: "\<And>s. (\<forall>x \<in> set xs. I x s) \<Longrightarrow> P s"
  shows "\<lbrace>\<lambda>s. (\<forall>x \<in> set xs. I x s)\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>" apply (rule hoare_post_imp[OF rl]) apply assumption apply (rule mapM_set) apply (rule hoare_pre) apply (rule hoare_vcg_ball_lift) apply (erule (1) ip) apply clarsimp apply (rule hoare_pre) apply (rule ip) apply assumption apply assumption apply clarsimp apply (rule hoare_pre) apply (rule ip) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x 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
 2. \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x 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\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. I x s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x s\<rbrace> f x \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. I x s\<rbrace>
 2. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x s\<rbrace> f x \<lbrace>\<lambda>_. I x\<rbrace>
 3. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>?Q8 x\<rbrace> f x \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. I x s\<rbrace>
 2. \<And>x s. \<lbrakk>x \<in> set xs; \<forall>x\<in>set xs. I x s\<rbrakk> \<Longrightarrow> ?Q8 x s
 3. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x s\<rbrace> f x \<lbrace>\<lambda>_. I x\<rbrace>
 4. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> set xs; xa \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?P11 x xa\<rbrace> f x \<lbrace>\<lambda>rv. I xa\<rbrace>
 2. \<And>x s. \<lbrakk>x \<in> set xs; \<forall>x\<in>set xs. I x s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set xs. ?P11 x xa s
 3. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x s\<rbrace> f x \<lbrace>\<lambda>_. I x\<rbrace>
 4. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set xs; \<forall>x\<in>set xs. I x s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set xs. (I x and I xa) s
 2. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x s\<rbrace> f x \<lbrace>\<lambda>_. I x\<rbrace>
 3. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set xs. I x s\<rbrace> f x \<lbrace>\<lambda>_. I x\<rbrace>
 2. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>?Q15 x\<rbrace> f x \<lbrace>\<lambda>_. I x\<rbrace>
 2. \<And>x s. \<lbrakk>x \<in> set xs; \<forall>x\<in>set xs. I x s\<rbrakk> \<Longrightarrow> ?Q15 x s
 3. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> x \<in> set xs
 2. \<And>x. x \<in> set xs \<Longrightarrow> x \<in> set xs
 3. \<And>x s. \<lbrakk>x \<in> set xs; \<forall>x\<in>set xs. I x s\<rbrakk> \<Longrightarrow> (I x and I x) s
 4. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> x \<in> set xs
 2. \<And>x s. \<lbrakk>x \<in> set xs; \<forall>x\<in>set xs. I x s\<rbrakk> \<Longrightarrow> (I x and I x) s
 3. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set xs; \<forall>x\<in>set xs. I x s\<rbrakk> \<Longrightarrow> (I x and I x) s
 2. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>set xs. I x s) and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 x y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace>
 2. \<And>x y s. \<lbrakk>x \<in> set xs; y \<in> set xs; ((\<lambda>s. \<forall>x\<in>set xs. I x s) and I y) s\<rbrakk> \<Longrightarrow> ?Q21 x y s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> x \<in> set xs
 2. \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> y \<in> set xs
 3. \<And>x y s. \<lbrakk>x \<in> set xs; y \<in> set xs; ((\<lambda>s. \<forall>x\<in>set xs. I x s) and I y) s\<rbrakk> \<Longrightarrow> (I x and I y) s proof (prove)
goal:
No subgoals!