theory MonadicRewrite

lemma monadic_rewrite_gets_the_walk:
  "\<lbrakk> \<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv);
     \<And>Q. f \<lbrace>\<lambda>s. Q (pf s)\<rbrace>;
     \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f \<rbrakk>
   \<Longrightarrow> monadic_rewrite True False R (f >>= (\<lambda>rv. g rv))
                                   (do v \<leftarrow> gets_the pf; x \<leftarrow> f; g' x v od)" apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_trans) apply (erule(1) monadic_rewrite_bind_tail) apply (simp add: gets_the_def bind_assoc) apply (rule monadic_rewrite_symb_exec_r) apply (rule monadic_rewrite_trans) apply (rule monadic_rewrite_bind_tail) apply (rule_tac rv=x in monadic_rewrite_symb_exec_l_known_F) apply (rule monadic_rewrite_refl) apply (wp empty_fail_gets)+ apply assumption apply (rule_tac P="x = None" in monadic_rewrite_cases[where Q=\<top>]) apply (simp add: assert_opt_def) apply (clarsimp simp: monadic_rewrite_def fail_def snd_bind) apply (rule ccontr, drule(1) empty_failD2) apply clarsimp apply (simp add: assert_opt_def case_option_If2) apply (rule monadic_rewrite_refl) apply wp+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False R (f >>= g) (do v <- gets_the pf;
x <- f;
g' x v
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q (f >>= g) (do v <- gets_the pf;
x <- f;
g' x v
od)
 2. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?P3 (f >>= g) ?g3
 2. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q3 ?g3 (do v <- gets_the pf;
x <- f;
g' x v
od)
 3. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q3 (do x <- f;
gets_the pf >>= g' x
od) (do v <- gets_the pf;
x <- f;
g' x v
od)
 2. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False ?Q3 (do x <- f;
xa <- gets pf;
assert_opt xa >>= g' x
od) (do x <- gets pf;
v <- assert_opt x;
x <- f;
g' x v
od)
 2. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and ?Q3) s proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q8 x) (do x <- f;
xa <- gets pf;
assert_opt xa >>= g' x
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 2. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 3. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>?Q8\<rbrace>
 5. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?P13 x) (do x <- f;
xa <- gets pf;
assert_opt xa >>= g' x
od) (?g13 x)
 2. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q13 x) (?g13 x) (do v <- assert_opt x;
x <- f;
g' x v
od)
 3. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 5. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. ?P13 x and ?Q13 x\<rbrace>
 6. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (7 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q16 x xa) (do x <- gets pf;
assert_opt x >>= g' xa
od) (?j16 x xa)
 2. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P13 x\<rbrace> f \<lbrace>?Q16 x\<rbrace>
 3. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q13 x) (f >>= ?j16 x) (do v <- assert_opt x;
x <- f;
g' x v
od)
 4. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 5. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 6. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. ?P13 x and ?Q13 x\<rbrace>
 7. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (10 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q19 x xa) (assert_opt x >>= g' xa) (?j16 x xa)
 2. \<And>x xa Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 3. \<And>x xa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> empty_fail (gets pf)
 4. \<And>x xa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P19 x xa\<rbrace> gets pf \<lbrace>\<lambda>rv' _. rv' = x\<rbrace>
 5. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P13 x\<rbrace> f \<lbrace>\<lambda>xa. ?P19 x xa and ?Q19 x xa\<rbrace>
 6. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q13 x) (f >>= ?j16 x) (do v <- assert_opt x;
x <- f;
g' x v
od)
 7. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 8. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 9. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. ?P13 x and ?Q13 x\<rbrace>
 10. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (9 subgoals):
 1. \<And>x xa Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 2. \<And>x xa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> empty_fail (gets pf)
 3. \<And>x xa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P19 x xa\<rbrace> gets pf \<lbrace>\<lambda>rv' _. rv' = x\<rbrace>
 4. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P13 x\<rbrace> f \<lbrace>\<lambda>xa. ?P19 x xa and (\<lambda>_. True)\<rbrace>
 5. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q13 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 6. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 7. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 8. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. ?P13 x and ?Q13 x\<rbrace>
 9. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P13 x\<rbrace> f \<lbrace>\<lambda>xa s. pf s = x \<and> True\<rbrace>
 2. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q13 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 3. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 5. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. ?P13 x and ?Q13 x\<rbrace>
 6. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q13 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 2. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 3. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and ?Q13 x\<rbrace>
 5. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; x = None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (\<lambda>_. True) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 2. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; x \<noteq> None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?R36 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 3. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 5. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and (\<lambda>s. (x = None \<longrightarrow> True) \<and> (x \<noteq> None \<longrightarrow> ?R36 x s))\<rbrace>
 6. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
(case x of None \<Rightarrow> fail | Some v \<Rightarrow> return v) >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; x = None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (\<lambda>_. True) (do x <- f;
fail
od) fail
 2. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; x \<noteq> None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?R36 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 3. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 5. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and (\<lambda>s. (x = None \<longrightarrow> True) \<and> (x \<noteq> None \<longrightarrow> ?R36 x s))\<rbrace>
 6. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. P rv s \<and> \<not> snd (g rv s) \<longrightarrow> fst ((do x <- gets pf;
(case x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= g' rv
od) s) \<subseteq> fst (g rv s) \<and> \<not> snd (gets pf s) \<and> (\<forall>x\<in>fst (gets pf s). \<not> (case x of (r, s') \<Rightarrow> snd ((case r of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s') \<or> (\<exists>x\<in>fst ((case r of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s'). case x of (r, s') \<Rightarrow> snd (g' rv r s')))); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; \<forall>a b. (a, b) \<notin> fst (f s)\<rbrakk> \<Longrightarrow> snd (f s)
 2. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; x \<noteq> None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?R36 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 3. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 5. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and (\<lambda>s. (x = None \<longrightarrow> True) \<and> (x \<noteq> None \<longrightarrow> ?R36 x s))\<rbrace>
 6. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>\<And>rv. \<forall>s. P rv s \<and> \<not> snd (g rv s) \<longrightarrow> fst ((do x <- gets pf;
(case x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= g' rv
od) s) \<subseteq> fst (g rv s) \<and> \<not> snd (gets pf s) \<and> (\<forall>x\<in>fst (gets pf s). \<not> (case x of (r, s') \<Rightarrow> snd ((case r of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s') \<or> (\<exists>x\<in>fst ((case r of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s'). case x of (r, s') \<Rightarrow> snd (g' rv r s')))); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; \<forall>a b. (a, b) \<notin> fst (f s); \<not> snd (f s); \<exists>v. v \<in> fst (f s)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; x \<noteq> None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?R36 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 3. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 5. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and (\<lambda>s. (x = None \<longrightarrow> True) \<and> (x \<noteq> None \<longrightarrow> ?R36 x s))\<rbrace>
 6. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; x \<noteq> None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?R36 x) (do xa <- f;
assert_opt x >>= g' xa
od) (do v <- assert_opt x;
x <- f;
g' x v
od)
 2. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 3. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and (\<lambda>s. (x = None \<longrightarrow> True) \<and> (x \<noteq> None \<longrightarrow> ?R36 x s))\<rbrace>
 5. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
(if \<exists>y. x = Some y then return (the x) else fail) >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; \<exists>y. x = Some y\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?R36 x) (do xa <- f;
g' xa (the x)
od) (do xa <- f;
g' xa (the x)
od)
 2. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 3. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 4. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and (\<lambda>s. (x = None \<longrightarrow> True) \<and> (x \<noteq> None \<longrightarrow> ?R36 x s))\<rbrace>
 5. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>Pa\<rbrace> gets pf \<lbrace>\<lambda>_. Pa\<rbrace>
 2. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> no_fail ?P'8 (gets pf)
 3. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (do x <- gets pf;
assert_opt x >>= g' rv
od); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f\<rbrakk> \<Longrightarrow> \<lbrace>?P8\<rbrace> gets pf \<lbrace>\<lambda>x. (\<lambda>s. pf s = x \<and> True) and (\<lambda>s. (x = None \<longrightarrow> True) \<and> (x \<noteq> None \<longrightarrow> True))\<rbrace>
 4. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and (?P8 and ?P'8)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>rv. monadic_rewrite True False (P rv) (g rv) (gets_the pf >>= g' rv); \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f; R s\<rbrakk> \<Longrightarrow> (R and ((\<lambda>s. ((\<lambda>sa. pf sa = pf s \<and> True) and (\<lambda>sa. (pf s = None \<longrightarrow> True) \<and> (pf s \<noteq> None \<longrightarrow> True))) s) and (\<lambda>_. True))) s proof (prove)
goal:
No subgoals!