theory SubMonadLib

lemma select_f_walk:
  assumes m1: "empty_fail m1"
  assumes S: "fst S = {} \<Longrightarrow> snd S"
  shows "(do a \<leftarrow> m1; b \<leftarrow> select_f S; m2 a b od) = (do b \<leftarrow> select_f S; a \<leftarrow> m1; m2 a b od)" apply (rule ext) apply (rule prod.expand) apply (rule conjI) apply (simp add: select_f_def bind_def split_def) apply fastforce apply (simp add: select_f_def bind_def split_def) apply (case_tac "fst S = {}") apply clarsimp apply (case_tac "fst (m1 x) = {}") apply (simp add: empty_failD [OF m1] S) apply (frule S) apply force apply safe apply clarsimp apply force apply force apply clarsimp apply force apply clarsimp apply (case_tac "fst (m1 x) = {}", simp add: empty_failD [OF m1]) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do a <- m1;
select_f S >>= m2 a
od = do b <- select_f S;
a <- m1;
m2 a b
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do a <- m1;
select_f S >>= m2 a
od) x = (do b <- select_f S;
a <- m1;
m2 a b
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. fst ((do a <- m1;
select_f S >>= m2 a
od) x) = fst ((do b <- select_f S;
a <- m1;
m2 a b
od) x) \<and> snd ((do a <- m1;
select_f S >>= m2 a
od) x) = snd ((do b <- select_f S;
a <- m1;
m2 a b
od) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. fst ((do a <- m1;
select_f S >>= m2 a
od) x) = fst ((do b <- select_f S;
a <- m1;
m2 a b
od) x)
 2. \<And>x. snd ((do a <- m1;
select_f S >>= m2 a
od) x) = snd ((do b <- select_f S;
a <- m1;
m2 a b
od) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<Union>x\<in>fst (m1 x). \<Union>xa\<in>fst S \<times> {snd x}. fst (m2 (fst x) (fst xa) (snd xa))) = (\<Union>x\<in>fst S \<times> {x}. \<Union>xa\<in>fst (m1 (snd x)). fst (m2 (fst xa) (fst x) (snd xa)))
 2. \<And>x. snd ((do a <- m1;
select_f S >>= m2 a
od) x) = snd ((do b <- select_f S;
a <- m1;
m2 a b
od) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. snd ((do a <- m1;
select_f S >>= m2 a
od) x) = snd ((do b <- select_f S;
a <- m1;
m2 a b
od) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S) proof (prove)
goal (2 subgoals):
 1. \<And>x. fst S = {} \<Longrightarrow> ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S)
 2. \<And>x. fst S \<noteq> {} \<Longrightarrow> ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S) proof (prove)
goal (2 subgoals):
 1. \<And>x. fst S = {} \<Longrightarrow> ((\<exists>a b. (a, b) \<in> fst (m1 x)) \<and> snd S \<or> snd (m1 x)) = snd S
 2. \<And>x. fst S \<noteq> {} \<Longrightarrow> ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>fst S = {}; fst (m1 x) = {}\<rbrakk> \<Longrightarrow> ((\<exists>a b. (a, b) \<in> fst (m1 x)) \<and> snd S \<or> snd (m1 x)) = snd S
 2. \<And>x. \<lbrakk>fst S = {}; fst (m1 x) \<noteq> {}\<rbrakk> \<Longrightarrow> ((\<exists>a b. (a, b) \<in> fst (m1 x)) \<and> snd S \<or> snd (m1 x)) = snd S
 3. \<And>x. fst S \<noteq> {} \<Longrightarrow> ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>fst S = {}; fst (m1 x) \<noteq> {}\<rbrakk> \<Longrightarrow> ((\<exists>a b. (a, b) \<in> fst (m1 x)) \<and> snd S \<or> snd (m1 x)) = snd S
 2. \<And>x. fst S \<noteq> {} \<Longrightarrow> ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>fst S = {}; fst (m1 x) \<noteq> {}; snd S\<rbrakk> \<Longrightarrow> ((\<exists>a b. (a, b) \<in> fst (m1 x)) \<and> snd S \<or> snd (m1 x)) = snd S
 2. \<And>x. fst S \<noteq> {} \<Longrightarrow> ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S) proof (prove)
goal (1 subgoal):
 1. \<And>x. fst S \<noteq> {} \<Longrightarrow> ((\<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S) \<or> snd (m1 x)) = ((\<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)) \<or> snd S) proof (prove)
goal (4 subgoals):
 1. \<And>x xa a b xb. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd S; (a, b) \<in> fst (m1 x); xb \<in> fst S; snd (m2 (fst (a, b)) xb (snd (a, b)))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)
 2. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd S; snd (m1 x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)
 3. \<And>x xa xb a b. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); xb \<in> fst S; (a, b) \<in> fst (m1 x); snd (m2 (fst (a, b)) xb (snd (a, b)))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S
 4. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); snd S\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S proof (prove)
goal (4 subgoals):
 1. \<And>x xa a b xb. \<lbrakk>xa \<in> fst S; \<not> snd S; (a, b) \<in> fst (m1 x); xb \<in> fst S; snd (m2 a xb b)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)
 2. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd S; snd (m1 x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)
 3. \<And>x xa xb a b. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); xb \<in> fst S; (a, b) \<in> fst (m1 x); snd (m2 (fst (a, b)) xb (snd (a, b)))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S
 4. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); snd S\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd S; snd (m1 x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst S. (\<exists>x\<in>fst (m1 x). snd (m2 (fst x) xa (snd x))) \<or> snd (m1 x)
 2. \<And>x xa xb a b. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); xb \<in> fst S; (a, b) \<in> fst (m1 x); snd (m2 (fst (a, b)) xb (snd (a, b)))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S
 3. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); snd S\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb a b. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); xb \<in> fst S; (a, b) \<in> fst (m1 x); snd (m2 (fst (a, b)) xb (snd (a, b)))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S
 2. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); snd S\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb a b. \<lbrakk>xa \<in> fst S; \<not> snd (m1 x); xb \<in> fst S; (a, b) \<in> fst (m1 x); snd (m2 a xb b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S
 2. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); snd S\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> fst S; xa \<notin> {}; \<not> snd (m1 x); snd S\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m1 x). (\<exists>xa\<in>fst S. snd (m2 (fst x) xa (snd x))) \<or> snd S proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> fst S; \<not> snd (m1 x); snd S\<rbrakk> \<Longrightarrow> \<exists>a b. (a, b) \<in> fst (m1 x) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> fst S; \<not> snd (m1 x); snd S; fst (m1 x) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>a b. (a, b) \<in> fst (m1 x) proof (prove)
goal:
No subgoals!