theory LemmaBucket

lemma mapM_x_accumulate_checks':
  assumes P:  "\<And>x. x \<in> set xs' \<Longrightarrow> \<lbrace>\<top>\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>"
  assumes P': "\<And>x y. \<lbrakk> x \<in> set xs'; y \<in> set xs' \<rbrakk>
                   \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>"
  shows       "set xs \<subseteq> set xs' \<Longrightarrow>
               \<lbrace>\<top>\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set xs. P x s\<rbrace>" apply (induct xs) apply (simp add: mapM_x_Nil) apply (simp add: mapM_x_Cons) apply (rule hoare_pre) apply (wp mapM_x_wp'[OF P']) apply blast apply simp apply assumption apply simp apply (rule P) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> set xs' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> set xs' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> mapM_x f [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set []. P x s\<rbrace>
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> set xs' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; set (a # xs) \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (a # xs). P x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>set xs \<subseteq> set xs' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; set (a # xs) \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>rv s. \<forall>x\<in>set (a # xs). P x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- f a;
mapM_x f xs
od \<lbrace>\<lambda>rv s. P a s \<and> (\<forall>x\<in>set xs. P x s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a xs\<rbrace> do y <- f a;
mapM_x f xs
od \<lbrace>\<lambda>rv s. P a s \<and> (\<forall>x\<in>set xs. P x s)\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> ?Q9 a xs s proof (prove)
goal (5 subgoals):
 1. \<And>a xs y x. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; x \<in> set xs\<rbrakk> \<Longrightarrow> x \<in> set xs'
 2. \<And>a xs y x. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; x \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set xs'
 3. \<And>a xs y. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 a xs y\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>
 4. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a xs\<rbrace> f a \<lbrace>\<lambda>y s. P a s \<and> ?P'14 a xs y s\<rbrace>
 5. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> ?Q9 a xs s proof (prove)
goal (4 subgoals):
 1. \<And>a xs y x. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; x \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set xs'
 2. \<And>a xs y. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 a xs y\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>
 3. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a xs\<rbrace> f a \<lbrace>\<lambda>y s. P a s \<and> ?P'14 a xs y s\<rbrace>
 4. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> ?Q9 a xs s proof (prove)
goal (3 subgoals):
 1. \<And>a xs y. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 a xs y\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a xs\<rbrace> f a \<lbrace>\<lambda>y s. P a s \<and> ?P'14 a xs y s\<rbrace>
 3. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> ?Q9 a xs s proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a xs\<rbrace> f a \<lbrace>\<lambda>y s. P a s \<and> True\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> ?Q9 a xs s proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 a xs\<rbrace> f a \<lbrace>\<lambda>y. P a\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> ?Q9 a xs s proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'\<rbrakk> \<Longrightarrow> a \<in> set xs'
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>; a \<in> set xs' \<and> set xs \<subseteq> set xs'; True\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!