theory Corres_D

lemma hoare_mapM_idempotent: "\<lbrakk> \<And> a R. \<lbrace> R \<rbrace> x a \<lbrace> \<lambda>_. R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> R \<rbrace> mapM x y \<lbrace> \<lambda>_. R \<rbrace>" 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 (erule_tac x=R in allE) apply (rule hoare_seq_ext) apply wp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>) \<Longrightarrow> \<lbrace>R\<rbrace> mapM x y \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>) \<Longrightarrow> \<lbrace>R\<rbrace> mapM x [] \<lbrace>\<lambda>_. R\<rbrace>
 2. \<And>a list. \<lbrakk>\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> mapM x list \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> mapM x (a # list) \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> mapM x list \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> mapM x (a # list) \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []) \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> 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 \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>a R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []) \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> 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 \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<lbrace>R\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []) \<lbrace>\<lambda>_. R\<rbrace>; \<forall>R. \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> 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 \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<lbrace>R\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []) \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> 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 \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a list xa. \<lbrakk>\<lbrace>R\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []) \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?B3 a list xa\<rbrace> do y <- foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []);
return (xa # y)
od \<lbrace>\<lambda>_. R\<rbrace>
 2. \<And>a list. \<lbrakk>\<lbrace>R\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []) \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> x a \<lbrace>?B3 a list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<lbrace>R\<rbrace> foldr (\<lambda>p q. do x <- p;
y <- q;
return (x # y)
od) (map x list) (return []) \<lbrace>\<lambda>_. R\<rbrace>; \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>_. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> x a \<lbrace>\<lambda>x. R\<rbrace> proof (prove)
goal:
No subgoals!