theory Nondet_Monad_Equations

lemma bind_inv_inv_comm:
  "\<lbrakk> \<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>;
     empty_fail f; empty_fail g \<rbrakk> \<Longrightarrow>
   do x \<leftarrow> f; y \<leftarrow> g; n x y od = do y \<leftarrow> g; x \<leftarrow> f; n x y od" apply (rule ext) apply (rule trans[where s="(do (x, y) \<leftarrow> do x \<leftarrow> f; y \<leftarrow> (\<lambda>_. g s) ; (\<lambda>_. return (x, y) s) od;
                                 n x y od) s" for s]) apply (simp add: bind_assoc) apply (intro bind_apply_cong, simp_all)[1] apply (metis in_inv_by_hoareD) apply (simp add: return_def bind_def) apply (metis in_inv_by_hoareD) apply (rule trans[where s="(do (x, y) \<leftarrow> do y \<leftarrow> g; x \<leftarrow> (\<lambda>_. f s) ; (\<lambda>_. return (x, y) s) od;
                                 n x y od) s" for s, rotated]) apply (simp add: bind_assoc) apply (intro bind_apply_cong, simp_all)[1] apply (metis in_inv_by_hoareD) apply (simp add: return_def bind_def) apply (metis in_inv_by_hoareD) apply (rule bind_apply_cong, simp_all) apply (clarsimp simp: bind_def split_def return_def) apply (auto | drule(1) empty_failD3)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> do x <- f;
g >>= n x
od = do y <- g;
x <- f;
n x y
od proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do x <- f;
g >>= n x
od) x = (do y <- g;
x <- f;
n x y
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do x <- f;
g >>= n x
od) x = (do (x, y) <- do xa <- f;
y <- \<lambda>_. g (?s5 x);
\<lambda>_. return (xa, y) (?s5 x)
od;
n x y
od) (?s5 x)
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g (?s5 x);
\<lambda>_. return (xa, y) (?s5 x)
od;
n x y
od) (?s5 x) = (do y <- g;
x <- f;
n x y
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do x <- f;
g >>= n x
od) x = (do xa <- f;
xb <- \<lambda>_. g (?s5 x);
(x, y) <- \<lambda>_. return (xa, xb) (?s5 x);
n x y
od) (?s5 x)
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g (?s5 x);
\<lambda>_. return (xa, y) (?s5 x)
od;
n x y
od) (?s5 x) = (do y <- g;
x <- f;
n x y
od) x proof (prove)
goal (3 subgoals):
 1. \<And>x rv st. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (f x)\<rbrakk> \<Longrightarrow> g st = g x
 2. \<And>x rv st rva sta. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (f x); (rva, sta) \<in> fst (g x)\<rbrakk> \<Longrightarrow> n rv rva sta = (do (x, y) <- \<lambda>_. return (rv, rva) x;
n x y
od) sta
 3. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do y <- g;
x <- f;
n x y
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x rv st rva sta. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (f x); (rva, sta) \<in> fst (g x)\<rbrakk> \<Longrightarrow> n rv rva sta = (do (x, y) <- \<lambda>_. return (rv, rva) x;
n x y
od) sta
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do y <- g;
x <- f;
n x y
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x rv st rva sta. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (f x); (rva, sta) \<in> fst (g x)\<rbrakk> \<Longrightarrow> n rv rva sta = n rv rva x
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do y <- g;
x <- f;
n x y
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do y <- g;
x <- f;
n x y
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do y <- g;
xa <- \<lambda>_. f (?s22 x);
\<lambda>_. return (xa, y) (?s22 x)
od;
n x y
od) (?s22 x) = (do y <- g;
x <- f;
n x y
od) x
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do (x, y) <- do y <- g;
xa <- \<lambda>_. f (?s22 x);
\<lambda>_. return (xa, y) (?s22 x)
od;
n x y
od) (?s22 x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do xa <- g;
xb <- \<lambda>_. f (?s22 x);
(x, y) <- \<lambda>_. return (xb, xa) (?s22 x);
n x y
od) (?s22 x) = (do y <- g;
x <- f;
n x y
od) x
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do (x, y) <- do y <- g;
xa <- \<lambda>_. f (?s22 x);
\<lambda>_. return (xa, y) (?s22 x)
od;
n x y
od) (?s22 x) proof (prove)
goal (3 subgoals):
 1. \<And>x rv st. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (g x)\<rbrakk> \<Longrightarrow> f x = f st
 2. \<And>x rv st rva sta. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (g x); (rva, sta) \<in> fst (f st)\<rbrakk> \<Longrightarrow> (do (x, y) <- \<lambda>_. return (rva, rv) x;
n x y
od) sta = n rva rv sta
 3. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do (x, y) <- do y <- g;
xa <- \<lambda>_. f x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x rv st rva sta. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (g x); (rva, sta) \<in> fst (f st)\<rbrakk> \<Longrightarrow> (do (x, y) <- \<lambda>_. return (rva, rv) x;
n x y
od) sta = n rva rv sta
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do (x, y) <- do y <- g;
xa <- \<lambda>_. f x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x rv st rva sta. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g; (rv, st) \<in> fst (g x); (rva, sta) \<in> fst (f st)\<rbrakk> \<Longrightarrow> n rva rv x = n rva rv sta
 2. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do (x, y) <- do y <- g;
xa <- \<lambda>_. f x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do (x, y) <- do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x = (do (x, y) <- do y <- g;
xa <- \<lambda>_. f x;
\<lambda>_. return (xa, y) x
od;
n x y
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (do xa <- f;
y <- \<lambda>_. g x;
\<lambda>_. return (xa, y) x
od) x = (do y <- g;
xa <- \<lambda>_. f x;
\<lambda>_. return (xa, y) x
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> (\<Union>xa\<in>fst (f x). \<Union>xb\<in>fst (g x). {((fst xa, fst xb), x)}) = (\<Union>xa\<in>fst (g x). \<Union>xb\<in>fst (f x). {((fst xb, fst xa), x)}) \<and> ((\<exists>a b. (a, b) \<in> fst (f x)) \<and> snd (g x) \<or> snd (f x)) = ((\<exists>a b. (a, b) \<in> fst (g x)) \<and> snd (f x) \<or> snd (g x)) proof (prove)
goal:
No subgoals!