theory Move_R

lemma get_mapM_x_lower:
  fixes P :: "'a option \<Rightarrow> 's \<Rightarrow> bool"
  fixes f :: "('s,'a) nondet_monad"
  fixes g :: "'a \<Rightarrow> 'b \<Rightarrow> ('s,'c) nondet_monad"
  \<comment> \<open>@{term g} preserves the state that @{term f} cares about\<close>
  assumes g: "\<And>x y. \<lbrace> P (Some x) \<rbrace> g x y \<lbrace> \<lambda>_. P (Some x) \<rbrace>"
  \<comment> \<open>@{term P} specifies whether @{term f} either fails or returns a deterministic result\<close>
  assumes f: "\<And>opt_x s. P opt_x s \<Longrightarrow> f s = case_option ({},True) (\<lambda>x. ({(x,s)},False)) opt_x"
  \<comment> \<open>Every state determines P, and therefore the behaviour of @{term f}\<close>
  assumes x: "\<And>s. \<exists> opt_x. P opt_x s"
  \<comment> \<open>If @{term f} may fail, ensure there is at least one @{term f}\<close>
  assumes y: "\<exists>s. P None s \<Longrightarrow> ys \<noteq> []"
  shows "do x \<leftarrow> f; mapM_x (g x) ys od = mapM_x (\<lambda>y. do x \<leftarrow> f; g x y od) ys" proof - have f_rv: "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>r. P (Some r)\<rbrace>" using x f apply (clarsimp simp: valid_def) apply (drule_tac x=s in meta_spec; clarsimp) apply (case_tac opt_x; simp) done { fix y and h :: "'a \<Rightarrow> ('s,'d) nondet_monad" have "do x \<leftarrow> f; _ \<leftarrow> g x y; h x od
              = do x \<leftarrow> f; _ \<leftarrow> g x y; x \<leftarrow> f; h x od" apply (rule ext) apply (subst monad_eq_split[where g="do x \<leftarrow> f; g x y; return x od"
                                      and P="\<top>" and Q="\<lambda>r. P (Some r)"
                                      and f="h" and f'="\<lambda>_. f >>= h",
                                    simplified bind_assoc, simplified]) apply (wpsimp wp: g f_rv simp: f return_def bind_def)+ done } note f_redundant = this show ?thesis proof (cases "\<exists>s. P None s") case True show ?thesis apply (cases ys; simp add: True y mapM_x_Cons bind_assoc) subgoal for y ys apply (thin_tac _) apply (induct ys arbitrary: y; simp add: mapM_x_Nil mapM_x_Cons bind_assoc) apply (subst f_redundant; simp) done done next case False show ?thesis using False apply (induct ys; simp add: mapM_x_Nil mapM_x_Cons bind_assoc) apply (rule ext) subgoal for s by (insert x[of s]; drule spec[of _ s]; clarsimp; case_tac opt_x;
               clarsimp simp: bind_def return_def f) apply (subst f_redundant; simp) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>r. P (Some r)\<rbrace> proof (prove)
using this:
\<exists>opt_x. P opt_x ?s
P ?opt_x ?s \<Longrightarrow> f ?s = (case ?opt_x of None \<Rightarrow> ({}, True) | Some x \<Rightarrow> ({(x, ?s)}, False))

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>r. P (Some r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s. \<exists>opt_x. P opt_x s; \<And>opt_x s. P opt_x s \<Longrightarrow> f s = (case opt_x of None \<Rightarrow> ({}, True) | Some x \<Rightarrow> ({(x, s)}, False)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> P (Some a) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b opt_x. \<lbrakk>\<And>opt_x s. P opt_x s \<Longrightarrow> f s = (case opt_x of None \<Rightarrow> ({}, True) | Some x \<Rightarrow> ({(x, s)}, False)); (a, b) \<in> fst (case opt_x of None \<Rightarrow> ({}, True) | Some x \<Rightarrow> ({(x, s)}, False)); P opt_x s\<rbrakk> \<Longrightarrow> P (Some a) b proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>r. P (Some r)\<rbrace>

goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
this:
\<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>r. P (Some r)\<rbrace>

goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
goal (1 subgoal):
 1. do x <- f;
_ <- g x y;
h x
od = do x <- f;
_ <- g x y;
f >>= h
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- f;
_ <- g x y;
h x
od) x = (do x <- f;
_ <- g x y;
f >>= h
od) x proof (prove)
goal (3 subgoals):
 1. \<And>x r s. P (Some r) s \<Longrightarrow> h r s = (f >>= h) s
 2. \<And>x. \<lbrace>\<lambda>_. True\<rbrace> do x <- f;
y <- g x y;
return x
od \<lbrace>\<lambda>r. P (Some r)\<rbrace>
 3. \<And>x. (do x <- f;
x <- g x y;
f >>= h
od) x = (do x <- f;
_ <- g x y;
f >>= h
od) x proof (prove)
goal:
No subgoals! proof (state)
this:
do x <- f;
_ <- g x y;
h x
od = do x <- f;
_ <- g x y;
f >>= h
od

goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
this:
do x <- f;
_ <- g x ?y2;
?h2 x
od = do x <- f;
_ <- g x ?y2;
f >>= ?h2
od

goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
this:
do x <- f;
_ <- g x ?y2;
?h2 x
od = do x <- f;
_ <- g x ?y2;
f >>= ?h2
od

goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
goal (2 subgoals):
 1. \<exists>s. P None s \<Longrightarrow> do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
 2. \<nexists>s. P None s \<Longrightarrow> do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
this:
\<exists>s. P None s

goal (2 subgoals):
 1. \<exists>s. P None s \<Longrightarrow> do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
 2. \<nexists>s. P None s \<Longrightarrow> do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> do x <- f;
y <- g x a;
mapM_x (g x) list
od = do x <- f;
y <- g x a;
mapM_x (\<lambda>y. do x <- f;
g x y
od) list
od proof (prove)
goal (1 subgoal):
 1. ys = y # ys \<Longrightarrow> do x <- f;
y <- g x y;
mapM_x (g x) ys
od = do x <- f;
y <- g x y;
mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
od proof (prove)
goal (1 subgoal):
 1. do x <- f;
y <- g x y;
mapM_x (g x) ys
od = do x <- f;
y <- g x y;
mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
od proof (prove)
goal (1 subgoal):
 1. \<And>a ys y. (\<And>y. do x <- f;
y <- g x y;
mapM_x (g x) ys
od = do x <- f;
y <- g x y;
mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
od) \<Longrightarrow> do x <- f;
y <- g x y;
y <- g x a;
mapM_x (g x) ys
od = do x <- f;
y <- g x y;
x <- f;
y <- g x a;
mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
od proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals! proof (state)
this:
do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys

goal (1 subgoal):
 1. \<nexists>s. P None s \<Longrightarrow> do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
goal (1 subgoal):
 1. \<nexists>s. P None s \<Longrightarrow> do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (state)
this:
\<nexists>s. P None s

goal (1 subgoal):
 1. \<nexists>s. P None s \<Longrightarrow> do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
using this:
\<nexists>s. P None s

goal (1 subgoal):
 1. do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys proof (prove)
goal (2 subgoals):
 1. \<forall>x. \<not> P None x \<Longrightarrow> do x <- f;
return ()
od = return ()
 2. \<And>a ys. \<lbrakk>do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys; \<forall>x. \<not> P None x\<rbrakk> \<Longrightarrow> do x <- f;
y <- g x a;
mapM_x (g x) ys
od = do x <- f;
y <- g x a;
mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
od proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>x. \<not> P None x \<Longrightarrow> (do x <- f;
return ()
od) x = return () x
 2. \<And>a ys. \<lbrakk>do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys; \<forall>x. \<not> P None x\<rbrakk> \<Longrightarrow> do x <- f;
y <- g x a;
mapM_x (g x) ys
od = do x <- f;
y <- g x a;
mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
od proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<not> P None x \<Longrightarrow> (do x <- f;
return ()
od) s = return () s proof (prove)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys; \<forall>x. \<not> P None x\<rbrakk> \<Longrightarrow> do x <- f;
y <- g x a;
mapM_x (g x) ys
od = do x <- f;
y <- g x a;
mapM_x (\<lambda>y. do x <- f;
g x y
od) ys
od proof (prove)
goal:
No subgoals! proof (state)
this:
do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys

goal:
No subgoals! proof (state)
this:
do x <- f;
mapM_x (g x) ys
od = mapM_x (\<lambda>y. do x <- f;
g x y
od) ys

goal:
No subgoals!