theory Trace_Monad_Equations

lemma repeat_n_choice:
  "S \<noteq> {}
   \<Longrightarrow> repeat_n n (do x \<leftarrow> select S; f x od)
       = (do xs \<leftarrow> select {xs. set xs \<subseteq> S \<and> length xs = n}; mapM_x f xs od)" apply (induct n; simp?) apply (simp add: select_def bind_def mapM_x_Nil cong: conj_cong) apply (simp add: select_early bind_assoc) apply (subst select_early) apply simp apply (auto intro: exI[where x="replicate n xs" for n xs])[1] apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) apply (simp only: conj_comms[where Q="length xs = n" for xs n]) apply (simp only: ex_simps[symmetric] conj_assoc length_Suc_conv, simp) apply (auto simp: mapM_x_Cons) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f proof (prove)
goal (2 subgoals):
 1. S \<noteq> {} \<Longrightarrow> return () = select {xs. xs = [] \<and> set xs \<subseteq> S} >>= mapM_x f
 2. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> do y <- select S >>= f;
select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f
od = select {xs. set xs \<subseteq> S \<and> length xs = Suc n} >>= mapM_x f proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> do y <- select S >>= f;
select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f
od = select {xs. set xs \<subseteq> S \<and> length xs = Suc n} >>= mapM_x f proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> do x <- select S;
y <- f x;
select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f
od = select {xs. set xs \<subseteq> S \<and> length xs = Suc n} >>= mapM_x f proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> {xs. set xs \<subseteq> S \<and> length xs = n} \<noteq> {}
 2. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> do x <- select S;
y <- select {xs. set xs \<subseteq> S \<and> length xs = n};
x <- f x;
mapM_x f y
od = select {xs. set xs \<subseteq> S \<and> length xs = Suc n} >>= mapM_x f proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x. set x \<subseteq> S \<and> length x = n
 2. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> do x <- select S;
y <- select {xs. set xs \<subseteq> S \<and> length xs = n};
x <- f x;
mapM_x f y
od = select {xs. set xs \<subseteq> S \<and> length xs = Suc n} >>= mapM_x f proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> do x <- select S;
y <- select {xs. set xs \<subseteq> S \<and> length xs = n};
x <- f x;
mapM_x f y
od = select {xs. set xs \<subseteq> S \<and> length xs = Suc n} >>= mapM_x f proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. set xs \<subseteq> S \<and> length xs = n} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x a b. (\<exists>xa\<in>S. \<exists>y. set y \<subseteq> S \<and> length y = n \<and> (a, b) \<in> (do x <- f xa;
mapM_x f y
od) x) = (\<exists>xa. set xa \<subseteq> S \<and> length xa = Suc n \<and> (a, b) \<in> mapM_x f xa x) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. length xs = n \<and> set xs \<subseteq> S} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x a b. (\<exists>xa\<in>S. \<exists>y. length y = n \<and> set y \<subseteq> S \<and> (a, b) \<in> (do x <- f xa;
mapM_x f y
od) x) = (\<exists>xa. length xa = Suc n \<and> set xa \<subseteq> S \<and> (a, b) \<in> mapM_x f xa x) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>repeat_n n (select S >>= f) = select {xs. length xs = n \<and> set xs \<subseteq> S} >>= mapM_x f; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x a b. (\<exists>xa\<in>S. \<exists>y. length y = n \<and> set y \<subseteq> S \<and> (a, b) \<in> (do x <- f xa;
mapM_x f y
od) x) = (\<exists>y ys. length ys = n \<and> y \<in> S \<and> set ys \<subseteq> S \<and> (a, b) \<in> mapM_x f (y # ys) x) proof (prove)
goal:
No subgoals!