kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_No_Fail

lemma no_fail_bind[wp]:
  "\<lbrakk> \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))" unfolding no_fail_def bind_def using post_by_hoare by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; no_fail P f\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. \<forall>s. R rv s \<longrightarrow> \<not> snd (g rv s); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; \<forall>s. P s \<longrightarrow> \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<forall>s. (P and Q) s \<longrightarrow> \<not> snd (\<Union> (fst ` (\<lambda>(x, y). g x y) ` fst (f s)), True \<in> snd ` (\<lambda>(x, y). g x y) ` fst (f s) \<or> snd (f s)) proof (prove)
using this:
\<lbrakk>\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>; ?P ?s; (?r, ?s') \<in> fst (?f ?s)\<rbrakk> \<Longrightarrow> ?Q ?r ?s'

goal (1 subgoal):
 1. \<lbrakk>\<And>rv. \<forall>s. R rv s \<longrightarrow> \<not> snd (g rv s); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; \<forall>s. P s \<longrightarrow> \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<forall>s. (P and Q) s \<longrightarrow> \<not> snd (\<Union> (fst ` (\<lambda>(x, y). g x y) ` fst (f s)), True \<in> snd ` (\<lambda>(x, y). g x y) ` fst (f s) \<or> snd (f s))
theory Nondet_No_Fail

lemma no_fail_get[simp, wp]:
  "no_fail \<top> get" by (simp add: get_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) get
theory Nondet_No_Fail

lemma no_fail_put[simp, wp]:
  "no_fail \<top> (put s)" by (simp add: put_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (put s)
theory Nondet_No_Fail

lemma no_fail_modify[wp,simp]:
  "no_fail \<top> (modify f)" by (wpsimp simp: modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (modify f)
theory Nondet_No_Fail

lemma no_fail_gets_simp[simp]:
  "no_fail P (gets f)" by (wpsimp simp: gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (gets f)
theory Nondet_No_Fail

lemma no_fail_gets[wp]:
  "no_fail \<top> (gets f)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (gets f)
theory Nondet_No_Fail

lemma no_fail_select[wp,simp]:
  "no_fail \<top> (select S)" by (simp add: no_fail_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (select S)
theory Nondet_No_Fail

lemma no_fail_alt[wp]:
  "\<lbrakk> no_fail P f; no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f \<sqinter> g)" by (simp add: no_fail_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; no_fail Q g\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f \<sqinter> g)
theory Nondet_No_Fail

lemma no_fail_when[wp]:
  "(P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else \<top>) (when P f)" by (simp add: when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else (\<lambda>_. True)) (when P f)
theory Nondet_No_Fail

lemma no_fail_unless[wp]:
  "(\<not>P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then \<top> else Q) (unless P f)" by (simp add: unless_def when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then \<lambda>_. True else Q) (unless P f)
theory Nondet_No_Fail

lemma no_fail_fail[simp, wp]:
  "no_fail \<bottom> fail" by (simp add: fail_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) fail
theory Nondet_No_Fail

lemma no_fail_assert[simp, wp]:
  "no_fail (\<lambda>_. P) (assert P)" by (simp add: assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P) (assert P)
theory Nondet_No_Fail

lemma no_fail_assert_opt[simp, wp]:
  "no_fail (\<lambda>_. P \<noteq> None) (assert_opt P)" by (simp add: assert_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P \<noteq> None) (assert_opt P)
theory Nondet_No_Fail

lemma no_fail_case_option[wp]:
  assumes f: "no_fail P f"
  assumes g: "\<And>x. no_fail (Q x) (g x)"
  shows "no_fail (if x = None then P else Q (the x)) (case_option f g x)" by (clarsimp simp add: f g)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (if x = None then P else Q (the x)) (case x of None \<Rightarrow> f | Some x \<Rightarrow> g x)
theory Nondet_No_Fail

lemma no_fail_if[wp]:
  "\<lbrakk> P \<Longrightarrow> no_fail Q f; \<not>P \<Longrightarrow> no_fail R g \<rbrakk> \<Longrightarrow> no_fail (if P then Q else R) (if P then f else g)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> no_fail Q f; \<not> P \<Longrightarrow> no_fail R g\<rbrakk> \<Longrightarrow> no_fail (if P then Q else R) (if P then f else g)
theory Nondet_No_Fail

lemma no_fail_apply[wp]:
  "no_fail P (f (g x)) \<Longrightarrow> no_fail P (f $ g x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (f (g x)) \<Longrightarrow> no_fail P (f $ g x)
theory Nondet_No_Fail

lemma no_fail_undefined[simp, wp]:
  "no_fail \<bottom> undefined" by (simp add: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) undefined
theory Nondet_No_Fail

lemma no_fail_assume_pre:
  "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f" by (simp add: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f
theory Nondet_No_Fail

lemma no_fail_liftM_eq[simp]:
  "no_fail P (liftM f m) = no_fail P m" by (auto simp: liftM_def no_fail_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (liftM f m) = no_fail P m
theory Nondet_No_Fail

lemma no_fail_select_f[wp]:
  "no_fail (\<lambda>s. \<not>snd S) (select_f S)" by (simp add: select_f_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. \<not> snd S) (select_f S)
theory Nondet_No_Fail

lemma no_fail_liftM[wp]:
  "no_fail P m \<Longrightarrow> no_fail P (liftM f m)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P m \<Longrightarrow> no_fail P (liftM f m)
theory Nondet_No_Fail

lemma no_fail_pre_and:
  "no_fail P f \<Longrightarrow> no_fail (P and Q) f" by (erule no_fail_pre) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail (P and Q) f
theory Nondet_No_Fail

lemma no_fail_spec:
  "\<lbrakk> \<And>s. no_fail (((=) s) and P) f \<rbrakk> \<Longrightarrow> no_fail P f" by (simp add: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. no_fail ((=) s and P) f) \<Longrightarrow> no_fail P f
theory Nondet_No_Fail

lemma no_fail_assertE[wp]:
  "no_fail (\<lambda>_. P) (assertE P)" by (simp add: assertE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P) (assertE P)
theory Nondet_No_Fail

lemma no_fail_spec_pre:
  "\<lbrakk> no_fail (((=) s) and P') f; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> no_fail (((=) s) and P) f" by (erule no_fail_pre, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail ((=) s and P') f; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> no_fail ((=) s and P) f
theory Nondet_No_Fail

lemma no_fail_whenE[wp]:
  "\<lbrakk> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. G \<longrightarrow> P s) (whenE G f)" by (simp add: whenE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<longrightarrow> P s) (whenE G f)
theory Nondet_No_Fail

lemma no_fail_unlessE[wp]:
  "\<lbrakk> \<not> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)" by (simp add: unlessE_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)
theory Nondet_No_Fail

lemma no_fail_throwError[wp]:
  "no_fail \<top> (throwError e)" by (simp add: throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (throwError e)
theory Nondet_No_Fail

lemma no_fail_liftE[wp]:
  "no_fail P f \<Longrightarrow> no_fail P (liftE f)" unfolding liftE_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail P (liftE f) proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail P (do r <- f;
return (Inr r)
od)
theory Nondet_No_Fail

lemma no_fail_gets_the[wp]:
  "no_fail (\<lambda>s. f s \<noteq> None) (gets_the f)" unfolding gets_the_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s \<noteq> None) (gets_the f) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s \<noteq> None) (gets f >>= assert_opt)
theory Nondet_No_Fail

lemma no_fail_lift:
  "(\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not>isl x \<longrightarrow> P s) (lift f x)" unfolding lift_def by (wpsimp wp: no_fail_throwError split: sum.splits | assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not> isl x \<longrightarrow> P s) (lift f x) proof (prove)
goal (1 subgoal):
 1. (\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not> isl x \<longrightarrow> P s) (case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> f v')
theory Nondet_No_Fail

lemma validE_R_valid_eq:
  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - = \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. \<not> isl rv \<longrightarrow> R (projr rv) s\<rbrace>" unfolding validE_R_def validE_def valid_def by (fastforce split: sum.splits prod.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - = \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. \<not> isl rv \<longrightarrow> R (projr rv) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>s. Q s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). case r of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s')) = (\<forall>s. Q s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). \<not> isl r \<longrightarrow> R (projr r) s'))
theory Nondet_No_Fail

lemma no_fail_bindE[wp]:
  "\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<rbrakk>
     \<Longrightarrow> no_fail (P and Q) (f >>=E g)" unfolding bindE_def by (wpsimp wp: no_fail_lift simp: validE_R_valid_eq | assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>=E g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= lift g)
theory Nondet_No_Fail

lemma no_fail_False[simp]:
  "no_fail (\<lambda>_. False) X" by (clarsimp simp: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) X
theory Nondet_No_Fail

lemma no_fail_gets_map[wp]:
  "no_fail (\<lambda>s. f s p \<noteq> None) (gets_map f p)" unfolding gets_map_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s p \<noteq> None) (gets_map f p) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s p \<noteq> None) (do m <- gets f;
assert_opt (m p)
od)
theory Nondet_No_Fail

lemma no_fail_or:
  "\<lbrakk>no_fail P a; no_fail Q a\<rbrakk> \<Longrightarrow> no_fail (P or Q) a" by (clarsimp simp: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P a; no_fail Q a\<rbrakk> \<Longrightarrow> no_fail (P or Q) a
theory Nondet_No_Fail

lemma no_fail_state_assert[wp]:
  "no_fail P (state_assert P)" unfolding state_assert_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (state_assert P) proof (prove)
goal (1 subgoal):
 1. no_fail P (do s <- get;
assert (P s)
od)
theory Nondet_No_Fail

lemma no_fail_condition[wp]:
  "\<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) (condition C A B)" unfolding condition_def no_fail_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) condition C
  A
  B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. Q s \<longrightarrow> \<not> snd (A s); \<forall>s. R s \<longrightarrow> \<not> snd (B s)\<rbrakk> \<Longrightarrow> \<forall>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s) \<longrightarrow> \<not> snd (if C s then A s else B s)
theory Nondet_No_Fail

lemma no_fail_ex_lift:
  "(\<And>x. no_fail (P x) f) \<Longrightarrow> no_fail (\<lambda>s. \<exists>x. P x s) f" by (clarsimp simp: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_fail (P x) f) \<Longrightarrow> no_fail (\<lambda>s. \<exists>x. P x s) f
theory Nondet_No_Fail

lemma no_fail_grab_asm:
  "(G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<and> P s) f" by (cases G; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<and> P s) f
theory Reader_Option_Monad

lemma opt_map_cong[fundef_cong]:
  "\<lbrakk> f = f'; \<And>v s. f s = Some v \<Longrightarrow> g v = g' v\<rbrakk> \<Longrightarrow> f |> g = f' |> g'" by (rule ext) (simp add: opt_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = f'; \<And>v s. f s = Some v \<Longrightarrow> g v = g' v\<rbrakk> \<Longrightarrow> f |> g = f' |> g'
theory Reader_Option_Monad

lemma in_opt_map_eq:
  "((f |> g) s = Some v) = (\<exists>v'. f s = Some v' \<and> g v' = Some v)" by (simp add: opt_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((f |> g) s = Some v) = (\<exists>v'. f s = Some v' \<and> g v' = Some v)
theory Reader_Option_Monad

lemma opt_mapE:
  "\<lbrakk> (f |> g) s = Some v; \<And>v'. \<lbrakk>f s = Some v'; g v' = Some v \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (auto simp: in_opt_map_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f |> g) s = Some v; \<And>v'. \<lbrakk>f s = Some v'; g v' = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Reader_Option_Monad

lemma opt_map_red:
  "f x = Some y \<Longrightarrow> (f |> g) x = g y" by (clarsimp simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x = Some y \<Longrightarrow> (f |> g) x = g y
theory Reader_Option_Monad

lemma opt_map_left_None:
  "f x = None \<Longrightarrow> (f |> g) x = None" by (clarsimp simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x = None \<Longrightarrow> (f |> g) x = None
theory Reader_Option_Monad

lemma opt_map_assoc:
  "f |> (g |> h) = f |> g |> h" by (fastforce simp: opt_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f |> (g |> h) = f |> g |> h
theory Reader_Option_Monad

lemma opt_map_if_l:
  "(if P then f else f') |> g = (if P then f |> g else f' |> g)" by (auto simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then f else f') |> g = (if P then f |> g else f' |> g)
theory Reader_Option_Monad

lemma opt_map_if_r:
  "f |> (if P then g else g') = (if P then f |> g else f |> g')" by (auto simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f |> (if P then g else g') = (if P then f |> g else f |> g')
theory Reader_Option_Monad

lemma opt_map_upd_None:
  "f(x := None) |> g = (f |> g)(x := None)" by (auto simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f(x := None) |> g = (f |> g)(x := None)
theory Reader_Option_Monad

lemma opt_map_upd_Some:
  "f(x \<mapsto> v) |> g = (f |> g)(x := g v)" by (auto simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f(x \<mapsto> v) |> g = (f |> g)(x := g v)
theory Reader_Option_Monad

lemma opt_map_Some_upd_Some:
  "f(x \<mapsto> v) ||> g = (f ||> g)(x \<mapsto> g v)" by (simp add: opt_map_upd_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f(x \<mapsto> v) ||> g = (f ||> g)(x \<mapsto> g v)
theory Reader_Option_Monad

lemma opt_map_upd_triv:
  "t k = Some x \<Longrightarrow> (t |> f)(k := f x) = t |> f" by (rule ext) (clarsimp simp add: opt_map_red)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t k = Some x \<Longrightarrow> (t |> f)(k := f x) = t |> f
theory Reader_Option_Monad

lemma opt_map_Some_upd_triv:
  "t k = Some x \<Longrightarrow> (t ||> f)(k \<mapsto> f x) = t ||> f" by (rule ext) (clarsimp simp add: opt_map_red)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t k = Some x \<Longrightarrow> (t ||> f)(k \<mapsto> f x) = t ||> f
theory Reader_Option_Monad

lemma opt_map_upd_triv_None:
  "t k = None \<Longrightarrow> (t |> f)(k := None) = t |> f" by (rule ext) (clarsimp simp add: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t k = None \<Longrightarrow> (t |> f)(k := None) = t |> f
theory Reader_Option_Monad

lemma opt_map_foldr_upd:
  "foldr (\<lambda>p kh. kh(p := new)) ptrs f |> g
   = foldr (\<lambda>p kh. kh(p := (case new of Some x \<Rightarrow> g x | _ \<Rightarrow> None))) ptrs (f |> g)" by (induct ptrs arbitrary: new; clarsimp split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p kh. kh(p := new)) ptrs f |> g = foldr (\<lambda>p kh. kh(p := case new of None \<Rightarrow> None | Some x \<Rightarrow> g x)) ptrs (f |> g)
theory Reader_Option_Monad

lemma opt_map_Some_foldr_upd:
  "foldr (\<lambda>p kh. kh(p := new)) ptrs f ||> g
   = foldr (\<lambda>p kh. kh(p := map_option g new)) ptrs (f ||> g)" by (induct ptrs arbitrary: new; clarsimp simp: map_option_case split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p kh. kh(p := new)) ptrs f ||> g = foldr (\<lambda>p kh. kh(p := map_option g new)) ptrs (f ||> g)
theory Reader_Option_Monad

lemma opt_map_Some_comp[simp]:
  "f ||> g ||> h = f ||> h o g" by (fastforce simp: opt_map_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f ||> g ||> h = f ||> h \<circ> g
theory Reader_Option_Monad

lemma opt_map_fold_l:
  "(id |> g) (f x) = (f |> g) x" by (clarsimp simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (id |> g) (f x) = (f |> g) x
theory Reader_Option_Monad

lemma opt_map_Some_id_r[simp]:
  "f |> Some = f" by (fastforce simp: opt_map_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f |> Some = f
theory Reader_Option_Monad

lemma opt_map_Some_id_l[simp]:
  "Some |> f = f" by (clarsimp simp: opt_map_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Some |> f = f
theory Reader_Option_Monad

lemma opt_map_zero_l[simp]:
  "Map.empty |> g = Map.empty" by (clarsimp simp: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. None) |> g = (\<lambda>x. None)
theory Reader_Option_Monad

lemma opt_map_zero_r[simp]:
  "f |> Map.empty = Map.empty" by (fastforce simp: opt_map_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f |> (\<lambda>x. None) = (\<lambda>x. None)
theory Reader_Option_Monad

lemma opt_map_Some_eta_fold:
  "f |> (\<lambda>x. Some (g x)) = f ||> g" by (simp add: o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f |> (\<lambda>x. Some (g x)) = f ||> g
theory Reader_Option_Monad

lemma case_opt_map_distrib:
  "(\<lambda>s. case_option None g (f s)) |> h = (\<lambda>s. case_option None (g |> h) (f s))" by (fastforce simp: opt_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> g x) |> h = (\<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> (g |> h) x)
theory Reader_Option_Monad

lemma opt_map_apply_left_eq:
  "f s = f s' \<Longrightarrow> (f |> g) s = (f |> g) s'" by (simp add: opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f s = f s' \<Longrightarrow> (f |> g) s = (f |> g) s'
theory Reader_Option_Monad

lemma "\<lbrakk> (f |> g) x = None; g v = None \<rbrakk> \<Longrightarrow> f(x \<mapsto> v) |> g = f |> g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f |> g) x = None; g v = None\<rbrakk> \<Longrightarrow> f(x \<mapsto> v) |> g = f |> g
theory Reader_Option_Monad

lemma opt_pred_conj:
  "((P |< hp) p \<and> (Q |< hp) p) = ((P and Q) |< hp) p" by (fastforce simp: pred_conj_def opt_pred_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P |< hp) p \<and> (Q |< hp) p) = ((P and Q) |< hp) p
theory Reader_Option_Monad

lemma opt_pred_disj:
  "((P |< hp) p \<or> (Q |< hp) p) = ((P or Q) |< hp) p" by (fastforce simp: pred_disj_def opt_pred_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P |< hp) p \<or> (Q |< hp) p) = ((P or Q) |< hp) p
theory Reader_Option_Monad

lemma in_opt_pred:
  "(P |< f) p = (\<exists>v. f p = Some v \<and> P v)" by (auto simp: opt_pred_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P |< f) p = (\<exists>v. f p = Some v \<and> P v)
theory Reader_Option_Monad

lemma opt_predE:
  "\<lbrakk>(P |< proj) x; \<And>y. \<lbrakk>proj x = Some y; P y\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by (blast dest: opt_predD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P |< proj) x; \<And>y. \<lbrakk>proj x = Some y; P y\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Reader_Option_Monad

lemma opt_pred_unfold_map:
  "P |< (f |> g) = P |< g |< f" by (fastforce simp: opt_map_def in_opt_pred split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P |< (f |> g) = P |< g |< f
theory Reader_Option_Monad

lemma opt_pred_unfold_proj:
  "P |< (f ||> g) = P o g |< f" by (clarsimp simp: opt_map_def opt_pred_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P |< (f ||> g) = P \<circ> g |< f
theory Reader_Option_Monad

lemma opt_pred_proj_upd_eq[simp]:
  "(P |< proj (p \<mapsto> v)) p = P v" by (simp add: in_opt_pred)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P |< proj(p \<mapsto> v)) p = P v
theory Reader_Option_Monad

lemma ogets_def:
  "ogets f = (\<lambda>s. Some (f s))" by (clarsimp simp: asks_def obind_def oreturn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ogets f = (\<lambda>s. Some (f s))
theory Reader_Option_Monad

lemma oreturn_bind[simp]:
  "(oreturn x |>> f) = f x" by (auto simp add: oreturn_def obind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oreturn x >>= f = f x
theory Reader_Option_Monad

lemma obind_return[simp]:
  "(m |>> oreturn) = m" by (auto simp add: oreturn_def obind_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= oreturn = m