kings-crown/FVELER_Isabelle huggingface dataset:
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_r_known_nE:
  "\<lbrakk> monadic_rewrite F False Q x (y rv);
     \<And>P. m \<lbrace>P\<rbrace>; no_fail P' m;
     \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv \<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F False (P and P' and Q) x (m >>= y)" apply (rule monadic_rewrite_guard_imp) apply (erule monadic_rewrite_trans) apply (rule monadic_rewrite_symb_exec_r_nE[OF monadic_rewrite_pre_imp_eq, rotated -1], simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F False Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F False (P and P' and Q) x (m >>= y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monadic_rewrite F False Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F False ?Q x (m >>= y)
 2. \<And>s. \<lbrakk>monadic_rewrite F False Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>; (P and P' and Q) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F False ?Q3 (y rv) (m >>= y)
 2. \<And>s. \<lbrakk>monadic_rewrite F False Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>; (P and P' and Q) s\<rbrakk> \<Longrightarrow> (Q and ?Q3) s proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_l_drop_F:
  "\<lbrakk> monadic_rewrite True E P g h; \<And>P. m \<lbrace>P\<rbrace>; empty_fail m \<rbrakk>
   \<Longrightarrow> monadic_rewrite True E P (m >>= (\<lambda>_. g)) h" by (rule monadic_rewrite_symb_exec_l, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite True E P g h; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m\<rbrakk> \<Longrightarrow> monadic_rewrite True E P (do _ <- m;
g
od) h
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_l_drop_nF:
  "\<lbrakk> monadic_rewrite False E P g h; \<And>P. m \<lbrace>P\<rbrace>; empty_fail m; no_fail P' m \<rbrakk>
   \<Longrightarrow> monadic_rewrite False E (P and P') (m >>= (\<lambda>_. g)) h" by (rule monadic_rewrite_symb_exec_l, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite False E P g h; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m\<rbrakk> \<Longrightarrow> monadic_rewrite False E (P and P') (do _ <- m;
g
od) h
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_r_drop_E:
  "\<lbrakk> monadic_rewrite F True P g h; \<And>P. m \<lbrace>P\<rbrace>; empty_fail m; no_fail P' m \<rbrakk>
   \<Longrightarrow> monadic_rewrite F True (P and P') g (m >>= (\<lambda>_. h))" by (rule monadic_rewrite_symb_exec_r, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F True P g h; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m\<rbrakk> \<Longrightarrow> monadic_rewrite F True (P and P') g (do _ <- m;
h
od)
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_r_drop_nE:
  "\<lbrakk> monadic_rewrite F False P g h; \<And>P. m \<lbrace>P\<rbrace>; no_fail P' m \<rbrakk>
   \<Longrightarrow> monadic_rewrite F False (P and P') g (m >>= (\<lambda>_. h))" by (rule monadic_rewrite_symb_exec_r, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F False P g h; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; no_fail P' m\<rbrakk> \<Longrightarrow> monadic_rewrite F False (P and P') g (do _ <- m;
h
od)
theory MonadicRewrite

lemma monadic_rewrite_if_r:
  "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q a b; \<not> P \<Longrightarrow> monadic_rewrite F E R a c \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) a (If P b c)" by (cases P, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> monadic_rewrite F E Q a b; \<not> P \<Longrightarrow> monadic_rewrite F E R a c\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) a (if P then b else c)
theory MonadicRewrite

lemma monadic_rewrite_if_r_True:
  "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q a b \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. P) and Q) a (If P b c)" by (rule monadic_rewrite_gen_asm, cases P, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> monadic_rewrite F E Q a b) \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. P) and Q) a (if P then b else c)
theory MonadicRewrite

lemma monadic_rewrite_if_r_False:
  "\<lbrakk> \<not> P \<Longrightarrow> monadic_rewrite F E R a c \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. \<not> P) and R) a (If P b c)" by (rule monadic_rewrite_gen_asm, cases P, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> monadic_rewrite F E R a c) \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. \<not> P) and R) a (if P then b else c)
theory MonadicRewrite

lemma monadic_rewrite_if_l:
  "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q b a; \<not> P \<Longrightarrow> monadic_rewrite F E R c a \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) (If P b c) a" by (cases P, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> monadic_rewrite F E Q b a; \<not> P \<Longrightarrow> monadic_rewrite F E R c a\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) (if P then b else c) a
theory MonadicRewrite

lemma monadic_rewrite_if_l_True:
  "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q b a \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. P) and Q) (If P b c) a" by (rule monadic_rewrite_gen_asm, cases P, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> monadic_rewrite F E Q b a) \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. P) and Q) (if P then b else c) a
theory MonadicRewrite

lemma monadic_rewrite_if_known:
  "monadic_rewrite F E ((\<lambda>s. C = X) and \<top>) (if C then f else g) (if X then f else g)" by (rule monadic_rewrite_gen_asm)
     (simp add: monadic_rewrite_refl split del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E ((\<lambda>s. C = X) and (\<lambda>_. True)) (if C then f else g) (if X then f else g)
theory MonadicRewrite

lemma monadic_rewrite_liftM:
  "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P (liftM fn f) (liftM fn g)" by (clarsimp simp: liftM_def elim!: monadic_rewrite_bind_head)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P (liftM fn f) (liftM fn g)
theory MonadicRewrite

lemma monadic_rewrite_split_fn:
  "\<lbrakk> monadic_rewrite F E P (liftM fn a) c;
     \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv));
     \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and R) (a >>= (\<lambda>rv. b rv)) (c >>= d)" apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_trans[rotated]) apply (erule monadic_rewrite_bind_head) apply (simp add: liftM_def) apply (erule(1) monadic_rewrite_bind_tail) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (a >>= b) (c >>= d) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E ?Q (a >>= b) (c >>= d)
 2. \<And>s. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>; (P and R) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E ?Q3 ?g3 (c >>= d)
 2. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E ?P3 (a >>= b) ?g3
 3. \<And>s. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>; (P and R) s\<rbrakk> \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E ?P3 (a >>= b) (liftM fn a >>= d)
 2. \<And>s. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>; (P and R) s\<rbrakk> \<Longrightarrow> (?P3 and P) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monadic_rewrite F E P (do x <- a;
return (fn x)
od) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E ?P3 (a >>= b) (do x <- a;
d (fn x)
od)
 2. \<And>s. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>; (P and R) s\<rbrakk> \<Longrightarrow> (?P3 and P) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>monadic_rewrite F E P (liftM fn a) c; \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>; (P and R) s\<rbrakk> \<Longrightarrow> (R and P) s proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma monadic_rewrite_add_assert:
  "monadic_rewrite F E (\<lambda>s. P) m (assert P >>= (\<lambda>_. m))" by (simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. P) m (do _ <- assert P;
m
od)
theory MonadicRewrite

lemma monadic_rewrite_assert:
  "\<lbrakk> Q \<Longrightarrow> monadic_rewrite True E P (f ()) g \<rbrakk>
   \<Longrightarrow> monadic_rewrite True E (\<lambda>s. Q \<longrightarrow> P s) (assert Q >>= f) g" by (simp add: assert_def split: if_split)
     (simp add: monadic_rewrite_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<Longrightarrow> monadic_rewrite True E P (f ()) g) \<Longrightarrow> monadic_rewrite True E (\<lambda>s. Q \<longrightarrow> P s) (assert Q >>= f) g
theory MonadicRewrite

lemma monadic_rewrite_assert2:
  "\<lbrakk> Q \<Longrightarrow> monadic_rewrite F E P (f ()) g \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E ((\<lambda>s. Q \<longrightarrow> P s) and (\<lambda>_. Q)) (assert Q >>= f) g" by (auto simp add: assert_def monadic_rewrite_def fail_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<Longrightarrow> monadic_rewrite F E P (f ()) g) \<Longrightarrow> monadic_rewrite F E ((\<lambda>s. Q \<longrightarrow> P s) and (\<lambda>_. Q)) (assert Q >>= f) g
theory MonadicRewrite

lemma monadic_rewrite_state_assert:
  "monadic_rewrite F E P (f ()) g
   \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (F \<longrightarrow> Q s \<longrightarrow> P s) \<and> (\<not>F \<longrightarrow> P s \<and> Q s))
                      (state_assert Q >>= f) g" by (fastforce simp: monadic_rewrite_def exec_get state_assert_def bind_assoc assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P (f ()) g \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (F \<longrightarrow> Q s \<longrightarrow> P s) \<and> (\<not> F \<longrightarrow> P s \<and> Q s)) (state_assert Q >>= f) g
theory MonadicRewrite

lemma monadic_rewrite_alternative_r:
  "\<lbrakk> monadic_rewrite F E P a b; monadic_rewrite F E Q a c \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and Q) a (b \<sqinter> c)" by (auto simp: monadic_rewrite_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P a b; monadic_rewrite F E Q a c\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and Q) a (b \<sqinter> c)
theory MonadicRewrite

lemma monadic_rewrite_alternatives:
  "\<lbrakk> monadic_rewrite E F P a c; monadic_rewrite E F Q b d \<rbrakk>
   \<Longrightarrow> monadic_rewrite E F (P and Q) (a \<sqinter> b) (c \<sqinter> d)" by (auto simp: monadic_rewrite_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite E F P a c; monadic_rewrite E F Q b d\<rbrakk> \<Longrightarrow> monadic_rewrite E F (P and Q) (a \<sqinter> b) (c \<sqinter> d)
theory MonadicRewrite

lemma monadic_rewrite_alternative_l:
  "monadic_rewrite F False \<top> (alternative f g) g" by (clarsimp simp: monadic_rewrite_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F False (\<lambda>_. True) (f \<sqinter> g) g
theory MonadicRewrite

lemma monadic_rewrite_introduce_alternative:
  "\<lbrakk> f = f'; monadic_rewrite F E P (alternative f' f) g \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E P f g" by (simp add: alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = f'; monadic_rewrite F E P (f' \<sqinter> f) g\<rbrakk> \<Longrightarrow> monadic_rewrite F E P f g
theory MonadicRewrite

lemma monadic_rewrite_pick_alternative_1:
  "monadic_rewrite F False \<top> (alternative f g) f" by (auto simp add: monadic_rewrite_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F False (\<lambda>_. True) (f \<sqinter> g) f
theory MonadicRewrite

lemma monadic_rewrite_select_x:
  "monadic_rewrite F False (\<lambda>s. x \<in> S) (select S) (return x)" by (simp add: monadic_rewrite_def return_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F False (\<lambda>s. x \<in> S) (select S) (return x)
theory MonadicRewrite

lemma monadic_rewrite_add_get:
  "monadic_rewrite F E P (do x <- get; f od) (do x <- get; g od)
   \<Longrightarrow> monadic_rewrite F E P f g" by (clarsimp simp: bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P (do x <- get;
f
od) (do x <- get;
g
od) \<Longrightarrow> monadic_rewrite F E P f g
theory MonadicRewrite

lemma monadic_rewrite_add_gets:
  "monadic_rewrite F E \<top> m (gets f >>= (\<lambda>_. m))" by (simp add: monadic_rewrite_def exec_gets)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>_. True) m (do _ <- gets f;
m
od)
theory MonadicRewrite

lemma monadic_rewrite_gets_known:
  "monadic_rewrite F E (\<lambda>s. f s = rv) (gets f >>= m) (m rv)" by (simp add: monadic_rewrite_def exec_gets)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. f s = rv) (gets f >>= m) (m rv)
theory MonadicRewrite

lemma monadic_rewrite_gets_the_known_v:
  "monadic_rewrite F E (\<lambda>s. f s = Some v)
     (gets_the f) (return v)" by (simp add: monadic_rewrite_def gets_the_def
                exec_gets assert_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. f s = Some v) (gets_the f) (return v)
theory MonadicRewrite

lemma monadic_rewrite_gets_l:
  "(\<And>x. monadic_rewrite F E (P x) (g x) m)
   \<Longrightarrow> monadic_rewrite F E (\<lambda>s. P (f s) s) (gets f >>= (\<lambda>x. g x)) m" by (auto simp add: monadic_rewrite_def exec_gets)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. monadic_rewrite F E (P x) (g x) m) \<Longrightarrow> monadic_rewrite F E (\<lambda>s. P (f s) s) (gets f >>= g) m
theory MonadicRewrite

lemma monadic_rewrite_gets_the_bind:
  assumes mr: "(\<And>rv. monadic_rewrite F E (Q rv) (g rv) m)"
  shows "monadic_rewrite F E (\<lambda>s. f s \<noteq> None \<and> Q (the (f s)) s) (gets_the f >>= (\<lambda>rv. g rv)) m" apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_exists[where P="\<lambda>v s. f s = Some v"]) apply (subst return_bind[symmetric, where f="\<lambda>_. m"]) apply (rule monadic_rewrite_bind) apply (rule_tac v=v in monadic_rewrite_gets_the_known_v) apply (rule mr) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. f s \<noteq> None \<and> Q (the (f s)) s) (gets_the f >>= g) m proof (prove)
goal (2 subgoals):
 1. monadic_rewrite F E ?Q (gets_the f >>= g) m
 2. \<And>s. f s \<noteq> None \<and> Q (the (f s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>v. monadic_rewrite F E (?Q3 v) (gets_the f >>= g) m
 2. \<And>s. f s \<noteq> None \<and> Q (the (f s)) s \<Longrightarrow> ((\<lambda>s. \<forall>v. f s = Some v \<longrightarrow> ?Q3 v s) and (\<lambda>s. \<exists>v. f s = Some v)) s proof (prove)
goal (2 subgoals):
 1. \<And>v. monadic_rewrite F E (?Q6 v (?v6 v)) (gets_the f >>= g) (do _ <- return (?x6 v);
m
od)
 2. \<And>s. f s \<noteq> None \<and> Q (the (f s)) s \<Longrightarrow> ((\<lambda>s. \<forall>v. f s = Some v \<longrightarrow> ?Q6 v (?v6 v) s) and (\<lambda>s. \<exists>v. f s = Some v)) s proof (prove)
goal (4 subgoals):
 1. \<And>v. monadic_rewrite F E (?P14 v (?v6 v)) (gets_the f) (return (?x6 v))
 2. \<And>v uu_. monadic_rewrite F E (?Q8 v uu_) (g uu_) m
 3. \<And>v. \<lbrace>?R13 v (?v6 v)\<rbrace> return (?x6 v) \<lbrace>?Q8 v\<rbrace>
 4. \<And>s. f s \<noteq> None \<and> Q (the (f s)) s \<Longrightarrow> ((\<lambda>s. \<forall>v. f s = Some v \<longrightarrow> (?P14 v (?v6 v) and ?R13 v (?v6 v)) s) and (\<lambda>s. \<exists>v. f s = Some v)) s proof (prove)
goal (3 subgoals):
 1. \<And>v uu_. monadic_rewrite F E (?Q8 v uu_) (g uu_) m
 2. \<And>v. \<lbrace>?R13 v v\<rbrace> return v \<lbrace>?Q8 v\<rbrace>
 3. \<And>s. f s \<noteq> None \<and> Q (the (f s)) s \<Longrightarrow> ((\<lambda>s. \<forall>v. f s = Some v \<longrightarrow> ((\<lambda>a. f a = Some v) and ?R13 v v) s) and (\<lambda>s. \<exists>v. f s = Some v)) s proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrace>?R13 v v\<rbrace> return v \<lbrace>Q\<rbrace>
 2. \<And>s. f s \<noteq> None \<and> Q (the (f s)) s \<Longrightarrow> ((\<lambda>s. \<forall>v. f s = Some v \<longrightarrow> ((\<lambda>a. f a = Some v) and ?R13 v v) s) and (\<lambda>s. \<exists>v. f s = Some v)) s proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma monadic_rewrite_gets_the_gets:
  "monadic_rewrite F E (\<lambda>s. f s \<noteq> None) (gets_the f) (gets (the o f))" apply (simp add: monadic_rewrite_def gets_the_def assert_opt_def exec_gets
            split: option.split) apply (auto simp: simpler_gets_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. f s \<noteq> None) (gets_the f) (gets (the \<circ> f)) proof (prove)
goal (1 subgoal):
 1. \<forall>s x2. f s = Some x2 \<longrightarrow> (F \<longrightarrow> \<not> snd (return x2 s)) \<longrightarrow> (E \<longrightarrow> return x2 s = gets (the \<circ> f) s) \<and> (\<not> E \<longrightarrow> fst (gets (the \<circ> f) s) \<subseteq> fst (return x2 s) \<and> (snd (gets (the \<circ> f) s) \<longrightarrow> snd (return x2 s))) proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma gets_oapply_liftM_rewrite:
  "monadic_rewrite False True (\<lambda>s. f s p \<noteq> None)
                   (gets (oapply p \<circ> f)) (liftM Some (gets_map f p))" unfolding monadic_rewrite_def by (simp add: liftM_def simpler_gets_def bind_def gets_map_def assert_opt_def return_def
           split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False True (\<lambda>s. f s p \<noteq> None) (gets (oapply p \<circ> f)) (liftM Some (gets_map f p)) proof (prove)
goal (1 subgoal):
 1. \<forall>s. f s p \<noteq> None \<and> (False \<longrightarrow> \<not> snd (gets (oapply p \<circ> f) s)) \<longrightarrow> (True \<longrightarrow> gets (oapply p \<circ> f) s = liftM Some (gets_map f p) s) \<and> (\<not> True \<longrightarrow> fst (liftM Some (gets_map f p) s) \<subseteq> fst (gets (oapply p \<circ> f) s) \<and> (snd (liftM Some (gets_map f p) s) \<longrightarrow> snd (gets (oapply p \<circ> f) s)))
theory MonadicRewrite

lemma monadic_rewrite_case_option:
  "\<lbrakk> \<And>y. x = Some y \<Longrightarrow> monadic_rewrite E F (P x) f (g y);
     x = None \<Longrightarrow> monadic_rewrite E F Q f h \<rbrakk>
   \<Longrightarrow> monadic_rewrite E F (\<lambda>s. (\<forall>y. x = Some y \<longrightarrow> P x s) \<and> (x = None \<longrightarrow> Q s))
                          f (case x of Some y \<Rightarrow> g y | None \<Rightarrow> h)" by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. x = Some y \<Longrightarrow> monadic_rewrite E F (P x) f (g y); x = None \<Longrightarrow> monadic_rewrite E F Q f h\<rbrakk> \<Longrightarrow> monadic_rewrite E F (\<lambda>s. (\<forall>y. x = Some y \<longrightarrow> P x s) \<and> (x = None \<longrightarrow> Q s)) f (case x of None \<Rightarrow> h | Some y \<Rightarrow> g y)
theory MonadicRewrite

lemma monadic_rewrite_refine_valid:
  "\<lbrakk> monadic_rewrite F E P f g;
     \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>;
     F \<longrightarrow> no_fail P'' f \<rbrakk>
   \<Longrightarrow> \<lbrace>P and P' and P''\<rbrace> g \<lbrace>Q\<rbrace>" by (fastforce simp: monadic_rewrite_def valid_def no_fail_def imp_conjL Ball_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; F \<longrightarrow> no_fail P'' f\<rbrakk> \<Longrightarrow> \<lbrace>P and P' and P''\<rbrace> g \<lbrace>Q\<rbrace>
theory MonadicRewrite

lemma monadic_rewrite_refine_validE_R:
  "\<lbrakk> monadic_rewrite F E P f g;
     \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -;
     F \<longrightarrow> no_fail P'' f \<rbrakk>
   \<Longrightarrow> \<lbrace>P and P' and P''\<rbrace> g \<lbrace>Q\<rbrace>, -" by (simp add: validE_R_def validE_def monadic_rewrite_refine_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -; F \<longrightarrow> no_fail P'' f\<rbrakk> \<Longrightarrow> \<lbrace>P and P' and P''\<rbrace> g \<lbrace>Q\<rbrace>, -
theory MonadicRewrite

lemma monadic_rewrite_is_valid:
  "\<lbrakk> monadic_rewrite False E P' f f'; \<lbrace>P\<rbrace> do x <- f; g x od \<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>P and P'\<rbrace> do x <- f'; g x od \<lbrace>Q\<rbrace>" by (fastforce simp: monadic_rewrite_def valid_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite False E P' f f'; \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f' >>= g \<lbrace>Q\<rbrace>
theory MonadicRewrite

lemma monadic_rewrite_to_eq:
  "monadic_rewrite False True \<top> f g \<Longrightarrow> f = g" by (simp add: monadic_rewrite_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False True (\<lambda>_. True) f g \<Longrightarrow> f = g