kings-crown/FVELER_Isabelle huggingface dataset:
theory Reader_Option_Monad

lemma obind_assoc:
  "(m |>> f) |>> g  =  m |>> (\<lambda>x. f x |>> g)" by (auto simp add: oreturn_def obind_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= f >>= g = do {
  x \<leftarrow> m;
f x >>= g
}
theory Reader_Option_Monad

lemma ofail_bind [simp]:
  "ofail |>> m = ofail" by (auto simp add: ofail_def obind_def split: option.splits)

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

lemma opt_bind_cong[fundef_cong]:
  "\<lbrakk> f = f'; \<And>v s. f' s = Some v \<Longrightarrow> g v s = g' v s \<rbrakk> \<Longrightarrow> f |>> g = f' |>> g'" by (rule ext) (simp add: obind_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 s = g' v s\<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'
theory Reader_Option_Monad

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

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

lemma oassert_bind_cong[fundef_cong]:
  "\<lbrakk> P = P'; P' \<Longrightarrow> m = m' \<rbrakk> \<Longrightarrow> oassert P |>> m = oassert P' |>> m'" by (auto simp: oassert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = P'; P' \<Longrightarrow> m = m'\<rbrakk> \<Longrightarrow> oassert P >>= m = oassert P' >>= m'
theory Reader_Option_Monad

lemma oassert_bind_cong_apply[fundef_cong]:
  "\<lbrakk> P = P'; P' \<Longrightarrow> m () s = m' () s \<rbrakk> \<Longrightarrow> (oassert P |>> m) s = (oassert P' |>> m') s" by (auto simp: oassert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = P'; P' \<Longrightarrow> m () s = m' () s\<rbrakk> \<Longrightarrow> (oassert P >>= m) s = (oassert P' >>= m') s
theory Reader_Option_Monad

lemma oreturn_bind_cong[fundef_cong]:
  "\<lbrakk> x = x'; m x' = m' x' \<rbrakk> \<Longrightarrow> oreturn x |>> m = oreturn x' |>> m'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = x'; m x' = m' x'\<rbrakk> \<Longrightarrow> oreturn x >>= m = oreturn x' >>= m'
theory Reader_Option_Monad

lemma oreturn_bind_cong_apply[fundef_cong]:
  "\<lbrakk> x = x'; m x' s = m' x' s \<rbrakk> \<Longrightarrow> (oreturn x |>> m) s = (oreturn x' |>> m') s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = x'; m x' s = m' x' s\<rbrakk> \<Longrightarrow> (oreturn x >>= m) s = (oreturn x' >>= m') s
theory Reader_Option_Monad

lemma oreturn_bind_cong2[fundef_cong]:
  "\<lbrakk> x = x'; m x' = m' x' \<rbrakk> \<Longrightarrow> (oreturn $ x) |>> m = (oreturn $ x') |>> m'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = x'; m x' = m' x'\<rbrakk> \<Longrightarrow> (oreturn $ x) >>= m = (oreturn $ x') >>= m'
theory Reader_Option_Monad

lemma oreturn_bind_cong2_apply[fundef_cong]:
  "\<lbrakk> x = x'; m x' s = m' x' s \<rbrakk> \<Longrightarrow> ((oreturn $ x) |>> m) s = ((oreturn $ x') |>> m') s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = x'; m x' s = m' x' s\<rbrakk> \<Longrightarrow> ((oreturn $ x) >>= m) s = ((oreturn $ x') >>= m') s
theory Reader_Option_Monad

lemma ocondition_cong[fundef_cong]:
"\<lbrakk>c = c'; \<And>s. c' s \<Longrightarrow> l s = l' s; \<And>s. \<not>c' s \<Longrightarrow> r s = r' s\<rbrakk>
  \<Longrightarrow> ocondition c l r = ocondition c' l' r'" by (auto simp: ocondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = c'; \<And>s. c' s \<Longrightarrow> l s = l' s; \<And>s. \<not> c' s \<Longrightarrow> r s = r' s\<rbrakk> \<Longrightarrow> ocondition c l r = ocondition c' l' r'
theory Reader_Option_Monad

lemma ocondition_K_true[simp]:
  "ocondition (\<lambda>_. True) T F = T" by (simp add: ocondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ocondition (\<lambda>_. True) T F = T
theory Reader_Option_Monad

lemma ocondition_K_false[simp]:
  "ocondition (\<lambda>_. False) T F = F" by (simp add: ocondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ocondition (\<lambda>_. False) T F = F
theory Reader_Option_Monad

lemma ocondition_False:
    "\<lbrakk> \<And>s. \<not> P s \<rbrakk> \<Longrightarrow> ocondition P L R = R" by (rule ext, clarsimp simp: ocondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<not> P s) \<Longrightarrow> ocondition P L R = R
theory Reader_Option_Monad

lemma ocondition_True:
    "\<lbrakk> \<And>s. P s \<rbrakk> \<Longrightarrow> ocondition P L R = L" by (rule ext, clarsimp simp: ocondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s) \<Longrightarrow> ocondition P L R = L
theory Reader_Option_Monad

lemma in_oreturn [simp]:
  "(oreturn x s = Some v) = (v = x)" by (auto simp: oreturn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (oreturn x s = Some v) = (v = x)
theory Reader_Option_Monad

lemma oreturn_None[simp]:
  "\<not> oreturn x s = None" by (simp add: oreturn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oreturn x s \<noteq> None
theory Reader_Option_Monad

lemma oreturnE:
  "\<lbrakk>oreturn x s = Some v; v = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oreturn x s = Some v; v = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Reader_Option_Monad

lemma in_ofail[simp]:
  "ofail s \<noteq> Some v" by (auto simp: ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ofail s \<noteq> Some v
theory Reader_Option_Monad

lemma ofailE:
  "ofail s = Some v \<Longrightarrow> P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ofail s = Some v \<Longrightarrow> P
theory Reader_Option_Monad

lemma in_oassert_eq[simp]:
  "(oassert P s = Some v) = P" by (simp add: oassert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (oassert P s = Some v) = P
theory Reader_Option_Monad

lemma oassert_True[simp]:
  "oassert True = oreturn ()" by (simp add: oassert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oassert True = oreturn ()
theory Reader_Option_Monad

lemma oassert_False[simp]:
  "oassert False = ofail" by (simp add: oassert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oassert False = ofail
theory Reader_Option_Monad

lemma oassertE:
  "\<lbrakk> oassert P s = Some v; P \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oassert P s = Some v; P \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
theory Reader_Option_Monad

lemma in_obind_eq:
  "((f |>> g) s = Some v) = (\<exists>v'. f s = Some v' \<and> g v' s = Some v)" by (simp add: obind_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' s = Some v)
theory Reader_Option_Monad

lemma obind_None_eq:
  "((f |>> g) s = None) = (f s = None \<or> (\<exists>v. f s = Some v \<and> g v s = None))" by (simp add: obind_def split: option.split)

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

lemma obind_eqI:
  "\<lbrakk> f s = f s' ; \<And>x. f s = Some x \<Longrightarrow> g x s = g' x s' \<rbrakk> \<Longrightarrow> obind f g s = obind f g' s'" by (simp add: obind_def split: option.splits)

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

lemma obindE:
  "\<lbrakk> (f |>> g) s = Some v; \<And>v'. \<lbrakk>f s = Some v'; g v' s = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by (auto simp: in_obind_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' s = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Reader_Option_Monad

lemma in_othrow_eq[simp]:
  "(othrow e s = Some v) = (v = Inl e)" by (auto simp: othrow_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (othrow e s = Some v) = (v = Inl e)
theory Reader_Option_Monad

lemma othrowE:
  "\<lbrakk>othrow e s = Some v; v = Inl e \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>othrow e s = Some v; v = Inl e \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Reader_Option_Monad

lemma in_oreturnOk_eq[simp]:
  "(oreturnOk x s = Some v) = (v = Inr x)" by (auto simp: oreturnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (oreturnOk x s = Some v) = (v = Inr x)
theory Reader_Option_Monad

lemma oreturnOkE:
  "\<lbrakk>oreturnOk x s = Some v; v = Inr x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oreturnOk x s = Some v; v = Inr x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Reader_Option_Monad

lemma in_opt_map_Some_eq:
  "((f ||> g) x = Some y) = (\<exists>v. f x = Some v \<and> g v = y)" by (simp add: in_opt_map_eq)

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

lemma in_opt_map_Some_None_eq[simp]:
  "((f ||> g) x = None) = (f x = None)" by (simp add: opt_map_def split: option.splits)

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

lemma oreturn_comp[simp]:
  "oreturn x \<circ> f = oreturn x" by (simp add: oreturn_def o_def)

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

lemma ofail_comp[simp]:
  "ofail \<circ> f = ofail" by (auto simp: ofail_def)

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

lemma oassert_comp[simp]:
  "oassert P \<circ> f = oassert P" by (simp add: oassert_def)

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

lemma fail_apply[simp]:
  "ofail s = None" by (simp add: ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ofail s = None
theory Reader_Option_Monad

lemma oassert_apply[simp]:
  "oassert P s = (if P then Some () else None)" by (simp add: oassert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oassert P s = (if P then Some () else None)
theory Reader_Option_Monad

lemma oapply_apply[simp]:
  "oapply x s = s x" by (simp add: oapply_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oapply x s = s x
theory Reader_Option_Monad

lemma oapply2_apply[simp]:
  "oapply2 x y s = s x y" by (simp add: oapply2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oapply2 x y s = s x y
theory Reader_Option_Monad

lemma obind_comp_dist:
  "obind f g o h = obind (f o h) (\<lambda>x. g x o h)" by (auto simp: obind_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f >>= g) \<circ> h = do {
  x \<leftarrow> f \<circ> h;
g x \<circ> h
}
theory Reader_Option_Monad

lemma if_comp_dist:
  "(if P then f else g) o h = (if P then f o h else g o h)" by auto

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

lemma obindK_is_opt_map:
  "f \<bind> (\<lambda>x. K $ g x) = f |> g" by (simp add: obind_def opt_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do {
  x \<leftarrow> f;
K $ g x
} = f |> g
theory Reader_Option_Monad

lemma option_while'_inj:
  assumes "(s,s') \<in> option_while' C B" "(s, s'') \<in> option_while' C B"
  shows "s' = s''" using assms by (induct rule: option_while'.induct) (auto elim: option_while'.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' = s'' proof (prove)
using this:
(s, s') \<in> option_while' C B
(s, s'') \<in> option_while' C B

goal (1 subgoal):
 1. s' = s''
theory Reader_Option_Monad

lemma option_while'_inj_step:
  "\<lbrakk> C s; B s = Some s'; (Some s, t) \<in> option_while' C B ; (Some s', t') \<in> option_while' C B \<rbrakk>
   \<Longrightarrow> t = t'" by (metis option_while'.step option_while'_inj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C s; B s = Some s'; (Some s, t) \<in> option_while' C B; (Some s', t') \<in> option_while' C B\<rbrakk> \<Longrightarrow> t = t'
theory Reader_Option_Monad

lemma option_while'_THE:
  assumes "(Some r, sr') \<in> option_while' C B"
  shows "(THE s. (Some r, s) \<in> option_while' C B) = sr'" using assms by (blast dest: option_while'_inj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (THE s. (Some r, s) \<in> option_while' C B) = sr' proof (prove)
using this:
(Some r, sr') \<in> option_while' C B

goal (1 subgoal):
 1. (THE s. (Some r, s) \<in> option_while' C B) = sr'
theory Reader_Option_Monad

lemma option_while_simps:
  "\<not> C s \<Longrightarrow> option_while C B s = Some s"
  "C s \<Longrightarrow> B s = None \<Longrightarrow> option_while C B s = None"
  "C s \<Longrightarrow> B s = Some s' \<Longrightarrow> option_while C B s = option_while C B s'"
  "(Some s, ss') \<in> option_while' C B \<Longrightarrow> option_while C B s = ss'" using option_while'_inj_step[of C s B s'] by (auto simp: option_while_def option_while'_THE
           intro: option_while'.intros
           dest: option_while'_inj
           elim: option_while'.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<not> C s \<Longrightarrow> option_while C B s = Some s) &&& (\<lbrakk>C s; B s = None\<rbrakk> \<Longrightarrow> option_while C B s = None)) &&& (\<lbrakk>C s; B s = Some s'\<rbrakk> \<Longrightarrow> option_while C B s = option_while C B s') &&& ((Some s, ss') \<in> option_while' C B \<Longrightarrow> option_while C B s = ss') proof (prove)
using this:
\<lbrakk>C s; B s = Some s'; (Some s, ?t) \<in> option_while' C B; (Some s', ?t') \<in> option_while' C B\<rbrakk> \<Longrightarrow> ?t = ?t'

goal (1 subgoal):
 1. ((\<not> C s \<Longrightarrow> option_while C B s = Some s) &&& (\<lbrakk>C s; B s = None\<rbrakk> \<Longrightarrow> option_while C B s = None)) &&& (\<lbrakk>C s; B s = Some s'\<rbrakk> \<Longrightarrow> option_while C B s = option_while C B s') &&& ((Some s, ss') \<in> option_while' C B \<Longrightarrow> option_while C B s = ss')
theory Reader_Option_Monad

lemma option_while_rule:
  assumes "option_while C B s = Some s'"
  assumes "I s"
  assumes istep: "\<And>s s'. C s \<Longrightarrow> I s \<Longrightarrow> B s = Some s' \<Longrightarrow> I s'"
  shows "I s' \<and> \<not> C s'" proof - { fix ss ss' assume "(ss, ss') \<in> option_while' C B" "ss = Some s" "ss' = Some s'" then have ?thesis using \<open>I s\<close> by (induct arbitrary: s) (auto intro: istep) } then show ?thesis using assms(1) by (auto simp: option_while_def option_while'_THE split: if_split_asm) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (state)
goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (state)
goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (state)
goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (state)
this:
(ss, ss') \<in> option_while' C B
ss = Some s
ss' = Some s'

goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (chain)
picking this:
(ss, ss') \<in> option_while' C B
ss = Some s
ss' = Some s' proof (prove)
using this:
(ss, ss') \<in> option_while' C B
ss = Some s
ss' = Some s'

goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (prove)
using this:
(ss, ss') \<in> option_while' C B
ss = Some s
ss' = Some s'
I s

goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (state)
this:
I s' \<and> \<not> C s'

goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (state)
this:
\<lbrakk>(?ss2, ?ss'2) \<in> option_while' C B; ?ss2 = Some s; ?ss'2 = Some s'\<rbrakk> \<Longrightarrow> I s' \<and> \<not> C s'

goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (chain)
picking this:
\<lbrakk>(?ss2, ?ss'2) \<in> option_while' C B; ?ss2 = Some s; ?ss'2 = Some s'\<rbrakk> \<Longrightarrow> I s' \<and> \<not> C s' proof (prove)
using this:
\<lbrakk>(?ss2, ?ss'2) \<in> option_while' C B; ?ss2 = Some s; ?ss'2 = Some s'\<rbrakk> \<Longrightarrow> I s' \<and> \<not> C s'

goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (prove)
using this:
\<lbrakk>(?ss2, ?ss'2) \<in> option_while' C B; ?ss2 = Some s; ?ss'2 = Some s'\<rbrakk> \<Longrightarrow> I s' \<and> \<not> C s'
option_while C B s = Some s'

goal (1 subgoal):
 1. I s' \<and> \<not> C s' proof (state)
this:
I s' \<and> \<not> C s'

goal:
No subgoals!
theory Reader_Option_Monad

lemma owhile_unroll:
  "owhile C B r = ocondition (C r) (B r |>> owhile C B) (oreturn r)" by (auto simp: ocondition_def obind_def oreturn_def owhile_def
                 option_while_simps
           split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. owhile C B r = ocondition (C r) (B r >>= owhile C B) (oreturn r)
theory Reader_Option_Monad

lemma owhile_rule:
  assumes "I r s"
  assumes "wf M"
  assumes less: "\<And>r r'. \<lbrakk>I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> (r',r) \<in> M"
  assumes step: "\<And>r r'. \<lbrakk>I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> I r' s"
  assumes fail: "\<And>r. \<lbrakk>I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> Q None"
  assumes final: "\<And>r. \<lbrakk>I r s; \<not>C r s\<rbrakk> \<Longrightarrow> Q (Some r)"
  shows "Q (owhile C B r s)" proof - let ?rs' = "owhile C B r s" have "(case ?rs' of Some r \<Rightarrow> I r s | _ \<Rightarrow> Q None)
      \<and> (case ?rs' of Some r' \<Rightarrow> \<not> C r' s | _ \<Rightarrow> True)" by (rule option_while_rule'[where B="\<lambda>r. B r s" and s=r, OF _ \<open>wf _\<close>])
       (auto simp: owhile_def intro: assms) then show ?thesis by (auto intro: final split: option.split_asm) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q (owhile C B r s) proof (state)
goal (1 subgoal):
 1. Q (owhile C B r s) proof (state)
goal (1 subgoal):
 1. Q (owhile C B r s) proof (prove)
goal (1 subgoal):
 1. (case owhile C B r s of None \<Rightarrow> Q None | Some r \<Rightarrow> I r s) \<and> (case owhile C B r s of None \<Rightarrow> True | Some r' \<Rightarrow> \<not> C r' s) proof (state)
this:
(case owhile C B r s of None \<Rightarrow> Q None | Some r \<Rightarrow> I r s) \<and> (case owhile C B r s of None \<Rightarrow> True | Some r' \<Rightarrow> \<not> C r' s)

goal (1 subgoal):
 1. Q (owhile C B r s) proof (chain)
picking this:
(case owhile C B r s of None \<Rightarrow> Q None | Some r \<Rightarrow> I r s) \<and> (case owhile C B r s of None \<Rightarrow> True | Some r' \<Rightarrow> \<not> C r' s) proof (prove)
using this:
(case owhile C B r s of None \<Rightarrow> Q None | Some r \<Rightarrow> I r s) \<and> (case owhile C B r s of None \<Rightarrow> True | Some r' \<Rightarrow> \<not> C r' s)

goal (1 subgoal):
 1. Q (owhile C B r s) proof (state)
this:
Q (owhile C B r s)

goal:
No subgoals!
theory Reader_Option_VCG

lemma no_ofail_is_ovalidNF: "no_ofail P f \<equiv> ovalidNF P f (\<lambda>_ _. True)" by (simp add: no_ofail_def ovalidNF_def)

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

lemma ovalidNF_combine: "\<lbrakk> ovalid P f Q; no_ofail P f \<rbrakk> \<Longrightarrow> ovalidNF P f Q" by (auto simp: ovalidNF_def ovalid_def no_ofail_def)

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

lemma use_ovalidE:
  "\<lbrakk>ovalid P f Q; P s; f s = Some r; Q r s \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by (clarsimp simp: ovalid_def)

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

lemma use_ovalid:
  "\<lbrakk>ovalid P f Q; f s = Some r; P s \<rbrakk> \<Longrightarrow> Q r s" by (clarsimp simp: ovalid_def)

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

lemma ovalid_post_taut[wp]:
  "\<lblot>P\<rblot> f \<lblot>\<top>\<top>\<rblot>" by (simp add: ovalid_def)

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

lemma ovalid_inv[wp]:
  "ovalid P f (\<lambda>_. P)" by (simp add: ovalid_def)

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

lemma obind_wp[wp]:
  "\<lbrakk> \<And>r. ovalid (R r) (g r) Q; ovalid P f R \<rbrakk> \<Longrightarrow> ovalid P (obind f g) Q" by (simp add: ovalid_def obind_def split: option.splits, fast)

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

lemma ocondition_wp[wp]:
  "\<lbrakk> ovalid L l Q; ovalid R r Q \<rbrakk>
   \<Longrightarrow> ovalid (\<lambda>s. if C s then L s else R s) (ocondition C l r) Q" by (auto simp: ovalid_def ocondition_def)

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

lemma ofail_wp[wp]:
  "ovalid (\<lambda>_. True) ofail Q" by (simp add: ovalid_def ofail_def)

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

lemma asks_wp[wp]:
  "ovalid (\<lambda>s. P (f s) s) (asks f) P" by (simp add: split_def asks_def oreturn_def obind_def ovalid_def)

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

lemma oassert_wp[wp]:
  "\<lblot>\<lambda>s. Q \<longrightarrow> P () s\<rblot> oassert Q \<lblot>P\<rblot>" apply (simp add: oassert_def) apply (intro conjI; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>\<lambda>s. Q \<longrightarrow> P () s\<rblot> oassert Q \<lblot>P\<rblot> proof (prove)
goal (1 subgoal):
 1. (Q \<longrightarrow> \<lblot>P ()\<rblot> oreturn () \<lblot>P\<rblot>) \<and> (\<not> Q \<longrightarrow> \<lblot>\<lambda>s. True\<rblot> ofail \<lblot>P\<rblot>) proof (prove)
goal:
No subgoals!
theory Reader_Option_VCG

lemma oguard_wp[wp]:
  "ovalid (\<lambda>s. f s \<longrightarrow> P () s) (oguard f) P" by (simp add: ovalid_def oguard_def)

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

lemma oskip_wp[wp]:
  "ovalid (\<lambda>s. P () s) oskip P" by (simp add: ovalid_def oskip_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>P ()\<rblot> oskip \<lblot>P\<rblot>