theory Monad_Commute

lemma mapM_x_commute:
  assumes commute: "\<And>r. monad_commute (P r) a (b r)"
     and   single: "\<And>r x. \<lbrace>P r and K (f r \<noteq> f x) and P x\<rbrace> b x \<lbrace>\<lambda>v. P r \<rbrace>"
  shows "monad_commute (\<lambda>s. (distinct (map f list)) \<and> (\<forall>r\<in> set list. P r s)) a (mapM_x b list)" apply (induct list) apply (clarsimp simp: mapM_x_Nil return_def bind_def monad_commute_def) apply (clarsimp simp: mapM_x_Cons) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split) apply assumption apply (rule monad_commute_guard_imp[OF commute]) apply assumption apply (wp hoare_vcg_const_Ball_lift) apply (rule single) apply (clarsimp simp: image_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) proof (prove)
goal (2 subgoals):
 1. monad_commute (\<lambda>s. distinct (map f []) \<and> (\<forall>r\<in>set []. P r s)) a (mapM_x b [])
 2. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> monad_commute (\<lambda>s. distinct (map f (aa # list)) \<and> (\<forall>r\<in>set (aa # list). P r s)) a (mapM_x b (aa # list)) proof (prove)
goal (1 subgoal):
 1. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> monad_commute (\<lambda>s. distinct (map f (aa # list)) \<and> (\<forall>r\<in>set (aa # list). P r s)) a (mapM_x b (aa # list)) proof (prove)
goal (1 subgoal):
 1. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> monad_commute (\<lambda>s. f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)) a (do y <- b aa;
mapM_x b list
od) proof (prove)
goal (2 subgoals):
 1. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> monad_commute (?P18 aa list) a (do y <- b aa;
mapM_x b list
od)
 2. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)\<rbrakk> \<Longrightarrow> ?P18 aa list s proof (prove)
goal (4 subgoals):
 1. \<And>aa list r. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> monad_commute (?Q21 aa list r) a (mapM_x b list)
 2. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> monad_commute (?P21 aa list) a (b aa)
 3. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> \<lbrace>?P'21 aa list\<rbrace> b aa \<lbrace>?Q21 aa list\<rbrace>
 4. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)\<rbrakk> \<Longrightarrow> (?P21 aa list and ?P'21 aa list) s proof (prove)
goal (3 subgoals):
 1. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> monad_commute (?P21 aa list) a (b aa)
 2. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> \<lbrace>?P'21 aa list\<rbrace> b aa \<lbrace>\<lambda>r s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)\<rbrace>
 3. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)\<rbrakk> \<Longrightarrow> (?P21 aa list and ?P'21 aa list) s proof (prove)
goal (3 subgoals):
 1. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); ?P21 aa list s\<rbrakk> \<Longrightarrow> P aa s
 2. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> \<lbrace>?P'21 aa list\<rbrace> b aa \<lbrace>\<lambda>r s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)\<rbrace>
 3. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)\<rbrakk> \<Longrightarrow> (?P21 aa list and ?P'21 aa list) s proof (prove)
goal (2 subgoals):
 1. \<And>aa list. monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list) \<Longrightarrow> \<lbrace>?P'21 aa list\<rbrace> b aa \<lbrace>\<lambda>r s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)\<rbrace>
 2. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)\<rbrakk> \<Longrightarrow> (P aa and ?P'21 aa list) s proof (prove)
goal (2 subgoals):
 1. \<And>aa list r. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); r \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P32 aa list r\<rbrace> b aa \<lbrace>\<lambda>rv. P r\<rbrace>
 2. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)\<rbrakk> \<Longrightarrow> (P aa and (\<lambda>s. distinct (map f list) \<and> (\<forall>x\<in>set list. ?P32 aa list x s))) s proof (prove)
goal (1 subgoal):
 1. \<And>aa list s. \<lbrakk>monad_commute (\<lambda>s. distinct (map f list) \<and> (\<forall>r\<in>set list. P r s)) a (mapM_x b list); f aa \<notin> f ` set list \<and> distinct (map f list) \<and> P aa s \<and> (\<forall>r\<in>set list. P r s)\<rbrakk> \<Longrightarrow> (P aa and (\<lambda>s. distinct (map f list) \<and> (\<forall>x\<in>set list. (P x and K (f x \<noteq> f aa) and P aa) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>aa list s x. \<lbrakk>monad_commute (\<lambda>s. \<forall>r\<in>set list. P r s) a (mapM_x b list); x \<in> set list; \<forall>x\<in>set list. f aa \<noteq> f x; distinct (map f list); P aa s; \<forall>r\<in>set list. P r s; f x = f aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!