theory EquivValid

lemma mapME_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 (mapME m lst)" using assms apply(atomize) apply(rule_tac Q=I in equiv_valid_guard_imp) apply(induct lst) apply(simp add: mapME_Nil returnOk_ev_pre) apply(subst mapME_Cons) apply wp apply fastforce apply (rule hoare_True_E_R[where P="\<top>"]) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (mapME 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 (mapME 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 (mapME 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 (mapME 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 (mapME 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 (mapME 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 (mapME 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 (mapME 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 (mapME 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 (mapME 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 (doE y <- m a;
ys <- mapME m lst;
returnOk (y # ys)
odE)
 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 (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 (mapME 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'8 a lst rv) (mapME 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 (mapME 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''8 a lst rv\<rbrace> mapME m lst \<lbrace>\<lambda>rva _. 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 (mapME 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'7 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 (mapME 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''7 a lst\<rbrace> m a \<lbrace>\<lambda>rv s. ?P'8 a lst rv s \<and> ?P''8 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 (mapME 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'7 a lst s \<and> ?P''7 a lst 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 (mapME 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''8 a lst rv\<rbrace> mapME m lst \<lbrace>\<lambda>rva _. 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 (mapME 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'7 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 (mapME 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''7 a lst\<rbrace> m a \<lbrace>\<lambda>rv s. I s \<and> ?P''8 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 (mapME 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'7 a lst s \<and> ?P''7 a lst 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 (mapME 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'7 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 (mapME 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''7 a lst\<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 (mapME 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'7 a lst s \<and> ?P''7 a lst 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!