theory SubMonadLib

lemma submonad_comm:
  assumes x1: "submonad_args f r g" and x2: "submonad_args f' r' g'"
  assumes y: "m = submonad_fn f r g im" "m' = submonad_fn f' r' g' im'"
  assumes z: "\<And>s x x'. r x (r' x' s) = r' x' (r x s)"
  assumes gp: "\<And>s x. g (r' x s) = g s" and gp': "\<And>s x. g' (r x s) = g' s"
  assumes efim: "empty_fail im" and efim': "empty_fail im'"
  shows      "(do x \<leftarrow> m; y \<leftarrow> m'; n x y od) = (do y \<leftarrow> m'; x \<leftarrow> m; n x y od)" proof - have P: "\<And>x s. g s \<Longrightarrow> f (r' x s) = f s" apply (subgoal_tac "f (r' x (r (f s) s)) = f s") apply (simp add: submonad_args.args[OF x1]) apply (simp add: z[symmetric]) apply (subst(asm) gp [symmetric]) apply (fastforce dest: submonad_args.argsD1[OF x1]) done have Q: "\<And>x s. g' s \<Longrightarrow> f' (r x s) = f' s" apply (subgoal_tac "f' (r x (r' (f' s) s)) = f' s") apply (simp add: submonad_args.args[OF x2]) apply (simp add: z) apply (subst(asm) gp' [symmetric]) apply (fastforce dest: submonad_args.argsD1[OF x2]) done note empty_failD [OF efim, simp] note empty_failD [OF efim', simp] note empty_fail_select_f[simp] show ?thesis apply (clarsimp simp: submonad_fn_def y bind_assoc split_def) apply (subst bind_subst_lift [OF modify_stateAssert], rule gp gp')+ apply (simp add: bind_assoc) apply (subst select_f_stateAssert, rule efim efim')+ apply (subst gets_stateAssert bind_subst_lift [OF stateAssert_stateAssert])+ apply (rule bind_cong) apply (simp add: pred_conj_def conj_comms) apply (simp add: bind_assoc select_f_walk[symmetric]) apply (clarsimp dest!: fst_stateAssertD) apply (subst bind_assoc[symmetric],
           subst bind_subst_lhs_inv [OF gets_modify_comm],
           erule P Q, wp, simp, simp)+ apply (simp add: bind_assoc) apply (simp add: select_f_walk[symmetric]) apply (subst gets_comm) apply (rule bind_apply_cong [OF refl])+ apply (subst select_f_walk, simp, simp,
           subst select_f_walk, simp, simp,
           rule bind_apply_cong [OF refl]) apply (subst select_f_walk, simp, simp, rule bind_apply_cong [OF refl]) apply (clarsimp simp: simpler_gets_def select_f_def) apply (simp add: bind_def get_def put_def modify_def z) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (state)
goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (prove)
goal (1 subgoal):
 1. \<And>x s. g s \<Longrightarrow> f (r' x s) = f s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>g s; f (r' x (r (f s) s)) = f s\<rbrakk> \<Longrightarrow> f (r' x s) = f s
 2. \<And>x s. g s \<Longrightarrow> f (r' x (r (f s) s)) = f s proof (prove)
goal (1 subgoal):
 1. \<And>x s. g s \<Longrightarrow> f (r' x (r (f s) s)) = f s proof (prove)
goal (1 subgoal):
 1. \<And>x s. g s \<Longrightarrow> f (r (f s) (r' x s)) = f s proof (prove)
goal (1 subgoal):
 1. \<And>x s. g (r' (?x1 x s) s) \<Longrightarrow> f (r (f s) (r' x s)) = f s proof (prove)
goal:
No subgoals! proof (state)
this:
g ?s \<Longrightarrow> f (r' ?x ?s) = f ?s

goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (prove)
goal (1 subgoal):
 1. \<And>x s. g' s \<Longrightarrow> f' (r x s) = f' s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>g' s; f' (r x (r' (f' s) s)) = f' s\<rbrakk> \<Longrightarrow> f' (r x s) = f' s
 2. \<And>x s. g' s \<Longrightarrow> f' (r x (r' (f' s) s)) = f' s proof (prove)
goal (1 subgoal):
 1. \<And>x s. g' s \<Longrightarrow> f' (r x (r' (f' s) s)) = f' s proof (prove)
goal (1 subgoal):
 1. \<And>x s. g' s \<Longrightarrow> f' (r' (f' s) (r x s)) = f' s proof (prove)
goal (1 subgoal):
 1. \<And>x s. g' (r (?x1 x s) s) \<Longrightarrow> f' (r' (f' s) (r x s)) = f' s proof (prove)
goal:
No subgoals! proof (state)
this:
g' ?s \<Longrightarrow> f' (r ?x ?s) = f' ?s

goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (state)
this:
fst (im ?s) = {} \<Longrightarrow> snd (im ?s)

goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (state)
this:
fst (im' ?s) = {} \<Longrightarrow> snd (im' ?s)

goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (state)
this:
(fst ?S = {} \<Longrightarrow> snd ?S) \<Longrightarrow> empty_fail (select_f ?S)

goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (prove)
goal (1 subgoal):
 1. do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od proof (prove)
goal (1 subgoal):
 1. do x <- stateAssert g [];
x <- gets f;
x <- select_f (im x);
y <- modify (r (snd x));
xa <- stateAssert g' [];
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od = do x <- stateAssert g' [];
x <- gets f';
x <- select_f (im' x);
y <- modify (r' (snd x));
xa <- stateAssert g [];
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od proof (prove)
goal (1 subgoal):
 1. do x <- stateAssert g [];
x <- gets f;
x <- select_f (im x);
a <- do u <- stateAssert g' [];
modify (r (snd x))
od;
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od = do x <- stateAssert g' [];
x <- gets f';
x <- select_f (im' x);
a <- do u <- stateAssert g [];
modify (r' (snd x))
od;
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od proof (prove)
goal (1 subgoal):
 1. do x <- stateAssert g [];
x <- gets f;
x <- select_f (im x);
xa <- stateAssert g' [];
a <- modify (r (snd x));
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od = do x <- stateAssert g' [];
x <- gets f';
x <- select_f (im' x);
xa <- stateAssert g [];
a <- modify (r' (snd x));
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od proof (prove)
goal (1 subgoal):
 1. do x <- stateAssert g [];
x <- gets f;
u <- stateAssert g' [];
x <- select_f (im x);
a <- modify (r (snd x));
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od = do x <- stateAssert g' [];
x <- gets f';
u <- stateAssert g [];
x <- select_f (im' x);
a <- modify (r' (snd x));
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od proof (prove)
goal (1 subgoal):
 1. do u <- stateAssert (g and g') [];
x <- gets f;
x <- select_f (im x);
a <- modify (r (snd x));
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od = do u <- stateAssert (g' and g) [];
x <- gets f';
x <- select_f (im' x);
a <- modify (r' (snd x));
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od proof (prove)
goal (2 subgoals):
 1. stateAssert (g and g') [] = stateAssert (g' and g) []
 2. \<And>v s s'. (v, s') \<in> fst (stateAssert (g' and g) [] s) \<Longrightarrow> (do x <- gets f;
x <- select_f (im x);
a <- modify (r (snd x));
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s' = (do x <- gets f';
x <- select_f (im' x);
a <- modify (r' (snd x));
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s' proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> fst (stateAssert (g' and g) [] s) \<Longrightarrow> (do x <- gets f;
x <- select_f (im x);
a <- modify (r (snd x));
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s' = (do x <- gets f';
x <- select_f (im' x);
a <- modify (r' (snd x));
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. ((), s') \<in> fst (stateAssert (g' and g) [] s) \<Longrightarrow> (do x <- gets f;
x <- select_f (im x);
a <- modify (r (snd x));
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s' = (do x <- gets f';
x <- select_f (im' x);
a <- modify (r' (snd x));
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s' proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>g' s; g s\<rbrakk> \<Longrightarrow> (do x <- gets f;
x <- select_f (im x);
a <- modify (r (snd x));
xa <- gets f';
xa <- select_f (im' xa);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s = (do x <- gets f';
x <- select_f (im' x);
a <- modify (r' (snd x));
xa <- gets f;
xa <- select_f (im xa);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>g' s; g s\<rbrakk> \<Longrightarrow> (do x <- do x <- gets f;
select_f (im x)
od;
y <- gets f';
xa <- modify (r (snd x));
xa <- select_f (im' y);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s = (do x <- do x <- gets f';
select_f (im' x)
od;
y <- gets f;
xa <- modify (r' (snd x));
xa <- select_f (im y);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>g' s; g s\<rbrakk> \<Longrightarrow> (do x <- gets f;
x <- select_f (im x);
y <- gets f';
xa <- modify (r (snd x));
xa <- select_f (im' y);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s = (do x <- gets f';
x <- select_f (im' x);
y <- gets f;
xa <- modify (r' (snd x));
xa <- select_f (im y);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>g' s; g s\<rbrakk> \<Longrightarrow> (do x <- gets f;
y <- gets f';
x <- select_f (im x);
xa <- modify (r (snd x));
xa <- select_f (im' y);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s = (do x <- gets f';
y <- gets f;
x <- select_f (im' x);
xa <- modify (r' (snd x));
xa <- select_f (im y);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>g' s; g s\<rbrakk> \<Longrightarrow> (do y <- gets f';
x <- gets f;
x <- select_f (im x);
xa <- modify (r (snd x));
xa <- select_f (im' y);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) s = (do x <- gets f';
y <- gets f;
x <- select_f (im' x);
xa <- modify (r' (snd x));
xa <- select_f (im y);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s rv st rva sta. \<lbrakk>g' s; g s; (rv, st) \<in> fst (gets f' s); (rva, sta) \<in> fst (gets f st)\<rbrakk> \<Longrightarrow> (do x <- select_f (im rva);
xa <- modify (r (snd x));
xa <- select_f (im' rv);
y <- modify (r' (snd xa));
n (fst x) (fst xa)
od) sta = (do x <- select_f (im' rv);
xa <- modify (r' (snd x));
xa <- select_f (im rva);
y <- modify (r (snd xa));
n (fst xa) (fst x)
od) sta proof (prove)
goal (1 subgoal):
 1. \<And>s rv st rva sta rvb stb. \<lbrakk>g' s; g s; (rv, st) \<in> fst (gets f' s); (rva, sta) \<in> fst (gets f st); (rvb, stb) \<in> fst (select_f (im' rv) sta)\<rbrakk> \<Longrightarrow> (do a <- select_f (im rva);
aa <- modify (r (snd a));
y <- modify (r' (snd rvb));
n (fst a) (fst rvb)
od) stb = (do x <- modify (r' (snd rvb));
x <- select_f (im rva);
y <- modify (r (snd x));
n (fst x) (fst rvb)
od) stb proof (prove)
goal (1 subgoal):
 1. \<And>s rv st rva sta rvb stb rvc stc. \<lbrakk>g' s; g s; (rv, st) \<in> fst (gets f' s); (rva, sta) \<in> fst (gets f st); (rvb, stb) \<in> fst (select_f (im' rv) sta); (rvc, stc) \<in> fst (select_f (im rva) stb)\<rbrakk> \<Longrightarrow> (do a <- modify (r (snd rvc));
y <- modify (r' (snd rvb));
n (fst rvc) (fst rvb)
od) stc = (do a <- modify (r' (snd rvb));
y <- modify (r (snd rvc));
n (fst rvc) (fst rvb)
od) stc proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>g' s; g s; (a, b) \<in> fst (im' (f' s)); (aa, ba) \<in> fst (im (f s))\<rbrakk> \<Longrightarrow> (do ab <- modify (r ba);
y <- modify (r' b);
n aa a
od) s = (do ab <- modify (r' b);
y <- modify (r ba);
n aa a
od) s proof (prove)
goal:
No subgoals! proof (state)
this:
do x <- m;
m' >>= n x
od = do y <- m';
x <- m;
n x y
od

goal:
No subgoals!