theory EquivValid

lemma mapM_ev_pre:
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)"
  assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>"
  assumes inv_established: "\<And> s. P s \<Longrightarrow> I s"
  shows "equiv_valid_inv D A P (mapM m lst)" using assms apply(atomize) apply(rule_tac Q=I in equiv_valid_guard_imp) apply(induct lst) apply(simp add: mapM_Nil return_ev_pre) apply(subst mapM_Cons) apply(rule bind_ev_pre[where P''="I"]) apply(rule bind_ev[OF return_ev]) apply fastforce apply (rule wp_post_taut) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (mapM m lst) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m ?x)
?x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> m ?x \<lbrace>\<lambda>_. I\<rbrace>
P ?s \<Longrightarrow> I ?s

goal (1 subgoal):
 1. equiv_valid_inv D A P (mapM m lst) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A P (mapM m lst) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst)
 2. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x. x \<in> set [] \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set [] \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m [])
 2. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m (a # lst))
 3. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (2 subgoals):
 1. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m (a # lst))
 2. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (2 subgoals):
 1. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (do y <- m a;
ys <- mapM m lst;
return (y # ys)
od)
 2. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (5 subgoals):
 1. \<And>a lst rv. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?Q6 a lst rv) (do ys <- mapM m lst;
return (rv # ys)
od)
 2. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (m a)
 3. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> m a \<lbrace>?Q6 a lst\<rbrace>
 4. \<And>a lst s. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 5. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (6 subgoals):
 1. \<And>a lst rv. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'11 a lst rv) (mapM m lst)
 2. \<And>a lst rv. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>?P''11 a lst rv\<rbrace> mapM m lst \<lbrace>\<lambda>ys _. True\<rbrace>
 3. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (m a)
 4. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> m a \<lbrace>\<lambda>rv s. ?P'11 a lst rv s \<and> ?P''11 a lst rv s\<rbrace>
 5. \<And>a lst s. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 6. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (5 subgoals):
 1. \<And>a lst rv. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>?P''11 a lst rv\<rbrace> mapM m lst \<lbrace>\<lambda>ys _. True\<rbrace>
 2. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (m a)
 3. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> m a \<lbrace>\<lambda>rv s. I s \<and> ?P''11 a lst rv s\<rbrace>
 4. \<And>a lst s. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 5. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (4 subgoals):
 1. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A (?P'6 a lst) (m a)
 2. \<And>a lst. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> m a \<lbrace>\<lambda>rv s. I s \<and> True\<rbrace>
 3. \<And>a lst s. \<lbrakk>\<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> equiv_valid_inv D A I (mapM m lst); \<forall>x. x \<in> set (a # lst) \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set (a # lst) \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; I s\<rbrakk> \<Longrightarrow> ?P'6 a lst s \<and> I s
 4. \<And>s. \<lbrakk>\<forall>x. x \<in> set lst \<longrightarrow> equiv_valid_inv D A I (m x); \<forall>x. x \<in> set lst \<longrightarrow> \<lbrace>I\<rbrace> m x \<lbrace>\<lambda>_. I\<rbrace>; \<forall>s. P s \<longrightarrow> I s; P s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal:
No subgoals!