kings-crown/FVELER_Isabelle huggingface dataset:
theory Reader_Option_VCG

lemma ovalid_if_split:
  "\<lbrakk> P \<Longrightarrow> \<lblot>Q\<rblot> f \<lblot>S\<rblot>; \<not>P \<Longrightarrow> \<lblot>R\<rblot> g \<lblot>S\<rblot> \<rbrakk> \<Longrightarrow> \<lblot>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rblot> if P then f else g \<lblot>S\<rblot>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> \<lblot>Q\<rblot> f \<lblot>S\<rblot>; \<not> P \<Longrightarrow> \<lblot>R\<rblot> g \<lblot>S\<rblot>\<rbrakk> \<Longrightarrow> \<lblot>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)\<rblot> if P then f else g \<lblot>S\<rblot>
theory Reader_Option_VCG

lemma owhile_ovalid[wp]:
  "\<lbrakk>\<And>a. ovalid (\<lambda>s. I a s \<and> C a s) (B a) I;
    \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk>
   \<Longrightarrow> ovalid (I a) (owhile_inv C B a I M) Q" unfolding owhile_inv_def owhile_def ovalid_def apply clarify apply (frule (1) option_while_rule[where I = "\<lambda>a. I a s" for s]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. \<lblot>\<lambda>s. I a s \<and> C a s\<rblot> B a \<lblot>I\<rblot>; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk> \<Longrightarrow> \<lblot>I a\<rblot> owhile_inv C B a I M \<lblot>Q\<rblot> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. \<forall>s r. (I a s \<and> C a s) \<and> B a s = Some r \<longrightarrow> I r s; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk> \<Longrightarrow> \<forall>s r. I a s \<and> option_while (\<lambda>a. C a s) (\<lambda>a. B a s) a = Some r \<longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>\<And>a. \<forall>s r. (I a s \<and> C a s) \<and> B a s = Some r \<longrightarrow> I r s; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; option_while (\<lambda>a. C a s) (\<lambda>a. B a s) a = Some r\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>s r sa s'. \<lbrakk>\<And>a. \<forall>s r. (I a s \<and> C a s) \<and> B a s = Some r \<longrightarrow> I r s; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; option_while (\<lambda>a. C a s) (\<lambda>a. B a s) a = Some r; C sa s; I sa s; B sa s = Some s'\<rbrakk> \<Longrightarrow> I s' s
 2. \<And>s r. \<lbrakk>\<And>a. \<forall>s r. (I a s \<and> C a s) \<and> B a s = Some r \<longrightarrow> I r s; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; option_while (\<lambda>a. C a s) (\<lambda>a. B a s) a = Some r; I r s \<and> \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!
theory Reader_Option_VCG

lemma assert_opt_ovalid:
  "\<lblot>\<lambda>s. \<forall>y. x = Some y \<longrightarrow> Q y s\<rblot> oassert_opt x \<lblot>Q\<rblot>" unfolding oassert_opt_def by (case_tac x; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>\<lambda>s. \<forall>y. x = Some y \<longrightarrow> Q y s\<rblot> oassert_opt x \<lblot>Q\<rblot> proof (prove)
goal (1 subgoal):
 1. \<lblot>\<lambda>s. \<forall>y. x = Some y \<longrightarrow> Q y s\<rblot> case x of None \<Rightarrow> ofail | Some x \<Rightarrow> oreturn x \<lblot>Q\<rblot>
theory Reader_Option_VCG

lemma ovalid_is_triple[wp_trip]:
  "ovalid P f Q = triple_judgement P f (ovalid_property Q (\<lambda>s f. f s))" by (auto simp: triple_judgement_def ovalid_def ovalid_property_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>P\<rblot> f \<lblot>Q\<rblot> = triple_judgement P f (ovalid_property Q (\<lambda>s f. f s))
theory Reader_Option_VCG

lemma ovalid_wp_comb1[wp_comb]:
  "\<lbrakk> ovalid P' f Q; ovalid P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalid P f (\<lambda>r s. Q r s \<and> Q' r s)" by (simp add: ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lblot>P'\<rblot> f \<lblot>Q\<rblot>; \<lblot>P\<rblot> f \<lblot>Q'\<rblot>; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lblot>P\<rblot> f \<lblot>\<lambda>r s. Q r s \<and> Q' r s\<rblot>
theory Reader_Option_VCG

lemma ovalid_wp_comb2[wp_comb]:
  "\<lbrakk> ovalid P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalid P' f Q" by (auto simp: ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lblot>P\<rblot> f \<lblot>Q\<rblot>; \<And>s. P' s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lblot>P'\<rblot> f \<lblot>Q\<rblot>
theory Reader_Option_VCG

lemma ovalid_wp_comb3[wp_comb]:
  "\<lbrakk> ovalid P f Q; ovalid P' f Q' \<rbrakk> \<Longrightarrow> ovalid (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)" by (auto simp: ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lblot>P\<rblot> f \<lblot>Q\<rblot>; \<lblot>P'\<rblot> f \<lblot>Q'\<rblot>\<rbrakk> \<Longrightarrow> \<lblot>\<lambda>s. P s \<and> P' s\<rblot> f \<lblot>\<lambda>r s. Q r s \<and> Q' r s\<rblot>
theory Reader_Option_VCG

lemma obind_NF_wp[wp]:
  "\<lbrakk> \<And>r. ovalidNF (R r) (g r) Q; ovalidNF P f R \<rbrakk> \<Longrightarrow> ovalidNF P (obind f g) Q" by (auto simp: ovalidNF_def obind_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. ovalidNF (R r) (g r) Q; ovalidNF P f R\<rbrakk> \<Longrightarrow> ovalidNF P (f >>= g) Q
theory Reader_Option_VCG

lemma oreturn_NF_wp[wp]:
  "ovalidNF (P x) (oreturn x) P" by (simp add: ovalidNF_def oreturn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF (P x) (oreturn x) P
theory Reader_Option_VCG

lemma ofail_NF_wp[wp]:
  "ovalidNF (\<lambda>_. False) ofail Q" by (simp add: ovalidNF_def ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF (\<lambda>_. False) ofail Q
theory Reader_Option_VCG

lemma ogets_NF_wp[wp]:
  "ovalidNF (\<lambda>s. P (f s) s) (ogets f) P" by (simp add: ovalidNF_def ogets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF (\<lambda>s. P (f s) s) (ogets f) P
theory Reader_Option_VCG

lemma oguard_NF_wp[wp]:
  "ovalidNF (\<lambda>s. f s \<and> P () s) (oguard f) P" by (simp add: ovalidNF_def oguard_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF (\<lambda>s. f s \<and> P () s) (oguard f) P
theory Reader_Option_VCG

lemma oskip_NF_wp[wp]:
  "ovalidNF (\<lambda>s. P () s) oskip P" by (simp add: ovalidNF_def oskip_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF (P ()) oskip P
theory Reader_Option_VCG

lemma ovalid_NF_case_prod[wp]:
  assumes "(\<And>x y. ovalidNF (P x y) (B x y) Q)"
  shows "ovalidNF (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q" using assms unfolding ovalidNF_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q proof (prove)
using this:
ovalidNF (P ?x ?y) (B ?x ?y) Q

goal (1 subgoal):
 1. ovalidNF (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q proof (prove)
using this:
\<forall>s. P ?x ?y s \<longrightarrow> B ?x ?y s \<noteq> None \<and> (\<forall>r. B ?x ?y s = Some r \<longrightarrow> Q r s)

goal (1 subgoal):
 1. \<forall>s. (case v of (x, xa) \<Rightarrow> P x xa) s \<longrightarrow> (case v of (x, xa) \<Rightarrow> B x xa) s \<noteq> None \<and> (\<forall>r. (case v of (x, xa) \<Rightarrow> B x xa) s = Some r \<longrightarrow> Q r s)
theory Reader_Option_VCG

lemma ovalidNF_is_triple[wp_trip]:
  "ovalidNF P f Q = triple_judgement P f (ovalidNF_property Q (\<lambda>s f. f s))" by (auto simp: triple_judgement_def ovalidNF_def ovalidNF_property_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF P f Q = triple_judgement P f (ovalidNF_property Q (\<lambda>s f. f s))
theory Reader_Option_VCG

lemma ovalidNF_wp_comb1[wp_comb]:
  "\<lbrakk> ovalidNF P' f Q; ovalidNF P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalidNF P f (\<lambda>r s. Q r s \<and> Q' r s)" by (simp add: ovalidNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ovalidNF P' f Q; ovalidNF P f Q'; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> ovalidNF P f (\<lambda>r s. Q r s \<and> Q' r s)
theory Reader_Option_VCG

lemma ovalidNF_wp_comb2[wp_comb]:
  "\<lbrakk> ovalidNF P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalidNF P' f Q" by (simp add: ovalidNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ovalidNF P f Q; \<And>s. P' s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> ovalidNF P' f Q
theory Reader_Option_VCG

lemma ovalidNF_wp_comb3[wp_comb]:
  "\<lbrakk> ovalidNF P f Q; ovalidNF P' f Q' \<rbrakk> \<Longrightarrow> ovalidNF (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)" by (simp add: ovalidNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ovalidNF P f Q; ovalidNF P' f Q'\<rbrakk> \<Longrightarrow> ovalidNF (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)
theory Reader_Option_VCG

lemma no_ofailD:
  "\<lbrakk> no_ofail P m; P s \<rbrakk> \<Longrightarrow> \<exists>y. m s = Some y" by (simp add: no_ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail P m; P s\<rbrakk> \<Longrightarrow> \<exists>y. m s = Some y
theory Reader_Option_VCG

lemma no_ofail_obind2[simp]:
  assumes f: "no_ofail P f"
  assumes v: "ovalid Q f R"
  assumes g: "\<And>r. no_ofail (R r) (g r)"
  shows "no_ofail (P and Q) (f |>> g)" using v g by (fastforce simp: no_ofail_def obind_def pred_conj_def ovalid_def dest: no_ofailD [OF f])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail (P and Q) (f >>= g) proof (prove)
using this:
\<lblot>Q\<rblot> f \<lblot>R\<rblot>
no_ofail (R ?r) (g ?r)

goal (1 subgoal):
 1. no_ofail (P and Q) (f >>= g)
theory Reader_Option_VCG

lemma no_ofail_ofail[wp]:
  "no_ofail \<bottom> ofail" by (simp add: no_ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail (\<lambda>_. False) ofail
theory Reader_Option_VCG

lemma no_ofail_asks_simp[simp]:
  "no_ofail P (asks f)" unfolding asks_def oreturn_def obind_def no_ofail_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail P (ogets f) proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (case Some s of None \<Rightarrow> None | Some x \<Rightarrow> (K \<circ> Some) (f x) s) \<noteq> None
theory Reader_Option_VCG

lemma no_ofail_asks[wp]:
  "no_ofail \<top> (asks f)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail (\<lambda>_. True) (ogets f)
theory Reader_Option_VCG

lemma no_ofail_ogets[wp]:
  "no_ofail \<top> (ogets f)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail (\<lambda>_. True) (ogets f)
theory Reader_Option_VCG

lemma no_ofail_obind[wp]:
  "\<lbrakk> \<And>r. no_ofail (R r) (g r); \<lblot>Q\<rblot> f \<lblot>R\<rblot>; no_ofail P f \<rbrakk> \<Longrightarrow> no_ofail (P and Q) (f |>> g)" by (auto simp: no_ofail_def obind_def ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. no_ofail (R r) (g r); \<lblot>Q\<rblot> f \<lblot>R\<rblot>; no_ofail P f\<rbrakk> \<Longrightarrow> no_ofail (P and Q) (f >>= g)
theory Reader_Option_VCG

lemma no_ofail_oguard[wp]:
  "no_ofail (\<lambda>s. f s) (oguard f)" by (auto simp: no_ofail_def oguard_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail f (oguard f)
theory Reader_Option_VCG

lemma no_ofail_ocondition[wp]:
  "\<lbrakk> no_ofail L l; no_ofail R r \<rbrakk>
     \<Longrightarrow> no_ofail (\<lambda>s. if C s then L s else R s) (ocondition C l r)" by (simp add: no_ofail_def ocondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail L l; no_ofail R r\<rbrakk> \<Longrightarrow> no_ofail (\<lambda>s. if C s then L s else R s) (ocondition C l r)
theory Reader_Option_VCG

lemma no_ofail_oskip[wp]:
  "no_ofail (\<lambda>_. True) oskip" by (simp add: no_ofail_def oskip_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail (\<lambda>_. True) oskip
theory Reader_Option_VCG

lemma no_ofail_oassert_opt[simp, wp]:
  "no_ofail (\<lambda>_. P \<noteq> None) (oassert_opt P)" by (simp add: no_ofail_def oassert_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail (\<lambda>_. P \<noteq> None) (oassert_opt P)
theory Reader_Option_VCG

lemma no_ofail_if[wp]:
  "\<lbrakk> P \<Longrightarrow> no_ofail Q f; \<not> P \<Longrightarrow> no_ofail R g \<rbrakk>
   \<Longrightarrow> no_ofail (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_ofail Q f; \<not> P \<Longrightarrow> no_ofail R g\<rbrakk> \<Longrightarrow> no_ofail (if P then Q else R) (if P then f else g)
theory Reader_Option_VCG

lemma no_ofail_owhen[wp]:
  "(P \<Longrightarrow> no_ofail Q f) \<Longrightarrow> no_ofail (if P then Q else \<top>) (owhen P f)" by (simp add: no_ofail_def owhen_def)

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

lemma no_ofail_ounless[wp]:
  "(\<not>P \<Longrightarrow> no_ofail Q f) \<Longrightarrow> no_ofail (if P then \<top> else Q) (ounless P f)" by (simp add: no_ofail_def ounless_def)

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

lemma no_ofail_oassert[simp, wp]:
  "no_ofail (\<lambda>_. P) (oassert P)" by (simp add: oassert_def no_ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail (\<lambda>_. P) (oassert P)
theory Reader_Option_VCG

lemma no_ofail_is_triple[wp_trip]:
  "no_ofail P f = triple_judgement P f (\<lambda>s f. f s \<noteq> None)" by (auto simp: triple_judgement_def no_ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail P f = triple_judgement P f (\<lambda>s f. f s \<noteq> None)
theory Reader_Option_VCG

lemma no_ofail_wp_comb1[wp_comb]:
  "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f" by (simp add: no_ofail_def)

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

lemma ovalid_grab_asm:
  "(G \<Longrightarrow> ovalid P f Q) \<Longrightarrow> ovalid (\<lambda>s. G \<and> P s) f Q" by (simp add: ovalid_def)

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

lemma ovalidNF_grab_asm:
  "(G \<Longrightarrow> ovalidNF P f Q) \<Longrightarrow> ovalidNF (\<lambda>s. G \<and> P s) f Q" by (simp add: ovalidNF_def)

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

lemma no_ofail_grab_asm:
  "(G \<Longrightarrow> no_ofail P f) \<Longrightarrow> no_ofail (\<lambda>s. G \<and> P s) f" by (simp add: no_ofail_def)

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

lemma ovalid_assume_pre:
  "(\<And>s. P s \<Longrightarrow> ovalid P f Q) \<Longrightarrow> ovalid P f Q" by (auto simp: ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> \<lblot>P\<rblot> f \<lblot>Q\<rblot>) \<Longrightarrow> \<lblot>P\<rblot> f \<lblot>Q\<rblot>
theory Reader_Option_VCG

lemma ovalidNF_assume_pre:
  "(\<And>s. P s \<Longrightarrow> ovalidNF P f Q) \<Longrightarrow> ovalidNF P f Q" by (simp add: ovalidNF_def)

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

lemma no_ofail_assume_pre:
  "(\<And>s. P s \<Longrightarrow> no_ofail P f) \<Longrightarrow> no_ofail P f" by (simp add: no_ofail_def)

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

lemma ovalid_pre_imp:
  "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P' f Q" by (simp add: ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P' s \<Longrightarrow> P s; \<lblot>P\<rblot> f \<lblot>Q\<rblot>\<rbrakk> \<Longrightarrow> \<lblot>P'\<rblot> f \<lblot>Q\<rblot>
theory Reader_Option_VCG

lemma ovalidNF_pre_imp:
  "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P' f Q" by (simp add: ovalidNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P' s \<Longrightarrow> P s; ovalidNF P f Q\<rbrakk> \<Longrightarrow> ovalidNF P' f Q
theory Reader_Option_VCG

lemma no_ofail_pre_imp[wp_pre]:
  "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f" by (simp add: no_ofail_def)

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

lemma ovalid_post_imp:
  "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> Q' r s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P f Q'" by (simp add: ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. Q r s \<Longrightarrow> Q' r s; \<lblot>P\<rblot> f \<lblot>Q\<rblot>\<rbrakk> \<Longrightarrow> \<lblot>P\<rblot> f \<lblot>Q'\<rblot>
theory Reader_Option_VCG

lemma ovalidNF_post_imp:
  "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> Q' r s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P f Q'" by (simp add: ovalidNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. Q r s \<Longrightarrow> Q' r s; ovalidNF P f Q\<rbrakk> \<Longrightarrow> ovalidNF P f Q'
theory Reader_Option_VCG

lemma ovalid_post_imp_assuming_pre:
  "\<lbrakk> \<And>r s. \<lbrakk> P s; Q r s \<rbrakk> \<Longrightarrow> Q' r s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P f Q'" by (simp add: ovalid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. \<lbrakk>P s; Q r s\<rbrakk> \<Longrightarrow> Q' r s; \<lblot>P\<rblot> f \<lblot>Q\<rblot>\<rbrakk> \<Longrightarrow> \<lblot>P\<rblot> f \<lblot>Q'\<rblot>
theory Reader_Option_VCG

lemma ovalidNF_post_imp_assuming_pre:
  "\<lbrakk> \<And>r s. \<lbrakk> P s; Q r s \<rbrakk> \<Longrightarrow> Q' r s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P f Q'" by (simp add: ovalidNF_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. \<lbrakk>P s; Q r s\<rbrakk> \<Longrightarrow> Q' r s; ovalidNF P f Q\<rbrakk> \<Longrightarrow> ovalidNF P f Q'
theory Nondet_Reader_Option

lemma ovalid_K_bind_wp[wp]:
  "ovalid P f Q \<Longrightarrow> ovalid P (K_bind f x) Q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>P\<rblot> f \<lblot>Q\<rblot> \<Longrightarrow> \<lblot>P\<rblot> K_bind f x \<lblot>Q\<rblot>
theory Nondet_Reader_Option

lemma ovalidNF_K_bind_wp[wp]:
  "ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q
theory Nondet_Reader_Option

lemma no_ofail_K_bind[wp]:
  "no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)
theory Nondet_Reader_Option

lemma no_ofail_gets_the_eq:
  "no_ofail P f \<longleftrightarrow> no_fail P (gets_the (f :: ('s, 'a) lookup))" by (auto simp: no_ofail_def no_fail_def gets_the_def gets_def
                 get_def assert_opt_def bind_def return_def fail_def
         split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail P f = no_fail P (gets_the f)
theory Nondet_Reader_Option

lemma ovalid_gets_the:
  "ovalid P f Q \<Longrightarrow> \<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace>" apply wpsimp apply (fastforce dest: use_ovalid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>P\<rblot> f \<lblot>Q\<rblot> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<lblot>P\<rblot> f \<lblot>Q\<rblot>; P s; f s = Some y\<rbrakk> \<Longrightarrow> Q y s proof (prove)
goal:
No subgoals!
theory Nondet_Reader_Option

lemma gets_the_opt_map:
  "gets_the (f |> g) = do x \<leftarrow> gets_the f; assert_opt (g x) od" by (rule ext) (simp add: monad_simps opt_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (f |> g) = do x <- gets_the f;
assert_opt (g x)
od
theory Nondet_Reader_Option

lemma gets_the_opt_o:
  "gets_the (f |> Some o g) = do x \<leftarrow> gets_the f; return (g x) od" by (simp add: gets_the_opt_map assert_opt_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (f ||> g) = do x <- gets_the f;
return (g x)
od
theory Nondet_Reader_Option

lemma gets_the_obind:
  "gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))" by (rule ext) (simp add: monad_simps obind_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (f >>= g) = do x <- gets_the f;
gets_the (g x)
od
theory Nondet_Reader_Option

lemma gets_the_return:
  "gets_the (oreturn x) = return x" by (simp add: monad_simps oreturn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oreturn x) = return x
theory Nondet_Reader_Option

lemma gets_the_fail:
  "gets_the ofail = fail" by (simp add: monad_simps ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the ofail = fail
theory Nondet_Reader_Option

lemma gets_the_ogets:
  "gets_the (ogets s) = gets s" by (clarsimp simp: monad_simps ogets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (ogets s) = gets s
theory Nondet_Reader_Option

lemma gets_the_returnOk:
  "gets_the (oreturnOk x) = returnOk x" by (simp add: monad_simps oreturnOk_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oreturnOk x) = returnOk x
theory Nondet_Reader_Option

lemma gets_the_assert:
  "gets_the (oassert P) = assert P" by (simp add: oassert_def assert_def gets_the_fail gets_the_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oassert P) = assert P
theory Nondet_Reader_Option

lemma gets_the_assert_opt:
  "gets_the (oassert_opt P) = assert_opt P" by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oassert_opt P) = assert_opt P
theory Nondet_Reader_Option

lemma gets_the_if_distrib:
  "gets_the (if P then f else g) = (if P then gets_the f else gets_the g)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (if P then f else g) = (if P then gets_the f else gets_the g)
theory Nondet_Reader_Option

lemma gets_the_oapply_comp:
  "gets_the (oapply x \<circ> f) = gets_map f x" by (fastforce simp: gets_map_def gets_the_def o_def gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oapply x \<circ> f) = gets_map f x