theory Corres_D

lemma dcorres_idempotent_mapM_rhs:
  "\<lbrakk> \<And> a R. \<lbrace> R \<rbrace> x a \<lbrace> \<lambda>_. R \<rbrace> \<rbrakk> \<Longrightarrow>
     dcorres dc P P' (return q) (mapM x y)" apply (induct_tac y) apply (clarsimp simp: mapM_def sequence_def) apply (clarsimp simp: mapM_def sequence_def) apply atomize apply (erule_tac x=a in allE) apply (rule corres_symb_exec_r [where Q'="\<lambda>_. P'"]) apply (clarsimp simp: corres_underlying_def bind_def return_def split_def) apply (erule_tac x=P' in allE, assumption) apply (erule_tac x="(=) s" in allE, assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>) \<Longrightarrow> dcorres dc P P' (return q) (mapM x y) proof (prove)
goal (2 subgoals):
 1. (\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>) \<Longrightarrow> dcorres dc P P' (return q) (mapM x [])
 2. \<And>a list. \<lbrakk>\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; dcorres dc P P' (return q) (mapM x list)\<rbrakk> \<Longrightarrow> dcorres dc P P' (return q) (mapM x (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; dcorres dc P P' (return q) (mapM x list)\<rbrakk> \<Longrightarrow> dcorres dc P P' (return q) (mapM x (a # list)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []))\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) P P' (return q) (do xa <- x a;
y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []);
return (xa # y)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []))\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) P P' (return q) (do xa <- x a;
y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []);
return (xa # y)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) P P' (return q) (do xa <- x a;
y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []);
return (xa # y)
od) proof (prove)
goal (4 subgoals):
 1. \<And>a list rv. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) P P' (return q) (do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []);
return (rv # y)
od)
 2. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> x a \<lbrace>\<lambda>_. P'\<rbrace>
 3. \<And>a list s. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> x a \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' (x a) proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> x a \<lbrace>\<lambda>_. P'\<rbrace>
 2. \<And>a list s. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> x a \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' (x a) proof (prove)
goal (2 subgoals):
 1. \<And>a list s. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> x a \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' (x a) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>dcorres (\<lambda>a b. True) P P' (return q) (foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return [])); \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' (x a) proof (prove)
goal:
No subgoals!